PRCCharacterDistinctPrimeMixedPairWitnesses
plain-language theorem explainer
Defines the proposition that a ratio-orbit character χ admits a mixed prime-pair witness on two distinct native primes: one prime axis is identity-oriented under χ, another different prime axis is reciprocal-oriented. Native-cost uniqueness and prime no-mixing arguments cite it as the distinct-axis half of mixed-pair existence. The body is a pure existential Prop packing two primeOrbit witnesses, inequality, and two crossEq alignments.
Claim. For a map $\chi$ on ratio orbits, the distinct-axis mixed-prime pair witness holds when there exist two distinct prime distinction-nats $p\neq r$ such that $\chi$ sends the prime direction of $p$ to a ratio orbit cross-equivalent to that same prime direction (identity orientation), and sends the prime direction of $r$ to a ratio orbit cross-equivalent to the reciprocal of that direction (reciprocal orientation).
background
In the Primitive Recognition Calculus, ratio data live as RatioOrbit displays: a signed-orbit numerator over a nonzero distinction-nat denominator. Equality of displays is internalised by crossEq, the cross-multiplication balance of scaled numerators (K4.10), rather than by floating-point rationals. Reciprocation flips a ratio orbit; identity orientation means $\chi$ fixes a prime direction up to crossEq, while reciprocal orientation means $\chi$ sends it to its reciprocal up to crossEq.
A PRC ratio character $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ is the discrete stand-in for how cost or trace data act on ratio axes. Prime axes are the primeOrbit directions in the distinction lattice. Mixed-prime witnesses record the bad configuration in which one prime axis is treated as identity-oriented and another (or the same) as reciprocal-oriented, violating uniform branch choice on primes.
This definition isolates the distinct-axis case: the identity witness and the reciprocal witness sit on different native primes. The companion same-axis form and the disjunction of the two make up the full mixed-pair witness used later in the module.
proof idea
Pure definitional Prop: unpack as existence of primes $p,r$ with primeOrbit certificates, the inequality $p\neq r$, crossEq of $\chi$ on the $p$-prime direction with that direction itself, and crossEq of $\chi$ on the $r$-prime direction with the reciprocal of that direction. No lemmas are applied; downstream proofs rcases the package and either drop the inequality (to get a plain mixed pair) or use it in absurdity arguments under branch uniformity.
why it matters
Atomic witness for distinct-axis prime mixing inside PRC native-cost uniqueness. Downstream, it is the right disjunct of the iff that splits mixed prime-pair witnesses into same-axis versus distinct-axis forms, and it is injected into the plain mixed-pair Prop by forgetting $p\neq r$. Negation of this Prop (together with negation of the same-axis form) is equivalent to having no mixed prime witnesses at all.
Under prime identity-branch uniformity, the distinct mixed-pair witness is absurd: once every native prime is forced identity-oriented, a reciprocal-oriented prime on a different axis cannot appear. That exclusion is the atomic form of prime no-mixing on the character, a discrete step toward uniqueness of the native cost functional (the J-cost side of the forcing chain, T5). It does not itself name J or $\phi$; it constrains the character that native cost is built from.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.