PRCCharacterTwoPrimeReciprocalIdentityPrimeMixed_iff_non_two
plain-language theorem explainer
For any character on rational orbits, the mixed branch with the two-axis reciprocal and some prime axis identity-oriented is equivalent to the sharpened form that forces the identity witness off the two-axis. Anyone excluding two-adic mixed characters in native-cost uniqueness will cite this. The proof is a one-line iff package of the two directed implications already proved nearby.
Claim. For every map $\chi$ from rational orbits to rational orbits, the following are equivalent: (i) $\chi$ sends the distinguished prime-$2$ direction to its reciprocal and fixes some native prime direction; (ii) $\chi$ sends the prime-$2$ direction to its reciprocal and fixes some native prime direction other than the orbit of $2$.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. Characters $\chi$ act on these orbits and may twist prime axes either to themselves (identity orientation) or to their reciprocals.
The two propositions compared here describe mixed branch configurations that would refute orbit-$2$ witness exclusion. The coarser form asserts that the two-prime direction is reciprocal-oriented while some native prime axis stays identity-oriented. The sharpened form adds the explicit side condition that the identity witness is not the two-orbit itself.
Both directed implications already exist in this module: one drops the non-two constraint by case analysis on whether the witness equals two, and the other forgets the non-two hypothesis. This declaration packages them as a single biconditional.
proof idea
Term-mode one-liner. Introduce the character $\chi$, then build the iff pair from the two directed lemmas already in scope: the forward map PRCCharacterTwoPrimeReciprocalIdentityNonTwoPrimeMixed_of_mixed (mixed implies sharpened non-two mixed) and the reverse map PRCCharacterTwoPrimeReciprocalIdentityPrimeMixed_of_non_two_mixed (sharpened non-two mixed implies mixed). No further casework occurs here.
why it matters
Native-cost uniqueness for PRC characters must rule out mixed two-adic twists. Equating the coarse mixed predicate with its sharpened non-two form lets later arguments work with whichever formulation is convenient without re-proving orientation bookkeeping.
Downstream, prc_universal_foundation_conditional_certificate in UniversalFoundation consumes this layer as part of the conditional certificate stack (kernel, real complete ordered field, trace logic). In the broader Recognition forcing chain this sits under the foundation that eventually forces the unique J-cost $J(x)=(x+x^{-1})/2-1$ (T5) and the self-similar fixed point $\varphi$ (T6); clearing mixed two-axis characters is local hygiene on the way to that uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.