PRCCharacterMixedPrimePairWitnesses_of_same
plain-language theorem explainer
If a ratio-orbit character carries a same-axis mixed-prime pair witness (identity and reciprocal branch conflicts on one native prime orbit), then it carries the weaker pair-packaged mixed-prime witness. Anyone tracking the mixed-prime obstruction in native cost uniqueness cites this implication. The proof is a one-step existential forgetful map: drop the equality of the two prime labels.
Claim. Let $\chi$ be a map on rational orbits. If there exist native prime orbits $p$ and $r$ with $p=r$ such that $\chi$ fixes the identity-oriented prime direction of $p$ and sends the prime direction of $r$ to its reciprocal (cross-equality of orbits), then the same data without the requirement $p=r$ form a mixed-prime pair witness for $\chi$.
background
In the Primitive Recognition Calculus, characters act on RatioOrbit objects: rational displays with a signed-orbit numerator and a nonzero distinction-nat denominator. Native prime orbits supply distinguished directions; each has an identity-oriented prime direction and a reciprocal orientation.
A mixed-prime pair witness packages two branch conflicts in one existential: $\chi$ agrees with the identity on one prime direction and with the reciprocal on another. The same-axis variant strengthens this by forcing both primes to be the same native orbit. That is the self-reciprocal branch-conflict case: one prime is asked to be both fixed and inverted under $\chi$.
The surrounding module develops uniqueness of the native cost from character data, including d'Alembert-type trace constraints and prime-calibrated specializations. The mixed-prime obstruction is the residual conflict that must be ruled out (or classified) before a character can be identified with the unique native cost.
proof idea
Term-style unpacking. Destructure the same-axis witness into primes $p,r$, primality proofs, the equality $p=r$, and the two crossEq branch conditions. Reassemble the mixed-pair witness from $p,r$ and the two branch conditions alone, discarding the equality hypothesis. No further lemmas are required.
why it matters
This is the same-axis arm of the case split that feeds PRCCharacterMixedPrimePairWitnesses_of_same_or_distinct, which collapses same-axis or distinct-axis witnesses into the single pair-packaged mixed-prime form. That packaging is what the no-mixed-prime obstruction talks about: the iff theorem equates absence of mixed-prime witnesses with simultaneous absence of both same-axis and distinct-axis pair witnesses.
Downstream, the prime-calibrated specialization PRCPrimeCalibratedMixedPrimePairWitnessCharacter_of_same applies the same forgetful step inside the calibrated character package. In the Recognition foundation stack this sits under native cost uniqueness for the PRC character, the layer that pins the cost functional before the forcing chain's J-uniqueness (T5) and the Recognition Composition Law are read off at the continuum level. It does not itself force $J$ or $\varphi$; it only tidies the discrete mixed-prime obstruction used on the way there.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.