PRCCharacterTwoPrimeReciprocalRespectsTraceConnected_of_reciprocal_twist_identity
plain-language theorem explainer
If the reciprocal twist of a ratio-orbit character satisfies identity branch transport along finite δ-trace connections from the orbit-2 prime axis, then the original character satisfies reciprocal branch transport on those same axes. Anyone proving two-prime reciprocal calibration from an identity hypothesis cites this bridge. The proof is a short term argument: convert the reciprocal seed at 2 into an identity seed for the twist, apply the hypothesis, and convert back at the target prime.
Claim. Let $\chi$ be a map on ratio orbits. Suppose the reciprocal twist $q \mapsto \mathrm{recip}(\chi(q))$ has the property that identity at the orbit-$2$ prime direction transports along any finite $\delta$-trace connection from the orbit-$2$ prime axis to a native prime axis $p$. Then $\chi$ itself has the reciprocal analogue: if $\chi$ sends the orbit-$2$ prime direction to its reciprocal, that reciprocal branch transports along the same connection to the prime-$p$ axis.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays built from a signed-orbit numerator and a nonzero distinction-nat denominator. Two ratio orbits are related by crossEq when cross-multiplication balances as signed orbits; this is the internal PRC stand-in for rational equality.
A character $\chi$ on ratio orbits may fix a prime axis or send it to its reciprocal. The identity two-prime trace-connected property says: if $\chi$ fixes the orbit-$2$ prime direction and a finite $\delta$-trace path connects that axis to a native prime $p$, then $\chi$ also fixes the $p$-axis. The reciprocal variant replaces both fixings by reciprocal images. The reciprocal twist of $\chi$ is the pointwise map $q \mapsto \mathrm{recip}(\chi(q))$.
This module develops native-cost uniqueness for PRC characters. The two-prime transport lemmas isolate how a calibration choice at orbit $2$ propagates to every trace-connected prime axis, which is the algebraic content needed before matching doubled-trace values to the unique $J$-cost.
proof idea
Term-mode proof with three steps. Introduce a prime $p$, a trace connection from the orbit-$2$ axis, and the reciprocal seed at $2$ for $\chi$. Apply the iff PRCCharacterReciprocalTwist_two_identity_iff_reciprocal to turn that reciprocal seed into an identity seed for the twist at the orbit-$2$ prime direction. Feed that seed into the assumed identity-transport property of the twist to obtain identity of the twist at the $p$-axis. Finally apply PRCCharacterReciprocalTwist_prime_identity_iff_reciprocal in the reverse direction to recover the reciprocal image of $\chi$ at the $p$-axis.
why it matters
Native-cost uniqueness in PRC needs both identity and reciprocal branch transport from the orbit-$2$ calibration. This lemma converts an identity-transport hypothesis on the reciprocal twist into reciprocal transport on the original character, so the two branches can be treated uniformly.
It is consumed by PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget_of_identity_trace_connected, which lifts a prime-calibration identity target to the corresponding reciprocal target, and it appears in the native-cost uniqueness blocker certificate that packages the proved factorization and refutation targets for the uniqueness argument.
In the broader Recognition chain this sits under T5 $J$-uniqueness: characters whose doubled-trace values obey the Recognition Composition Law must match the unique cost $J(x)=(x+x^{-1})/2-1$. Controlling reciprocal versus identity branches on prime axes is a necessary step before that matching.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.