PRCCharacterTwoPrimeReciprocalExcludesPrimeIdentityWitness_of_not_mixed
plain-language theorem explainer
If a ratio-orbit character is not in the mixed two-prime configuration, then reciprocal orientation at the distinguished orbit-2 axis already rules out any identity-oriented native prime witness. Calibration and uniqueness arguments cite this as the clean half of the mixed/exclusion equivalence. The proof is pure logic: pack the two premises into the mixed conjunction and discharge the negation.
Claim. Let $\chi$ be a map on rational orbits. If $\chi$ is not mixed in the sense that the distinguished prime axis of $2$ is reciprocal-oriented while some native prime axis stays identity-oriented, then reciprocal orientation of $\chi$ at the orbit-$2$ axis already excludes the existence of any identity-oriented native prime witness.
background
In the primitive recognition calculus, characters act on RatioOrbit displays (signed numerator over a nonzero distinction denominator). Orientation of a character along a prime axis is recorded by whether $\chi$ sends that axis to itself or to its reciprocal, compared via cross-equality of orbits.
Two atomic branch props sit at the orbit-$2$ axis. The exclusion prop says: if $\chi$ is reciprocal at the distinguished two-prime direction, then no native prime direction may remain identity-oriented. The mixed prop is exactly the conjunction that would refute that exclusion: reciprocal at orbit $2$, and at least one identity-oriented native prime witness.
This lemma lives in the native-cost uniqueness development, where character branch constraints feed uniqueness of the native cost functional tied to the Recognition Composition Law and J-cost.
proof idea
One-line logical unpacking. Assume the negation of the mixed configuration. To establish the exclusion implication, introduce the reciprocal-at-two hypothesis and an identity-oriented native prime witness. Pair them into the mixed conjunction and apply the given negation. No orbit arithmetic is used.
why it matters
This is the easy direction of the iff between exclusion and non-mixedness, used immediately by PRCCharacterTwoPrimeReciprocalExcludesPrimeIdentityWitness_iff_not_mixed. Downstream, prime-calibration forcing theorems invoke it to conclude the exclusion target once a global no-mixed-character hypothesis is in hand (PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_of_no_mixed_character).
In the Recognition framework this sits inside native-cost uniqueness for characters on ratio orbits: mixed two-prime branches would obstruct a single native cost, so excluding them is part of forcing the J-unique cost path (T5) on the discrete prime axes before continuum calibration. It is scaffolding glue rather than a physical law, but it closes a named branch obstruction used by the calibration chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.