PRCCharacterPrimeReciprocalForcesTwoPrimeReciprocal_of_reciprocal_twist_identity_forces_two
plain-language theorem explainer
If the reciprocal twist of a ratio-orbit character satisfies the one-sided rule that identity on any calibrated prime axis forces identity on the orbit-2 axis, then the original character satisfies the dual rule: reciprocal orientation on any calibrated prime forces reciprocal orientation on orbit-2. Cited by the native-cost uniqueness blocker and the prime-calibration target lift. Proof is a short transport: convert reciprocal data to twist-identity via the prime iff, apply the hypothesis, convert back at two.
Claim. Let $\chi$ be a map on ratio orbits. Suppose the reciprocal twist $q \mapsto \mathrm{recip}(\chi(q))$ obeys: whenever $\chi^{\mathrm{twist}}$ is identity-oriented on any calibrated prime axis, it is identity-oriented on the distinguished orbit-$2$ prime axis. Then $\chi$ itself obeys: whenever $\chi$ is reciprocal-oriented on any calibrated prime axis, it is reciprocal-oriented on the orbit-$2$ prime axis.
background
In the Primitive Recognition Calculus, ratio data live on RatioOrbit displays (signed numerator over nonzero distinction denominator). Equality of displays is the internal cross-multiplication relation crossEq: two orbits match when scaled numerators balance as signed orbits (K4.10).
A character $\chi$ assigns to each ratio orbit another orbit. The reciprocal twist replaces $\chi(q)$ by its reciprocal; it is the conjugation that swaps identity orientation with reciprocal orientation on axes. The one-sided normal form says identity at any calibrated prime axis forces identity at the distinguished orbit-$2$ prime axis. Its dual says reciprocal orientation at any calibrated prime forces reciprocal orientation at orbit-$2$; together with the two-to-all reciprocal rule this is reciprocal-witness globalization.
The module develops native-cost uniqueness for PRC characters: which orientation and calibration constraints force the cost to match the unique $J$-shape from the forcing chain (T5).
proof idea
Term-mode transport along the reciprocal twist, three steps.
- From the assumption that $\chi$ is reciprocal on the prime axis $p$, the iff
PRCCharacterReciprocalTwist_prime_identity_iff_reciprocalyields that the twist is identity-oriented on that same prime axis. - Feed that identity witness into the hypothesis
hforces(identity-forces-two for the twist) to conclude the twist is identity-oriented on the orbit-$2$ axis. - Apply the converse direction of
PRCCharacterReciprocalTwist_two_identity_iff_reciprocalto recover that $\chi$ is reciprocal-oriented on orbit-$2$.
No extra arithmetic: pure orientation conjugation.
why it matters
Closes the dual half of the distinguished-axis normal form: the identity-forces-two rule on the twist is exactly reciprocal-forces-two-reciprocal on the original character. Downstream, PRCPrimeCalibrationForcesPrimeReciprocalForcesTwoPrimeReciprocalTarget_of_identity_forces_two lifts the identity target to the reciprocal target under prime calibration, and both feed prc_native_cost_uniqueness_blocker_certificate and the conditional universal-foundation certificate.
In framework terms this is bookkeeping for T5 $J$-uniqueness inside PRC: reciprocal-witness globalization is how native characters are pinned to the unique cost shape $J(x)=(x+x^{-1})/2-1$ once prime axes and the orbit-$2$ axis are calibrated. Without this transport, the identity and reciprocal branches would remain separate hypotheses rather than a single conjugated package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.