PRCNativeCostUniquenessTarget_of_character_factorization_upgrade_and_prime_propagation
plain-language theorem explainer
Under three discrete hypotheses (character factorization of native RCL costs, upgrade of that factor to an admissible character, and prime-calibration propagation), every admissible PRC-native cost on ratio orbits equals the canonical orbit cost. Cite this when assembling the native uniqueness theorem from its factorization and rigidity blockers. The proof is a pure term composition of two intermediate upgrades into the admissible-character uniqueness lemma.
Claim. Assume (i) every admissible PRC-native RCL cost $F$ factors through some ratio character $\chi$ with $F(q)\sim\mathrm{cost}_\chi(q)$ on every ratio orbit $q$; (ii) any such factor may be replaced by an admissible ratio character generating the same cost; (iii) once a ratio character is calibrated on every prime direction, its character cost agrees with the canonical orbit cost on every rational direction. Then every admissible PRC-native cost equals the canonical cost on every ratio orbit.
background
Primitive Recognition Calculus works on normalized ratio orbits rather than bare positive reals. A PRC-native cost is a map $F$ on ratio orbits satisfying the discrete Recognition Composition Law hypotheses (reciprocity, normalization, and the cross-equation form of RCL). The canonical comparison object is the orbit-level cost onRatioOrbit, the discrete avatar of the unique continuous $J$-cost $J(x)=(x+x^{-1})/2-1$ forced at T5.
Three named targets package the remaining discrete work. Character factorization asks that every admissible native cost factor as $F\sim\mathrm{cost}_\chi$ for a ratio character $\chi$ (the discrete d'Alembert step). The admissibility upgrade weakens the demand that $\chi$ itself be admissible: because $J$ cannot tell a direction from its reciprocal, it is enough to replace $\chi$ by an admissible $\psi$ with the same generated cost. Prime-calibration propagation is the unique-factorization half of rigidity: calibration on prime axes extends to every rational orbit.
The uniqueness target itself asserts $\forall q,, F(q)\sim\mathrm{onRatioOrbit}(q)$ for every admissible native $F$. The continuous positive-real uniqueness theorem is intended as a corollary of this native statement, not a premise.
proof idea
Pure term-mode composition, no tactics. First apply the upgrade lemma that turns character factorization plus the admissibility-upgrade target into admissible-character factorization. Separately apply the lemma that turns prime-calibration propagation into admissible-character rigidity (it just unpacks the admissible character's ratio-character and prime-calibrated fields and feeds them to the propagation hypothesis). Feed those two derived admissible-character targets into the already-proved combiner that concludes native cost uniqueness from admissible factorization plus admissible rigidity.
why it matters
This is the top assembly step for the exact missing native uniqueness theorem in the PRC $J$-cost module: classify every admissible PRC cost on normalized ratio orbits, then transport to the continuous positive-real theorem as a corollary. It sits at the end of the discrete forcing path that realizes T5 ($J$-uniqueness) and the Recognition Composition Law on the orbit category, before continuous transport.
No downstream consumers are wired yet (used_by is empty), so the declaration is presently a proved reduction rather than a leaf of a larger closed theorem. Its value is architectural: it collapses three independently attackable blockers (factorization, admissibility upgrade, prime propagation) into a single uniqueness obligation. Closing those three targets discharges native uniqueness without smuggling in the real-domain uniqueness theorem as a premise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.