PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalBranchAgreementTarget_iff_local_identity_transport
plain-language theorem explainer
Under prime calibration, the local positive normal form that pairs orbit orientation with two-branch agreement is equivalent to the form that pairs the same orientation with identity-branch transport. Anyone tracking the nonunit branch-coupling blocker, or its later refutation, cites this bridge. The proof is a pure Iff constructor from the two already-proved one-direction implications.
Claim. The statement "local nonunit-orbit orientation together with two-branch agreement" is equivalent to "local nonunit-orbit orientation together with identity-branch transport." Both are positive normal forms of the global nonunit branch-coupling blocker under prime calibration; the second is the minimal form from which reciprocal transport follows.
background
In the Primitive Recognition Calculus native-cost uniqueness development, prime calibration forces a family of local targets that control how nonunit orbits orient and how their branches couple. Two of those targets share the same orientation half and differ only in the branch half.
The branch-agreement target asserts two-branch agreement and is documented as the positive normal form of the global nonunit branch-coupling blocker. The identity-transport target asserts identity-branch transport and is documented as the minimal positive normal form: reciprocal transport follows from orientation plus that identity transport alone.
Upstream, each direction of the equivalence is already a theorem: branch agreement yields identity transport (keeping orientation), and identity transport yields branch agreement (keeping orientation). The present declaration packages those two arrows as a single logical equivalence.
proof idea
Term-mode Iff introduction. The left-to-right arrow is the existing theorem that turns local orientation plus branch agreement into local orientation plus identity-branch transport. The right-to-left arrow is the dual theorem that turns local orientation plus identity transport into local orientation plus branch agreement. No new arithmetic or case analysis appears; the proof is exactly the pair of those two maps.
why it matters
This equivalence lets the development treat the two normal forms as interchangeable when discharging or refuting the nonunit branch-coupling blocker. Downstream, the branch-agreement target is refuted by transporting the hypothesis across this iff and invoking the already-proved refutation of the identity-transport target. The same bridge is consumed by the conditional universal-foundation certificate in UniversalFoundation, which assembles kernel, real-complete ordered field, and trace-logic certificates into a single PRC foundation package. In the broader Recognition forcing chain this sits inside native-cost uniqueness for the J-cost layer (T5), before phi self-similarity and the eight-tick octave are forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.