toNat_mul
plain-language theorem explainer
The recovery map from logic naturals to standard naturals preserves multiplication. Researchers building arithmetic from the Law of Logic cite it to transfer product identities between the two structures. The proof proceeds by induction on the second argument, reducing each case via the recursive multiplication rules and the successor definition.
Claim. Let $L$ be the inductive type generated by a zero element and successor. Let $ρ: L → ℕ$ be the recovery isomorphism. Then $ρ(a · b) = ρ(a) · ρ(b)$ for all $a, b ∈ L$.
background
LogicNat is the inductive type whose constructors are identity (the zero-cost multiplicative identity) and step (one further iteration of the generator). This encodes the smallest subset of positive reals closed under multiplication by a fixed γ and containing 1. The function toNat supplies the isomorphism that recovers ordinary natural numbers from this structure.
proof idea
Induction on the second argument b. The base case (b = identity) rewrites via mul_zero and toNat_zero to reach Nat.mul_zero. The inductive step applies mul_succ to expand the product, then invokes toNat_succ, toNat_add, the induction hypothesis, and Nat.mul_succ.
why it matters
It guarantees that multiplication on LogicNat agrees with the standard product, enabling transfer to integer multiplication via toInt_mul and to the square-budget identity in box_logic_toNat_square_budget. The result closes one link in the chain that embeds logic-forced arithmetic into conventional number theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.