PRCNativeCostUniquenessTarget_of_character_targets
plain-language theorem explainer
If every admissible PRC-native RCL cost factors through a ratio character, and every two-calibrated character cost is forced to the identity character, then the native cost is unique: it agrees with the canonical orbit cost under cross-multiplication. Foundation workers closing the PRC native-cost uniqueness blocker cite this reduction. The argument is a short composition of factorization, calibration transfer at two, and rigidity.
Claim. Assume (i) every $F:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ satisfying the PRC-native cost hypotheses factors as $F(q)\sim\mathrm{cost}_\chi(q)$ for some ratio character $\chi$, and (ii) any such character with $\mathrm{cost}_\chi(2)\sim\mathrm{id}(2)$ satisfies $\mathrm{cost}_\chi(q)\sim\mathrm{id}(q)$ for all orbits $q$. Then every admissible native cost $F$ obeys $F(q)\sim\mathrm{id}(q)$ for all $q$, where $\sim$ is cross-multiplication equivalence of ratio orbits.
background
In the Primitive Recognition Calculus, costs live on ratio orbits rather than on bare reals. Two orbits are identified by cross-multiplication equivalence: $a\sim b$ when the signed $\delta$-orbits $a.\mathrm{num}\cdot b.\mathrm{den}$ and $b.\mathrm{num}\cdot a.\mathrm{den}$ balance. That relation is the internal PRC stand-in for rational equality, and it is symmetric and transitive by the IntegerRational lemmas.
A PRC ratio character is a multiplicative map on orbits; costFromCharacter builds the associated cost, while onRatioOrbit is the canonical identity-character cost (the discrete native $J$-cost on orbits). Admissible native costs are those $F$ obeying the PRC-native hypotheses, including two-calibration: $F(2)\sim\mathrm{id}(2)$.
The module splits native-cost uniqueness into exact blockers. Factorization asks that every admissible $F$ come from some character (discrete d'Alembert step). Rigidity asks that a character already calibrated at two must be the identity character everywhere, killing prime-direction freedom.
proof idea
Term-style tactic proof. Fix an admissible native cost $F$ and an orbit $q$. Apply the factorization hypothesis to obtain a ratio character $\chi$ with $F(r)\sim\mathrm{cost}_\chi(r)$ for every $r$.
At $r=2$, symmetrize $F(2)\sim\mathrm{cost}\chi(2)$ and compose with the two-calibration hypothesis $F(2)\sim\mathrm{id}(2)$ via crossEq_trans / crossEq_symm, yielding $\mathrm{cost}\chi(2)\sim\mathrm{id}(2)$.
Feed that calibration into the rigidity hypothesis to get $\mathrm{cost}\chi(q)\sim\mathrm{id}(q)$. One more crossEq_trans with $F(q)\sim\mathrm{cost}\chi(q)$ closes $F(q)\sim\mathrm{id}(q)$.
why it matters
Native uniqueness of the PRC cost is the discrete counterpart of T5 $J$-uniqueness ($J(x)=\cosh(\log x)-1$) under the Recognition Composition Law. Closing it on ratio orbits is required before the continuous $J$-cost and the forcing chain can be treated as forced rather than chosen.
This theorem does not discharge uniqueness; it reduces the uniqueness target to the conjunction of the factorization and rigidity blockers. Downstream, prc_native_cost_uniqueness_blocker_certificate packages the Pass-25 status: uniqueness is not closed, but the missing mathematics is split into exact Lean targets (including zero-calibrated factorization variants already proved or refuted).
Anyone auditing whether the native RCL cost is forced to the identity character on orbits cites this glue step: uniqueness holds as soon as both character targets hold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.