succ_mul_eq
plain-language theorem explainer
Left-successor distributes through multiplication on finite distinction orbits: the product of the successor of a with b equals a times b plus b. Anyone assembling Peano-style arithmetic on DistinctionNat cites this when proving commutativity or the usual recursive laws. The argument is induction on b, closing the zero case by the zero-product and zero-sum identities and the successor case by the inductive hypothesis plus addition associativity and commutativity.
Claim. For all finite distinction orbits $a,b$, $(\mathrm{succ}\,a)\cdot b = a\cdot b + b$.
background
DistinctionNat is the inductive type of base-neutral finite orbits of repeated distinction: constructors zero and succ, the recognition-calculus stand-in for the natural numbers. OrbitArithmetic equips that type with addition and multiplication defined by the usual recursive clauses on the second argument (and the corresponding left-zero and left-successor lemmas already proved in the same module).
Successor itself is one more application of the generator, matching the ArithmeticFromLogic construction where Peano axioms are theorems of the inductive structure rather than postulates. The local setting is therefore pure orbit arithmetic: no integers, no rationals, only the finite distinction ladder and the add/mul operations derived from it.
Upstream, the proof relies on the module's own add_assoc and add_comm (and the parallel LogicNat/PRCInt versions that justify the same algebraic moves), together with the already-established mul_zero_eq, add_zero_eq, and add_succ_eq identities.
proof idea
Induction on the second factor b.
Zero case: both sides reduce by mul_zero_eq; the right-hand side then collapses by add_zero_eq.
Successor case: unfold the recursive clause for multiplication so the goal becomes succ a * n + succ a = (a * n + a) + succ n. Rewrite by the inductive hypothesis and by add_succ_eq on both sides, then use congr 1 and finish by two applications of add_assoc plus add_comm on a and n to realign the summands.
why it matters
This is a standard Peano multiplication lemma, needed so that multiplication on distinction orbits behaves like ordinary natural-number arithmetic. The sole recorded consumer is mul_comm in the same module, whose successor case applies the identity to swap factors after the inductive hypothesis.
In the Recognition Science stack the lemma sits in the Primitive Recognition Calculus foundation: arithmetic is recovered from repeated distinction before any continuum, cost functional, or physical constant appears. It does not itself touch the forcing chain (T5–T8), the Recognition Composition Law, or the phi-ladder mass formula; it only guarantees that the discrete counting layer those later constructions rest on is algebraically coherent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.