PRCStructuralSansAnchorUniquenessTarget
plain-language theorem explainer
Packages the uniqueness claim for the structural native-cost ledger with the unit anchor removed: every F on ratio orbits meeting the remaining structural hypotheses must match the canonical J-cost under cross-equivalence. Cited by the refutation proving the anchor is a genuine unit gauge, and by the free-side stratification certificate. Pure Prop definition; no proof content.
Claim. For every map $F$ from ratio orbits to ratio orbits, if $F$ satisfies the structural native-cost hypotheses without the unit anchor (base without two-point calibration, sign-reversing, monotone, and zero-calibrated doubled trace), then for every ratio orbit $q$, $F(q)$ is cross-equivalent to the canonical cost $J(q)=((q+q^{-1})/2)-1$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero orbit denominator: the internal rational display of PRC. Cross-equivalence of two ratio orbits means their cross-multiplied signed orbits balance (the PRC stand-in for rational equality). The canonical cost on this carrier is the ratio-orbit J-object $J(q)=((q+q^{-1})/2)-1$, not yet the real-analytic uniqueness theorem.
The structural native-cost hypotheses without anchor collect four fields on a candidate $F$: the base ledger minus two-point calibration, sign-reversal, monotonicity, and zero-calibration of the doubled trace. The module treats the full structural ledger as exactly this anchor-free package plus one unit-fixing anchor field.
This definition is the uniqueness target for that stripped ledger: agreement of $F$ with $J$ under cross-equivalence for every ratio orbit.
proof idea
Definitional packaging only. The body is the universal quantification over maps $F$ and ratio orbits $q$, with the antecedent the four-field structure PRCStructuralNativeCostHypothesesSansAnchor and the consequent cross-equivalence of $F(q)$ to onRatioOrbit q. No tactics, no lemmas applied.
why it matters
Marks the precise claim that the free-side structural ledger, without a unit anchor, would force the canonical cost. Downstream, PRCStructuralSansAnchorUniquenessTarget_refuted shows the claim is false: the cube-generated native cost meets the anchor-free hypotheses yet fails to match $J$ at the two-point, so the anchor is a genuine unit gauge rather than redundant structure.
That refutation feeds StructuralStratificationCertificate, whose uniqueness field restores the full structural ledger (with anchor) and records that arithmetic alone forces the form of the cost on the countable carrier, leaving only unit size free. In the broader forcing chain this is the ledger-level counterpart of T5 J-uniqueness: the Recognition Composition Law shape is forced structurally, while the overall scale is a one-parameter gauge choice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.