Module category_collapse 

The category of collapses — the 2-rung toward the ∞-tower.

Fix a problem and its refutation. Its Lyapunov measures (levelings of the proof) form a category: objects are valid measures (non-increasing potentials over the proof steps), and a morphism V → W is a refinement — a monotone map φ with W = φ ∘ V, so V distinguishes states at least as finely as W. This is a thin category (a preorder under refinement). Its initial object is the finest measure (the linear, one-level-per-step proof-induced measure); its terminal object is the coarsest valid leveling. Different physics give different objects; refinements are the 2-cells relating them.

Where the ∞ begins (honestly): this is one thin 1-category per problem. The next rung is functors between these categories — measure transfer between problems (a reduction F → F' carrying a measure of F' back to one of F). When those functors and the natural transformations between them cohere, you get a 2-category of collapses, then higher. We build this rung solidly and state the climb precisely; we do not claim the tower.

Structs

Reduction

A reduction ρ: F' → F — a sign-respecting variable→literal map. It acts on clauses, on substitution witnesses (by conjugation ρσρ⁻¹), and hence on whole refutations. When ρ(F') ⊆ F (the source embeds into the target), ρ carries any refutation of F' to one of F. This is the morphism along which the transfer functor moves collapses between problems.

Functions

iso

Are two measures isomorphic in the category — mutual refinements (the same partition of steps up to relabeling levels)?

refines

Does fine refine coarse? I.e., is there a monotone φ with coarse = φ ∘ fine? Equivalent to fine[i] ≥ fine[j] ⟹ coarse[i] ≥ coarse[j] for all i, j. Requires equal length (two levelings of the SAME proof). A true means fine is at least as fine a partition of the proof steps as coarse — the morphism fine → coarse in the category of collapses.

transfer

The transfer functor. Carry a refutation/measure of F' to one of F along ρ, preserving the level structure (ranks). Re-checks the transferred proof against F (fail-closed): returns the transferred ranked refutation iff it genuinely refutes the target. Functorial — transfer along the identity reduction is the identity, and along a composite is the composite.