PRCCharacterNonunitIdentityWitnessGlobalizes_of_local_excludes
plain-language theorem explainer
Local identity-or-reciprocal orientation plus one-sided exclusion of reciprocal witnesses already forces global identity-branch transport for nonunit ratio-orbit characters. Anyone proving native-cost uniqueness or prime-calibration branch locking cites this. The proof is a two-case split on the local alternative, with the reciprocal arm killed by the exclusion hypothesis.
Claim. Let $\chi$ be a map on rational ratio orbits. Suppose every nonunit orbit direction is locally oriented as either the identity branch or the reciprocal branch, and suppose that the existence of any nonunit identity witness excludes every nonunit reciprocal witness. Then a single nonunit identity witness globalizes: every nonunit orbit direction is identity-oriented.
background
In the Primitive Recognition Calculus, ratio orbits package a signed numerator over a nonzero distinction-natural denominator (K4.7). Characters $\chi$ act on these orbits; for nonunit directions one tracks whether $\chi$ follows the identity branch or the reciprocal branch.
Local orientation asserts that every nonunit direction is one or the other: identity or reciprocal. It is the nonprime analogue of the already-proved local-prime orientation alternative. The exclusion hypothesis is a one-sided branch-coupling statement: once any nonunit identity witness exists, no nonunit reciprocal witness can coexist with it (local orientation is not bundled into that Prop).
The target globalization Prop is the witness form of identity branch transport: one identity-oriented nonunit direction, if it exists, fixes the identity branch on every nonunit direction. This sits inside the native-cost uniqueness development that pins the PRC cost to the J-cost shape forced by the Recognition Composition Law.
proof idea
Term-mode case analysis. Introduce an identity witness and an arbitrary nonunit direction $r$. Apply local orientation at $r$ to obtain the disjunction identity-or-reciprocal. On the identity arm, return that orientation directly. On the reciprocal arm, feed the witness and the reciprocal orientation into the exclusion hypothesis to obtain False, then eliminate. No further lemmas are required beyond the two named hypotheses.
why it matters
Branch locking is the discrete step that turns local character orientation into a global identity (or reciprocal) choice, which is needed before the doubled-trace / d'Alembert route can force the native cost to match $J(x)=\cosh(\log x)-1$ (T5 J-uniqueness). Downstream, PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget_of_local_exclusion applies this lemma once prime calibration has produced the local-exclusion target, discharging the globalization target in one line. The result is pure logical glue inside PRC native-cost uniqueness: it packages local orientation with one-sided exclusion into the witness-globalization interface used by the prime-calibration forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.