PRCCharacterNonunitOrbitLocalOrientation_of_coherent
plain-language theorem explainer
Global coherence of nonunit orbit orientation for a ratio-orbit character implies pointwise local orientation: each nonunit direction is identity or reciprocal. Native-cost uniqueness and prime-calibration transport cite this bridge. The proof is a one-line case split on the two global branches.
Claim. Let $\chi$ map ratio orbits to ratio orbits. If nonunit orbit orientation is coherent for $\chi$ (every nonunit direction is identity, or every nonunit direction is reciprocal), then $\chi$ is locally oriented on nonunit directions: for every nonunit nonzero distinction $p$, the orbit direction at $p$ is either identity or reciprocal.
background
In the Primitive Recognition Calculus, a ratio orbit is a signed-orbit numerator over a nonzero distinction denominator. Characters act on these orbits; orientation of a nonunit direction records whether $\chi$ acts as the identity branch or the reciprocal branch along that direction.
Local orientation asks only that each nonunit direction pick one of the two branches. Coherence is stronger: the same branch is chosen for every nonunit direction (all identity, or all reciprocal). The module develops native-cost uniqueness by forcing characters through prime calibration and ruling out mixed product factors; coherence is exactly the global alternative strong enough for that no-mixing step.
This lemma is the elementary implication from the coherent alternative to the local alternative, the nonprime analogue of the already-proved local-prime orientation dichotomy.
proof idea
Term-mode case analysis on the coherence hypothesis. Introduce a nonunit nonzero distinction $p$. Coherence is a disjunction of two universal statements (all identity vs all reciprocal). In the first arm apply the identity universal at $p$; in the second arm apply the reciprocal universal at $p$. Each arm yields one side of the local disjunction, so local orientation holds.
why it matters
Feeds the native-cost uniqueness blocker certificate and several prime-calibration forcing targets: nonunit local orientation, local branch agreement, local no-mixed, and prime-floor successor transport (both from nonunit coherence and from sharpened local-adjacent no-mix). Downstream wrappers apply this lemma once coherence is known, then continue to factorization and transport.
In the Recognition chain this sits inside PRC native-cost uniqueness, which pins the cost functional before J-uniqueness (T5) and the self-similar fixed point $\phi$ (T6). Coherence-to-local is the cheap logical step that lets global branch agreement propagate multiplicatively without mixed factors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.