PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget_proved
plain-language theorem explainer
Any native cost map on ratio orbits that satisfies the slim ledger (zero calibration, signed strengthened native axioms) is cross-equivalent to the canonical J-cost J(q)=((q+q^{-1})/2)-1 at every orbit. Cited by the slim cost-selection package, the minimality certificate, and the sign-reversing uniqueness terminal. Proof factors through a character, transports pair and sign data, recovers prime calibration from the two-point anchor, then closes by signed-admissible rigidity.
Claim. Let $F$ be a map from ratio orbits to ratio orbits. If $F$ obeys the zero-calibrated signed strengthened native-cost hypotheses (native cost axioms, two-calibration, prime-pair product consistency, signed unit, and zero calibration), then for every ratio orbit $q$ one has $F(q)\sim J(q)$, where $\sim$ is cross-multiplication equivalence of ratio orbits and $J(q)=((q+q^{-1})/2)-1$ is the PRC rational $J$-cost.
background
Primitive Recognition Calculus works on ratio orbits: integer numerator over a nonzero distinction-nat denominator, with equality replaced by cross-multiplication balance of scaled signed orbits (crossEq). The canonical cost on this display is the ratio-orbit object $J(q)=((q+q^{-1})/2)-1$, written onRatioOrbit.
The slim uniqueness target asks that every $F$ meeting a contracted hypothesis package agree with $J$ under crossEq at all orbits. That package bundles native cost structure, two-calibration at the orbit $2$, prime-pair product consistency, signed-unit calibration, and zero calibration; the full per-prime axis field is deliberately omitted.
Upstream, character factorization (base plus zero) produces a multiplicative character $\chi$ with $F$ cross-equivalent to the cost built from $\chi$. Cross-equivalence is an equivalence relation (crossEq_symm, crossEq_trans). A transport lemma upgrades pair consistency plus two-calibration on $\chi$ into full prime-direction calibration of $\chi$.
proof idea
Introduce $F$ and the slim hypotheses, and fix an arbitrary orbit $q$. Apply the already-proved zero-calibrated native character factorization to obtain a character $\chi$ with $F\sim\mathrm{costFromCharacter},\chi$.
Transfer prime-pair product consistency from $F$ to $\chi$ by sandwiching with the factorization equivalence (symmetry then transitivity of crossEq). Likewise transfer two-calibration at the orbit $2$. The transport lemma character_pair_two_calibration_forces_prime_calibration then yields prime-direction calibration of $\chi$.
Transfer signed-unit data at $-1$ the same way, and invoke costFromCharacter_negativeOne_forces_signed_unit to get signed-unit calibration of $\chi$. Finally apply signed-admissible character rigidity to $\chi$ and compose with the factorization equivalence to conclude $F(q)\sim J(q)$.
why it matters
This is the uniqueness engine for the contracted (slim) native cost ledger: the slim package already forces $J$, so the all-prime axis field is redundant. Downstream, all_prime_axis_field_redundant is a one-line specialization to prime directions; costSelectionPackageNativeSlim_holds installs this theorem as j_unique_native_slim; the slim minimality certificate records it as slim_uniqueness; and the Round-4 sign-reversing uniqueness terminal reduces to it by packaging stronger hypotheses into the slim ones.
In the Recognition forcing chain this is the native, choice-free face of T5 $J$-uniqueness ($J(x)=(x+x^{-1})/2-1$), the same functional that satisfies the Recognition Composition Law. Closing uniqueness on the slim ledger keeps the premise ledger at the $\delta$-only floor and underwrites later selection and structural-ledger results without reintroducing per-prime calibration as an independent axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.