PRCCharacterNonunitIdentityBranchTransport_of_coherent
plain-language theorem explainer
Coherent nonunit orbit orientation (every nonunit direction is either all-identity or all-reciprocal) implies identity branch transport: a single identity-oriented nonunit forces every nonunit to be identity-oriented. Cited when globalizing local character orientation under PRC native-cost uniqueness. Proof is a two-branch case split: the all-identity arm is immediate; the all-reciprocal arm collides identity with reciprocal at one point and dies by the nonunit direction-not-reciprocal lemma.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose nonunit orbit orientation under $\chi$ is coherent: either every nonunit direction is identity-oriented, or every nonunit direction is reciprocal-oriented. Then identity branch transport holds: if some nonunit $p$ is identity-oriented, every nonunit $r$ is identity-oriented.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays built from signed numerator orbits over nonzero distinction denominators. Cross-equivalence crossEq is the internal PRC rational equality (balanced scaled numerators). Reciprocal is the total reciprocal on ratio orbits. Each nonzero distinction position $p$ has an associated ratio direction orbitDirection p (numerator the signed orbit of $p$, denominator one).
A character $\chi$ orients each such direction as identity or reciprocal. Coherence of nonunit orientation means the choice is global on nonunits: all identity, or all reciprocal. That rules out mixed product factors. Identity branch transport is the one-way coupling: one identity-oriented nonunit forces every nonunit to be identity-oriented.
The module develops native-cost uniqueness for PRC characters. Upstream, crossEq is symmetric and transitive (choice-free via the integer bridge), and a dedicated lemma says a nonunit orbit direction is never cross-equivalent to its own reciprocal.
proof idea
Introduce a nonunit $p$ that is identity-oriented and an arbitrary nonunit $r$. Case-split the coherence hypothesis.
All-identity arm: apply the universal identity orientation directly at $r$.
All-reciprocal arm: coherence gives reciprocal orientation at $p$. Symmetry of crossEq turns the identity witness at $p$ around; transitivity with the reciprocal witness yields crossEq between orbitDirection p and its reciprocal. That contradicts orbitDirection_nonunit_not_crossEq_recip. Eliminate the falsehood.
No further character algebra is needed; the transport is pure orientation bookkeeping plus the nonunit self-reciprocal ban.
why it matters
This is the identity half of nonunit branch-coupling under coherence. Downstream it pairs with the reciprocal twin to give full branch-transport pairs, and it feeds witness globalization: one local identity orientation spreads to all nonunits once coherence is known.
Prime-calibration targets also route through it: if prime calibration forces coherent nonunit orientation, this theorem upgrades that to forced identity branch transport. The uniqueness blocker certificate sits further downstream in the same native-cost uniqueness stack.
In the Recognition forcing picture this is bookkeeping inside the J-cost uniqueness lane (T5 / RCL), not a new physical constant. It closes a coherence-to-transport gap so character factorization cannot mix identity and reciprocal factors on nonunit orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.