PRCCharacterTwoPrimeReciprocalExcludesPrimeIdentity_iff_witness
plain-language theorem explainer
For any ratio-orbit character, the universal form of the orbit-2 reciprocal obstruction (no identity-oriented native prime) is equivalent to its existential witness form (even one such prime is impossible). Native-cost uniqueness and the conditional universal-foundation certificate cite this bridge. The proof is a two-direction packaging of the already-proved conversion lemmas.
Claim. For every map $\chi$ from ratio orbits to ratio orbits, the following are equivalent: (i) if $\chi$ sends the distinguished prime-$2$ direction to its reciprocal, then for every native prime direction $p$ one has $\chi(p)\not\equiv p$; (ii) if $\chi$ sends the distinguished prime-$2$ direction to its reciprocal, then there cannot exist even one native prime direction $p$ with $\chi(p)\equiv p$.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-natural denominator. Characters $\chi$ act on these orbits and may orient each prime axis either as the identity or as the reciprocal of that axis (detected by crossEq).
The distinguished orbit-$2$ prime direction is special in the native-cost uniqueness argument. The universal obstruction says: if $\chi$ is reciprocal on that axis, then no native prime axis may be identity-oriented. The witness form says the same thing existentially: reciprocal orientation at $2$ cannot coexist with even one identity-oriented native prime. Both are pure branch blockers on mixed identity/reciprocal prime orientations.
This module develops uniqueness of the native cost functional from character hypotheses (trace matching, d'Alembert structure, local prime orientation). The two formulations must be interchangeable before they can be chained into the prime-identity-forces-two-identity implication.
proof idea
One-line term proof. Introduce $\chi$, then package the two already-proved conversion lemmas as an Iff pair: the witness-from-universal direction and the universal-from-witness direction. No new arithmetic; pure logical packaging of $\forall$ versus $\exists\to\mathrm{False}$ on the same mixed-orientation hypothesis.
why it matters
Sits in the native-cost uniqueness spine of Primitive Recognition Calculus. Downstream, PRCCharacterPrimeIdentityForcesTwoPrimeIdentity_iff_two_prime_reciprocal_excludes_witness rewrites the prime-identity-forces-two-identity claim into the witness form of this obstruction (under local prime orientation). That bridge feeds the conditional universal-foundation certificate in UniversalFoundation, which assembles kernel, real-complete ordered field, and trace-logic certificates.
Framework role: the forcing chain needs a unique native cost before J-uniqueness (T5) and the Recognition Composition Law can be pinned as the only admissible cost. This lemma is bookkeeping, not physics, but without the $\forall$/witness equivalence the mixed-branch exclusion cannot be threaded cleanly through the uniqueness argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.