PRCCharacterTwoPrimeReciprocalExcludesPrimeIdentityWitness_iff_not_mixed
plain-language theorem explainer
For any orbit character χ, the atomic orbit-2 mixed-witness blocker (reciprocal orientation on the distinguished prime axis forbids any identity-oriented native prime) is equivalent to the negation of the mixed branch configuration. Cost-uniqueness arguments cite this to switch freely between the implication form and the conjunction form. The proof is a pure Iff packaging of the two one-way lemmas.
Claim. For every map $\chi$ from rational orbits to rational orbits, the following are equivalent: (i) if $\chi$ sends the distinguished prime-2 axis to its reciprocal, then no native prime axis is fixed by $\chi$ (identity-oriented); (ii) it is not the case that $\chi$ both reciprocal-orients the prime-2 axis and identity-orients some native prime axis.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. Characters $\chi : \mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ assign orientations (identity vs reciprocal) along prime axes; crossEq is the equality test used to read those orientations.
The distinguished axis is the orbit-2 prime direction. The mixed configuration asserts both that $\chi$ reciprocal-orients that axis and that some native prime remains identity-oriented. The exclusion witness is the implication form of the same obstruction: reciprocal orientation at orbit 2 forces the nonexistence of any identity-oriented native prime witness. Both props live in the native-cost uniqueness development, which isolates branch blockers before uniqueness of the native cost functional is concluded.
The two one-way lemmas already prove each direction of the equivalence by unpacking or packing the conjunction.
proof idea
Term-mode Iff construction. Introduce $\chi$, then build the biconditional as the pair of existing one-way theorems: exclusion implies not-mixed (by feeding the mixed pair into the implication), and not-mixed implies exclusion (by contraposing: the two premises of the exclusion would rebuild the mixed pair). No further arithmetic or orbit algebra is used.
why it matters
Native-cost uniqueness needs a clean atomic blocker for the orbit-2 mixed branch: reciprocal orientation at the distinguished prime cannot sit beside even one identity-oriented native prime. Packaging the blocker as an iff lets later arguments choose the implication form or the negated-conjunction form without re-proving the logical equivalence.
No downstream consumers are recorded yet; the lemma sits as local glue inside PRCNativeCostUniqueness, adjacent to doubled-trace and d'Alembert character machinery that ultimately feed J-cost uniqueness (T5 in the forcing chain: $J(x)=(x+x^{-1})/2-1$). It does not itself touch RCL, phi, or the eight-tick octave; it only clears a propositional interface for the character-branch analysis those landmarks rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.