PRCCharacterNonunitOrbitOrientationCoherent
plain-language theorem explainer
Nonunit orbit orientation coherence for a ratio-orbit character means every nonunit orbit direction picks one common branch: all identity, or all reciprocal. Native-cost uniqueness arguments cite it to bar mixed product factors across nonunit directions. The body is a pure Prop disjunction of two universal branch predicates; there is no proof content.
Claim. For a map $\chi$ on rational orbits, nonunit orbit orientation is coherent when either (i) every nonzero nonunit distinction $p$ satisfies the identity-branch direction condition for $\chi$ at $p$, or (ii) every such $p$ satisfies the reciprocal-branch direction condition for $\chi$ at $p$.
background
In the primitive recognition calculus, a rational orbit is an integer numerator over a nonzero distinction denominator (the K4.7 display). Distinctions themselves are the base-neutral finite orbit of repeated distinction (K2.12). A character $\chi$ acts on these rational orbits.
Each nonunit orbit direction can orient either toward the identity branch (the canonical zero-cost event at ratio $1$) or toward the reciprocal branch (the automorphism that swaps source and target and inverts the ratio). Local orientation only says some branch is chosen at each direction; it does not force the choices to agree.
This module builds native-cost uniqueness for PRC characters. Coherence is the global same-branch constraint on all nonunit directions, separated from local existence and from the unit case. The doc-comment states it is exactly the coherence strong enough to rule out mixed product factors.
proof idea
Definitional Prop, not a proved theorem. The body is the disjunction of two universal quantifications over nonzero nonunit distinctions: either the identity-direction predicate holds at every such $p$, or the reciprocal-direction predicate holds at every such $p$. No tactics, no lemmas applied.
why it matters
This is the branch-coupling hypothesis that turns local nonunit orientation into global nonunit structure for native cost uniqueness. Downstream, coherence immediately yields no mixed nonunit orientations, nonunit branch agreement, identity and reciprocal branch transport, transport pairs, and globalization of an identity witness. Under a local-orientation hypothesis it is equivalent to branch agreement.
In the Recognition framework this sits inside the foundation forcing that pins the native cost to the unique J-shape (T5: $J(x)=(x+x^{-1})/2-1$). Ruling out mixed nonunit factors keeps product structure compatible with a single global branch, which is required before doubled-trace and d'Alembert hypotheses can identify the character cost with $J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.