PRCCharacterNonunitOrbitLocalOrientation
plain-language theorem explainer
Packages the local-orientation alternative for nonunit ratio orbits under a character χ: each nonzero nonunit distinction is either identity-oriented or reciprocal-oriented. Downstream native-cost uniqueness lemmas cite it as the nonprime analogue of already-proved prime local orientation. It is a Prop definition, not a proved assertion.
Claim. A map $\chi$ on ratio orbits is said to have nonunit local orientation when, for every nonzero nonunit distinction $p$, the orbit direction of $p$ under $\chi$ is either the identity orientation or the reciprocal orientation.
background
In the Primitive Recognition Calculus, cost uniqueness is reduced to properties of characters $\chi$ acting on ratio orbits. Two canonical orientations appear from the cost algebra: the identity direction (fixed by the identity $J$-automorphism / identity recognition event at ratio $1$) and the reciprocal direction (the reciprocal $J$-automorphism, swapping source and target with inverse ratio).
A distinction $p$ is nonunit when it is not the multiplicative unit in the distinction naturals. Local orientation at $p$ means the character sends the orbit of $p$ along exactly one of those two branches. The prime case is already settled separately; this definition is the nonprime (composite) analogue stated pointwise for every nonunit $p\neq 0$.
The surrounding module builds native cost from doubled-trace / d'Alembert data and matches it to $J$-cost. Multiplicativity of $J$-automorphisms and the reciprocal automorphism supply the algebraic skeleton for identity-versus-reciprocal branching.
proof idea
Definition only: the body is the universal Prop $\forall p\neq 0,; \neg\mathrm{unit}(p)\Rightarrow$ (identity orbit direction $\lor$ reciprocal orbit direction). No tactics or lemmas are applied at the declaration site. Downstream constructors discharge it from prime local orientation plus product-factor propagation, or from global coherence by case split on the all-identity / all-reciprocal disjunction.
why it matters
This is the hinge hypothesis that lets the uniqueness chain pass from primes to all nonunit orbits. Downstream it appears in: the iff between nonunit branch agreement and orientation coherence under local orientation; identity-branch transport from local orientation plus no-mixed-orientation; globalization of an identity witness once reciprocal is excluded; and the lift of prime local orientation through product-local propagation to full nonunit local orientation.
In framework terms it supports the T5 $J$-uniqueness route inside PRC: characters must sit on the identity/reciprocal pair that preserves the Recognition Composition Law structure, so native cost collapses to the unique $J$-cost. Without packaging the nonunit alternative, composite orbit directions would remain an open gap between prime-axis control and global branch agreement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.