PRCPrimeCalibrationForcesNonunitBranchAgreementTarget_of_transport_pair
plain-language theorem explainer
If prime calibration forces both one-way nonunit branch transports (identity and reciprocal), then it forces full two-branch agreement across nonunit directions. Anyone closing the nonunit branch-coupling blocker or the agreement↔transport-pair equivalence cites this. The proof is a short term application of the character-level transport-pair-to-agreement lemma to each calibrated character.
Claim. Assume the split target: prime calibration forces both nonunit identity-branch transport and nonunit reciprocal-branch transport. Then the two-branch agreement target holds: for every ratio-orbit character $\chi$ that is prime-direction calibrated, the nonunit branch choice at one direction agrees with every other nonunit direction on both the identity and reciprocal branches.
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio-orbit characters $\chi$ encode orientation data on ratio orbits. Prime-direction calibration is the hypothesis that $\chi$ is normalized on prime directions. Nonunit directions are those outside the unit orbit; on them one must choose identity versus reciprocal branch orientation.
The transport-pair target packages two one-way statements: prime calibration forces identity-branch transport and reciprocal-branch transport on nonunit directions (comparability of finite $\delta$-orbit traces under the calibrated orientation). The agreement target is the global two-branch form: a nonunit branch choice at one direction agrees with every other nonunit direction for both branches.
Upstream, the character-level lemma already shows that a transport pair on a fixed $\chi$ yields nonunit branch agreement for that $\chi$. This declaration lifts that implication from a single character to the quantified prime-calibration targets.
proof idea
Term-mode, four lines. Introduce a ratio character $\chi$ with the ratio-character and prime-calibration hypotheses. From the assumed transport-pair target, project the two conjuncts and specialize each at $\chi$ to obtain the identity and reciprocal transport facts for $\chi$. Package them as a transport pair and apply PRCCharacterNonunitBranchAgreement_of_transport_pair, which converts that pair into nonunit branch agreement for $\chi$. No extra algebraic work.
why it matters
This is one direction of the equivalence between the two-branch agreement target and the split transport-pair target; the sibling iff theorem wires both directions together. That equivalence is the positive normal form of the global nonunit branch-coupling blocker in native-cost uniqueness: local orientation plus two-branch agreement replaces a harder global coupling obligation.
Downstream it feeds prc_universal_foundation_conditional_certificate in UniversalFoundation, so the conditional foundation certificate can treat agreement and transport-pair formulations interchangeably when assembling kernel, ordered-field, and trace-logic pieces. In the broader Recognition forcing picture this sits inside native J-cost uniqueness infrastructure (the T5 J-cost line), not a new physical constant derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.