PRCCharacterNonunitOrbitAllIdentity_of_all_prime_identity
plain-language theorem explainer
If a ratio-orbit character fixes every prime direction under cross-equivalence and respects native product display, then it fixes every nonzero non-unit orbit direction. Used to globalize prime-local orientation when proving native cost uniqueness for PRC characters. Proof is strong induction on natural size: primes are given, composites factor and reassemble by product-identity transport.
Claim. Let $\chi$ be a ratio-orbit character (unit-fixing, multiplicative, and reciprocal under cross-equivalence) that is compatible with the native display of orbit products. If $\mathrm{crossEq}(\chi(d_p), d_p)$ holds for every prime orbit direction $d_p$, then $\mathrm{crossEq}(\chi(d_q), d_q)$ holds for the orbit direction $d_q$ of every nonzero non-unit distinction number $q$.
background
In the Primitive Recognition Calculus, costs factor through ratio-orbit characters. A ratio character $\chi$ is a map on ratio orbits that fixes the unit orbit, is multiplicative, and sends reciprocals to reciprocals, all up to cross-equivalence (the internal PRC rational relation: two orbits match when cross-scaled numerators and denominators balance as signed orbits).
Identity orientation on an orbit direction means $\chi$ returns that same direction under cross-equivalence. The prime case is the local input; the present result lifts it to every composite non-unit axis. Product-display compatibility is the extra quotient-respect hypothesis: the character on a product orbit agrees with the character on the ratio product of the factor orbits, which bare multiplicativity does not automatically give at the display level.
Distinction numbers carry a toNat size recovered from the logic-arithmetic embedding, with multiplication agreeing with ordinary Nat multiplication. Non-prime non-units admit a nontrivial factorization into smaller nonzero non-units, which supplies the inductive step.
proof idea
Define a predicate $P(n)$: every distinction number of size $n$ that is nonzero and non-unit has identity orientation under $\chi$. Prove $P$ by strong induction on $n$.
For $q$ of size $n$, case-split on primality. If $q$ is prime, apply the given prime-identity hypothesis directly. If not, obtain a nontrivial factorization $a\cdot b=q$ with both factors nonzero non-units. Size multiplicativity gives $a.{\rm toNat}\cdot b.{\rm toNat}=n$; since each factor has size $>1$, both sizes are strictly less than $n$. Invoke the inductive hypothesis on $a$ and $b$, then reassemble with the product-identity lemma for characters (using character axioms and product-display compatibility) to conclude identity on $q$.
Instantiate at $n=p.{\rm toNat}$ to finish.
why it matters
Native cost uniqueness for PRC characters needs identity orientation not only on primes but on all composite non-unit axes, so that trace transport and mixed reciprocal witnesses can move freely through the orbit lattice. This theorem is the pure globalization step from prime-local identity to full non-unit identity under product-display compatibility.
Downstream it feeds mixed non-unit reciprocal witness reflection, non-unit identity respect for comparable traces, positive-orbit identity from all-prime identity, and globalization of prime-identity witnesses in the absence of mixed prime witnesses. It also appears in the native-cost-uniqueness blocker certificate assembly. In the broader Recognition chain this sits inside the foundation layer that forces the unique J-cost (T5) and the d'Alembert factorization used for native cost uniqueness, before constants and the mass ladder are read off.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.