PRCNativeCostUniquenessTarget_of_admissible_character_targets
plain-language theorem explainer
Any native cost on ratio orbits that factors through an admissible ratio character, and whose character-built cost is rigid to the canonical J-cost, must itself equal the canonical J-cost on every orbit. Cited by the upgrade path that discharges uniqueness from weaker factorization plus prime-propagation hypotheses. Proof is a three-line term: factor, apply rigidity, transit cross-equality.
Claim. Assume every native cost $F$ on ratio orbits factors as $F(q)\sim\mathrm{cost}_\chi(q)$ for some admissible ratio character $\chi$, and that for every admissible $\chi$ one has $\mathrm{cost}_\chi(q)\sim J(q)$ on all orbits (cross-equality). Then every native cost satisfies $F(q)\sim J(q)$ for all ratio orbits $q$.
background
In the Primitive Recognition Calculus, costs act on RatioOrbit displays: integer numerator over a nonzero orbit denominator. Equality of values is the choice-free relation crossEq (integer cross-multiplication), not bare rational equality.
A native cost $F$ is a map on ratio orbits obeying the PRC native-cost hypotheses (symmetry, normalization, and the discrete d'Alembert/RCL structure). The canonical target is the orbit-level J-cost onRatioOrbit, the discrete avatar of $J(x)=(x+x^{-1})/2-1$ from the T5 uniqueness step.
The two hypotheses package the repaired character interface: factorization says every native $F$ is cross-equal to costFromCharacter χ for an admissible ratio character $χ$; rigidity says that same character-built cost is already cross-equal to canonical J on every orbit.
proof idea
Term-mode, three steps. Fix a native cost $F$ and an orbit $q$. From the factorization target, obtain an admissible character $χ$ with $F(q)\sim\mathrm{cost}_χ(q)$. From the rigidity target, $\mathrm{cost}_χ(q)\sim J(q)$. Close by RatioOrbit.crossEq_trans, the choice-free transitivity of cross-equality (routed through the integer bridge).
why it matters
This is the clean composition step for native J-uniqueness on ratio orbits: admissible factorization plus admissible rigidity imply PRCNativeCostUniquenessTarget. Downstream, PRCNativeCostUniquenessTarget_of_character_factorization_upgrade_and_prime_propagation applies it after upgrading a raw character factorization and feeding prime-calibration propagation, so the full uniqueness target no longer needs the continuous real theorem as a premise.
In the forcing chain this is the discrete native half of T5 (J-uniqueness) inside PRC: once every admissible cost collapses to orbit-level J, the continuous positive-real uniqueness theorem becomes a corollary by transport rather than an input. It does not itself prove factorization or rigidity; those remain separate targets on the uniqueness ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.