structural_forces_slim
plain-language theorem explainer
Any cost map on ratio orbits that obeys the structural ledger (base native axioms, sign reversal, monotonicity, zero-orbit calibration) automatically obeys the slimmer round-2 ledger that still lists prime-pair product costs and signed-unit calibration. Stratification and uniqueness certificates cite this contraction. The proof rebuilds the slim package from structural uniqueness plus the signed-unit derivation from sign reversal.
Claim. Let $F$ map ratio orbits to ratio orbits. If $F$ satisfies the structural native-cost ledger (base reciprocity/normalization/nonzero composition/unit-zero/orbit-2 anchor, sign reversal, monotonicity, and zero-orbit calibration), then $F$ satisfies the zero-calibrated signed strengthened native-cost hypotheses: the same base, the prime-pair product cost family, signed-unit calibration, and zero-orbit calibration.
background
Ratio orbits are rational displays: a signed-orbit numerator over a nonzero distinction-orbit denominator. Native cost maps $F$ on these orbits are constrained by a hierarchy of hypothesis ledgers that encode Recognition Composition Law structure without naming the closed-form $J$-cost.
The structural ledger packages the base native axioms with sign reversal, monotonicity, and zero-orbit calibration. Relative to the round-2 slim ledger, it drops the countable prime-pair product family and the signed-unit calibration field; those are meant to be recovered rather than assumed.
The slim target is zero-calibrated signed strengthened native cost: base plus prime-pair products, signed unit, and zero orbit. Upstream, structural uniqueness already forces the canonical cost on every orbit, and sign reversal at the unit forces signed-unit calibration.
proof idea
Term-mode structure assembly, not a long tactic script.
First apply structural uniqueness: under the structural hypotheses, $F$ equals the canonical cost on every ratio orbit. That identity discharges the prime-pair product cost field for free (any instance of the canonical cost satisfies those identities).
Next apply the signed-unit derivation: unit-zero together with sign reversal yields signed-unit calibration, so that field is not an independent axiom.
Copy native and zero-calibration from the structural package, wrap them into the strengthened then signed-strengthened layers, and return the slim hypothesis structure.
why it matters
This is the ledger-contraction step in the structural stratification certificate: structural hypotheses imply the slim package (contracts_slim), so the prime-pair family is redundant once monotonicity and uniqueness are in hand. Downstream structuralStratificationCertificate_holds records uniqueness, this contraction, positivity-as-theorem, and a gauge-inhabitation refutation side-by-side.
In the Primitive Recognition Calculus cost program, the move is to thin countable calibration families down to structural axioms (sign reversal, monotonicity) that never mention the closed form of $J$. That supports the broader claim that the Recognition Composition Law cost is forced rather than fitted, aligning with the T5 $J$-uniqueness landmark in the forcing chain.
No open scaffold remains on this arrow: both uniqueness and signed-unit recovery are already proved inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.