PRCCharacterNonunitIdentityWitnessGlobalizes_of_coherent
plain-language theorem explainer
Coherence of nonunit orbit orientation under a ratio-orbit character forces identity-witness globalization: one identity-oriented nonunit direction, if it exists, fixes the identity branch on every nonunit direction. Native-cost uniqueness and prime-calibration arguments in PRC cite this bridge. The proof is a two-step term composition through the branch-transport intermediate.
Claim. Let $\chi$ be a map on rational orbits. If nonunit orbit orientation under $\chi$ is coherent (every nonunit direction is identity-oriented, or every nonunit direction is reciprocal-oriented), then the identity-witness globalization property holds for $\chi$: the existence of one identity-oriented nonunit direction implies that every nonunit direction is identity-oriented.
background
In the Primitive Recognition Calculus native-cost uniqueness development, characters act on rational orbits (integer numerator over a nonzero orbit denominator). Each nonunit orbit direction is oriented either as identity or as reciprocal under $\chi$.
Nonunit orbit orientation is coherent when the choice is uniform: all nonunit directions are identity-oriented, or all are reciprocal-oriented. The doc-comment states this is "the exact coherence statement strong enough to rule out mixed product factors."
Identity-witness globalization is the one-sided consequence: if any single nonunit direction is identity-oriented, then every nonunit direction is. Upstream, coherence already yields full identity branch transport (any identity nonunit direction forces identity at every other nonunit direction); the witness form is the existential packaging of that transport.
proof idea
One-line term composition. First apply the upstream lemma that coherence implies identity branch transport (case-split on the two disjuncts of coherence: all-identity or all-reciprocal). Then apply the packaging lemma that turns branch transport into the witness-globalization implication by unpacking the existential witness and feeding it to transport. No extra arithmetic or case analysis appears at this layer.
why it matters
This is a small but load-bearing bridge in the PRC native-cost uniqueness stack. Downstream, prime calibration that forces nonunit orientation coherence immediately upgrades to the witness-globalization target by applying this theorem. The same property is wired into the native-cost uniqueness blocker certificate, which packages zero-calibrated factorization and signed-admissible refutation results.
In the broader Recognition Science forcing picture, native-cost uniqueness is the PRC-side route toward the unique J-cost (T5: $J(x)=(x+x^{-1})/2-1$), so ruling out mixed nonunit branch choices is part of locking the character to the admissible cost. The declaration itself is fully proved; it closes no open scaffold, but it is the coherence-to-witness step those larger certificates invoke.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.