mul_zero
plain-language theorem explainer
Multiplication of any LogicNat element by the zero element returns zero. This identity is cited in derivations of minimum energy in quasicrystals, flatness minimization in cosmology, and inertia laws in mechanics. The proof reduces to a single reflexivity step that holds by the definition of multiplication on the LogicNat inductive type.
Claim. For every element $n$ of LogicNat, $n$ times the identity element equals the identity element.
background
LogicNat is the inductive type with constructors identity (the zero-cost element, multiplicative identity in the recognition orbit) and step (one iteration of the generator). Its doc-comment states that the structure mirrors the orbit {1, γ, γ², ...} as the smallest subset of positive reals closed under multiplication by γ and containing 1. The mul_zero theorem sits in the arithmetic layer of ArithmeticFromLogic, which builds natural-number operations directly from the Law of Logic without external axioms. It depends only on the upstream LogicNat inductive definition.
proof idea
The proof is a one-line wrapper that applies reflexivity (rfl). This succeeds immediately because the multiplication operation on LogicNat is defined such that any element multiplied by the identity constructor yields the identity.
why it matters
This identity supports over forty downstream results, including min_energy_zero (tiling_energy equals zero via simp with mul_zero), flat_minimizes_cost (curvatureCost simplification), and newton_first_law (inertia reduction). It closes a foundational step from the functional equation to concrete arithmetic, enabling the phi-ring structure, J-cost evaluations, and higher derivations such as G = phi^5 / pi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.