PRCCharacterMixedPrimeWitnesses
plain-language theorem explainer
A ratio-orbit character has mixed-prime witnesses when one native prime axis is identity-oriented and one (possibly different) prime axis is reciprocal-oriented under cross-equivalence. Downstream uniqueness and calibration lemmas cite this as the positive obstruction form. The body is pure definitional packaging: a conjunction of two existentials over prime orbits.
Claim. For a map $\chi$ on ratio orbits, there exist native primes $p$ and $r$ (possibly equal) such that $\chi$ sends the prime direction of $p$ to an orbit cross-equivalent to that same prime direction, and sends the prime direction of $r$ to an orbit cross-equivalent to its reciprocal.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays built from a signed-orbit numerator and a nonzero distinction-nat denominator. Cross-equivalence equates two ratio orbits when the scaled numerators balance under cross-multiplication on $\delta$-orbit positions (the internal PRC stand-in for rational equality). The reciprocal of a ratio orbit is the total inversion map, sending zero to zero as in $\mathbb{Q}$.
A native prime orbit is a nonzero, non-unit distinction-nat with no nontrivial factorization. Each such prime supplies a prime direction in the ratio-orbit space. The local module develops native-cost uniqueness for ratio characters: maps $\chi$ on ratio orbits that are meant to encode cost-like structure along these axes.
The mixed-prime witness form records a split orientation on the prime axes: identity on one prime direction and reciprocal on another. It is the positive side of the no-mixed-prime obstruction used later in calibration and uniqueness arguments.
proof idea
Definitional, not a proved theorem. The predicate is the conjunction of two existentials: some prime orbit $p$ with $\chi$ of its prime direction cross-equivalent to that direction itself, and some prime orbit $r$ with $\chi$ of its prime direction cross-equivalent to the reciprocal of that direction. No tactics or lemmas are applied; packaging only.
why it matters
This is the positive mixed-prime obstruction in the native-cost uniqueness stack. Pair-packaged and iff forms convert it to a single existential package and to its negation (no mixed-prime witnesses). The calibrated model packages a ratio character that is prime-direction calibrated and still carries mixed-prime witnesses; nonexistence of that model is definitionally the current no-mixed-prime blocker.
Universal foundation open-target ledgers reference this family of interfaces among the routes that either force or refute zero-calibrated native-cost uniqueness. In the broader Recognition chain, native cost uniqueness feeds the J-cost uniqueness step (T5: $J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law; mixed orientation on prime axes is exactly the combinatorial defect those uniqueness arguments must rule out.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.