identity_admissible_ratio_character
plain-language theorem explainer
The identity map on rational orbits is an admissible ratio character: it obeys the ratio laws, is prime-calibrated, and is consistent on prime-pair products. Native-cost uniqueness arguments cite it as the canonical baseline character against which twisted maps are compared. The proof is a three-field structure assembly from the three identity lemmas already on the shelf.
Claim. The identity map $\chi(q)=q$ on rational orbits is an admissible ratio character: it is a ratio character, it is prime-direction calibrated, and it satisfies prime-pair product cost consistency.
background
A rational orbit is an integer numerator over a nonzero orbit denominator (K4.7). Ratio characters are maps on these orbits that fix the unit and preserve multiplication up to the orbit cross-equality. After a two-adic countermodel, the admissible-character interface was repaired: a character must satisfy the ratio laws, prime calibration, and prime-pair product cost consistency. That package keeps the two global orientations and excludes valuation twists.
The module develops native-cost uniqueness for the primitive recognition calculus. The identity map is the sanity-check anchor: if the interface is sound, the identity must sit inside it and match the canonical cost. Upstream, the identity is already known to be a ratio character, to be rigid on prime directions, and to be rigid on products of two prime directions.
proof idea
Term-mode structure construction. Fill the three fields of the admissible-character interface by the three prior identity lemmas: the identity ratio-character theorem for the ratio laws; the identity prime-calibration theorem (which reduces each prime direction to identity rigidity); and the identity prime-pair product-cost theorem (which reduces each product of two prime directions to the same rigidity). No new algebra is done here.
why it matters
This declaration closes the baseline case of the repaired admissible-character interface inside native-cost uniqueness. The doc-comment on the identity ratio character calls it the sanity-check that anchors the character interface to the canonical cost; packaging that with prime calibration and prime-pair consistency makes the identity a full admissible character rather than a partial one.
In the Recognition forcing chain, cost uniqueness feeds the J-cost story (T5) and the self-similar fixed point $\phi$ (T6). An admissible identity character is the reference against which non-identity characters would have to be ruled out or reduced. No downstream consumers are wired yet; the lemma is infrastructure waiting on the uniqueness argument that compares general admissible characters to this baseline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.