PRCCharacterPrimeReciprocalForcesTwoPrimeReciprocal
plain-language theorem explainer
A character χ on ratio orbits has the converse distinguished-axis reciprocal property when reciprocal orientation on any prime axis forces reciprocal orientation on the orbit-2 prime axis. Cost-uniqueness and reciprocal-globalization arguments cite this Prop as one half of the split witness-globalization normal form. It is a pure definition of a universal implication over prime orbits; no proof obligations live here.
Claim. For a map $\chi$ on ratio orbits, the following holds: whenever $p$ is a prime distinction-orbit and $\chi$ sends the corresponding prime direction to its reciprocal (equality of ratio orbits under cross-multiplication), then $\chi$ also sends the orbit-$2$ prime direction to its reciprocal.
background
In the Primitive Recognition Calculus, ratio data live on RatioOrbit: a signed-orbit numerator over a nonzero distinction-orbit denominator. Two such displays are identified by cross-multiplication balance (crossEq), the internal PRC stand-in for rational equality. The total reciprocal on ratio orbits sends a nonzero display to its inverse and zero to zero, matching the usual $\mathbb{Q}$ reciprocal.
Distinction orbits (DistinctionNat) are the base-neutral finite iterates of repeated distinction; prime orbits among them label calibrated prime axes. Each such prime supplies a distinguished direction in ratio-orbit space; the orbit-$2$ prime is the distinguished binary axis used throughout the native-cost uniqueness development.
The surrounding module builds native cost uniqueness from character hypotheses on ratio orbits. Reciprocal orientation of a character at an axis means the character lands on the reciprocal of that axis under cross-equality. Upstream ledger and cost-algebra reciprocal maps supply the same inversion idea at the event and $J$-automorphism layers; here it is internalized purely on $\delta$-orbit positions.
proof idea
Definitional abbreviation only: the body is the quantified implication over prime distinction-orbits $p$, with hypothesis that $\chi$ matches the reciprocal on the prime direction of $p$, and conclusion that $\chi$ matches the reciprocal on the fixed orbit-$2$ prime direction. No tactics, no lemmas applied, no sorry.
why it matters
This is the converse distinguished-axis half of reciprocal-witness globalization. Paired with the two-to-all reciprocal rule it reconstitutes full reciprocal-witness globalization (the split form packages both conjuncts). Downstream, the globalization hypothesis implies this property by specializing the witness to the orbit-$2$ prime; reciprocal-twist bridges relate it to the identity-forces-two companion on the twisted character.
It appears as the conclusion target of the prime-calibration forcing target: any ratio character that is prime-direction calibrated should satisfy this implication. The native-cost uniqueness blocker certificate and the universal-foundation open-targets list keep this among the exact Lean obligations still separating the uniqueness theorem from closure. In the broader RS forcing picture it constrains how reciprocal branch choice propagates along prime axes before $J$-cost uniqueness (T5) and the self-similar fixed point $\varphi$ (T6) can be read off a native character.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.