PRCPrimeCalibrationForcesNonunitBranchAgreementTarget_of_local_identity_transport
plain-language theorem explainer
Prime calibration plus the minimal local package (orbit orientation and identity-branch transport) already forces full two-branch agreement across nonunit directions. Anyone closing the PRC native-cost uniqueness chain cites this reduction. The proof is a short pointwise application of the character-level transport lemma to both conjuncts of the hypothesis.
Claim. Assume that every prime-direction-calibrated ratio character satisfies local nonunit orbit orientation and identity-branch transport. Then every such character also satisfies two-branch nonunit agreement: a nonunit branch choice in one direction agrees with every other nonunit direction on both the identity and reciprocal branches.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ act on ratio orbits. Prime-direction calibration pins the character on a preferred generator direction. Nonunit directions still carry a discrete branch choice (identity versus reciprocal).
Two-branch agreement is the global coherence demand: once a nonunit branch is fixed in one direction, every other nonunit direction must match it on both branches. The local package is weaker: local orbit orientation plus identity-branch transport only. The module records that this package is the minimal positive normal form, because reciprocal transport is then forced.
Upstream, the character-level lemma already converts local orientation and identity transport into full nonunit branch agreement for a single $\chi$. The present target-level statement lifts that implication under the universal prime-calibration quantifiers.
proof idea
Introduce an arbitrary ratio character $\chi$ that is a PRC ratio character and prime-direction calibrated. Project the hypothesis into its two conjuncts (local-orientation target and identity-branch-transport target) and instantiate each at $\chi$. Feed those two facts into PRCCharacterNonunitBranchAgreement_of_local_identity_branch_transport, which returns nonunit branch agreement for $\chi$. That is exactly the body of the branch-agreement target.
why it matters
This is a target-reduction step inside PRC native-cost uniqueness: it shows the two-branch agreement blocker is no stronger than the minimal local identity-transport package once prime calibration is in force. Downstream, it is the second conjunct in the combined orientation-plus-branch-agreement target theorem, and it is consumed by prc_universal_foundation_conditional_certificate in UniversalFoundation. In the broader Recognition chain it supports uniqueness of the native cost (the J-cost forced at T5) by eliminating residual branch freedom on nonunit orbits before the doubled-trace and d'Alembert layers lock the functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.