Function proof_from_measure 

pub fn proof_from_measure<M: LyapunovMeasure>(measure: &M) -> RankedRefutation

The constructive proof of the ⟸ theorem. Drive the measure’s descent from L down to 0, self-checking every step (fail-closed), then close with unit propagation. Returns a ranked refutation whose descent has ≤ L·w steps — read its certificate with crate::complexity::RankedRefutation::certify.