StructuralStratificationCertificate
plain-language theorem explainer
On the countable ratio-orbit carrier, arithmetic alone forces the form of the native recognition cost; the only residual freedom is unit size, fixed by one orbit-2 anchor. Anyone citing free-side cost uniqueness, derived positivity, or the residual gauge analysis points here. The declaration is a Prop-structure bundling uniqueness, slim-ledger contraction, positivity, anchor necessity, infinite gauge orbit, gauge rigidity, and non-vacuity. No proof body: the inhabiting theorem fills the fields.
Claim. A certificate that: (1) every $F$ on ratio orbits obeying the structural ledger (base native axioms, sign reversal, monotonicity, zero-orbit calibration, and the orbit-2 anchor) agrees with the canonical native cost on every orbit; (2) those hypotheses imply the slim zero-calibrated signed strengthened ledger; (3) positivity of $F$ follows; (4) dropping the anchor destroys uniqueness; (5) the anchor-free class contains infinitely many odd-power-generated costs, pairwise unequal at the anchor; (6) under monotonicity and character factorization, equal anchor values force equal costs on all positive integer orbits; (7) the canonical selected native cost inhabits the structural class.
background
The module develops a primitive recognition calculus for native costs on the countable carrier of ratio orbits (pairs of nonzero rationals up to reciprocal identification). The structural ledger packages reciprocity, normalization invariance, the nonzero composition law, unit-zero, a single orbit-2 anchor, plus sign reversal, monotonicity on positive integer orbits, and zero-orbit calibration. Compared with earlier slim ledgers, prime-pair product families and signed-unit calibrations that mentioned the canonical cost are gone.
Uniqueness means any such $F$ is cross-equal to the canonical display cost on every orbit. Positivity (nonnegative cost on positive rationals) is listed as derived, not assumed. Removing the orbit-2 anchor yields a sans-anchor ledger whose uniqueness target is false: cube-type costs survive. Odd-power-generated native costs witness an infinite gauge orbit, distinguished by their value at the generator two. Gauge rigidity says that, given monotone character-factorized costs, matching at two forces matching on every positive integer orbit.
Upstream pieces include the reciprocal automorphism of the cost algebra, positive-integer-orbit predicates, and monotone native-cost predicates used to state the gauge fields.
proof idea
Definition only: a seven-field Prop structure with empty body. Each field is a named target or universal statement already proved elsewhere in the module. The companion theorem structuralStratificationCertificate_holds inhabits the structure by assigning proved lemmas fieldwise (uniqueness target proved, structural-forces-slim, structural-forces-positive, sans-anchor uniqueness refuted, plus the gauge-orbit, rigidity, and nonvacuity witnesses). No tactic work lives on this declaration itself.
why it matters
This is the free-side stratification receipt: on the countable carrier the cost form is forced by arithmetic, and residual freedom is only the unit gauge fixed by one anchor. Downstream, structuralStratificationCertificate_holds is the single inhabiting theorem that turns the bundle into a proved certificate.
In the Recognition framework this sits under native-cost uniqueness parallel to T5 J-uniqueness on the completed side: the structural ledger replaces ad-hoc slim hypotheses that mentioned the canonical cost, derives positivity, and isolates the anchor as a genuine unit gauge (without it the cube cost appears; with it the gauge orbit is infinite yet rigid). The module comment stresses that three of four reciprocal-generator facts are $\delta$-native on the carrier; the completion purchase is separate. The certificate is the public spine tag for that free-side claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.