PRCPrimeCalibrationForcesTwoPrimeIdentityTraceConnectedTarget_of_reciprocal_trace_connected
plain-language theorem explainer
Assuming prime calibration forces reciprocal two-prime orientation along any finite δ-trace connection, the same holds for identity orientation. Anyone tracking the native-cost uniqueness blockers or the reciprocal/identity equivalence cites this. The argument is a short term reduction: apply the reciprocal target to the reciprocal twist of the character and unwind via the twist-transport lemma.
Claim. If prime calibration forces reciprocal orientation at the orbit-$2$ prime axis to transport along every finite $\delta$-trace connection to a native prime axis, then prime calibration likewise forces identity orientation to transport along every such connection.
background
In the Primitive Recognition Calculus, ratio characters are maps $\chi$ on ratio orbits that encode admissible cost orientations. Prime-direction calibration fixes how $\chi$ sits on the orbit-$2$ prime axis. Two competing transport targets ask whether that calibrated orientation (identity or reciprocal) survives along any finite $\delta$-trace path to a native prime axis.
Pass 81 isolates the identity transport target as the same uniqueness blocker as reciprocal transport, viewed through reciprocal twist. The reciprocal twist of a character is $\chi^{\mathrm{tw}}(q) = \mathrm{recip}(\chi(q))$; it preserves the ratio-character and prime-calibration hypotheses. The reciprocal target is the universal statement that every calibrated character has reciprocal two-prime orientation respecting trace connection; the identity target is the parallel statement for identity orientation.
This module packages those targets as named propositions so uniqueness certificates can cite a single Prop rather than an open quantification.
proof idea
Term-mode one-liner after introducing $\chi$, the ratio-character hypothesis, and prime calibration. Apply the reciprocal target hypothesis to the reciprocal twist of $\chi$, using that twist preserves both the character and prime-calibration data. Feed the resulting reciprocal-respects-trace fact into the upstream lemma that converts reciprocal respect for the twist back into identity respect for the original character. No extra algebraic work; the reduction is pure orientation duality.
why it matters
Closes one direction of the equivalence between the reciprocal and identity two-prime trace-connected targets, so the uniqueness stack may treat them as interchangeable blockers. The immediate parent is the iff theorem equating the two targets; that equivalence feeds the native-cost uniqueness blocker certificate and, farther up, the conditional universal-foundation certificate.
In the Recognition forcing picture this sits inside native $J$-cost uniqueness (the T5 lineage): only after orientation transport is forced along $\delta$-traces can the cost character be pinned to the unique $J(x)=(x+x^{-1})/2-1$ solution of the Recognition Composition Law. The declaration does not itself prove either target; it shows they stand or fall together under reciprocal twist.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.