toNat_mul
plain-language theorem explainer
The recovery map toNat from LogicNat to standard naturals preserves multiplication. Researchers building integer arithmetic or divisor-box identities from the logic-forced naturals cite this result. The proof is a direct induction on the second argument that reduces via the recursive clauses for multiplication and the already-established addition and successor recoveries.
Claim. Let $L$ be the inductive type with constructors identity and step. Let $toNat : L → ℕ$ be the canonical recovery map. Then for all $a,b ∈ L$, $toNat(a · b) = toNat(a) · toNat(b)$.
background
LogicNat is the inductive type forced by the Law of Logic: identity is the zero-cost multiplicative identity and step iterates the generator, reproducing the orbit {1, γ, γ², …}. Multiplication on LogicNat is defined by the two recursive equations mul_zero (n · identity = identity) and mul_succ (n · step m = n · m + n). The map toNat is the unique homomorphism that sends identity to 0 and step to successor, already shown to preserve addition and successor in sibling theorems.
proof idea
Proof by induction on b. Base case (b = identity) rewrites with mul_zero, toNat_zero and Nat.mul_zero. Inductive step (b = succ b') rewrites with mul_succ, toNat_succ, toNat_add, applies the inductive hypothesis, and finishes with Nat.mul_succ.
why it matters
Feeds directly into the definition of multiplication on LogicInt and the proof of toInt_mul, and supplies the key rewriting step in box_logic_toNat_square_budget for the Erdos-Straus box phase. It completes the arithmetic-recovery layer that lets Recognition Science embed standard number-theoretic calculations while remaining inside the functional-equation foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.