PRCCharacterNonunitOrbitLocalOrientation_of_prime_and_product_local
plain-language theorem explainer
If a ratio-orbit character is identity-or-reciprocal on every prime axis and that local choice propagates under products of nonunit factors, then every nonunit orbit direction is locally oriented the same way. Native-cost uniqueness arguments cite this to lift prime-axis calibration to all composite directions. The proof is strong induction on the underlying natural size, splitting prime versus nontrivial-factor cases.
Claim. Let $\chi$ act on ratio orbits. Assume every prime orbit direction is sent by $\chi$ either to itself or to its reciprocal, and assume that whenever two nonunit nonzero factors are each identity-or-reciprocal oriented, their product is as well. Then for every nonunit nonzero orbit direction $p$, $\chi$ sends $p$ either to itself or to its reciprocal.
background
In the Primitive Recognition Calculus, a character $\chi$ on ratio orbits records how cost-matching chooses the identity versus reciprocal orientation on each direction. Local prime orientation means each prime axis is sent to itself or its reciprocal; the module doc ties that alternative to equality of $J$-costs on a single prime direction.
The conclusion is the nonprime analogue: every nonunit orbit direction (composite as well as prime) is identity-or-reciprocal oriented. Product-factor propagation is the multiplicative step: if two nonunit factors are locally oriented, so is their product. That is exactly what is needed to pass from prime axes to composite directions.
Sizes are read via the LogicNat/DistinctionNat embedding into ordinary $\mathbb{N}$, with multiplication recovered under toNat, so strong induction on natural size is legitimate. Reciprocal is the orbit-level inversion paired with the identity alternative.
proof idea
Package the goal as a predicate $P(n)$: every nonunit nonzero DistinctionNat of size $n$ is identity-or-reciprocal oriented under $\chi$. Prove $P$ by strong induction on $n$.
For $q$ of size $n$, if $q$ is prime-orbit, apply the prime-local hypothesis. Otherwise obtain a nontrivial factorization $a\cdot b=q$ with both factors nonunit and nonzero. Multiplication recovery under toNat plus $a,b>1$ yields $|a|<n$ and $|b|<n$, so the inductive hypothesis orients $a$ and $b$. Product-propagation then orients $q$.
Instantiate at $n=|p|$ and apply to the given nonunit $p$.
why it matters
This is the bridge from prime-axis calibration to full nonunit local orientation inside the native-cost uniqueness development. Three downstream target-closure theorems apply it once prime local orientation is forced and product propagation (or a hypothesis that yields it) is available: the identity-comparable-trace route, the product-local-orientation route, and the product-no-mixed coherent-orientation route.
Those feed the native-cost uniqueness blocker certificate, which packages zero-calibrated factorization targets for the uniqueness program. In the Recognition Science forcing chain this supports T5-style $J$-uniqueness: characters that match the native cost cannot choose inconsistent local orientations across the multiplicative monoid of orbit directions. The adjacent no-mixed law (prime-floor version) is the coherence companion once local alternatives are secured everywhere.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.