PRCCharacterNonunitBranchTransportPair_of_branch_agreement
plain-language theorem explainer
If a ratio-orbit character satisfies two-branch nonunit agreement (identity orientation at any nonunit direction forces identity at every nonunit direction, and likewise for reciprocal), then it satisfies the split transport-pair form of that law. Native-cost uniqueness and the agreement↔transport-pair equivalence cite this. The proof is a two-constructor packing of the identity and reciprocal transport lemmas.
Claim. Let $\chi$ map ratio orbits to ratio orbits. If $\chi$ obeys two-branch nonunit agreement (any nonunit identity-oriented direction transports identity to every nonunit direction, and any reciprocal-oriented direction transports reciprocal to every nonunit direction), then $\chi$ satisfies the split transport pair: nonunit identity-branch transport together with nonunit reciprocal-branch transport.
background
In the Primitive Recognition Calculus, characters act on RatioOrbit displays (signed numerator over a nonzero distinction-nat denominator). Orientation of a character along a nonunit direction is either identity-type or reciprocal-type. The two-branch agreement law says those orientations couple globally on the nonunit locus: identity at one nonunit direction forces identity at every other, and likewise for reciprocal.
The transport-pair packaging splits that single quantified conjunction into two separate transport predicates, one per branch. That split is the form later steps prefer when they reason about identity transport and reciprocal transport independently (including trace-order reformulations of identity transport).
This sits in the native-cost uniqueness development: characters that match the native cost must obey these branch-coupling constraints before uniqueness of the cost functional can be certified.
proof idea
Term-mode pair constructor. Apply PRCCharacterNonunitIdentityBranchTransport_of_branch_agreement to the agreement hypothesis for the first conjunct, and PRCCharacterNonunitReciprocalBranchTransport_of_branch_agreement for the second. Each upstream lemma is itself a one-line projection of the corresponding half of the agreement quantifier. No further case analysis.
why it matters
Closes one direction of PRCCharacterNonunitBranchAgreement_iff_transport_pair, so agreement and the split transport pair may be used interchangeably downstream. That equivalence feeds the native-cost uniqueness blocker certificate path, which packages zero-calibrated factorization targets for the uniqueness argument.
In the broader Recognition forcing chain, native cost uniqueness is the bridge from the Recognition Composition Law and J-uniqueness (T5) to a single admissible cost on ratio orbits. Branch-coupling lemmas like this pin how characters may orient nonunit directions without breaking the cost match. Without the transport-pair form, later trace-order and d'Alembert steps cannot separate identity from reciprocal obligations cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.