PRCPrimeCalibratedMixedPrimePairWitnessCharacter_of_same_or_distinct
plain-language theorem explainer
If a calibrated ratio character admits either a same-axis or a distinct-axis mixed-prime pair witness, then it admits the fully unpacked mixed-prime pair witness (named native primes p identity-oriented and r reciprocal-oriented). Native-cost uniqueness and the universal-foundation certificate cite this as the join of the two branch models. The proof is pure case analysis on the disjunction, routing each arm to its dedicated one-direction lemma.
Claim. Assume either (i) there exists a prime-direction-calibrated ratio character with a same-axis mixed-prime pair witness (mixed branch on a single native prime orbit), or (ii) there exists such a character with a distinct-axis mixed-prime pair witness (mixed branch between two different native prime orbits). Then there exists a prime-direction-calibrated ratio character together with the fully unpacked mixed-prime pair witnesses (named native primes $p$ identity-oriented and $r$ reciprocal-oriented).
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes how recognition cost transforms under multiplicative comparison. Prime-direction calibration fixes the orientation of native prime axes so that one axis is identity-oriented and another is reciprocal-oriented. The mixed-prime pair witness packages the obstruction that the mixed branch of the cost identity is realized on those axes.
Three propositional models sit in a hierarchy. The fully unpacked model asserts existence of a calibrated $\chi$ plus the mixed-pair witnesses with no further packaging. The same-axis model specializes to a single native prime orbit; the distinct-axis model specializes to two different native prime orbits. The module develops native-cost uniqueness by reducing cost identities to character-trace matching on these calibrated witnesses.
Upstream, the one-direction lemmas already convert each specialized model into the unpacked model by unpacking the existential and applying the corresponding witness-coercion on the character side.
proof idea
Case-split on the input disjunction. On the left (same-axis) arm, apply the dedicated coercion that turns a same-prime calibrated mixed-pair witness character into the unpacked mixed-pair witness character. On the right (distinct-axis) arm, apply the twin coercion for the distinct-prime model. Each arm is a single exact application; no further algebraic work is needed.
why it matters
This is the join half of the equivalence between the unpacked mixed-prime pair model and the disjunction of the same-axis and distinct-axis specializations. The immediate parent is the biconditional that packages both directions, which is the clean interface used when discharging the mixed-pair obstruction in native-cost uniqueness.
Downstream it is also pulled into the conditional universal-foundation certificate in UniversalFoundation, which assembles kernel, real-complete ordered field, and trace-logic certificates into a single PRC foundation package. In the broader Recognition Science chain, native-cost uniqueness feeds the J-cost uniqueness step (T5: $J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law; clearing the mixed-prime pair obstruction is part of showing that the cost functional is forced rather than chosen. The declaration itself is fully proved scaffolding glue, not an open hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.