PRCCharacterNonunitBranchAgreement_of_transport_pair
plain-language theorem explainer
From the split transport form of two-branch agreement (identity transport paired with reciprocal transport), one obtains the global two-branch coupling law on nonunit orbit directions. Anyone proving native-cost uniqueness or prime-calibration forcing of branch agreement will cite this direction of the equivalence. The proof is a direct unpacking: introduce the quantified directions and apply each conjunct of the transport pair.
Claim. Let $\chi$ be a map on ratio orbits. If $\chi$ satisfies both nonunit identity-branch transport and nonunit reciprocal-branch transport, then it satisfies two-branch nonunit agreement: for every pair of nonzero nonunit distinction naturals $p,r$, identity orientation of $\chi$ at $p$ implies identity orientation at $r$, and reciprocal orientation at $p$ implies reciprocal orientation at $r$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer-numerator display over a nonzero distinction-natural denominator (K4.7). Characters act as maps $\chi$ on these orbits. Orientation of a character at a nonzero distinction natural records whether the action is identity-like or reciprocal-like along that orbit direction.
Nonunit branch agreement is the two-branch global coupling law: any nonunit identity-oriented direction transports identity to every nonunit direction, and any reciprocal-oriented direction transports reciprocal to every nonunit direction. The transport-pair form splits that law into two separate transport predicates (identity branch transport and reciprocal branch transport) conjoined as a pair. The module develops native-cost uniqueness by forcing characters to match the unique J-cost structure; branch coupling is part of that forcing chain.
proof idea
Term-mode unpacking of a conjunction into a quantified biconditional-style agreement statement. Introduce the nonunit nonzero directions $p$ and $r$. The goal is a pair of implications (identity transport and reciprocal transport). The hypothesis is already that pair of transport predicates. Apply the first conjunct under an identity-orientation assumption at $p$, and the second conjunct under a reciprocal-orientation assumption at $p$. No auxiliary lemmas are required beyond the definitions of the pair and the agreement predicate.
why it matters
This is one direction of the equivalence between the split transport form and the global two-branch agreement law (PRCCharacterNonunitBranchAgreement_iff_transport_pair). Downstream, prime-calibration forcing of the transport pair is converted into forcing of full branch agreement by applying this theorem componentwise. That path feeds the native-cost uniqueness blocker certificate, which packages zero-calibrated factorization targets in the uniqueness program. In the broader Recognition framework, locking nonunit branch coupling is part of forcing the unique cost functional (the J-cost of T5) on the ratio-orbit character, so characters cannot freeload independent identity and reciprocal branches away from the self-similar fixed-point structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.