PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalIdentityTransportTarget_iff_local_comparable_trace
plain-language theorem explainer
Local orientation plus identity-branch transport is equivalent to the same orientation paired with finite δ-trace comparability on the identity branch. Anyone routing nonunit-orbit coherence through either normal form can cite this bridge. The proof is a two-line packaging of the already-proved directions.
Claim. Under prime calibration forcing nonunit orbits, the conjunction of local orbit orientation with identity-branch transport is equivalent to the conjunction of the same local orientation with finite $\delta$-trace comparability on the identity branch.
background
In the primitive recognition calculus, native cost uniqueness is reduced to sharpened local targets on nonunit orbits. Two active packages appear. The first pairs local orbit orientation with identity-branch transport; the module treats that pair as the minimal positive normal form, from which reciprocal transport is expected to follow. The second keeps the same orientation half and replaces the transport half by a finite $\delta$-trace comparability law on the identity branch (the trace-layer rewrite of the same content).
Both packages share the orientation conjunct and differ only in how the identity half is stated. Upstream one-direction lemmas already convert identity-branch transport into comparable-trace form and back, each preserving the orientation half. This declaration simply records that those two maps are mutual inverses at the level of the full conjunctions.
proof idea
Term-mode Iff introduction: the forward map is the existing lemma that turns local-identity-transport into local-comparable-trace (orientation kept, transport rewritten to $\delta$-trace comparability); the reverse map is the dual lemma that recovers identity-branch transport from comparable trace. No new algebra is done here.
why it matters
The bridge lets later arguments choose whichever normal form is convenient. Downstream, the identity-transport target is refuted by transporting a hypothesis across this iff and invoking the comparable-trace refutation. The same equivalence is also consumed by the conditional universal-foundation certificate, which packages kernel, real-complete ordered field, and trace-logic obligations for the PRC stack.
In the broader Recognition forcing picture this sits inside native-cost uniqueness for the J-cost layer (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$), where nonunit-orbit coherence must be reduced to local orientation plus a transport or trace law before global cost rigidity can be claimed. It does not itself settle uniqueness; it only equates two intermediate targets used on that path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.