toInt_mul
plain-language theorem explainer
Multiplication on logic-forced naturals is preserved by the integer recovery map: the image of a product equals the product of the images in ℤ. Cited when showing the forced naturals embed as a multiplicative monoid into the integers, and when discharging ring axioms for LogicInt via the recovery isomorphism. Proof unfolds the embedding, rewrites by the Nat-level multiplication recovery, then finishes with cast and ring.
Claim. For all logic-forced natural numbers $a$ and $b$ (built from identity and step), the integer recovery map preserves multiplication: the image of $a\cdot b$ equals the product of the images in $\mathbb{Z}$.
background
LogicNat is the natural-number type forced by the Law of Logic: two constructors, identity (zero-cost / multiplicative unit in the orbit) and step (one more generator iterate). It mirrors the orbit ${1,\gamma,\gamma^2,\ldots}$ as the smallest subset of $\mathbb{R}_+$ containing 1 and closed under multiplication by $\gamma$.
The recovery map toNat sends LogicNat to ordinary Nat. The upstream recovery theorem toNat_mul states that LogicNat multiplication agrees with Nat multiplication under that equivalence. In this module the integer recovery toInt on LogicNat is the composite of toNat with the canonical cast Nat → ℤ (nonnegative embedding).
The local setting is UniversalForcing.ForcedIntegers: integers as forced structure recovered from the logic-built arithmetic, imported from ForcedSemiring. Parallel toInt_mul results exist for LogicInt and for signed orbits in the primitive recognition calculus; this instance is the LogicNat case.
proof idea
Short tactic proof. Unfold toInt (so the goal is about casts of toNat). Rewrite the product with LogicNat.toNat_mul, which reduces LogicNat multiplication to Nat multiplication. push_cast moves the Nat → ℤ coercions through the product. ring closes the remaining integer identity. No induction at this layer; the inductive work lives in toNat_mul.
why it matters
Homomorphism fact needed so forced arithmetic matches classical ℤ multiplication on the nonnegative cone. Downstream, IntegersFromLogic uses the recovery maps and their mul/add lemmas to prove the ring laws for LogicInt by transporting across toInt: mul_assoc', mul_comm', mul_one', one_mul', left/right distributivity (mul_add', add_mul'), cancellation, and the no-zero-divisors statement mul_eq_zero ("Forced by the ring isomorphism with Int").
In the Recognition foundation stack this sits under UniversalForcing: arithmetic is not postulated but recovered from logic-forced constructors, then shown isomorphic to standard integers. It is scaffolding for the integer layer that later supports rationals, costs, and the forcing chain, not itself a T5–T8 landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.