PRCNativeCostAdmissibleCharacterRigidityTarget
plain-language theorem explainer
Defines the admissible-character rigidity target: every admissible ratio-orbit character must induce a cost that matches canonical J-cost on all orbits (via cross-equality). Uniqueness theorems cite it when factoring native cost through characters. It is a bare Prop interface, not a proved statement.
Claim. For every admissible character $\chi$ on ratio orbits and every ratio orbit $q$, the cost induced by $\chi$ at $q$ is cross-equivalent (balanced cross-multiplication of numerator/denominator orbits) to the canonical $J$-cost evaluated on $q$.
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display: a signed-orbit numerator over a nonzero distinction-nat denominator. Cross-equality is the internal PRC rational relation: two orbits match when scaled numerators balance under cross-multiplication (K4.10), i.e. the verifier-level equality of rationals without leaving orbit language.
Characters act as maps on ratio orbits. An admissible ratio character is one that respects the PRC structural constraints (ratio-character laws plus prime calibration and related side conditions used elsewhere in the module). From such a character one builds an induced cost via costFromCharacter; the canonical comparison cost is the J-cost pulled back to ratio orbits (onRatioOrbit).
J itself is the unique cost forced by the Recognition Composition Law (T5): $J(x)=(x+x^{-1})/2-1$. The present target weakens bare orientation rigidity: instead of forcing the character map to be pointwise identity or reciprocal, it only requires the induced cost to collapse to that canonical J-cost on every orbit.
proof idea
No proof: this is a definition of a proposition. The body is a universal statement over characters and orbits, packing admissibility of $\chi$ as the hypothesis and cross-equality of induced cost with canonical orbit J-cost as the conclusion. Downstream lemmas discharge the Prop from stronger orientation or propagation hypotheses; the definition itself only names the target.
why it matters
This is the repaired rigidity interface in the native-cost uniqueness stack. Parent results include the several discharge lemmas (..._of_admissible_global_orientation, ..._of_prime_calibration_propagation, ..._of_signed_unit_calibration, and the prime-coherence/global-propagation composites) and the assembly theorem that builds full native-cost uniqueness from admissible factorization plus this rigidity target. Strengthened uniqueness targets also take it as an input.
Framework role: it sits under T5 J-uniqueness. Once every admissible character yields the same cost as canonical J on ratio orbits, native cost cannot wander off the forced functional form. The doc-comment frames it as the admissible replacement for character rigidity: cost collapse, not orientation collapse, is what uniqueness needs. Open work is discharging the target from the remaining orientation/propagation hypotheses rather than assuming it raw.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.