PRCPrimeCalibrationForcesPrimeReciprocalForcesTwoPrimeReciprocalTarget_of_identity_forces_two
plain-language theorem explainer
If prime calibration forces identity on the orbit-2 axis whenever any calibrated prime axis is identity, then it also forces the reciprocal branch on orbit-2 whenever any native prime axis is reciprocal. Anyone closing the distinguished-axis half of native-cost uniqueness cites this transfer. The proof twists the character by reciprocal, applies the identity hypothesis to the twist, and untwists.
Claim. Assume that every prime-direction-calibrated ratio character $\chi$ with identity on some calibrated prime axis has identity on the orbit-$2$ prime axis. Then every such $\chi$ with a reciprocal-oriented native prime axis has the orbit-$2$ prime axis on the reciprocal branch.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a multiplicative map on ratio orbits (with unit fixed) used to factor a native cost in the d'Alembert sense. Calibration on prime directions means the cost generated by $\chi$ agrees with the canonical $J$-cost on every prime orbit.
Two distinguished-axis targets sit on opposite branches. The identity target says: if any calibrated prime axis is identity, then the orbit-$2$ prime axis is identity. The reciprocal target is the converse half of reciprocal globalization: if any native prime axis is reciprocal, then orbit-$2$ is reciprocal.
The reciprocal twist $\chi\mapsto q\mapsto(\chi q)^{-1}$ swaps the two branches while preserving the ratio-character and prime-calibration predicates. Upstream, the pointwise lemma already converts an identity-forces-two statement on the twist into a reciprocal-forces-two statement on $\chi$.
proof idea
Term-mode transfer, not a fresh calculation. Introduce a calibrated ratio character $\chi$. Form its reciprocal twist. The identity-forces target hypothesis, applied to that twist (using that twist preserves ratio-character and prime-direction calibration), yields identity-forces-two for the twist. Feed that into the upstream pointwise converter PRCCharacterPrimeReciprocalForcesTwoPrimeReciprocal_of_reciprocal_twist_identity_forces_two, which returns reciprocal-forces-two for the original $\chi$.
why it matters
This is one direction of the iff equating the identity and reciprocal distinguished-axis targets. That equivalence feeds the reciprocal-witness globalization step and the native-cost uniqueness blocker certificate in the same module. Downstream it also appears in the conditional universal-foundation certificate.
In the Recognition forcing chain, native $J$-cost uniqueness (T5: $J(x)=(x+x^{-1})/2-1$) is the algebraic spine behind the Recognition Composition Law. Closing the prime-axis branch dichotomy is part of showing no exotic calibrated character survives, so the cost is forced rather than chosen. The result does not itself prove either target; it only transfers one into the other.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.