PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_mixed_character
plain-language theorem explainer
The orbit-2 mixed-witness exclusion target is equivalent to nonexistence of a prime-calibrated mixed character that is reciprocal on orbit 2 and identity-oriented on some other native prime. Character-rigidity and native-cost uniqueness arguments cite this bridge. Proof is a term-mode pairing of the two already-proved directions.
Claim. The statement "every prime-direction-calibrated ratio character that is reciprocal on the orbit-$2$ prime axis excludes any identity-oriented native prime witness" holds if and only if there is no calibrated mixed character that is reciprocal on orbit $2$ while identity-oriented on some non-$2$ native prime.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ assigns to each ratio orbit another orbit and is required to obey the PRC character axioms. Prime-direction calibration fixes how $\chi$ acts on the prime axes of the ratio lattice. Orientation on a prime axis is either reciprocal or identity; mixed character means different primes take different orientations.
The exclusion target asserts: whenever $\chi$ is a ratio character, prime-direction calibrated, and reciprocal on the orbit-$2$ axis, it cannot admit any identity-oriented native prime witness. The mixed-character model is the existential dual: some calibrated $\chi$ that is reciprocal on orbit $2$ and identity-oriented on a non-$2$ native prime. The module treats these as the two faces of one rigidity obstruction on the way to native cost uniqueness (the J-cost route in the forcing chain).
proof idea
Term-mode Iff constructor. Left-to-right applies ..._absurd_of_witness_excludes: from the universal exclusion target, unpack any putative mixed model $\langle\chi,\ldots\rangle$ and derive a contradiction with the exclusion property on that $\chi$. Right-to-left applies ..._of_no_mixed_character: from nonexistence of mixed models, for arbitrary calibrated $\chi$ invoke the pointwise lemma that not-mixed yields the two-prime reciprocal exclusion property. No new algebra; pure packaging of the two directions.
why it matters
Closes the logical gap between the universal exclusion target and the concrete mixed-character nonexistence claim used as a rigidity blocker. Downstream, PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_iff_no_two_prime_mixed_character composes this iff with a prior bridge, collapsing a longer chain of prime-identity forcing targets to the same mixed-character nonexistence. The native-cost uniqueness blocker certificate and the universal-foundation conditional certificate both sit on this character-rigidity spine. In the RS forcing chain this is scaffolding toward T5 J-uniqueness: mixed orientations on prime axes would admit non-J native costs, so excluding them is part of forcing $J(x)=\cosh(\log x)-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.