PRCPrimeCalibratedMixedPrimePairWitnessCharacter_iff_same_or_distinct
plain-language theorem explainer
A calibrated mixed-prime pair obstruction on a ratio character is exactly the disjunction of the same-axis and distinct-axis cases. Anyone reducing native-cost uniqueness under prime calibration cites this split. The proof is a pure bidirectional packaging of the two one-way lemmas already proved in-module.
Claim. There exists a calibrated ratio character admitting mixed-prime pair witnesses if and only if there exists a calibrated ratio character admitting same-prime mixed pair witnesses, or one admitting distinct-prime mixed pair witnesses.
background
In the Primitive Recognition Calculus native-cost uniqueness development, a ratio character $\chi$ is a map on ratio orbits that encodes multiplicative recognition data. Prime-direction calibration pins the character so that native prime axes are oriented consistently (identity on one axis, reciprocal on the other).
A mixed-prime pair witness is the residual obstruction: the character still sees a mixed branch involving two native prime axes $p$ and $r$. That obstruction unpacks into two exclusive geometric cases: the mixed branch lives on a single native prime orbit (same-axis), or it straddles two different native prime orbits (distinct-axis).
The three propositions compared here are the fully unpacked calibrated mixed model and its same-axis and distinct-axis specializations. Upstream one-way lemmas already show that any mixed witness splits into same-or-distinct, and that either branch rebuilds a mixed witness.
proof idea
Term-mode Iff constructor. The forward arrow is the existing lemma that any calibrated mixed-prime pair witness character yields same-axis or distinct-axis; that lemma unpacks the existential character and case-splits the mixed-pair witness predicate. The reverse arrow is the existing lemma that either same-axis or distinct-axis rebuilds a calibrated mixed witness, by cases on the disjunction and re-packing the character data. No new algebra is performed here.
why it matters
This biconditional is the hinge that lets the no-mixed-witnesses and prime-pair product-cost consistency targets be rewritten as the joint negation of the same-axis and distinct-axis characters. Downstream, the negated targets become equivalent to the same-or-distinct disjunction via a one-line trans through this lemma.
Those rewritten targets feed the conditional universal-foundation certificate in UniversalFoundation, which packages kernel, real-complete ordered field, and trace-logic certificates. In the broader RS forcing picture this sits inside native-cost uniqueness for the recognition composition law and the J-cost fixed by T5: ruling out mixed-prime pair witnesses is part of forcing the cost to be the unique calibrated native cost on prime axes.
It does not itself discharge the obstruction; it only makes the case split official so later uniqueness arguments can attack same-axis and distinct-axis separately.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.