mul_def
plain-language theorem explainer
mul_def establishes that the multiplication operator on logic-forced natural numbers coincides exactly with the recursively defined mul function. Analysts building Navier-Stokes estimates from logic-derived arithmetic cite it to justify notation in integral identities. The proof is a one-line reflexivity step that follows from the Mul typeclass instance.
Claim. For elements $n, m$ of the natural numbers constructed from the Law of Logic, the product $n · m$ equals the recursively defined multiplication function applied to $n$ and $m$.
background
The module constructs natural-number arithmetic directly from the functional equation of logic. LogicNat is the inductive type with identity constructor (zero-cost multiplicative identity) and step constructor (one iteration of the generator), forming the orbit closed under multiplication by γ and containing 1. The mul function is defined by recursion on the second argument: mul n identity equals zero and mul n (step m) equals mul n m plus n; the * notation is bound to this mul via the Mul instance.
proof idea
The proof is a one-line wrapper that applies reflexivity. It holds because the Mul instance for LogicNat is defined to be exactly the mul function.
why it matters
This equality is a prerequisite for using standard multiplication notation in downstream Navier-Stokes results, including integrability of boundary terms for radial profiles and Sobolev decay estimates on the half-line. It completes the arithmetic layer in the foundation module before lifting to integers and rationals, supporting the derivation of physical quantities from the J-uniqueness and phi-ladder in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.