mul_def
plain-language theorem explainer
On distinction naturals, the infix product equals the named recursive multiplication. Orbit-arithmetic and ArithmeticFromLogic developments cite it to unfold notation. The proof is pure reflexivity: the instance of `*` is definitionally that function.
Claim. For any distinction naturals $a$ and $b$ (finite orbits of repeated distinction), the product $a \cdot b$ equals the recursively defined multiplication $\mathrm{mul}(a,b)$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive type with zero and successor, the primitive counting object in the recognition calculus (K2.12). OrbitArithmetic equips that type with the usual Peano-style operations so later layers can treat recognition counts as ordinary natural numbers.
Multiplication is introduced as a named recursive function mul and then exposed via the standard * notation. The parallel fact on LogicNat in ArithmeticFromLogic has the same shape: notation is definitionally the recursive multiplier. Sibling lemmas in this module do the same for addition (add_def) and then prove the ring-like identities (commutativity, associativity, cancellation) once the notation is pinned down.
proof idea
One-line reflexivity. The Mul instance on DistinctionNat is defined so that a * b reduces definitionally to mul a b; rfl closes the goal with no further lemmas.
why it matters
Notation hygiene for the arithmetic built on recognition orbits. Downstream, ArithmeticFromLogic’s own mul_def (and any simp-driven arithmetic on LogicNat or DistinctionNat) relies on this kind of unfolding so that recursive definitions, not overloaded symbols, are what proofs manipulate.
In the Recognition Science stack this sits under the foundation layer that derives counting and arithmetic from distinction before the forcing chain (T0–T8) and the Recognition Composition Law. It does not itself force phi, the eight-tick octave, or dimension; it only makes the orbit-level product usable as ordinary multiplication in later constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.