PRCCharacterNonunitIdentityBranchTransport
plain-language theorem explainer
Identity branch transport for nonunit orbit directions: if a ratio-orbit character orients one nonunit direction as the identity branch, it orients every nonunit direction that way. Cited when deriving global no-mixing or branch agreement from a single local identity witness. Propositional definition packaging the universal transport quantifiers; no proof content.
Claim. For a map $\chi$ on rational orbits, whenever a nonzero nonunit distinction orbit $p$ is identity-oriented under $\chi$ (cross-equality of $\chi$ on the orbit direction of $p$ with that direction itself), every nonzero nonunit distinction orbit $r$ is likewise identity-oriented under $\chi$.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction. Its native multiplicative unit is the one-step orbit; nonunits are all other nonzero positions. A RatioOrbit packages a signed numerator over a nonzero distinction denominator.
A character $\chi$ acts on ratio orbits. Identity orientation of a nonzero orbit direction $p$ means $\chi$ fixes that direction up to the native cross-equality on ratio orbits (the direction is sent to itself, not to its reciprocal). The companion reciprocal orientation is defined symmetrically.
The surrounding module develops native cost uniqueness for such characters: doubled-trace d'Alembert structure, cost-from-character reconstructions, and coherence of branch choices across nonunit axes. The identity event of observer forcing sits at the J-cost minimum $x=1$ and supplies the semantic meaning of the identity branch.
proof idea
Propositional definition, not a proved theorem. The body is the raw quantified statement: for every nonzero nonunit $p$, identity orientation of $p$ under $\chi$ implies identity orientation of every nonzero nonunit $r$. No tactics, no lemmas applied; downstream theorems discharge or consume this Prop.
why it matters
Packages the missing transport direction of nonunit branch coherence: one identity-oriented nonunit witness globalizes the identity branch. Downstream, it is half of the split transport pair (identity plus reciprocal), and it converts directly into no-mixed nonunit orientation and into nonunit branch agreement once local orientation is known.
Several closure theorems produce it from stronger hypotheses: full orientation coherence, comparable-trace respect, branch agreement, local no-mixing plus globalization, and witness globalization. In the Recognition forcing chain this sits under native cost uniqueness for characters, the layer that pins the J-cost shape before T5 J-uniqueness and the RCL are invoked at continuum scale. It does not itself force $\phi$ or $D=3$; it only locks branch choice on the discrete orbit skeleton.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.