PRCStrengthenedNativeCostUniquenessTarget_of_character_factorization_two_calibration_and_admissible_rigidity
plain-language theorem explainer
Under character factorization, two-point calibration forcing prime calibration, and admissible character rigidity, every strengthened native PRC cost equals the canonical J-cost on all ratio orbits. Uniqueness-reduction chains cite this when they swap rigidity for orientation or propagation hypotheses. Proof is a two-step term composition through the strengthened admissible-factorization intermediate.
Claim. Assume every admissible PRC-native RCL cost factors through a ratio character, two-point calibration at the orbit $2$ forces prime-direction calibration, and every admissible ratio character has cost equal to the canonical $J$-cost on all ratio orbits. Then every cost $F$ satisfying the strengthened native hypotheses obeys $F(q) = J(q)$ (cross-equality) for every ratio orbit $q$.
background
In the Primitive Recognition Calculus, native costs are maps $F$ on ratio orbits obeying the Recognition Composition Law (RCL) and related discrete d'Alembert structure. The canonical cost is the $J$-cost $J(x)=(x+x^{-1})/2-1$, realized on orbits by onRatioOrbit. A ratio character $\chi$ produces a cost via costFromCharacter; factorization asks that every admissible native $F$ equal some such character cost.
The two-calibration target says calibration of the character cost at the orbit $2$ forces calibration on every prime direction. Admissible character rigidity is the cost-level collapse: for every admissible $\chi$, costFromCharacter $\chi$ agrees with canonical $J$ on all orbits (rather than forcing orientation of $\chi$ itself).
The strengthened uniqueness target replaces a refuted older native uniqueness claim: under strengthened native hypotheses, $F$ must equal canonical $J$ everywhere. This theorem packages three interface Props into that uniqueness conclusion.
proof idea
Pure term composition, no tactics. First apply the intermediate theorem that turns character factorization plus two-calibration into the strengthened admissible character-factorization target (every strengthened-native $F$ factors through an admissible character). Feed that result, together with admissible character rigidity, into the already-proved lemma that strengthened admissible factorization plus rigidity imply strengthened native uniqueness. The three hypotheses therefore discharge uniqueness in two hops.
why it matters
This is a hub in the repaired native-cost uniqueness stack after the old uniqueness statement was refuted. Five downstream theorems reduce alternative hypothesis packages (global orientation, signed-unit calibration, prime propagation, coherent global propagation, prime coherence plus propagation) to uniqueness by invoking this lemma, often as a one-line wrapper. It sits on the discrete path toward T5 $J$-uniqueness: RCL costs on ratio orbits must collapse to $J$, once factorization, prime calibration from the two-point seed, and admissible rigidity are granted. It does not close those three interface targets; it only shows they jointly force uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.