PRCZeroCalibratedPrimeSignedStrengthenedNativeCostUniquenessTarget_proved
plain-language theorem explainer
Any map F on rational ratio-orbits that obeys the zero-calibrated, prime-signed, strengthened native-cost hypotheses is cross-equal to the canonical native cost on every orbit. Foundation and cost-selection arguments cite this as the repaired native J-uniqueness statement after zero-flat and absolute-value no-gos. The proof factorizes F through a signed-admissible character, then chains character rigidity by cross-equality transitivity.
Claim. For every map $F$ from ratio-orbits to ratio-orbits, if $F$ satisfies the zero-calibrated prime-signed strengthened native-cost hypotheses, then for every ratio-orbit $q$ one has $\mathrm{crossEq}(F(q),\,\mathrm{onRatioOrbit}(q))$: $F$ agrees with the canonical native cost up to cross-equality on orbits.
background
Primitive Recognition Calculus works with ratio-orbits: integer (signed-orbit) numerators over nonzero distinction-nat denominators. Cross-equality is the choice-free equivalence on those displays, routed through an integer bridge so middle denominators cancel. The canonical native cost appears as onRatioOrbit.
The ambient uniqueness target is the zero-calibrated replacement after zero-flat and absolute-value no-gos: one no longer claims bare uniqueness of an old native cost, but uniqueness under strengthened prime-signed hypotheses that force signed-admissible character factorization. Recognition cost elsewhere is J-cost (or doubled J under ratio weights); here the object is the discrete orbit-level native cost before real embedding.
Upstream, signed-admissible character rigidity already pins admissible characters to the canonical cost, and a factorization theorem produces such a character from any $F$ meeting the strengthened hypotheses. Cross-equality is transitive via the integer-bridge lemma.
proof idea
Term-mode proof by introduction on $F$, its hypotheses, and an orbit $q$. Apply the signed-admissible character factorization target to $F$ to obtain a character $\chi$, a signed-admissibility witness, and a cross-equality $F\sim\chi$. For the given $q$, feed $\chi$ and admissibility into the signed-admissible character rigidity theorem, which yields $\chi(q)\sim\mathrm{onRatioOrbit}(q)$. Close by RatioOrbit.crossEq_trans on those two cross-equalities. No further case splits.
why it matters
This is the native J-uniqueness leg of the cost-selection package: costSelectionPackageNative_holds installs it as j_unique_native, together with a non-vacuous canonical selected native cost. That package is how PRC selects the unique native cost after the repaired factorization path, aligning with framework T5 (J-uniqueness of $J(x)=(x+x^{-1})/2-1$) at the discrete orbit layer before continuum forcing.
It also feeds the native-cost uniqueness blocker certificate and the conditional universal-foundation certificate, so the zero-calibrated strengthened uniqueness is part of the foundation spine rather than a side lemma. The surrounding module records that older absolute-value and unsigned uniqueness targets were refuted; this strengthened signed prime form is the surviving replacement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.