PRCCharacterNonunitOrbitOrientationCoherent_of_local_branch_agreement
plain-language theorem explainer
Local identity-or-reciprocal orientation on every nonunit ratio-orbit direction, plus two-branch transport (identity or reciprocal at one nonunit forces the same choice everywhere), yields global coherence: all nonunits are identity-oriented or all are reciprocal. Cited in the native-cost uniqueness pipeline when ruling out mixed product factors. Proof is a case split on existence of one identity-oriented nonunit, then branch agreement or local orientation finishes each arm.
Claim. Let $\chi$ map ratio-orbits to ratio-orbits. Suppose every nonunit orbit direction is locally oriented (identity or reciprocal), and suppose branch agreement holds: identity orientation at any one nonunit transports to every nonunit, and likewise for reciprocal. Then nonunit orientation is coherent: either every nonunit direction is identity-oriented, or every nonunit direction is reciprocal-oriented.
background
In the Primitive Recognition Calculus, ratio-orbits are rational displays (signed numerator over a nonzero finite distinction-orbit denominator). Distinction orbits are the base-neutral finite iterates of repeated distinction; the only multiplicative unit among them is the one-step orbit. A character $\chi$ acts on ratio-orbits; for each nonunit direction one asks whether $\chi$ acts as the identity map or as reciprocal inversion along that direction.
Local orientation asserts that every nonunit direction is one or the other (the nonprime analogue of the already-proved local-prime alternative). Branch agreement is the two-branch global coupling law: an identity choice at any nonunit forces identity at every nonunit, and a reciprocal choice forces reciprocal everywhere. Coherence is the global same-branch statement: all identity or all reciprocal. The module doc frames this as the exact coherence needed to rule out mixed product factors in native-cost uniqueness.
proof idea
Tactic proof by cases on whether there exists a nonunit $p$ with identity orientation under $\chi$.
If such a $p_0$ exists, branch agreement applied to $p_0$ and an arbitrary nonunit $q$ yields the identity-to-identity transport, so the left disjunct of coherence holds for every nonunit.
If no nonunit is identity-oriented, take an arbitrary nonunit $q$. Local orientation gives identity or reciprocal at $q$; the identity arm contradicts the case hypothesis, so $q$ is reciprocal. Thus the right disjunct of coherence holds.
No external lemmas beyond the three named predicates and the identity-orientation atom; pure case analysis and elimination.
why it matters
Coherence is the exact global statement strong enough to rule out mixed product factors in the native-cost uniqueness argument. Downstream it is the forward direction of the local-orientation equivalence between branch agreement and coherence, and it discharges the coherent-target half of the prime-calibration forcing lemma: once prime calibration forces local branch agreement, this theorem upgrades to full nonunit coherence.
It also appears in the native-cost uniqueness blocker certificate assembly, which packages the zero-calibrated factorization and signed-admissible refutation steps. In the broader Recognition forcing chain this sits under T5 J-uniqueness infrastructure: characters on ratio-orbits must not mix identity and reciprocal branches if the native cost is to match the unique $J$-cost fixed by the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.