PRCCharacterReciprocalTwist
plain-language theorem explainer
The reciprocal twist of a ratio-orbit map χ is the map q ↦ recip(χ(q)). It lifts the dual-recognition involution to characters on rational orbits. Native-cost uniqueness arguments cite it to close admissibility under twist and to swap prime-identity forcing with prime-reciprocal forcing. The body is a one-line composition with the total reciprocal on ratio orbits.
Claim. Given a map $\chi$ from ratio orbits to ratio orbits, its reciprocal twist is the map sending each orbit $q$ to the total reciprocal of $\chi(q)$ (zero fixed, as on $\mathbb{Q}$).
background
Ratio orbits (K4.7) package a signed-orbit numerator over a nonzero distinction-nat denominator: the discrete stand-in for rationals in the primitive recognition calculus. Their total reciprocal (K4.12) mirrors $x\mapsto x^{-1}$ on $\mathbb{Q}$, sending the zero orbit to itself.
This module studies ratio characters: unit-preserving, multiplicative, reciprocal-compatible maps on ratio orbits whose generated cost matches canonical J-cost on primes and prime pairs. Admissibility packages those laws after the two-adic countermodel, keeping the two global orientations while excluding valuation twists.
Upstream, the real reciprocal $\iota(x)=x^{-1}$ is the dual-recognition symmetry the framework is built on; the present definition is its character-level counterpart on ratio orbits.
proof idea
One-line definition: apply $\chi$, then RatioOrbit.recip.
The companion lemmas (same block) show the twist preserves structure. Ratio-character laws transport by ratioOrbit_recip_congr, the reciprocal-of-product crossEq, and inv_ne_zero. Prime calibration and prime-pair product cost consistency each flip one crossEq via reciprocal_symmetric then reapply the original witness. Full admissibility is the structure of those three preservations.
why it matters
Closes the repaired admissible-character interface under dual-recognition: if $\chi$ is admissible, so is its reciprocal twist. Downstream, that closure swaps prime-identity forcing with prime-reciprocal forcing (and conversely), yielding the identity-vs-two iff reciprocal-vs-two equivalence for admissible characters.
Those equivalences feed the uniqueness path for native cost up to the two global orientations, excluding valuation twists. The construction is the discrete shadow of the reciprocal involution behind J-uniqueness (T5) and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.