PRCCharacterPrimeIdentityForcesTwoPrimeIdentity_iff_two_prime_reciprocal_excludes
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 its contrapositive branch "reciprocal on orbit-2 excludes identity on every prime." Native-cost uniqueness and mixed-orientation blocker arguments cite this bridge. The proof is a pure Iff constructor from the two already-proved directed lemmas.
Claim. Let $\chi$ be a map on rational orbits. Assume that on every prime direction, $\chi$ acts by identity or by reciprocal (local prime orientation). Then the following are equivalent: (i) whenever $\chi$ fixes any calibrated prime axis, it also fixes the distinguished prime axis of orbit $2$; (ii) if $\chi$ sends the orbit-$2$ axis to its reciprocal, then $\chi$ fixes no native prime axis.
background
In the Primitive Recognition Calculus, rational comparison data live on RatioOrbit: an integer numerator over a nonzero orbit denominator. A character $\chi$ is a self-map of these orbits. Local prime orientation says each prime axis is sent either to itself or to its reciprocal; that is the algebraic content of matching J-costs on a single prime direction.
Two normal forms package the mixed-orientation obstruction around the distinguished orbit-$2$ prime axis. The one-sided form asserts that identity orientation at any calibrated prime forces identity at orbit $2$. The contrapositive branch asserts that reciprocal orientation at orbit $2$ forbids identity on every native prime axis. The reverse direction of the one-sided form is recovered at target level by twisting the character by reciprocity.
This module develops native-cost uniqueness for PRC characters whose doubled-trace data match the J-cost. The present statement equates the two normal forms once local orientation is assumed, so either packaging can be used downstream.
proof idea
Term-mode Iff constructor, no tactics. The forward arrow is the already-proved directed lemma that turns the one-sided identity-forces-two form into the reciprocal-excludes-identity form (no local-orientation hypothesis needed). The reverse arrow applies the companion directed lemma that, under local prime orientation, recovers the one-sided form from the reciprocal-exclusion form, feeding in the ambient local-orientation hypothesis. The resulting pair is exactly the $\leftrightarrow$ inhabitant.
why it matters
This equivalence is the packaging bridge inside native-cost uniqueness. It is consumed immediately by the witness-form variant of the same Iff, which swaps the universal exclusion statement for an atomic mixed-witness blocker. That blocker feeds prc_native_cost_uniqueness_blocker_certificate, the certificate that zero-calibrated native-cost character factorization is proved while the signed-admissible competitor is refuted.
The same edge appears in prc_universal_foundation_conditional_certificate, so the bridge sits on the path from PRC kernel and trace-logic certificates up to the conditional universal foundation. In framework terms it is local algebraic hygiene for T5-style J-uniqueness: once J-costs match on prime axes, mixed identity/reciprocal orientations cannot be chosen independently, and the orbit-$2$ axis is the distinguished witness that forces global coherence. No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.