PRCPrimeCalibratedTwoPrimeReciprocalIdentityPrimeMixedCharacter_absurd_of_witness_excludes
plain-language theorem explainer
If every prime-direction-calibrated ratio character with reciprocal orbit-2 orientation excludes identity-oriented native prime witnesses, then no calibrated mixed character model exists. Character-rigidity and native-cost uniqueness arguments cite this to turn a universal exclusion hypothesis into nonexistence of a mixed model. The proof unpacks the existential mixed model and applies the pointwise non-mixed lemma.
Claim. Assume that for every ratio character $\chi$ that is prime-direction calibrated, reciprocal orientation of the orbit-$2$ prime axis excludes any identity-oriented native prime witness. Then there does not exist a ratio character that is prime-direction calibrated and mixed in the sense that orbit $2$ is reciprocal while some native prime witness is identity-oriented.
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio characters are maps $\chi$ on ratio orbits that encode orientation data for prime axes. Prime-direction calibration fixes how those axes sit relative to the native cost. A mixed character orients the orbit-$2$ axis reciprocally while some native prime witness remains identity-oriented.
The exclusion target is the universal statement: whenever $\chi$ is a ratio character and prime-direction calibrated, reciprocal orbit-$2$ forces absence of any identity-oriented native prime witness. The mixed-character model is the existential dual: some calibrated $\chi$ realizes exactly that mixed pattern. The module treats nonexistence of the mixed model as equivalent to the exclusion target along the character-rigidity route.
Upstream, the pointwise lemma already says that if exclusion holds for a fixed $\chi$, then that $\chi$ is not mixed. The present result lifts that fact from a single character to the calibrated existential model.
proof idea
Assume the universal exclusion target and, for contradiction, a calibrated mixed model. Destructure the existential to a single ratio character $\chi$ that is a character, prime-direction calibrated, and mixed. Instantiate the exclusion target at that $\chi$ to obtain the pointwise exclusion hypothesis. Feed it to the upstream lemma that exclusion implies not-mixed, and discharge the mixed conjunct.
why it matters
This is one direction of the equivalence between the orbit-$2$ mixed-witness exclusion target and nonexistence of the calibrated mixed-character model. Downstream it is the left-to-right arrow of that iff, and it feeds the sharpened non-two mixed variant as well.
It sits on the character-rigidity path toward native-cost uniqueness: constructing the mixed model would refute that route, so ruling the model out under the exclusion hypothesis is a blocker step. The native-cost uniqueness blocker certificate and the conditional universal-foundation certificate both depend on this cluster. In the broader Recognition forcing chain this supports uniqueness of the native cost (the $J$-cost of T5) by eliminating mixed orientation data on prime axes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.