PRCCharacterReciprocalTwist_two_identity_iff_reciprocal
plain-language theorem explainer
For any map χ on ratio orbits, the reciprocal twist of χ fixes the two-prime direction under cross-equality exactly when χ sends that direction to its reciprocal. Used when reducing identity-at-two conditions on twisted characters to reciprocal conditions on the original map. One-line wrapper of the left-reciprocal cross-equality swap lemma.
Claim. For any map $\chi$ from ratio orbits to ratio orbits, $\mathrm{crossEq}(\mathrm{recip}(\chi(2^\bullet)),\, 2^\bullet)$ if and only if $\mathrm{crossEq}(\chi(2^\bullet),\, \mathrm{recip}(2^\bullet))$, where $2^\bullet$ is the two-prime direction and $\mathrm{crossEq}$ is cross-multiplication equality of ratio orbits.
background
In the primitive recognition calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator (K4.7). Two ratio orbits are related by crossEq when scaled numerators balance under cross-multiplication; this is the internal PRC stand-in for rational equality (K4.10). Reciprocal on ratio orbits is total and sends zero to zero, matching $\mathbb{Q}$ (K4.12).
The two-prime direction is the ratio-orbit display of the prime orbit for $2$. The reciprocal twist of a map $\chi$ is the pointwise composition $\mathrm{recip}\circ\chi$. The ambient module develops native-cost uniqueness for PRC characters: maps on ratio orbits whose doubled-trace data recover the J-cost and obey d'Alembert-type identities.
Upstream, ratioOrbit_recip_left_crossEq_iff already records that left-reciprocal and right-reciprocal swap under cross-equality: $\mathrm{crossEq}(\mathrm{recip},a,,b)\leftrightarrow\mathrm{crossEq}(a,,\mathrm{recip},b)$. The present statement is that swap specialized at $a=\chi(2^\bullet)$ and $b=2^\bullet$.
proof idea
One-line wrapper. Instantiate the upstream swap lemma ratioOrbit_recip_left_crossEq_iff at $a = \chi(2^\bullet)$ and $b = 2^\bullet$. Unfolding the reciprocal-twist definition, the left-hand side is exactly $\mathrm{crossEq}(\mathrm{recip}(\chi(2^\bullet)),,2^\bullet)$, so the biconditional is immediate by exact.
why it matters
Native-cost uniqueness in PRC needs control of how characters act at the two-prime direction and under reciprocal. This lemma converts an identity condition on the reciprocal twist at $2^\bullet$ into a reciprocal condition on the original map at $2^\bullet$, without any admissibility hypothesis.
Downstream it is used by the theorems that push prime-identity-forces-two-prime-identity through the reciprocal twist, that transfer two-prime reciprocal respect for trace-connectedness from the twist back to $\chi$, and that assemble the prime-calibration target equating prime identity with two-prime identity. Those feed the native-cost uniqueness blocker certificate. In the broader forcing chain this is bookkeeping on the rational skeleton that supports J-uniqueness (T5) and the Recognition Composition Law, not a new physical constant claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.