slim_class_iff_full_class
plain-language theorem explainer
The slim native-cost hypothesis class (no explicit all-prime axis field) coincides with the full zero-calibrated prime-signed class. Native-cost uniqueness and minimality arguments in the Primitive Recognition Calculus cite this equivalence to drop a redundant premise. One direction forgets the prime-axis field; the other rebuilds it from the redundancy theorem that slim inhabitants are automatically prime-axis calibrated.
Claim. For any map $F$ from ratio orbits to ratio orbits, $F$ satisfies the slim zero-calibrated signed-strengthened native-cost hypotheses (base reciprocity, normalization invariance, nonzero RCL, unit-zero, two-calibration, prime-pair products, signed unit, and zero-orbit calibration) if and only if it satisfies the full zero-calibrated prime-signed strengthened hypotheses, which add explicit calibration on every native prime axis.
background
Ratio orbits are rational displays: an integer numerator over a nonzero distinction-nat denominator. Native costs are maps $F$ on those orbits; the doubled-trace package records their cost along the recognition composition law (RCL).
Two hypothesis bundles sit over such an $F$. The slim class packages signed-strengthened native-cost axioms (reciprocity, normalization invariance, nonzero RCL, unit-zero, two-calibration, prime-pair products, signed unit) together with zero-orbit calibration of the doubled trace. The full class adds an explicit all-prime axis field: calibration on every native prime direction.
The local module contracts the premise ledger for native-cost selection. Immediately upstream, the redundancy theorem states that every slim inhabitant is automatically calibrated on every native prime axis, so the extra field is not independent data.
proof idea
Term-mode constructor on the biconditional.
Forward: from a slim package, rebuild the full package by keeping signed_strengthened and zero_calibrated, and filling prime_direction_cost with all_prime_axis_field_redundant F hF (every slim inhabitant is prime-axis calibrated).
Reverse: from a full package, drop the prime-axis field and retain prime_signed.signed_strengthened with zero_calibrated. Pure structure reassembly; no new analytic work.
why it matters
Lets the minimality track work with a strictly smaller premise ledger while retaining the full uniqueness interface. Downstream, canonicalSelectedNativeCost_slim_hypotheses uses the reverse direction to place the round-1 non-vacuity witness in the slim class from its full-class membership. The contracted slim premise ledger is then shown to sit entirely at the $\delta$-only strength floor.
In the Recognition stack this is bookkeeping on the native-cost side of the forcing chain: RCL, J-uniqueness (T5), and the zero/unit calibrations that pin the cost before mass and coupling extractions. It closes the gap between the minted round-1 ledger and the slim selection ledger without adding physics assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.