PRCCharacterReciprocalTwist_two_reciprocal_iff_identity
plain-language theorem explainer
For any map χ on ratio orbits, the reciprocal twist of χ sends the two-prime direction to the reciprocal of that direction (up to cross-equivalence) exactly when χ itself fixes the two-prime direction. Native-cost uniqueness arguments cite this to move prime-identity forcing statements across the reciprocal twist. The proof is a short iff by recip-congruence, double-reciprocal cancellation, and crossEq transitivity.
Claim. Let $\chi$ be any map on ratio orbits. Write $\mathrm{twist}(\chi)(q) := \mathrm{recip}(\chi(q))$. Then $\mathrm{twist}(\chi)(2_{\mathrm{prime}}) \sim \mathrm{recip}(2_{\mathrm{prime}})$ if and only if $\chi(2_{\mathrm{prime}}) \sim 2_{\mathrm{prime}}$, where $\sim$ is cross-multiplication equivalence of ratio orbits.
background
Primitive Recognition Calculus works with ratio orbits: integer numerator over a nonzero distinction-orbit denominator (K4.7). Two orbits are related by crossEq when cross-multiplication balances as signed orbits (K4.10); this is the internal rational equality, choice-free on δ-orbit positions. Reciprocal on ratio orbits is total and sends zero to zero as in $\mathbb{Q}$ (K4.12).
The reciprocal twist of a character map $\chi$ is pointwise $\mathrm{recip}\circ\chi$. The two-prime direction is the distinguished ratio-orbit generator used when forcing prime-identity behaviour of PRC characters. Congruence of reciprocal under crossEq and cancellation of double reciprocal are already available upstream.
This module builds native-cost uniqueness: characters whose doubled-trace cost matches the J-cost must be forced toward the identity on the prime ladder. Reciprocal twist is the symmetry that swaps identity-forcing statements with reciprocal-forcing statements.
proof idea
Term-mode constructor on the biconditional.
Forward: assume crossEq (twist χ 2, recip 2). Unfold twist to crossEq (recip(χ 2), recip 2). Apply ratioOrbit_recip_left_crossEq_iff to obtain crossEq (χ 2, recip(recip 2)). Transitivity with ratioOrbit_recip_recip_crossEq_self cancels the double reciprocal and yields crossEq (χ 2, 2).
Backward: assume crossEq (χ 2, 2). ratioOrbit_recip_congr gives crossEq (recip(χ 2), recip 2), which is the twist statement after simpa on the definition.
why it matters
Feeds PRCCharacterPrimeIdentityForcesTwoPrimeIdentity_of_reciprocal_twist_reciprocal_forces_two, which converts a reciprocal-forcing hypothesis on the twisted character into an identity-forcing statement on the original character. That bridge is recorded in the native-cost uniqueness blocker certificate (prc_native_cost_uniqueness_blocker_certificate).
In the Recognition stack, native cost uniqueness is the PRC-side route toward J-uniqueness (forcing chain T5): the cost functional on ratio characters must be the unique d'Alembert/J solution fixed by the Recognition Composition Law. Controlling the two-prime direction under reciprocal twist is a concrete algebraic step in that uniqueness ladder, not a physics claim by itself.
No open scaffold: the theorem is fully proved and only rearranges already-established recip/crossEq algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.