PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget_iff_identity_trace_connected
plain-language theorem explainer
The reciprocal and identity two-prime trace-connected targets are equivalent: prime calibration forces reciprocal orientation transport along finite δ-trace connections exactly when it forces identity orientation transport. Native-cost uniqueness and blocker-certificate work cite this collapse. The proof is a pure Iff constructor from the two already-proved one-direction implications.
Claim. The following two propositions are equivalent. (R) Every prime-direction-calibrated ratio character transports reciprocal orientation at the orbit-$2$ prime axis along any finite $\delta$-trace connection to a native prime axis. (I) The same statement with identity orientation in place of reciprocal orientation.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits obeying the PRC character axioms. Prime-direction calibration fixes how $\chi$ acts on the orbit-$2$ prime axis. Trace connection means a finite $\delta$-trace path linking that axis to a native prime axis; the targets ask whether calibrated characters must transport a chosen orientation (reciprocal or identity) along every such path.
The reciprocal target asserts that calibration forces reciprocal orientation to respect every finite $\delta$-trace connection. The identity target asserts the same for identity orientation. Pass 81 isolates the identity form as the same blocker as reciprocal trace transport, viewed through reciprocal twist.
Both targets live in the native-cost uniqueness module, where they sit among doubled-trace and d'Alembert hypotheses that constrain which cost functionals can arise from characters.
proof idea
Term-mode Iff introduction. The forward direction applies the already-proved implication from the reciprocal target to the identity target. The reverse applies the already-proved implication from the identity target to the reciprocal target. No new algebraic work occurs here; the declaration packages those two lemmas as a single equivalence.
why it matters
Collapsing the two targets lets the development refute one and automatically refute the other. Downstream, the reciprocal-target refutation rewrites through this Iff and the identity-target refutation. The native-cost uniqueness blocker certificate and the universal-foundation conditional certificate both sit on this blocker cluster.
In the Recognition forcing chain this is local scaffolding hygiene around T5 J-uniqueness and the Recognition Composition Law: it shows that two surface formulations of the same two-prime orientation obstruction are the same proposition, so uniqueness arguments need not track them separately. Pass 81's claim that identity is reciprocal-through-twist is thereby made formal as logical equivalence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.