one_mul_eq
plain-language theorem explainer
Left multiplication by the unit orbit leaves every finite distinction orbit unchanged: $1\cdot a=a$. Anyone building native divisibility or factorization on DistinctionNat cites this as the left-unit law. The proof is a one-line rewrite: commute past the already-proved right-unit identity.
Claim. For every finite distinction orbit $a$, left multiplication by the multiplicative unit satisfies $1 \cdot a = a$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, carrying the native arithmetic of the Primitive Recognition Calculus. Multiplication and the unit one live in the OrbitArithmetic / OrbitDivisibility layer; one is the successor of zero.
The sibling right-unit law already states $a\cdot 1=a$, proved by unfolding one and reducing via successor multiplication and zero laws. Commutativity of multiplication on DistinctionNat is available by induction on the left factor. Together those two facts give the left-unit law without a fresh inductive argument.
Local setting is the divisibility package on orbits: unit, divides, nontrivial factorization, and prime-orbit predicates all sit in the same module and expect both unit laws.
proof idea
One-line wrapper. Rewrite with multiplication commutativity on DistinctionNat, then apply the sibling right-unit theorem $a\cdot 1=a$. No induction and no unfolding of one at this site; both are already discharged upstream.
why it matters
Supplies the missing left-unit identity so that divides one a is immediate: the witness is $a$ itself via $1\cdot a=a$. That feeds the native divisibility layer used by nontrivial factorization of a proper nonunit divisor (the reusable endpoint for period-readout factoring once a gcd witness appears). It also appears in the prime-coordinate product append law, where empty-prefix products must act as a true unit.
Within Recognition Science this is pure foundation scaffolding under the Primitive Recognition Calculus, not a forcing-chain step (T5–T8). It keeps orbit arithmetic honest so later period and factorization theorems can quote unit laws without re-proving them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.