PRCZeroCalibratedPrimeSignedStrengthenedNativeCostUniquenessTarget
plain-language theorem explainer
Any native cost map on ratio orbits that meets the zero-calibrated, prime-signed strengthened ledger is forced to agree, under cross-multiplication equivalence, with the canonical J-cost at every orbit. Cost-selection packages and uniqueness certificates cite this as the repaired uniqueness surface after zero-flat and absolute-value routes were refuted. The declaration is a pure Prop packaging that universal claim; a sibling theorem discharges it.
Claim. For every map $F$ from ratio orbits to ratio orbits, if $F$ satisfies the zero-calibrated prime-signed strengthened native-cost hypotheses (zero doubled-trace at the zero orbit, signed unit, and calibration on all native prime axes and prime-pair products), then for every ratio orbit $q$ one has $F(q)\sim_{\times} J(q)$, where $J(q)=\frac{q+q^{-1}}{2}-1$ is the canonical ratio-orbit J-cost and $\sim_{\times}$ is cross-multiplication equivalence of ratio orbits.
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display: a signed-orbit numerator over a nonzero distinction-nat denominator. Cross-multiplication equivalence equates two such displays when the scaled numerators balance as signed orbits; it is the internal PRC stand-in for rational equality. The canonical cost on a ratio orbit is the rational J-object $J(q)=((q+q^{-1})/2)-1$, built entirely from orbit arithmetic (add, recip, half, sub).
The surrounding module repairs native-cost uniqueness after earlier zero-flat and absolute-value statements were refuted. The hypothesis bundle attached here strengthens the native ledger: the cost must have zero doubled-trace at the zero orbit, see the signed unit, and be calibrated on every native prime axis and every prime-pair product. That bundle is the final character-factorization interface for the zero-calibrated route.
Locally this sits inside PRC native-cost uniqueness, which feeds the δ-native cost-selection package and the universal-foundation open-target ledger.
proof idea
Definitional packaging only: the body is the universal Prop that every $F$ satisfying the zero-calibrated prime-signed strengthened native-cost hypotheses is pointwise crossEq-equal to the canonical onRatioOrbit cost. No tactics or lemmas are invoked at this declaration. The discharging proof is the sibling theorem that introduces $F$ and the hypotheses, obtains the signed-admissible character factorization for that ledger, and reduces each orbit to the crossEq identity with $J$.
why it matters
This is the repaired uniqueness surface for native J after the old zero-calibrated uniqueness target was refuted. Downstream, CostSelectionPackageNative takes it as j_unique_native: every native cost on the full itemized ledger (base hypotheses, prime-pair products, signed unit, all prime axes, zero orbit) is crossEq-pointwise the canonical cost, paired with a non-vacuous witness. The sibling proved theorem closes the target; the blocker certificate and PRCUniversalFoundationOpenTargets record it among the positive repaired interfaces while keeping the refuted routes as negative entries.
Framework-wise it is the δ-native counterpart of T5 J-uniqueness: the cost forced by the Recognition Composition Law is $J(x)=(x+x^{-1})/2-1$, here realized on ratio orbits rather than on reals. It does not reopen the absolute-value or zero-flat routes; those remain explicitly refuted in the open-target ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.