PRCCharacterNonunitOrbitOrientationCoherent_of_local_identity_branch_transport
plain-language theorem explainer
Local identity-or-reciprocal orientation of every nonunit ratio-orbit direction, plus identity-branch transport (one identity forces all identity), yields global coherence: all nonunit directions share one branch. Cited in the native-cost uniqueness blocker certificate. Proof is a two-lemma term composition: transport implies no-mixing, then local-plus-no-mix gives coherence.
Claim. Let $\chi$ map ratio orbits to ratio orbits. If every nonunit orbit direction is locally either identity-oriented or reciprocal-oriented, and if identity orientation at any one nonunit direction forces identity orientation at every nonunit direction, then nonunit orbit orientation is coherent: either every nonunit direction is identity-oriented, or every nonunit direction is reciprocal-oriented.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator (K4.7). Characters $\chi$ act on these orbits; each nonunit direction can be identity-oriented or reciprocal-oriented.
Local orientation says every nonunit direction picks one of those two branches (the nonprime analogue of the already-proved local-prime alternative). Identity branch transport is the one-way coupling: if any nonunit direction is identity-oriented, all are. Coherence is the global dichotomy: all identity or all reciprocal, strong enough to rule out mixed product factors.
The module builds native-cost uniqueness for PRC characters. Upstream, no-mixing is already derived from identity branch transport, and coherence is already derived from local orientation plus no-mixing.
proof idea
Term-mode one-liner. First apply the upstream lemma that identity branch transport implies no mixed nonunit orientations (if one direction is identity and another reciprocal, transport would force the second to be identity, contradiction). Feed that no-mixing witness, together with the local-orientation hypothesis, into the already-proved lemma that local orientation plus no-mixing yields global coherence. No further case analysis is done here.
why it matters
Coherence of nonunit orbit orientation is a gate on the path to unique native cost for PRC characters. Mixed identity/reciprocal factors would spoil the doubled-trace d'Alembert structure that pins the cost to the J-functional of the forcing chain (T5: $J(x)=(x+x^{-1})/2-1$).
Downstream, the native-cost uniqueness blocker certificate packages proved factorization targets and refutations; this lemma supplies the orientation-coherence step those certificates rely on when assembling the uniqueness obstruction. It closes the gap between the transport form of branch coupling and the coherence form needed for product-factor arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.