PRCCharacterNonunitBranchAgreement_iff_coherent_of_local
plain-language theorem explainer
Under local identity-or-reciprocal orientation of every nonunit ratio-orbit direction, global two-branch coupling is equivalent to full orientation coherence (all nonunit directions identity, or all reciprocal). Native-cost uniqueness arguments cite this to collapse mixed-branch characters. The proof is a two-constructor Iff packaging the two one-way lemmas already proved in-module.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Assume every nonunit orbit direction is locally oriented: either the identity branch or the reciprocal branch. Then the two-branch coupling law (identity at one nonunit direction forces identity at every nonunit direction, and likewise for reciprocal) holds if and only if orientation is globally coherent: every nonunit direction is identity, or every nonunit direction is reciprocal.
background
In the Primitive Recognition Calculus, characters act on ratio orbits (integer numerator over a nonzero distinction-nat denominator). Nonunit orbit directions carry an orientation: identity versus reciprocal. Local orientation says each nonunit direction is one or the other; it is the nonprime analogue of the already-proved local-prime orientation alternative.
Branch agreement is the two-branch global coupling law: any identity-oriented nonunit direction transports identity to every other nonunit direction, and any reciprocal-oriented nonunit direction transports reciprocal everywhere. Coherence is stronger and simpler: the whole nonunit sector lies on a single branch (all identity, or all reciprocal). The module doc-comment on coherence stresses that this is "the exact coherence statement strong enough to rule out mixed product factors."
The local hypothesis is essential for one direction of the equivalence: without it, branch agreement need not force a uniform global choice. The converse (coherence implies branch agreement) holds unconditionally and is already recorded upstream.
proof idea
Term-mode Iff constructor. The forward arrow applies PRCCharacterNonunitOrbitOrientationCoherent_of_local_branch_agreement to the given local-orientation hypothesis, turning branch agreement into coherence. The reverse arrow is the unconditional lemma PRCCharacterNonunitBranchAgreement_of_coherent, which case-splits on the two disjuncts of coherence and discharges the universal quantifiers of branch agreement. No further tactic work.
why it matters
Native cost uniqueness in PRC needs to kill characters that mix identity and reciprocal factors on nonunit orbits. This equivalence lets the uniqueness pipeline treat branch agreement and full coherence as interchangeable once local orientation is in hand, so mixed-product factorizations are ruled out by a single coherent-branch alternative.
It feeds prc_native_cost_uniqueness_blocker_certificate, which packages the zero-calibrated factorization target and the refutation of signed-admissible mixed factorizations. In the broader Recognition forcing chain this sits under T5 J-uniqueness: the native cost is forced to the unique J-cost $J(x)=(x+x^{-1})/2-1$ once character orientations cannot mix branches. Closing the nonunit sector is the multiplicative step that extends prime-axis orientation control to all composite directions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.