PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget_of_identity_trace_connected
plain-language theorem explainer
If prime calibration forces identity orientation at the orbit-2 prime axis to transport along any finite δ-trace connection, then it also forces reciprocal orientation transport. Anyone tracking the two-prime native-cost uniqueness blockers cites this. The proof twists the character by reciprocity, feeds the identity target, and untwists via the reciprocal-twist identity lemma.
Claim. Assume that every ratio character $\chi$ that is prime-direction calibrated has identity orientation at the orbit-$2$ prime axis transporting along any finite $\delta$-trace connection to a native prime axis. Then every such $\chi$ also has reciprocal orientation at that axis transporting along any finite $\delta$-trace connection.
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio characters $\chi : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$ encode orientation data on ratio orbits. Prime-direction calibration pins the character at the orbit-$2$ prime axis. Two target propositions ask whether that calibration forces the character's orientation (identity or reciprocal) to transport along any finite $\delta$-trace connection to a native prime axis.
The reciprocal twist sends $\chi$ to $q \mapsto \mathrm{recip}(\chi, q)$. Pass 81 isolates the identity and reciprocal two-prime trace-connected targets as the same blocker, related by this twist. Upstream, PRCCharacterTwoPrimeReciprocalRespectsTraceConnected_of_reciprocal_twist_identity converts an identity-respect statement on the twisted character into a reciprocal-respect statement on the original character. The identity target is the hypothesis of this implication; the reciprocal target is the conclusion.
proof idea
Term-mode proof. Introduce a ratio character $\chi$ with the character and prime-calibration hypotheses. Apply the identity-target hypothesis to the reciprocal twist of $\chi$, using that reciprocal twist preserves both the ratio-character property and prime-direction calibration. Feed that identity-respect conclusion into PRCCharacterTwoPrimeReciprocalRespectsTraceConnected_of_reciprocal_twist_identity, which returns reciprocal trace-connected respect for the original $\chi$.
why it matters
This is one direction of the equivalence between the two-prime identity and reciprocal trace-connected targets (the iff theorem packages both directions). Downstream, the identity target is lifted further to full prime-identity trace transport, and both sit inside the native-cost uniqueness blocker certificate and the conditional universal-foundation certificate. In the Recognition forcing chain the native cost is the unique $J$ of T5; these targets are the remaining orientation-transport obligations that must close before prime calibration forces the native cost character on connected components. Closing either target (they are equivalent) removes a named blocker on the uniqueness path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.