PRCCharacterMixedPrimeWitnesses_iff_pair_witnesses
plain-language theorem explainer
The split mixed-prime witness condition on a ratio-orbit character is equivalent to the single paired existential that names both prime axes at once. Anyone packaging the mixed-prime obstruction for native cost uniqueness or the universal foundation certificate can cite this. The proof is the two-direction packaging of the already-proved one-way implications.
Claim. For any map $\chi$ on rational orbits, the following are equivalent: (i) there exists a native prime axis on which $\chi$ acts as the identity orientation and (separately) a native prime axis on which $\chi$ acts as the reciprocal orientation; (ii) there exist native primes $p$ and $r$ such that $\chi$ is identity-oriented on the $p$-direction and reciprocal-oriented on the $r$-direction in one joint witness package.
background
In the Primitive Recognition Calculus, ratio orbits are the native display of rational data: a signed numerator orbit over a nonzero distinction-natural denominator. Characters here are maps $\chi$ on those orbits. Native prime directions supply distinguished axes along which one can test orientation.
The mixed-prime witness says the character is identity-oriented on at least one native prime axis and reciprocal-oriented on at least one (possibly different) native prime axis, via cross-equality of orbits. The split form is a conjunction of two independent existentials. The pair form packages both branches inside one existential, removing an outer propositional wrapper around the obstruction.
This module develops uniqueness of the native cost from character and doubled-trace hypotheses. The mixed-prime obstruction is the remaining combinatorial gate before cost uniqueness and the conditional universal foundation certificate can treat the character as fully constrained.
proof idea
Term-mode biconditional: the forward arrow is the already-proved packaging lemma that turns the split conjunction into a joint existential; the reverse arrow is the unpacking lemma that splits the joint witness back into the two separate existentials. No new arithmetic is introduced.
why it matters
This equivalence lets downstream certificates choose whichever packaging of the mixed-prime obstruction is convenient without changing meaning. It is used by the conditional universal foundation certificate in UniversalFoundation, which assembles kernel, real complete ordered field, and trace-logic pieces under PRC hypotheses.
In the Recognition Science forcing picture, native cost uniqueness feeds the J-cost story (T5: $J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law. Cleaning the last propositional wrapper around mixed-prime witnesses is bookkeeping, but it is the bookkeeping that makes the obstruction a single Prop usable in certificate structures rather than a conjunction that must be threaded by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.