identity_character_rigid
plain-language theorem explainer
For every rational orbit q, the cost generated by the identity character equals the native PRC J-cost of q under cross-multiplication. Anyone calibrating characters against the native cost cites this rigidity fact. The proof is a one-line appeal to reflexivity of cross-equivalence after unfolding the identity character.
Claim. For every ratio orbit $q$, the cost generated from the identity character $\chi(q)=q$ is cross-equivalent to the native rational $J$-cost $J(q)=((q+q^{-1})/2)-1$ on that orbit.
background
In the Primitive Recognition Calculus, rationals are carried as ratio orbits: a signed-orbit numerator over a nonzero distinction-nat denominator. Two such orbits are identified by cross-equivalence when the scaled numerators balance under the internal signed-orbit relation (K4.10).
The native PRC cost on a ratio orbit is the orbit-level $J$-object $J(q)=((q+q^{-1})/2)-1$, written onRatioOrbit. A general character $\chi$ produces a cost by composing: cost-from-character sends $q$ to $J(\chi(q))$. The identity character is the map $q\mapsto q$, so its generated cost is literally the native $J$ on $q$.
This module develops uniqueness of that native cost among admissible characters. The present statement is the base rigidity check that the identity character reproduces native $J$ under cross-equivalence.
proof idea
Unfolding cost-from-character on the identity map yields exactly onRatioOrbit q. The goal therefore reduces to cross-equivalence of that orbit with itself. Apply reflexivity of cross-equivalence (crossEq_refl) to onRatioOrbit q. No arithmetic on numerators or denominators is required.
why it matters
Identity-character rigidity is the seed for the prime-direction and prime-pair product calibrations that follow immediately: both identity_character_prime_calibrated and identity_character_prime_pair_product_cost_consistent invoke this theorem on prime directions and their products. Those calibrations feed the native-cost uniqueness blocker certificate, which packages the zero-calibrated factorization target as proved and the signed-admissible factorization target as refuted.
In the broader Recognition chain this anchors the T5 J-uniqueness story at the PRC rational level: the cost that characters are measured against is forced to be the identity-character instance of $J(x)=(x+x^{-1})/2-1$, before analytic uniqueness is bridged. Without this trivial but named rigidity step, the character-calibration ladder has no base case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.