mul_succ_eq
plain-language theorem explainer
On distinction orbits, multiplying by a successor expands as the product plus the multiplicand: a·S(b) = a·b + a. Anyone assembling Peano-style ring laws for DistinctionNat cites this identity. The equality is definitional, discharged by reflexivity from the recursive clause of multiplication.
Claim. For distinction naturals $a$ and $b$, writing $S$ for successor, $a \cdot S(b) = a \cdot b + a$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive type with constructors zero and succ, introduced as K2.12 in the primitive recognition calculus. It is the carrier on which orbit arithmetic is built, parallel to LogicNat but tied to recognition orbits rather than pure logic steps.
Successor on this type is one more application of the generator (the same pattern as ArithmeticFromLogic, where succ n := step n and Peano axioms are theorems of the inductive structure, not postulates). Addition and multiplication are defined by recursion on the second argument in the usual way, so the successor clause of multiplication is part of the definition rather than a derived lemma.
This module develops the elementary arithmetic identities (add_zero, add_succ, mul_zero, mul_succ, commutativity, etc.) needed before divisibility and further orbit structure.
proof idea
One-line definitional proof: rfl. The recursive clause of multiplication on DistinctionNat is exactly the stated identity, so both sides are definitionally equal and no rewriting or induction is required.
why it matters
This is the successor clause that unlocks the rest of multiplicative arithmetic on distinction orbits. Downstream, mul_comm inducts on the first factor and rewrites through this identity in the succ case; mul_one_eq unfolds one as succ zero and chains mul_succ_eq with mul_zero_eq and zero_add_eq to recover a · 1 = a.
In the Recognition framework this sits in the foundation layer that turns repeated distinction into a Peano-like calculus before forcing-chain landmarks (T5–T8) and physical constants are attached. It does not itself force phi or dimension; it supplies the arithmetic substrate those later steps assume when counting ticks, rungs, and orbit periods.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.