mul
plain-language theorem explainer
Defines multiplication on DistinctionNat by nested addition: a·0 = 0 and a·(b+1) = a·b + a. Equips the orbit type with a Mul instance so orbit positions can be scaled by repeated distinction. Anyone building Peano-style arithmetic on recognition orbits cites this. The body is the standard recursive clause on the successor, reusing the already-defined addition.
Claim. Multiplication on the base-neutral finite orbit type is the binary operation given by $a \cdot 0 = 0$ and $a \cdot S(b) = a \cdot b + a$, where $S$ is the successor (one more application of the distinction generator) and $+$ is the previously defined orbit addition. This makes the orbit type a multiplicative monoid candidate under nested repetition of positions.
background
DistinctionNat is the inductive type of finite orbits of repeated distinction: constructors zero and succ, with no preferred base. It is the K2.12 carrier for orbit arithmetic in the Primitive Recognition Calculus. Successor means one more application of the generator, matching the LogicNat successor used elsewhere in the foundation stack.
This module builds Peano-style operations on those orbits. Addition is already defined by recursion on the second argument (siblings: add, add_zero_eq, add_succ_eq, add_comm, add_assoc). Multiplication is the next layer: nested repetition of addition, labeled K4.7 in the local numbering.
The setting is foundation-level arithmetic extracted from recognition structure rather than postulated Peano axioms. Operations are definitions on the inductive orbit, so later lemmas can prove the usual ring/semiring identities as theorems.
proof idea
Pure definition by pattern match on the second argument. The zero clause returns zero. The successor clause recurses as mul a b + a, using the already-defined addition on DistinctionNat. A one-line Mul instance packages the definition so the * notation is available. No lemmas are invoked; there is no proof body beyond the recursive equations.
why it matters
Completes the basic arithmetic toolkit on recognition orbits after addition: positions can be scaled by nested repetition. That is the natural multiplicative structure once orbits are treated as base-neutral natural numbers. Downstream work that needs products of orbit ranks, rung multiplications on the phi-ladder, or counting repeated distinction steps will depend on this operation and its forthcoming algebraic laws (commutativity, associativity, distributivity), even though no used_by edges are recorded yet.
In the broader Recognition Science stack, orbit arithmetic sits under the forcing chain and the recognition composition law: discrete counts of distinctions feed the eight-tick octave and ladder bookkeeping. K4.7 is the multiplication step of that bookkeeping, not a physical law by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.