PRCSignReversingNativeCostUniquenessTarget_proved
plain-language theorem explainer
Any ledger map on ratio orbits that meets the sign-reversing native-cost hypotheses is forced to match the canonical cost on every orbit. This is the Round 4 terminal uniqueness statement in the primitive recognition calculus. The structural stratification certificate cites it. The proof packages the sign-reversing data into the zero-calibrated signed-strengthened hypotheses and applies that uniqueness theorem.
Claim. For every map $F$ from ratio orbits to ratio orbits, if $F$ satisfies the sign-reversing native-cost hypotheses (strengthened native cost structure, zero calibration, and sign-reversal), then for every ratio orbit $q$ one has $\mathrm{crossEq}(F(q),\,J_{\mathrm{can}}(q))$, i.e. $F$ agrees with the canonical cost orbit of $q$.
background
In the primitive recognition calculus, candidate cost ledgers are maps $F$ on ratio orbits. The canonical target is the orbit of the RS cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), recovered here via cross-equality with the canonical orbit map. Round 4 of the structural ledger asks how little structure forces that identification.
The sign-reversing package keeps strengthened native-cost structure and zero calibration, and adds ledger antisymmetry (sign-reversal) instead of an explicit signed-unit calibration. Upstream, the signed-unit field is not independent: applying ledger antisymmetry at the unit yields it ("The signed-unit field is not an assumption. Ledger antisymmetry applied at the unit produces it.").
One step further upstream, the zero-calibrated signed-strengthened uniqueness theorem already forces the canonical cost: "The slim ledger already forces $J$." Factorization uses base plus zero; pair and sign fields transfer to the factor character; transport recovers per-prime calibration; signed-admissible rigidity closes.
proof idea
Term-mode reduction, not a fresh rigidity argument. Introduce $F$, the sign-reversing hypotheses, and an orbit $q$. Apply the zero-calibrated signed-strengthened uniqueness theorem to the same $F$ and $q$, supplying a goal for the missing hypothesis bundle.
Build that bundle by copying strengthened structure and zero calibration from the sign-reversing package, and filling the signed-unit field with signReversing_forces_signed_unit on the native unit-zero fact together with the sign-reversing hypothesis. Once the bundle matches, the upstream uniqueness theorem returns cross-equality with the canonical cost orbit.
why it matters
This is the Round 4 terminal: the sign-reversing ledger forces the canonical cost. It sits on the uniqueness spine that realizes T5 $J$-uniqueness inside the primitive recognition calculus, closing a structural stratum where antisymmetry replaces an explicit signed-unit axiom.
Downstream it feeds structuralStratificationCertificate_holds, which assembles uniqueness, slim contraction, positivity, and a gauge non-inhabitation refutation into the structural stratification certificate. That certificate is the bookkeeping object showing which ledger fragments already pin $J$ and which remain open.
Relative to the forcing chain, the content is local foundation rather than a new physical constant: once ledgers are forced to $J$, the RCL and the later T6--T8 steps (phi, eight-tick octave, $D=3$) inherit a unique cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.