PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalIdentityTransportTarget_of_local_branch_agreement
plain-language theorem explainer
Local orbit orientation together with two-branch agreement already yields the minimal positive normal form that pairs orientation with identity-branch transport. Anyone closing the nonunit branch-coupling blocker or the PRC universal-foundation certificate cites this reduction. The proof is a two-field pair: keep orientation and discharge transport by the branch-agreement-to-identity-transport lemma.
Claim. If the prime-calibration nonunit package holds in the form "local orbit orientation and two-branch agreement," then it holds in the form "local orbit orientation and identity-branch transport." Reciprocal transport is then automatic from those two facts.
background
In the Primitive Recognition Calculus native-cost uniqueness development, several Prop packages record successive normal forms of the nonunit branch-coupling blocker under prime calibration. Two of them appear here. Local orbit orientation plus two-branch agreement is the positive normal form of that global blocker. Local orbit orientation plus identity-branch transport is the minimal positive normal form: once those two hold, reciprocal transport follows.
The upstream lemma used in the second component states that two-branch agreement alone forces identity-branch transport for every admissible character: given branch agreement, each prime-calibrated character satisfies the identity-branch transport law. The present declaration simply packages that implication with the shared orientation half.
proof idea
Term-mode pair construction. The hypothesis is a conjunction; its first conjunct (local orbit orientation) is copied unchanged into the conclusion. The second conjunct (two-branch agreement) is fed to PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget_of_branch_agreement, which returns identity-branch transport. The resulting pair is exactly the identity-transport normal form.
why it matters
This is one direction of the local equivalence between the branch-agreement normal form and the identity-transport normal form; the sibling converse and this arrow assemble the iff used when either package is acceptable as a hypothesis. Downstream it is consumed by prc_universal_foundation_conditional_certificate, which bundles kernel, real-complete ordered field, and trace-logic certificates into the conditional universal-foundation claim. In the broader Recognition forcing chain the step sits inside native-cost uniqueness for the J-cost (T5), clearing a nonunit obstruction before phi-fixed-point and octave structure are forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.