PRCCharacterTwoPrimeReciprocalExcludesPrimeIdentityWitness_of_excludes
plain-language theorem explainer
If a ratio-orbit character that is reciprocal on the distinguished prime-2 axis forbids identity orientation on every native prime axis, then it also forbids even a single identity-oriented prime witness. Anyone tracking the two-prime branch obstruction in native cost uniqueness cites this bridge. The proof unpacks the existential witness and applies the universal exclusion.
Claim. Let $\chi$ be a map on rational orbits. Suppose that whenever $\chi$ sends the distinguished prime-$2$ direction to its reciprocal, no native prime direction is fixed by $\chi$ (identity-oriented). Then the same reciprocal hypothesis on the prime-$2$ axis cannot coexist with even one identity-oriented native prime witness: the mixed configuration is impossible.
background
In the Primitive Recognition Calculus, characters act on RatioOrbit displays (signed numerator over a nonzero distinction-natural denominator). Orientation of a character on a prime axis is read by cross-equality: identity orientation means $\chi$ fixes the prime direction; reciprocal orientation means $\chi$ sends it to its reciprocal orbit.
The distinguished prime-$2$ axis is special in the native-cost uniqueness argument. One normal form of the branch obstruction says: if that axis is reciprocal-oriented, then every native prime axis fails to be identity-oriented. The witness form weakens the conclusion to a single existential blocker: reciprocal orientation at $2$ cannot sit beside even one identity-oriented prime witness.
This module develops uniqueness of the native cost from character and doubled-trace hypotheses; the two-prime reciprocal branch is an atomic mixed-witness obstruction used later in prime-calibration forcing.
proof idea
Term-mode unpacking of the witness form. Assume the universal exclusion hypothesis. Introduce the reciprocal-at-$2$ premise and an existential identity witness. Destructure the witness to a prime $p$, a primality certificate, and an identity cross-equality. Apply the universal exclusion at that $p$ to obtain a contradiction with the identity orientation. No external lemmas beyond the two Prop definitions.
why it matters
Closes the easy direction from the contrapositive (forall) normal form of the orbit-$2$ branch obstruction to its atomic mixed-witness blocker. Downstream, the iff theorem equates the two forms, and the prime-calibration forcing target lifts the exclusion hypothesis into the witness-shaped calibration goal used in native cost uniqueness.
In the Recognition forcing picture this sits inside the foundation layer that pins the native cost before J-uniqueness (T5) and the self-similar fixed point $\phi$ (T6) are consumed by later physics. It does not itself force $\phi$ or the eight-tick structure; it only keeps the two-prime reciprocal branch free of identity-oriented prime witnesses so calibration can proceed cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.