PRCCharacterTwoPrimeReciprocalExcludesPrimeIdentity_of_witness_excludes
plain-language theorem explainer
Converts the existential witness form of the orbit-2 reciprocal exclusion into the universal form: if the distinguished prime-2 axis is reciprocal under χ, then no native prime axis is identity-oriented. Downstream calibration and prime-identity forcing theorems cite this bridge. The proof packages a universal prime witness into an existential and applies the given blocker.
Claim. Let $\chi$ be a map on ratio orbits. If reciprocal orientation of $\chi$ at the distinguished prime-$2$ axis cannot coexist with even one identity-oriented native prime witness, then reciprocal orientation at that axis implies that for every native prime $p$, $\chi$ is not identity-oriented on the $p$-axis.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays (signed numerator over a nonzero distinction-nat denominator). A character $\chi$ assigns to each ratio orbit another orbit; orientation is read by crossEq against either the identity direction or the reciprocal direction of a given axis.
The distinguished axis is the prime-$2$ direction. Two equivalent formulations of the mixed-branch obstruction appear: the witness form says reciprocal orientation at $2$ plus existence of any identity-oriented native prime yields False; the normal form says reciprocal orientation at $2$ implies every native prime fails to be identity-oriented.
This lemma sits in the native-cost uniqueness development, where branch orientation of $\chi$ is constrained so that the cost reconstructed from the character matches the unique J-cost forced by the Recognition Composition Law.
proof idea
One-line packaging proof. Introduce the reciprocal hypothesis at the prime-$2$ axis together with an arbitrary native prime $p$, its primality certificate, and an identity-orientation hypothesis at that prime. Bundle $(p, hp, hpId)$ into an existential witness and apply the given witness-form blocker, obtaining False. That discharges the universal negation in the normal form.
why it matters
Closes the witness-to-universal direction of the orbit-2 mixed-branch obstruction. Immediate parent is the biconditional PRCCharacterTwoPrimeReciprocalExcludesPrimeIdentity_iff_witness. Also applied inside PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget_of_witness, which lifts a witness-level calibration target to the universal target, and feeds the larger chain toward PRCCharacterPrimeIdentityForcesTwoPrimeIdentity_of_prime_pair_product_cost_consistent.
In the Recognition framework this is bookkeeping on the character side of native-cost uniqueness: forbidding mixed identity/reciprocal orientations on prime axes is part of forcing the character (and hence the reconstructed cost) onto the unique J-cost branch (T5 J-uniqueness, RCL). It does not itself invoke phi or the eight-tick octave; those enter later once the cost is identified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.