PRCCharacterMixedPrimePairWitnesses
plain-language theorem explainer
A ratio-orbit character has a mixed-prime pair witness when two native prime directions exist so that the character fixes one on the identity branch and sends the other to its reciprocal branch, up to cross-equality. Cost-uniqueness arguments cite this packaging to collapse separate identity and reciprocal prime witnesses into one existential. It is a pure Prop definition packaging the mixed-prime obstruction, not a proved claim.
Claim. For a map $\chi$ on ratio orbits, the mixed-prime pair witness property holds when there exist prime distinction-orbits $p$ and $r$ such that $\chi$ of the prime direction of $p$ is cross-equal to that same direction, and $\chi$ of the prime direction of $r$ is cross-equal to the reciprocal of that direction.
background
In the Primitive Recognition Calculus, ratio orbits are the native rational objects built from signed $\delta$-orbits. Cross-equality is the internal PRC relation: two ratio orbits match when cross-multiplication balances numerator and denominator orbits as signed orbits (K4.10). The reciprocal of a ratio orbit reverses orientation, matching the reciprocal automorphism used elsewhere in the cost algebra and ledger forcing.
A character $\chi$ on ratio orbits is the algebraic stand-in for how a candidate cost acts on directions. Prime orbits of distinction naturals supply the irreducible generators. An identity-oriented prime witness means $\chi$ fixes a prime direction up to cross-equality; a reciprocal-oriented witness means $\chi$ sends a prime direction to its reciprocal.
The ambient module develops uniqueness of the native cost from character hypotheses. Mixed-prime witnesses are the obstruction pattern that forces both branches at once on primes.
proof idea
Definitional Prop, not a theorem. The body is a single four-fold existential: primes $p$ and $r$ (each with a prime-orbit certificate), plus the conjunction of an identity-branch cross-equality on the prime direction of $p$ and a reciprocal-branch cross-equality on the prime direction of $r$. No tactics or upstream lemmas fire; the declaration is the packaged obstruction predicate itself.
why it matters
Downstream lemmas treat this as the canonical pair form of the mixed-prime obstruction. The same-or-distinct split factors it into same-prime versus distinct-prime cases; the of-same, of-distinct, and of-same-or-distinct constructors rebuild it; and the pair-witnesses bridge connects it to the older non-pair mixed-prime witness form. The doc-comment states it removes the last propositional wrapper around the current mixed-prime obstruction.
In the Recognition Science stack this sits inside native cost uniqueness, feeding the path toward T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$). The mixed-prime conflict is the combinatorial reason a non-J character cannot satisfy both identity and reciprocal prime branches without collapsing to the forced cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.