PRCCharacterNonunitReciprocalBranchTransport_of_branch_agreement
plain-language theorem explainer
If a ratio-orbit character satisfies two-branch nonunit agreement, then reciprocal orientation on any single nonunit direction forces reciprocal orientation on every nonunit direction. Native-cost uniqueness and prime-calibration arguments cite this to split the dual half of branch coupling. The proof is a one-line projection of the second conjunct of the agreement hypothesis.
Claim. Let $\chi$ be a map on rational orbits. Suppose that for every pair of nonunit nonzero 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$. Then $\chi$ satisfies reciprocal branch transport: whenever one nonunit direction is reciprocal-oriented under $\chi$, every nonunit direction is reciprocal-oriented.
background
In the Primitive Recognition Calculus, characters act on RatioOrbit displays (signed numerator over a nonzero distinction-natural denominator). Orbit directions on nonunit primes split into identity-oriented and reciprocal-oriented branches; coherence of a candidate native cost requires that these branches couple globally rather than mix.
Two-branch agreement packages both couplings at once: any nonunit identity-oriented direction transports identity to every nonunit direction, and any reciprocal-oriented direction transports reciprocal to every nonunit direction. Reciprocal branch transport is the dual half alone: if one nonunit orbit direction is reciprocal-oriented, every nonunit orbit direction is reciprocal-oriented (Pass 57 isolates this split).
The ambient module develops uniqueness of the native cost functional on these characters, feeding the broader forcing chain that pins $J$ and the self-similar scale $\varphi$.
proof idea
Term-style extraction after introducing the universal quantifiers of reciprocal transport. Apply the two-branch agreement hypothesis at the source nonunit $p$ and target nonunit $r$; the resulting conjunction has reciprocal transport as its second component. Discharge that component with the assumed reciprocal orientation at $p$. No auxiliary lemmas are required beyond the definitions of the two propositions.
why it matters
This is the reciprocal half of the split of two-branch agreement. Downstream, PRCCharacterNonunitBranchTransportPair_of_branch_agreement packages it with the identity half into a transport pair. Prime-calibration forcing reuses it to push calibrated characters onto the reciprocal-transport target. The native-cost uniqueness blocker certificate ultimately depends on this branch of the graph, so the lemma sits on the path that certifies uniqueness of the PRC native cost (the local stand-in for $J$-cost uniqueness in the T5 forcing step). Without the split, later targets cannot cite reciprocal transport independently of identity transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.