calibrated_recip
plain-language theorem explainer
Calibration of a PRC ratio character is closed under taking reciprocals: if χ acts as the identity on an orbit direction x, it also does so on x⁻¹. Anyone proving single-prime character rigidity cites this to push the calibration datum from p to p⁻¹. The argument is a short rational-display rewrite using reciprocal symmetry of χ and of RatioOrbit.
Claim. Let $\chi$ be a PRC ratio character on ratio orbits. If $\chi$ is calibrated at an orbit $x$ (i.e. $\chi(x)$ is cross-equivalent to $x$), then $\chi$ is calibrated at the reciprocal orbit $x^{-1}$.
background
In the Primitive Recognition Calculus continuum layer, ratio orbits are rational displays: an integer numerator over a nonzero orbit denominator, with a verifier map toRat into $\mathbb{Q}$. Cross-equivalence of two orbits is the discrete stand-in for equality of those rational displays (cross-multiplication agrees with toRat equality).
A PRC ratio character $\chi$ is a multiplicative, reciprocal map on ratio orbits. Calibration at $q$ means $\chi(q)$ is cross-equivalent to $q$ itself: $\chi$ acts as the identity character on that orbit direction. The cost hypotheses of PRC typically supply calibration only at a single point (classically the direction two); the forcing lemmas must then propagate that datum along the group generated by a prime direction.
Upstream, reciprocal symmetry of $\chi$ on the rational display states $(\chi(x^{-1})).\mathrm{toRat}=(\chi(x).\mathrm{toRat})^{-1}$, and the orbit reciprocal satisfies the same identity on toRat.
proof idea
Unfold calibration on both the hypothesis and the goal to cross-equivalence of $\chi(x)$ with $x$ and of $\chi(x^{-1})$ with $x^{-1}$. Replace both cross-equivalences by equality of rational displays via the crossEq/toRat bridge. Apply reciprocal symmetry of the character on the display, then the reciprocal identity for ratio orbits, and finish by rewriting with the calibration hypothesis on $x$.
why it matters
This is one of the three local closure facts (one, mul, recip) that turn a single calibration point into identity on a cyclic subgroup. The parent theorem prime_calibration_forces_identity_on_direction packages exactly that: calibration at a prime direction $p$ forces calibration at $p\cdot p$ and at $p^{-1}$, and forces the induced cost on $p$ to the canonical PRC J-cost on that orbit. That single-prime rigidity is the discrete step toward global character rigidity and uniqueness of the native PRC cost, which sits under the continuum forcing that recovers the unique J-cost of the Recognition Composition Law (T5 landmark $J(x)=(x+x^{-1})/2-1$). Without reciprocal closure, the inverse generator would remain uncalibrated and the cost match would fail on half the cyclic subgroup.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.