PRCCharacterPrimeIdentityForcesTwoPrimeIdentity_of_reciprocal_twist_reciprocal_forces_two
plain-language theorem explainer
If reciprocal orientation at any calibrated prime forces reciprocal orientation at the orbit-2 prime for the reciprocal twist of a ratio-orbit character, then identity at any calibrated prime forces identity at orbit-2 for the original character. Native-cost uniqueness and the universal-foundation certificate cite this transfer. The proof converts identity to twisted reciprocal by two iff lemmas, applies the force hypothesis, and converts back.
Claim. Let $\chi$ be a map on ratio orbits. Write $\tau(\chi)$ for the reciprocal twist $q \mapsto \mathrm{recip}(\chi(q))$. Suppose that for $\tau(\chi)$, reciprocal orientation (cross-equality with the reciprocal) at any calibrated prime axis forces reciprocal orientation at the distinguished orbit-$2$ prime axis. Then for $\chi$, identity orientation (cross-equality with the axis itself) at any calibrated prime axis forces identity orientation at the orbit-$2$ prime axis.
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display: a signed numerator orbit over a nonzero distinction-nat denominator. Two ratio orbits are related by cross-equality when the cross-multiplied signed orbits balance; this is the internal PRC stand-in for rational equality. The total reciprocal sends a ratio orbit to its inverse (zero to zero), matching $\mathbb{Q}$.
A character here is a map $\chi$ on ratio orbits. Identity orientation at a prime axis means $\chi$ fixes that axis up to cross-equality; reciprocal orientation means $\chi$ sends it to its reciprocal. The distinguished orbit-$2$ prime axis is the calibration anchor. The one-sided normal form says identity at any calibrated prime forces identity at orbit-$2$. The converse distinguished-axis form says reciprocal at any calibrated prime forces reciprocal at orbit-$2$.
The reciprocal twist is $\tau(\chi)(q) = \mathrm{recip}(\chi(q))$. The module develops native-cost uniqueness by reducing character constraints to these distinguished-axis force properties and transferring between identity and reciprocal sides via the twist.
proof idea
Short tactic proof. Fix a calibrated prime $p$ and assume $\chi$ is identity-oriented there. The iff lemma relating twist-reciprocal to original-identity at primes converts that assumption into reciprocal orientation of $\tau(\chi)$ at $p$. Apply the given force hypothesis for $\tau(\chi)$ to obtain reciprocal orientation of $\tau(\chi)$ at the orbit-$2$ axis. The companion iff lemma (twist-reciprocal iff original-identity at orbit-$2$) converts that conclusion back into identity orientation of $\chi$ at orbit-$2$. No extra algebraic work: pure orientation transfer across the twist.
why it matters
This closes the reverse direction advertised in the one-sided normal form: identity-forces-two is recovered from reciprocal-forces-two by applying the latter to the reciprocal twist. Downstream, the prime-calibration target theorem uses it to promote a reciprocal-side force hypothesis into the identity-side target needed for native-cost uniqueness. The native-cost uniqueness blocker certificate and the universal-foundation conditional certificate both depend on that chain.
In the Recognition framework this sits inside the foundation layer that pins the native cost before the forcing chain reaches T5 J-uniqueness and the Recognition Composition Law. Without the identity/reciprocal transfer, the distinguished-axis globalization would be one-sided and the uniqueness certificate could not discharge both orientations. No open scaffold remains on this lemma itself; it is fully proved and only packages existing iff facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.