PRCCharacterNonunitBranchAgreement_iff_transport_pair
plain-language theorem explainer
Equivalence between the two-branch nonunit coupling law for a ratio-orbit character and its split transport form (identity transport paired with reciprocal transport). Anyone working the PRC native-cost uniqueness chain cites this to switch formulations. The proof is a pure biconditional packaging of the two directed lemmas.
Claim. For a map $\chi$ on ratio orbits, the two-branch nonunit agreement law (any nonunit identity-oriented direction forces identity orientation on every nonunit direction, and likewise for reciprocal orientation) holds if and only if $\chi$ satisfies the split transport pair: nonunit identity-branch transport together with nonunit reciprocal-branch transport.
background
In the Primitive Recognition Calculus, a character $\chi$ acts on ratio orbits and orients each nonunit distinction either toward the identity branch or the reciprocal branch. The two-branch agreement law says that orientation is globally rigid on the nonunit locus: once one nonunit direction is identity-oriented, every other nonunit direction is identity-oriented, and the same for reciprocal orientation.
The transport-pair formulation splits that global statement into two independent transport predicates, one per branch. The module develops native cost uniqueness from character data, J-cost structure, and d'Alembert-type trace laws; this equivalence is a bookkeeping bridge between the global coupling language and the split transport language used in later uniqueness arguments.
proof idea
Term-mode biconditional: the forward direction is the existing lemma that builds the transport pair from branch agreement; the reverse is the lemma that rebuilds branch agreement from the transport pair. No extra algebra is performed here.
why it matters
Native-cost uniqueness in PRC needs a clean handoff between global branch-coupling hypotheses and the split identity/reciprocal transport obligations that feed doubled-trace and d'Alembert arguments. This iff lets later proofs choose whichever packaging is convenient without changing mathematical content. It sits in the foundation layer that ultimately supports J-uniqueness (T5) and the forced self-similar fixed point $\phi$ (T6), by keeping character orientation data interchangeable across formulations. No downstream edges are recorded on this page, so its immediate consumers are sibling uniqueness lemmas in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.