PRCCharacterTwoPrimeIdentityRespectsTraceConnected_of_reciprocal_twist_reciprocal
plain-language theorem explainer
If the reciprocal twist of a ratio-orbit character transports the reciprocal branch along δ-trace connections from the orbit-2 prime axis, then the untwisted character transports the identity branch along those same connections. Cited when reducing identity-branch calibration to the reciprocal case in native-cost uniqueness. The proof applies the twist hypothesis, then cancels a double reciprocal via crossEq transitivity.
Claim. Let $\chi$ be a map on ratio orbits. Write $\tau(\chi)(q) := \mathrm{recip}(\chi(q))$ for its reciprocal twist. Suppose that whenever a native prime axis $p$ is $\delta$-trace-connected to the orbit-$2$ prime axis and $\tau(\chi)$ sends the orbit-$2$ prime direction to its reciprocal, then $\tau(\chi)$ sends the $p$-prime direction to its reciprocal. Then the same holds for $\chi$ with the identity branch: if $\chi$ fixes the orbit-$2$ prime direction under cross-multiplication equivalence, it fixes every trace-connected native prime direction.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays built from signed $\delta$-orbits (numerator) over 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. The total reciprocal on ratio orbits mirrors $\mathbb{Q}$, sending zero to zero.
A character $\chi$ on ratio orbits may fix a prime direction or send it to its reciprocal. The identity two-prime trace-connected transport property says: if $\chi$ fixes the orbit-$2$ prime direction and a native prime axis $p$ is reachable by a finite $\delta$-trace connection from that axis, then $\chi$ also fixes the $p$-prime direction. The reciprocal analogue replaces both fixings by reciprocal branch transport.
The reciprocal twist $\tau(\chi)(q) = \mathrm{recip}(\chi(q))$ swaps identity and reciprocal branches. This lemma converts a reciprocal-transport hypothesis on $\tau(\chi)$ into an identity-transport conclusion for $\chi$, which is the algebraic content needed when local prime orientation is reduced to a single calibrated branch.
proof idea
Tactic proof. Fix a prime $p$, a trace connection from the orbit-$2$ axis, and the identity hypothesis that $\chi$ fixes the two-prime direction under crossEq.
Apply reciprocal congruence to that identity hypothesis to obtain that the twisted character sends the two-prime direction to its reciprocal. Feed this into the assumed reciprocal-transport property of the twist at $p$, yielding that $\mathrm{recip}(\chi(\mathrm{primeDir},p))$ is cross-equivalent to $\mathrm{recip}(\mathrm{primeDir},p)$.
Left-reciprocal cancellation (ratioOrbit_recip_left_crossEq_iff) rewrites this as $\chi(\mathrm{primeDir},p)$ cross-equivalent to the double reciprocal of the prime direction. Transitivity of crossEq with the double-reciprocal identity (ratioOrbit_recip_recip_crossEq_self) closes the identity transport for $\chi$ at $p$.
why it matters
Native-cost uniqueness in PRC aims to force the recognition cost to the unique $J$-shape from the forcing chain (T5: $J(x)=(x+x^{-1})/2-1$). Branch transport along prime axes is part of calibrating characters so that cost equality on primes lifts to the full ladder.
This lemma is the bridge from reciprocal-branch calibration to identity-branch calibration under twist. Downstream, PRCPrimeCalibrationForcesTwoPrimeIdentityTraceConnectedTarget_of_reciprocal_trace_connected applies exactly this reduction: assuming the reciprocal trace-connected target, it concludes the identity target. That feeds the native-cost uniqueness blocker certificate, which packages proved factorization targets and refuted signed-admissible alternatives.
Without the twist reduction, identity and reciprocal cases would need separate prime-calibration arguments. The lemma keeps the uniqueness spine on a single branch and lets reciprocity do the rest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.