PRCNativeCostUniquenessTarget
plain-language theorem explainer
Every map on ratio orbits that obeys the PRC native cost hypotheses must agree with the discrete J-cost under cross-multiplication equality. Foundation authors cite this Prop when discharging δ-native cost classification without taking the continuous real uniqueness theorem as a premise. It is a pure definition packaging that quantified statement for later certificates and reduction lemmas.
Claim. For every map $F$ from ratio orbits to ratio orbits, if $F$ satisfies reciprocal symmetry, normalization invariance, the canonical Recognition Composition Law on orbits, and two-point calibration, then for every ratio orbit $q$ one has $F(q)\simeq J(q)$ under cross-multiplication, where $J(q)=\frac{q+q^{-1}}{2}-1$ is the orbit-level J-cost.
background
Primitive Recognition Calculus works on ratio orbits: each orbit is a signed-orbit numerator over a nonzero distinction-nat denominator. Equality of orbits is internal cross-multiplication balance (a.num·b.den against b.num·a.den), not real equality of displays. The discrete J-cost on an orbit is the orbit object $J(q)=((q+q^{-1})/2)-1$, built from orbit add, recip, mul, and half.
The native cost hypotheses package the discrete stand-ins for the continuous law-of-logic axioms: reciprocal symmetry of $F$, invariance under normalization of the ratio, a canonical Recognition Composition Law identity on orbits, and a two-point calibration that rules out the zero cost (the discrete analogue of unit log-curvature). The module goal is to classify admissible costs on this rational surface first, then transport to the positive-real theorem as a corollary.
Upstream, the continuous side still records an explicit Aczél smoothness package: continuous d'Alembert solutions with $H(0)=1$ are $C^\infty$, with classification $H\equiv 1$ or $H(t)=\cosh(\lambda t)$. The native target is meant to replace reliance on that real theorem as a premise.
proof idea
No proof body: this is a def equating a name to a quantified Prop. The right-hand side is the universal statement that any $F:(\mathrm{RatioOrbit}\to\mathrm{RatioOrbit})$ satisfying the native cost hypotheses is cross-equivalent, at every orbit $q$, to the discrete J-cost object. Downstream lemmas discharge the name by intro on $F$, the hypothesis pack, and $q$, then reduce via character factorization and rigidity targets.
why it matters
This is the exact missing native theorem named in the doc-comment: classify every admissible PRC cost on normalized ratio orbits, then obtain the continuous positive-real uniqueness as a corollary rather than a premise. It sits on the path to T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$) inside the forcing chain, expressed on the δ-native carrier instead of $\mathbb{R}_{>0}$.
Downstream, the PRC cost certificate records the rational formula and the real bridge; several reduction theorems derive this target from admissible character factorization plus rigidity, or from factorization upgrade plus prime calibration propagation. The continuum-price residue wall uses its negation: the base ledger (and several strengthenings) still admit non-J costs, so uniqueness is not closed on the native surface. The pass-25 blocker certificate splits the remaining gap into exact Lean targets rather than a single sorry.
Until those character and prime-propagation targets close, the framework still pays a continuum price for forcing J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.