reciprocal_admissible_ratio_character
plain-language theorem explainer
The global reciprocal on rational orbits is an admissible ratio character: it obeys the ratio-character laws, prime calibration, and prime-pair product cost consistency. Cite this when showing that the repaired admissible-character interface admits both global orientations, not only the identity. The proof is a three-field structure package of prior reciprocal lemmas.
Claim. The map $q \mapsto q^{-1}$ on rational orbits (sending zero to zero) is an admissible ratio character: it satisfies the ratio-character laws, is prime-direction calibrated, and is consistent for prime-pair product cost. Admissibility here is the repaired interface that keeps the two global orientations and excludes valuation twists.
background
Ratio orbits are the PRC display of rationals: a signed-orbit numerator over a nonzero distinction-nat denominator. Their total reciprocal mirrors $\mathbb{Q}$, sending the zero orbit to itself and inverting nonzero orbits.
After a two-adic countermodel, the admissible-character interface was repaired. An admissible character $\chi$ on ratio orbits must satisfy three fields: the multiplicative ratio-character laws, prime-direction calibration, and prime-pair product cost consistency. The repair keeps the two global orientations and rules out valuation twists.
Upstream, the reciprocal map is already known to be a ratio character ("the first explicit witness that the multiplicative character laws alone do not choose the identity orientation"), and separate lemmas establish its prime calibration and prime-pair product cost consistency.
proof idea
Term-mode structure construction for PRCAdmissibleRatioCharacter applied to $q \mapsto q^{-1}$. The three fields are filled by named prior theorems: ratio-character laws from the reciprocal ratio-character lemma; prime calibration from the reciprocal prime-calibration lemma (via cross-equality symmetry of the reciprocal of a prime direction); prime-pair product cost from the matching consistency lemma (again via cross-equality symmetry). No new algebra is done here.
why it matters
Native cost uniqueness in the Primitive Recognition Calculus needs a tight admissible-character class. This declaration places the global reciprocal inside that class, so both identity and reciprocal orientations survive the repaired interface. That matches the framework picture in which J-cost uniqueness (forcing chain T5) and the Recognition Composition Law fix the cost shape while still allowing a discrete orientation choice at the character level.
The module is building uniqueness of native cost from character data (cost-from-character, doubled-trace d'Alembert hypotheses, character-trace matching). Packaging reciprocal as fully admissible closes the orientation side of that story. No downstream consumers are wired yet; the natural parents are uniqueness or classification theorems that quantify over admissible characters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.