Skip to main content

compose_collapses

Function compose_collapses 

Source
pub fn compose_collapses(
    num_vars: usize,
    formula: &[Vec<Lit>],
    stages: &[&dyn LyapunovMeasure],
) -> RankedRefutation
Expand description

Compose collapses — the Poly wiring diagram on certified descents. Each stage’s descent runs on the residual database of the previous; the potentials are banded (earlier stages occupy the higher rank band) so the composite strictly descends across every stage boundary; the whole closes by resolution. The result is ONE refutation carrying ONE combined Lyapunov certificate — two (or more) collapses wired into a single descent. Fail-closed: each step is PR-self-checked.

Categorically this is sequential composition of coalgebras: stages wire end-to-end, and the banded potential is the single countdown morphism of the composite system.