PRCNativeCostUniquenessTarget_of_prime_character_targets
plain-language theorem explainer
Under factorization through a ratio character, two-point calibration forcing prime calibration, and prime-to-rational propagation, every admissible PRC-native RCL cost equals the canonical orbit cost. The uniqueness blocker certificate cites this composition. The proof factors the cost, transfers the two-calibration, and applies character rigidity with cross-equality transitivity.
Claim. Assume (i) every admissible PRC-native cost $F$ factors as $F(q)\simeq C_\chi(q)$ for some ratio character $\chi$, (ii) two-point calibration of $C_\chi$ at the orbit $2$ forces prime-direction calibration of $\chi$, and (iii) prime calibration of $\chi$ propagates so $C_\chi(q)\simeq C(q)$ on every rational orbit $q$. Then every such $F$ satisfies $F(q)\simeq C(q)$ for the canonical native cost $C$, for all ratio orbits $q$.
background
Primitive Recognition Calculus (PRC) studies costs on ratio orbits: discrete multiplicative directions generated by positive rationals, with a canonical native cost onRatioOrbit built from the Recognition Composition Law cost $J$. Equality of costs is up to RatioOrbit.crossEq, the orbit-level identification used throughout the module.
A ratio character $\chi$ is a multiplicative map on orbits; costFromCharacter turns it into an RCL-style cost. The first hypothesis is the discrete d'Alembert factorization step: every $F$ meeting the native-cost hypotheses factors through some character. The second and third are the rigidity half: calibration of the character cost at the orbit $2$ should force calibration on every prime axis, and unique factorization should then push that calibration to every rational direction.
Locally this sits in the native-cost uniqueness development: the goal is to pin every admissible PRC-native cost to the single canonical $J$-derived cost, matching the broader T5 uniqueness of $J(x)=(x+x^{-1})/2-1$.
proof idea
Tactic proof, short composition. Fix an admissible native cost $F$ and an orbit $q$. Apply the factorization target to obtain a ratio character $\chi$ with $F\simeq C_\chi$ pointwise. Transfer $F$'s two-calibration across that identification (symmetry then transitivity of crossEq) to get $C_\chi$ calibrated at the orbit $2$. Invoke the companion rigidity lemma PRCNativeCostCharacterRigidityTarget_of_prime_targets on the two prime-calibration targets; it yields $C_\chi(q)\simeq C(q)$. Transitivity with $F(q)\simeq C_\chi(q)$ finishes $F(q)\simeq C(q)$.
why it matters
This is the exact glue step from three surface targets (factorization, two-forces-primes, prime-propagation) to the full native-cost uniqueness target. Downstream it is consumed by prc_native_cost_uniqueness_blocker_certificate, which packages proved and refuted blocker fragments for the uniqueness program.
In the Recognition forcing chain this is the discrete, orbit-level face of T5 $J$-uniqueness and the RCL: once costs factor through characters and characters are rigid under two-point calibration, no second native cost can survive. It does not yet close the open prime-axis control gap named in the two-calibration target doc; it only records that uniqueness follows once those three targets hold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.