slim_iff_sansSign_and_signed_unit
plain-language theorem explainer
The full slim native-cost hypothesis package on a map F of rational orbits is equivalent to the sans-sign slim package plus signed-unit calibration at −1. Anyone separating absolute-value uniqueness from the signed repair cites this bridge. The proof is a pure structure-field reassociation: no arithmetic is invoked.
Claim. For any $F : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$, the zero-calibrated signed strengthened native-cost hypotheses on $F$ hold if and only if both (i) the slim sans-sign hypotheses hold (strengthened base-plus-pairs package together with doubled-trace zero calibration) and (ii) $F$ is signed-unit calibrated, i.e. $F(-1)$ matches the native cost display at the signed unit.
background
In the Primitive Recognition Calculus, native costs act on RatioOrbit displays: integer numerator over a nonzero orbit denominator. The uniqueness program packages reciprocity, normalization invariance, nonzero RCL, unit-zero, two-calibration, and prime-pair probes into a strengthened class, then adds a signed-unit repair and a zero-orbit calibration.
The full slim class (PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses) is exactly that package: signed-strengthened hypotheses plus doubled-trace zero calibration. The sans-sign slice drops only the signed-unit field, keeping strengthened base-plus-pairs and zero calibration. Signed-unit calibration itself is the discrete cross-equality F(−1) = onRatioOrbit(−1), forced after the absolute-value no-go so the cost sees the signed unit, not only positive prime probes.
This module certifies minimality of the slim ledger. The present declaration is the bookkeeping bridge that factors the signed-unit field out of, and back into, the full slim package.
proof idea
Bidirectional structure unpacking via constructor.
Forward: from the full slim package, project signed_strengthened.strengthened and zero_calibrated into the sans-sign structure, and project signed_strengthened.signed_unit as the signed-unit calibration conjunct.
Reverse: given sans-sign hypotheses h and signed-unit calibration hsign, rebuild signed_strengthened from h.strengthened and hsign, then pair with h.zero_calibrated.
No lemmas about costs, orbits, or arithmetic are applied; the iff is definitional reassociation of nested Prop structures.
why it matters
This bridge lets the certificate layer treat the signed-unit field as an independent conjunct. Downstream, canonicalSelectedNativeCost_sans_sign_hypotheses applies the forward direction to the canonical selected native cost, proving non-vacuity of the sans-sign class. The tagged deposit slim_ledger_minimality_certificate_tagged sits on the same spine and records the delta-only slim ledger minimality certificate.
In the Recognition framework this is foundation bookkeeping for native-cost uniqueness under the Recognition Composition Law, not a forcing-chain step (T5–T8). It isolates the signed repair forced after the absolute-value no-go so minimality and uniqueness arguments can run first on the unsigned slim package, then reattach the −1 calibration. Without the iff, every consumer would have to unpack nested hypothesis structures by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.