PRCStructuralNativeCostUniquenessTarget_proved
plain-language theorem explainer
Any cost map on ratio orbits that satisfies the structural native-cost hypotheses is cross-equivalent to the canonical cost on every orbit. Round-5 terminal uniqueness: the structural ledger forces the J-cost. Cited by positivity, slim-ledger collapse, and the structural stratification certificate. Proof factors F through a zero-calibrated character, calibrates it on positive integers, primes, prime products and the signed unit, then applies signed admissible character rigidity.
Claim. If $F$ is a map on ratio orbits satisfying the structural native-cost hypotheses, then for every ratio orbit $q$ one has $F(q)\sim_{\times} J(q)$, where $\sim_{\times}$ is cross-multiplication equivalence of orbits and $J$ is the canonical cost on ratio orbits.
background
The Primitive Recognition Calculus works with ratio orbits: pairs of signed $\delta$-orbits encoding rational displays. Two orbits are related by crossEq when cross-multiplication balances (K4.10); this agrees with equality of rational displays via crossEq_iff_toRat_eq.
A positive integer orbit is one whose display is a natural number $n\ge 1$. The structural native-cost hypotheses package zero-calibration, sign-reversal, and native RCL-type structure on $F$. The canonical cost on orbits is the discrete $J$-cost (the T5 unique cost $J(x)=(x+x^{-1})/2-1$ in display).
Upstream, zero-calibrated native costs factor as $F=\mathrm{costFromCharacter},\chi$ for a real character $\chi$. Characters that respect cross-equivalence, are calibrated on prime directions and prime-pair products, and fix the signed unit, are rigid: they reproduce the canonical cost on every orbit.
proof idea
Tactic proof. From structural hypotheses extract a zero-calibrated native factorization $F\sim\mathrm{costFromCharacter},\chi$. Structural calibration gives $\chi$ correct on positive integer orbits; normalize-ratio canonicity upgrades $\chi$ to respect crossEq, so display equality of orbits implies display equality of $\chi$-images.
Positive-integer calibration of the character cost follows by transporting along natOrbit. Restrict to prime directions and to products of two prime directions (using toNat and mul_toRat) to obtain prime and prime-pair calibration. Sign-reversal plus unit-zero forces the cost at $-1$ to match the canonical signed unit; that yields signed-unit calibration of $\chi$.
Conclude by transitivity of crossEq: $F(q)\sim\mathrm{costFromCharacter},\chi(q)$, and signed admissible character rigidity identifies the latter with the canonical cost at $q$.
why it matters
Doc-comment labels this the Round 5 terminal: the structural ledger forces the canonical cost. It is the uniqueness engine that turns a short structural axiom pack into full identification with $J$ on ratio orbits, aligning with T5 $J$-uniqueness in the forcing chain.
Downstream, structural_forces_positive quotes it to prove positivity is a theorem ("Recognizing a positive imbalance never pays"). structural_forces_slim uses it to collapse the structural pack onto the zero-calibrated signed strengthened ledger, making the prime-pair family redundant against monotonicity. structuralStratificationCertificate_holds installs it as the uniqueness field of the structural stratification certificate, alongside slim contraction, positivity, and gauge non-inhabitation.
Without this theorem the structural ledger would not pin $F$ to the RS native cost; with it, later ledger strata inherit canonicity rather than re-axiomatizing $J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.