PRCPrimeCalibratedMixedPrimePairWitnessCharacter_of_same
plain-language theorem explainer
A prime-calibrated ratio character that admits a same-axis mixed-prime pair witness also admits the fully unpacked mixed-prime pair witness (named identity-oriented and reciprocal-oriented native prime axes). Anyone eliminating mixed-pair obstructions under prime calibration cites this one-way implication. The proof unpacks the same-axis package and applies the character-level same-to-mixed witness lemma.
Claim. If there exists a ratio-orbit map $\chi$ that is a PRC ratio character, is prime-direction calibrated, and carries a same-prime mixed-pair witness (mixed branch on a single native prime orbit), then there exists such a $\chi$ that is a PRC ratio character, prime-direction calibrated, and carries a mixed-prime pair witness (named native primes $p$ identity-oriented and $r$ reciprocal-oriented).
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 pins how $\chi$ acts on native prime axes. Mixed-prime pair witnesses are the residual obstruction: a pair of native primes $p,r$ with $p$ identity-oriented and $r$ reciprocal-oriented under $\chi$, so the mixed branch is realized concretely.
The same-axis package strengthens that picture by forcing the mixed branch onto a single native prime orbit (the two axes coincide up to the same-prime witness data). The fully unpacked mixed-prime package drops that coincidence and keeps only the oriented pair $(p,r)$ plus character and calibration. Locally this module reduces native cost uniqueness to ruling out such calibrated mixed witnesses.
Upstream, the character-level lemma already shows that a same-prime mixed-pair witness on $\chi$ yields an ordinary mixed-prime pair witness on $\chi$ by discarding the equality packaging and retaining the oriented axes.
proof idea
Term-mode existence unpack. Destructure the hypothesis as $\langle \chi, h_\chi, h_{\mathrm{prime}}, h_{\mathrm{same}} \rangle$. Rebuild the target triple with the same $\chi$, character proof, and calibration, replacing the same-prime witness by PRCCharacterMixedPrimePairWitnesses_of_same h_same, which forgets the same-axis equality data and returns the mixed-pair witness package.
why it matters
This is the same-axis arm of the calibrated mixed-pair obstruction lattice. Downstream, PRCPrimeCalibratedMixedPrimePairWitnessCharacter_of_same_or_distinct cases on same versus distinct axis packages and routes both into the fully unpacked mixed witness; the present lemma discharges the same branch. The biconditional PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_iff_no_same_and_no_distinct_pair_witness_character then rewrites the no-mixed-witnesses target as the conjunction of no same-axis and no distinct-axis calibrated packages.
In the broader Recognition forcing story this sits inside native $J$-cost uniqueness for PRC characters (the T5 J-uniqueness lane: $J(x)=(x+x^{-1})/2-1$), clearing mixed-prime witness models so the cost is forced rather than merely constrained. It does not itself prove absence of witnesses; it only collapses packaging so absence proofs can target the split forms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.