PRCNativeCostAdmissibleCharacterRigidityTarget_of_prime_calibration_propagation
plain-language theorem explainer
Prime calibration propagation implies admissible character rigidity for native cost: every admissible ratio character has character-cost equal to canonical J-cost on all ratio orbits. Cited by anyone assembling native-cost uniqueness from factorization and calibration hypotheses. Proof is a one-line specialization unpacking admissibility into ratio-character plus prime-calibration data.
Claim. Assume that whenever a ratio character $\chi$ is calibrated on every prime direction, its character-cost equals the canonical cost on every rational ratio orbit. Then for every admissible ratio character $\chi$ and every ratio orbit $q$, the character-cost of $\chi$ at $q$ equals the canonical cost at $q$ (cross-equality of values).
background
In the Primitive Recognition Calculus native-cost uniqueness module, costs on ratio orbits are compared via crossEq, which identifies values up to the orbit's internal equivalence. The canonical cost on an orbit $q$ is written onRatioOrbit q; a character $\chi$ induces a competing cost costFromCharacter $\chi$ $q$.
Target B (PRCPrimeCalibrationPropagationTarget) is the unique-factorization side of rigidity: once every prime direction is calibrated, character-cost propagates to every rational direction. The admissible rigidity target replaces orientation rigidity by a cost-level demand: for admissible ratio characters, character-cost must collapse to canonical J-cost on all orbits. Admissibility packages a ratio-character structure together with prime-direction calibration, so the two targets sit in a direct specialization relation.
Local setting is the foundation layer that forces the native cost toward the unique J-cost $J(x)=(x+x^{-1})/2-1$ (T5), rather than fixing character orientation pointwise.
proof idea
One-line term proof. Introduce an admissible character $\chi$, its admissibility witness, and an arbitrary ratio orbit $q$. Unpack admissibility into the two fields the propagation target expects (ratio_character and prime_calibrated), then apply the given PRCPrimeCalibrationPropagationTarget hypothesis at $(\chi,q)$. No extra algebraic work.
why it matters
Closes the admissible-rigidity leg of the native-cost uniqueness assembly. Downstream, PRCNativeCostUniquenessTarget_of_character_factorization_upgrade_and_prime_propagation composes character factorization, an admissibility upgrade, and prime propagation into full uniqueness; the strengthened variant does the same with two-point calibration forcing prime calibration. Both routes invoke this reduction so that uniqueness only needs the sharper prime-propagation hypothesis rather than a separate admissible-rigidity proof.
In the Recognition forcing chain this is infrastructure for T5 J-uniqueness inside PRC: the cost, not the character orientation, is what must match $J$. It does not itself discharge prime propagation or factorization; those remain separate targets feeding the same uniqueness theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.