PRCPrimeCalibratedMixedPrimePairWitnessCharacter_of_distinct
plain-language theorem explainer
A calibrated ratio character that admits a mixed-prime pair witness on two distinct native prime orbits also admits the unpacked mixed-prime pair witness (identity-oriented p, reciprocal-oriented r). Anyone closing the no-mixed-prime obstruction under prime calibration cites this. The proof unpacks the existential and applies the character-level distinct-to-mixed implication.
Claim. If there exists a ratio character $\chi$ that is prime-direction calibrated and carries a mixed-prime pair witness on two distinct native prime orbits, then there exists a ratio character that is prime-direction calibrated and carries a mixed-prime pair witness (identity-oriented prime axis $p$, reciprocal-oriented prime axis $r$).
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio characters $\chi : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$ encode multiplicative structure on orbits. Prime-direction calibration fixes how $\chi$ acts along native prime axes. A mixed-prime pair witness names two native primes $p$ and $r$ with $p$ identity-oriented and $r$ reciprocal-oriented under $\chi$.
The distinct-axis model packages the same data plus $p \neq r$: the mixed branch sits between two different native prime orbits. The target mixed model drops that inequality and is the fully unpacked obstruction used downstream ("no remaining propositional packaging around the two branch witnesses").
Upstream, the character-level lemma already shows that distinct-prime mixed pair witnesses imply ordinary mixed pair witnesses by discarding the inequality. This theorem lifts that implication through the calibrated existential packaging.
proof idea
Term-mode unpack-and-repack. Destruct the hypothesis to obtain $\chi$, the ratio-character and prime-calibration facts, and the distinct-prime mixed witnesses. Rebuild the target existential with the same $\chi$ and calibration data, replacing the distinct witnesses by PRCCharacterMixedPrimePairWitnesses_of_distinct applied to them (which forgets $p \neq r$ and keeps the oriented pair).
why it matters
Feeds the case split PRCPrimeCalibratedMixedPrimePairWitnessCharacter_of_same_or_distinct, which unifies same-axis and distinct-axis mixed models into one obstruction. That obstruction appears in the biconditional equating the prime-calibration "no mixed prime witnesses" target with the conjunction of no same-axis and no distinct-axis calibrated mixed witnesses.
Via that chain it supports prc_universal_foundation_conditional_certificate in UniversalFoundation, part of the conditional certificate stack for the PRC foundation. In the Recognition framework this is bookkeeping on the native-cost uniqueness path: ruling out mixed prime-axis witnesses under calibration is a step toward uniqueness of the native cost (tied to J-cost uniqueness in the forcing chain). It does not itself force J or $\phi$; it only collapses packaging so the no-mixed target can be attacked by cases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.