PRCCharacterNonunitBranchAgreement
plain-language theorem explainer
Defines global two-branch agreement for a ratio-orbit character: if any nonunit nonzero direction is identity-oriented, every nonunit direction is; same for reciprocal orientation. Cited when coupling local orbit orientations into a single global branch choice. Pure Prop packaging of two universal implications over nonunit DistinctionNat directions.
Claim. A map $\chi$ on rational orbits satisfies nonunit branch agreement when, for every pair of nonzero nonunit finite distinction orbits $p,r$: if $\chi$ is identity-oriented at $p$ then it is identity-oriented at $r$, and if $\chi$ is reciprocal-oriented at $p$ then it is reciprocal-oriented at $r$. Identity (resp. reciprocal) orientation means $\chi$ of the orbit direction of $p$ is cross-equal to that direction (resp. to its reciprocal).
background
In the Primitive Recognition Calculus, finite distinction orbits are the inductive type DistinctionNat (zero and successors). The native unit predicate holds only for the one-step orbit. A RatioOrbit is a signed-orbit numerator over a nonzero distinction denominator: the display of a rational ratio of orbits.
A character is a self-map $\chi$ on ratio orbits. Identity orientation at a nonzero direction $p$ means $\chi$ fixes the orbit direction of $p$ up to cross-equality; reciprocal orientation means $\chi$ sends that direction to its reciprocal. These local orientation predicates are stated for arbitrary nonzero orbits, not only primes, so transport can pass through composites.
The present definition packages the two-branch global coupling law on the nonunit locus: orientation at one nonunit direction forces the same orientation at every other nonunit direction.
proof idea
Definitional Prop, not a proved theorem. The body is a universal quantifier over nonzero nonunit $p$ and $r$, asserting the conjunction of two implications: identity orientation of $\chi$ at $p$ implies identity at $r$, and reciprocal orientation at $p$ implies reciprocal at $r$. It directly composes the upstream orientation predicates (identity and reciprocal) with the native unit and nonzero filters on distinction orbits.
why it matters
This is the two-branch form of the global branch-coupling law used throughout native cost uniqueness. Downstream it is shown equivalent to the branch-transport pair and, under local orientation, to full nonunit orbit-orientation coherence. Introduction lemmas build it from coherence, from a transport pair, or from local orientation plus identity-branch transport; elimination lemmas recover transport and coherence from agreement.
In the Recognition forcing chain this sits inside the uniqueness apparatus for the native cost character (the J-cost side of T5), ensuring a single global choice of identity versus reciprocal branch on nonunit directions before matching doubled-trace data to the cost. It does not itself force $\phi$ or the eight-tick structure; it is scaffolding for character uniqueness on the orbit lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.