PRCCharacterSamePrimeMixedPairWitnesses_absurd
plain-language theorem explainer
No ratio-orbit character can carry both an identity-oriented and a reciprocal-oriented prime witness on the same native prime orbit. Anyone ruling out self-reciprocal branch conflicts in PRC native-cost uniqueness cites this. The proof collapses the two witnesses by substitution, transports reciprocity across cross-equality, and contradicts that a prime direction is never cross-equal to its reciprocal.
Claim. For every map $\chi$ from ratio orbits to ratio orbits, it is impossible that there exist a single native prime orbit $p$ such that $\chi$ is cross-equal to the identity on the prime direction of $p$ and simultaneously cross-equal to the reciprocal on that same prime direction.
background
Primitive Recognition Calculus works with ratio orbits: integer-numerator displays over nonzero distinction-nat denominators. Two ratio orbits are related by crossEq when cross-multiplication balances as signed orbits (the internal PRC stand-in for rational equality). Reciprocal is the total involution on ratio orbits that swaps numerator and denominator (sending zero to zero).
A character here is simply a self-map $\chi$ of ratio orbits. The same-prime mixed-pair witness asserts that identity-oriented and reciprocal-oriented prime witnesses live on one common native prime orbit: $\chi$ fixes the prime direction of $p$ up to cross-equality, and also sends that same direction to its reciprocal. The module treats this as the self-reciprocal branch-conflict case for native-cost uniqueness.
Upstream, cross-equality is symmetric and transitive (choice-free via the integer bridge), and a dedicated lemma states that a prime direction is never cross-equal to its own reciprocal.
proof idea
Assume a same-prime mixed-pair witness and unpack the existential: primes $p$ and $r$, primality proofs, $p=r$, identity orientation on $p$, and reciprocal orientation on $r$. Substitute $r:=p$. The two prime-direction displays agree definitionally, so the reciprocal-orientation hypothesis rewrites as $\chi(\mathrm{primeDir},p)\sim\mathrm{recip}(\mathrm{primeDir},p)$. Symmetry of cross-equality on the identity orientation, then transitivity, yields $\mathrm{primeDir},p\sim\mathrm{recip}(\mathrm{primeDir},p)$. That contradicts primeDirection_not_crossEq_recip.
why it matters
Native-cost uniqueness for PRC characters must exclude mixed identity/reciprocal prime calibrations. This lemma kills the same-axis (self-reciprocal) branch outright, so the remaining obstruction is only the distinct-prime mixed-pair case. Downstream, it feeds the equivalence that no-mixed-prime-witnesses is exactly the negation of the distinct-prime mixed-pair witness, and it is the one-line engine of PRCPrimeCalibratedSamePrimeMixedPairWitnessCharacter_absurd.
It also sits on the dependency path into the universal-foundation conditional certificate, which packages kernel, real-complete ordered field, and trace-logic certificates. In the broader Recognition forcing picture this is bookkeeping inside the cost-uniqueness layer that supports the unique $J$-cost (T5) rather than a new physical constant; it keeps character-level prime calibration free of self-reciprocal collisions before monotone d'Alembert and doubled-trace matching are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.