one_mul
plain-language theorem explainer
The theorem establishes that multiplication by the multiplicative identity leaves every element of the logic-generated naturals unchanged. Researchers building the ring structure on the phi-ladder from the Recognition functional equation cite this when verifying unit properties before constructing cost algebras. The proof proceeds by induction on the two constructors of LogicNat, reducing the successor case with the recursive rules for multiplication and addition.
Claim. Let $N_L$ be the inductive type generated by the constructors identity and step. Then for every $n$ in $N_L$, the product of the successor of zero with $n$ equals $n$.
background
LogicNat is the inductive type forced by the Law of Logic, where the identity constructor represents the zero-cost element (the multiplicative identity in the orbit) and the step constructor represents one further iteration of the generator, mirroring the orbit {1, γ, γ², ...} as the smallest subset of positive reals closed under multiplication by γ and containing 1. The module ArithmeticFromLogic derives the usual arithmetic operations as theorems from this structure rather than positing them as axioms. Upstream results supply the recursive definitions: addition satisfies n + succ m = succ (n + m) and n + zero = n, while multiplication satisfies n * succ m = n * m + n; these are applied directly in the inductive step.
proof idea
The proof uses induction on the LogicNat structure. The identity case holds immediately by reflexivity. In the step case, the mul_succ rule rewrites the product into a sum, the induction hypothesis replaces the first summand, and the add_succ and add_zero rules then recover the successor on the right-hand side.
why it matters
This supplies the left-unit property for multiplication on the logic naturals and is invoked in downstream results such as the level-set classification J_eq_iff_eq_or_inv in CostAlgebra and the canonical PhiRing object construction. It forms a basic link in the forcing chain from the functional equation through arithmetic to the phi-ladder and RecognitionCategory structures. No open scaffolding questions are addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.