PRCCharacterNoMixedPrimeWitnesses_iff_no_mixed_prime_orientation
plain-language theorem explainer
The existential and universal formulations of prime-axis no-mixing for a ratio-orbit character are equivalent. Anyone citing the trace-coherence condition that forbids identity on one native prime axis and reciprocal on another can use either packing. The proof is a one-line Iff.intro from the two already-proved one-direction lemmas.
Claim. For any map $\chi$ from ratio orbits to ratio orbits, the following are equivalent: (i) it is not the case that some native prime axis is identity-oriented under $\chi$ while some (possibly different) native prime axis is reciprocal-oriented; (ii) whenever $\chi$ fixes one prime direction and sends another to its reciprocal, a contradiction follows.
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. Characters act as maps $\chi$ on these orbits. Native prime axes are the prime directions primeDirection p hp; orientation is read by RatioOrbit.crossEq against the identity direction or its reciprocal.
PRCCharacterNoMixedPrimeOrientation is the universal packing: no character may choose identity on one prime axis and reciprocal on another. Its doc-comment calls this "the trace-coherence condition that rules out independent prime-axis inversions." PRCCharacterNoMixedPrimeWitnesses is the dual existential packing: the conjunction of an identity-oriented prime witness and a reciprocal-oriented prime witness is forbidden.
Both live in the native-cost uniqueness development, where doubled-trace and d'Alembert hypotheses force the cost character to be coherent across prime axes before uniqueness of the native $J$-cost is concluded.
proof idea
Term-mode Iff constructor. Left-to-right applies PRCCharacterNoMixedPrimeOrientation_of_no_mixed_prime_witnesses, which unpacks the universal quantifiers and feeds the two witnesses into the existential negation. Right-to-left applies PRCCharacterNoMixedPrimeWitnesses_of_no_mixed_prime_orientation, which cases on the existential pair and discharges via the universal no-mix hypothesis. No further algebra.
why it matters
Feeds the conditional universal-foundation certificate prc_universal_foundation_conditional_certificate, which assembles kernel, real-complete ordered field, and trace-logic packages. Equating the two no-mix packings lets downstream certificates cite whichever form is convenient when enforcing trace coherence on prime axes. In the Recognition forcing chain this sits under native-cost uniqueness for the $J$-cost (T5 landmark $J(x)=(x+x^{-1})/2-1$), ensuring characters cannot invert prime axes independently before the cost is identified. It is bookkeeping rather than a new physical constraint, but it closes the interface between witness-style and orientation-style statements used by the certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.