mul_one_eq
plain-language theorem explainer
Right-multiplication by the unit orbit leaves any finite distinction orbit unchanged. Orbit-arithmetic and divisibility arguments cite this as the right unit law on DistinctionNat. The proof unfolds the unit as successor of zero, then reduces by the successor-multiplication, zero-multiplication, and left-zero-addition identities.
Claim. For every finite distinction orbit $a$, $a \cdot 1 = a$, where $1$ denotes the successor of the zero orbit.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive type with constructors zero and succ, playing the role of the natural numbers inside the Primitive Recognition Calculus (K2.12).
Orbit arithmetic equips this type with addition and multiplication defined by the usual recursive clauses. In particular, multiplication by a successor expands as $a \cdot (\mathrm{succ}, b) = a \cdot b + a$, multiplication by zero is zero, and zero is a left identity for addition. The unit orbit is the successor of zero.
This module develops divisibility on those orbits; the right unit law is the first multiplicative identity needed before reflexivity of divides and the left unit law.
proof idea
Unfold the definition of the unit (successor of zero). Rewrite once with the successor-multiplication identity, obtaining $a \cdot 0 + a$. Rewrite with zero-multiplication to replace $a \cdot 0$ by zero, then with left-zero addition to collapse $0 + a$ to $a$. All three rewrites are definitional or already-proved equalities from OrbitArithmetic; no induction is required here.
why it matters
Supplies the witness that every orbit divides itself: divides_refl packages the unit together with this identity. It is also the rewrite target for the left unit law one_mul_eq (via commutativity) and appears in the factorization analysis behind unit_or_eq_of_divides_prime, which classifies divisors of prime orbits.
Inside the Recognition foundation this is elementary scaffolding for orbit divisibility, not a forcing-chain step (T0–T8). It keeps the multiplicative monoid of distinction orbits well-behaved so later prime-orbit and factorization lemmas can speak in ordinary number-theoretic language without leaving the base-neutral setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.