Module complexity 

Certified complexity bounds — a refutation that carries a checkable proof of its own size.

A correctness certificate (the crate::pr refutation) answers “is this UNSAT?”. A complexity certificate answers “and how big is the proof, provably?”. The carrier is a rank function: a per-step natural-number measure that descends. If the measure is non-increasing and each of its levels contributes at most w steps, then a proof spanning L levels has at most L · w steps — a bound a checker confirms by reading the annotation, without trusting how the proof was built.

This is a termination-proof-with-a-clock: the same descent that shows the construction halts also counts its steps. For the steered pigeonhole/coloring refutations the measure is “active items remaining,” L = O(n) levels of w = O(n) steps each, so the certificate reads off a clean O(n²) bound — turning “we measured it polynomial” into “here is the proof it is.”

Structs

RankedRefutation

A refutation whose every step carries a rank (a progress/termination measure).

SizeBound

A certified upper bound on a refutation’s size, read off a valid rank descent.

Functions

certify_size_bound

Verify that ranks is a valid non-increasing measure and read off the SizeBound it certifies. Returns None if the measure ever increases (then it is not a termination measure and certifies nothing). The bound levels · max_width is a structural consequence of the annotation, so the checker never re-derives the proof — it only counts.