character_recip_toRat
plain-language theorem explainer
A PRC ratio character preserves reciprocal symmetry on the rational display: the character of a reciprocal orbit evaluates to the reciprocal of the character value. Anyone proving that calibration sets are closed under inversion cites this. The proof converts the character's built-in reciprocal axiom from cross-equality to rational equality via the K4.10 bridge and the orbit reciprocal display lemma.
Claim. If $\chi$ is a PRC ratio character on ratio orbits, then for every ratio orbit $x$, $(\chi(\mathrm{recip}\, x))^{\mathbb{Q}} = \bigl((\chi x)^{\mathbb{Q}}\bigr)^{-1}$, where $(\,\cdot\,)^{\mathbb{Q}}$ denotes the rational verifier display of a ratio orbit.
background
Ratio orbits (K4.7) package a signed-orbit numerator over a nonzero distinction-nat denominator, serving as the discrete rational display of recognition ratios. Their total reciprocal sends zero to zero as in $\mathbb{Q}$, and the display lemma recip_toRat records that this operation matches ordinary inversion on the rational verifier.
A PRC ratio character is a map on ratio orbits satisfying the multiplicative and reciprocal axioms of the primitive recognition calculus. The reciprocal axiom asserts that $\chi(\mathrm{recip}, x)$ is cross-equal to $\mathrm{recip}(\chi x)$. Cross-equality is the integer-level comparison that, by K4.10 (crossEq_iff_toRat_eq), is equivalent to equality of rational displays: "Cross-multiplication agrees with rational equality of the verifier displays."
This module forces character rigidity in the continuum limit. Reciprocal symmetry is one of the subgroup axioms needed so that the calibration set of a character is closed under inversion.
proof idea
Short tactic proof. Apply the character's reciprocal field to $x$, obtaining a cross-equality $\chi(\mathrm{recip}, x)\sim\mathrm{recip}(\chi x)$. Rewrite that cross-equality as rational equality via crossEq_iff_toRat_eq. Then replace the right-hand side by $((\chi x)^{\mathbb{Q}})^{-1}$ using recip_toRat. Three rewrites; no induction or case split.
why it matters
Feeds directly into calibrated_recip, which shows the calibration set of a PRC ratio character is closed under reciprocals ("Calibration is closed under reciprocals"). Together with the companion unit and multiplication lemmas in this module, that makes the calibration locus a subgroup of the ratio-orbit group, the algebraic backbone of character rigidity forcing.
In the Recognition Science chain this sits under continuum forcing of the cost functional. Once characters are rigid on ratio orbits, the J-cost (T5 uniqueness, $J(x)=(x+x^{-1})/2-1$) is the unique continuous extension compatible with reciprocal symmetry from the Recognition Composition Law. The identity proved here is the discrete shadow of $J(x)=J(x^{-1})$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.