mul_one
plain-language theorem explainer
Multiplication by the successor of zero returns the original element unchanged in the logic-forced naturals. Algebraists deriving ring structures and cost functions from a single functional equation cite this when building multiplicative identities. The proof is a one-line rewrite chain that applies the successor multiplication rule, the zero multiplication rule, and the zero addition identity.
Claim. For every element $n$ of the logic-forced natural numbers, $n$ multiplied by the successor of the identity element equals $n$.
background
LogicNat is the inductive type with constructors identity (the zero-cost element, serving as multiplicative identity in the orbit) and step (one iteration of the generator). This structure encodes the smallest subset of positive reals closed under multiplication by the generator and containing the identity, as forced by the Law of Logic. The theorem lives in the module that derives Peano-style arithmetic directly from that functional equation rather than positing axioms separately.
proof idea
One-line wrapper that applies the successor multiplication rule (n times successor of m equals n times m plus n), substitutes the zero case to obtain n times zero plus n, invokes the zero multiplication rule, and finishes with the zero addition identity.
why it matters
This identity supplies the multiplicative unit needed for downstream results in cost algebra and phi-ring constructions. It feeds theorems such as the exact level-set classification for the J function and the definition of canonical objects in the recognition category. Within the Recognition framework it closes a basic step in obtaining arithmetic from the single functional equation before moving to J-uniqueness and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.