PRCStructuralNativeCostUniquenessTarget
plain-language theorem explainer
Names the uniqueness target for structural native costs: any map on ratio orbits obeying the structural native-cost hypotheses must match the canonical orbit embedding up to display cross-equality (identity modulo reciprocal orientation the cost cannot see). Round-5 ledger work and the free-side stratification certificate cite this Prop as the statement to discharge. Pure definitional packaging of a quantified claim, not a proof.
Claim. For every map $F$ from ratio orbits to ratio orbits, if $F$ satisfies the structural native-cost hypotheses, then for every ratio orbit $q$ one has $F(q)$ cross-equal (in display) to the canonical image of $q$ on the ratio orbit, up to the global reciprocal orientation invisible to the cost.
background
In the Primitive Recognition Calculus, recognition events carry positive ratios and a non-negative cost given by the J-cost $J$ (the unique symmetric cost forced by the Recognition Composition Law). Ratio orbits are the discrete carriers on which structural ledger arguments run; the canonical embedding sends each orbit to its standard representative on that carrier.
A structural native-cost map is a self-map of ratio orbits obeying a package of hypotheses (native cost axioms plus zero-calibration). Cross-equality on orbits is display identity up to the reciprocal automorphism: swapping source/target and inverting the ratio leaves $J$ unchanged, so the cost cannot fix global orientation.
This module sits in the structural ledger layer of PRC native-cost forcing. Upstream cost constructions (observer J-cost, multiplicative-recognizer derived cost, rung-coarsened summed weights) all feed the same uniqueness pressure: arithmetic on the countable carrier should pin the form of the cost once calibration is fixed.
proof idea
Definitional, not a proof. The body is a single universal Prop: quantify over self-maps $F$ of ratio orbits, assume the structural native-cost hypothesis package on $F$, and demand that every orbit $q$ satisfies display cross-equality between $F(q)$ and the canonical on-orbit image of $q$. No tactics, no lemmas applied at this site; discharge happens downstream when the hypotheses are unpacked into character factorization and zero-calibration.
why it matters
This is the round-5 engine statement for the structural ledger: the character attached to a structural cost is forced to the identity in display on every positive integer orbit, up to reciprocal orientation. Downstream, PRCStructuralNativeCostUniquenessTarget_proved discharges it ("Round 5 terminal. The structural ledger forces the canonical cost") by factoring through the zero-calibrated native-cost character factorization target.
It is also a required field of StructuralStratificationCertificate, the free-side stratification: on the countable carrier the form of the cost is forced by arithmetic alone, with residual freedom only the unit size fixed by one anchor. In the broader RS chain this is the ledger-side face of T5 J-uniqueness: once structural hypotheses hold, no competing native cost survives on ratio orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.