mul_add
plain-language theorem explainer
The mul_add theorem asserts distributivity of multiplication over addition for elements of LogicNat. Researchers deriving cost algebras or growth ODEs from the Law of Logic would cite it when rearranging sums inside phi-ladder expressions. The proof proceeds by induction on the third argument, reducing the successor case via add_succ, mul_succ, the inductive hypothesis, and add_assoc while the base case collapses with add_zero and mul_zero.
Claim. For all $a, b, c$ in LogicNat, $a · (b + c) = (a · b) + (a · c)$.
background
LogicNat is the inductive type whose constructors identity and step mirror the orbit {1, γ, γ², …} closed under multiplication by the generator γ; identity plays the role of zero and step the role of successor. The module ArithmeticFromLogic recovers the standard arithmetic operations on this type directly from the functional equation without external Peano axioms. The proof depends on the already-established lemmas add_zero (n + zero = n), add_succ (n + succ m = succ (n + m)), add_assoc, and the matching multiplication rules mul_zero and mul_succ.
proof idea
The proof is by induction on c. The identity case rewrites the left side with add_zero, applies mul_zero, then closes with add_zero. The step case rewrites both sides with add_succ and mul_succ, invokes the inductive hypothesis on the resulting expression, and finishes with add_assoc.
why it matters
This lemma supplies the distributive law required for the arithmetic recovery that identifies LogicNat with the ordinary naturals. It is invoked by downstream results including windowSums_shift_equivariant in CostAlgebra, AApply_add in the Ndim projector, add_mem_Radical in RadicalDistribution, and growth_satisfies_ode in the ILG growth model. Within the Recognition framework it completes the passage from the Law of Logic through the eight-tick octave to the phi-ladder mass formula and the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.