identity_character_prime_calibrated
plain-language theorem explainer
The identity map on rational orbits is calibrated on every native prime direction: the cost it generates matches canonical J-cost on each prime orbit. Anyone packaging admissible ratio characters cites this fact. The argument is a one-line specialization of global identity rigidity to prime directions.
Claim. The identity character $\chi(q)=q$ on rational orbits is prime-direction calibrated: for every native prime orbit $p$, the cost generated from $\chi$ at the prime direction of $p$ agrees (via cross-equality of ratio orbits) with the canonical $J$-cost evaluated on that same prime direction.
background
In the primitive recognition calculus, a rational orbit is an integer numerator over a nonzero distinction-nat denominator. Ratio characters act on these orbits; each character $\chi$ induces a cost via costFromCharacter. Calibration means that induced cost matches the canonical $J$-cost (the unique cost forced by the Recognition Composition Law and T5) on designated test directions.
A native prime direction is the ratio orbit associated to a prime distinction-nat orbit. Prime-direction calibration requires agreement of induced cost with canonical $J$-cost on every such prime direction. Upstream, identity rigidity already asserts that the identity character matches canonical $J$-cost on every rational orbit, not merely primes.
proof idea
One-line specialization. Introduce an arbitrary native prime $p$ with primality witness $hp$, form its prime direction, and apply the global identity-rigidity theorem at that orbit. No separate prime arithmetic is needed: rigidity already covers the whole orbit space.
why it matters
This lemma is the prime-calibration field in the package that declares the identity map an admissible ratio character. Downstream, that package feeds native-cost uniqueness arguments: only characters whose generated cost agrees with $J$ on primes (and satisfies product consistency) can serve as native costs. In the forcing chain this sits under T5 $J$-uniqueness and the Recognition Composition Law, confirming that the identity display of orbits already realizes the forced cost on the prime axes that generate the multiplicative structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.