PRCZeroCalibratedNativeCostUniquenessTarget
plain-language theorem explainer
Any ratio-orbit cost F that obeys the PRC native hypotheses and whose doubled trace vanishes at zero is forced to match the canonical J-cost under cross-multiplication. Foundation and cost-classification work cite this Prop as the exact uniqueness surface to prove or refute. The declaration is a pure definition packaging that universal statement; no proof is attached.
Claim. For every map $F$ from ratio orbits to ratio orbits, if $F$ satisfies the native cost hypotheses (reciprocal symmetry, normalization invariance, and the canonical recognition composition law) and the doubled trace $T_F(q)=2(F(q)+1)$ is zero-calibrated ($T_F(0)\sim 0$ under cross-multiplication), then for every ratio orbit $q$ one has $F(q)\sim J(q)$ under cross-multiplication, where $J(q)=((q+q^{-1})/2)-1$.
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display: a signed-orbit numerator over a nonzero distinction-nat denominator. Two ratio orbits are identified by cross-equality when the cross-multiplied signed orbits balance; that is the internal PRC stand-in for rational equality.
The canonical cost on this surface is the ratio-orbit J-object $J(q)=((q+q^{-1})/2)-1$. Native cost hypotheses on a candidate $F$ require reciprocal symmetry, invariance under denominator normalization, and the discrete recognition composition law. The doubled trace of $F$ is $T_F(q)=2(F(q)+1)$; for character-generated costs this recovers $\chi(q)+\chi(q)^{-1}$. Zero-calibration demands $T_F(0)\sim 0$, the missing zero-orbit constraint that the nonzero d'Alembert law cannot supply.
This module packages uniqueness and factorization targets for that discrete surface, bridging toward the continuous T5 J-uniqueness result without assuming a completed real analytic layer.
proof idea
Definition only: the body is the quantified Prop itself. No tactics, no lemmas applied, no wrapper. Downstream theorems either assume this Prop, derive it from stronger factorization or rigidity targets, or refute it by exhibiting a counterexample cost.
why it matters
This is the exact uniqueness surface for zero-calibrated native costs on the PRC rational orbit layer, the discrete analogue of T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$). It feeds the Pass-25 blocker certificate, which records that native cost uniqueness is not closed and splits the missing mathematics into named Lean targets. The universal-foundation open-target ledger carries a negative entry: the target has been refuted by the absolute-value generated native cost, which satisfies the native hypotheses and zero-calibration yet fails to match canonical $J$ at $-1$. Positive repair routes go through character factorization plus rigidity, or through signed-admissible factorization (the latter route is itself refuted). The definition therefore pins both the failed uniqueness claim and the surviving factorization interfaces that remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.