pub fn cutting_planes_lyapunov(n: usize) -> (Vec<u64>, bool)Expand description
The Lyapunov function for the cardinality / cutting-planes collapse — the THIRD physics. The
Cook–Coullard–Turán refutation of PHP sums 2n-1 pseudo-Boolean constraints; each addition cancels
a literal against its negation and tightens the accumulated constraint toward the infeasible
0 ≥ 1. The potential is the number of constraints still to combine, descending to 0 exactly as
the contradiction is exposed.
Its significance is non-uniqueness: PHP has a covering-symmetry measure (n levels × n
width) and this cutting-planes measure (2n-1 linear steps) — two valid Lyapunov functions for
the same formula, in two different proof systems. The measure is a property of the
problem-plus-structure, not a unique object — which is exactly why the framework spans systems.