PRCSlimSansSignUniquenessTarget
plain-language theorem explainer
Defines the uniqueness target for cost maps on ratio orbits that obey the slim ledger without the signed-unit field: strengthened native-cost axioms plus zero calibration. Any such map is required to match the canonical rational J-cost under cross-multiplication equality. Cited by the signed-unit necessity refutation and the slim-ledger minimality certificate. Pure propositional packaging; no proof content.
Claim. The sans-sign uniqueness target is the proposition that every map $F$ from ratio orbits to ratio orbits satisfying the slim-sans-sign hypotheses (strengthened native-cost axioms together with zero calibration of the doubled trace) obeys $\mathrm{crossEq}(F(q), J(q))$ for every ratio orbit $q$, where $J(q)=((q+q^{-1})/2)-1$ is the rational $J$-cost on ratio orbits.
background
In the Primitive Recognition Calculus, rationals are carried as ratio orbits: a signed-orbit numerator over a nonzero distinction-nat denominator. Equality of two such displays is internal cross-multiplication balance (crossEq), not a real embedding.
The native cost object on a ratio orbit is the rational $J$-cost $J(q)=((q+q^{-1})/2)-1$, built from orbit addition, reciprocal, and half. The slim ledger is a minimal axiom package meant to force this $J$. The sans-sign variant keeps the strengthened package (base axioms plus pairs) and zero calibration of the doubled trace, but drops the signed-unit field.
PRCSlimSansSignHypotheses F packages exactly those remaining constraints on a candidate cost map $F$. The present definition turns that package into a uniqueness claim: every such $F$ must agree with canonical $J$ under crossEq.
proof idea
Definitional packaging only. The body is the universal quantification over maps $F:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ of the implication from PRCSlimSansSignHypotheses F to pointwise crossEq agreement with onRatioOrbit. No tactics, no lemmas applied, no reduction steps.
why it matters
This target is the exact claim that the slim ledger without the signed-unit field would force uniqueness of the rational $J$-cost. Downstream, PRCSlimSansSignUniquenessTarget_refuted shows the claim is false: the absolute-value generated native cost satisfies the sans-sign hypotheses yet fails canonicity at the signed unit (negative one). That refutation is one of the four necessity legs in SlimLedgerMinimalityCertificate, which records that each removable calibration field of the slim ledger is essential.
In the Recognition framework this sits under T5 $J$-uniqueness: the composition law forces $J(x)=(x+x^{-1})/2-1$, and the ledger axioms are the discrete native packaging of that uniqueness. Showing the signed unit cannot be dropped keeps the native cost sensitive to orientation on ratio orbits, not merely to absolute magnitude.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.