PRCCharacterPrimeIdentityForcesTwoPrimeIdentity_iff_two_prime_reciprocal_excludes_witness
plain-language theorem explainer
Under local prime orientation of a ratio-orbit character, the one-sided normal form "identity on any prime forces identity on the orbit-2 axis" is equivalent to the atomic witness obstruction "reciprocal on orbit-2 forbids any identity-oriented prime." Native-cost uniqueness arguments cite this when packaging branch normal forms. The proof is a two-step Iff chain through the non-witness exclusion form.
Claim. Let $\chi$ map rational orbits to rational orbits, and assume each prime direction is sent by $\chi$ either to itself or to its reciprocal. Then the following are equivalent: (i) whenever $\chi$ fixes any calibrated prime direction, it also fixes the distinguished prime-$2$ direction; (ii) if $\chi$ sends the prime-$2$ direction to its reciprocal, then no native prime direction is fixed by $\chi$ (witness form).
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. Characters act on these orbits. Local prime orientation means each prime axis is sent individually to itself or to its reciprocal; that is the algebraic content of matching $J$-costs on a single prime direction.
The one-sided normal form says identity at any calibrated prime forces identity at the distinguished orbit-$2$ prime axis (the reverse is recovered by reciprocal twist). The witness obstruction is the atomic mixed-branch blocker: reciprocal orientation at orbit-$2$ cannot coexist with even one identity-oriented native prime.
This module develops native-cost uniqueness for PRC characters, tying orientation constraints on prime axes to the doubled-trace/$J$-cost picture that feeds T5 $J$-uniqueness.
proof idea
Term-mode one-liner. Apply the prior equivalence that, under local prime orientation, the identity-forces-two-prime form is iff the non-witness reciprocal-excludes-identity form. Then chain via Iff.trans with the pure logical equivalence between that non-witness form and its existential-witness packaging. No new case analysis.
why it matters
Closes a packaging step in the native-cost uniqueness ladder: the one-sided prime-identity normal form is interchangeable with the atomic orbit-$2$ mixed-witness blocker once local orientation is assumed. Downstream consumers (none wired yet in the graph) can pick whichever normal form is convenient when ruling out mixed prime-axis inversions that would break trace coherence.
In the broader Recognition chain this sits under T5 $J$-uniqueness: characters that preserve $J$-cost on prime directions must not mix identity and reciprocal orientations across primes. The orbit-$2$ axis is the distinguished calibration point for that coherence. No open scaffold remains; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.