pub fn proof_induced_measure(n_steps: usize) -> Vec<u64>Expand description
The ⟹ direction of the characterization: any checkable refutation of n_steps steps induces
a Lyapunov measure — rank the steps in descending order. The induced trajectory is a valid
Lyapunov function of size n_steps, so the minimum measure cost μ*(F) ≤ (min proof size).
Combined with the ⟸ theorem (proof_from_measure: proof size ≤ L·w), this gives the
CHARACTERIZATION μ*(F) = Θ(min proof size) — the measure framework is equivalent to the
proof framework, so a lower bound on the measure cost IS a proof-size lower bound. That equivalence
is the rigorous foundation of the “no bounded measure ⟹ no short proof” direction (the prize),
stated honestly: it makes measure lower bounds and proof lower bounds the same problem, rather
than giving a new technique to prove either.