PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalBranchAgreementTarget_of_local_identity_transport
plain-language theorem explainer
Under prime calibration, local orbit orientation together with identity-branch transport already forces the two-branch agreement normal form for nonunit orbits. Anyone equating the two positive normal forms of the nonunit branch-coupling blocker, or assembling the universal foundation certificate, cites this implication. The proof is a one-line pair constructor: keep orientation and apply the branch-agreement-from-transport lemma.
Claim. Assume the local identity-transport target: local nonunit-orbit orientation together with identity-branch transport, under prime calibration. Then the local branch-agreement target holds: the same local orientation together with two-branch agreement for nonunit characters.
background
In the Primitive Recognition Calculus native-cost uniqueness layer, several Prop-valued targets package the positive normal forms of the global nonunit branch-coupling blocker. Local orientation of nonunit orbits is the shared first conjunct. The second conjunct may be either identity-branch transport or full two-branch agreement.
The identity-transport package is documented as the minimal positive normal form: reciprocal transport follows from orientation plus identity-branch transport alone. The branch-agreement package is the positive normal form of the blocker itself: orientation plus agreement of the two branches on nonunit characters.
Upstream, a sibling theorem already converts the full identity-transport target into bare two-branch agreement by specializing to a prime-calibrated nonunit character and invoking the character-level identity-branch transport lemma.
proof idea
Term-mode pair construction. From the hypothesis (orientation ∧ identity-branch transport), take the left projection as the orientation conjunct of the conclusion. For the right conjunct, apply the upstream theorem that turns the same identity-transport target into two-branch agreement. No extra tactics or case splits.
why it matters
This is one direction of the equivalence between the two positive normal forms of the nonunit branch-coupling blocker. The sibling iff theorem is assembled exactly as the pair of this implication and its converse. Downstream, the universal foundation conditional certificate in UniversalFoundation consumes the branch-agreement normal form as part of the kernel and trace-logic stack that certifies the PRC foundation under named hypotheses. In the broader Recognition forcing picture, clearing the nonunit branch-coupling blocker is a prerequisite for uniqueness of the native cost (the J-cost fixed by the Recognition Composition Law), so collapsing the two normal forms keeps the certificate surface minimal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.