toInt_mul
plain-language theorem explainer
The theorem shows that the canonical recovery map from the logic integers to the standard integers preserves multiplication. Researchers verifying the ring axioms on LogicInt cite it when reducing identities to Int. The proof proceeds by double quotient induction on pair representatives, followed by rewriting with toNat lemmas and algebraic simplification in Int.
Claim. Let $Z_ℓ$ be the Grothendieck completion of the logic naturals under addition, equipped with the induced multiplication, and let $ι : Z_ℓ → ℤ$ be the recovery map sending the class of $(a,b)$ to toNat$(a)$ − toNat$(b)$. Then $ι(a · b) = ι(a) · ι(b)$ for all $a,b ∈ Z_ℓ$.
background
LogicInt is the quotient of LogicNat × LogicNat by the setoid encoding the Grothendieck construction, so that mk a b represents the formal difference a − b. The map toInt is the unique lift of the core difference map toNat a − toNat b that respects the equivalence. Upstream, toNat_add and toNat_mul establish that the operations on LogicNat recover ordinary Nat addition and multiplication exactly. The module constructs integers from logic primitives to supply the arithmetic substrate for the Recognition Science forcing chain.
proof idea
Apply Quotient.inductionOn to a, then to b. Unpack the representatives as pairs (a,b) and (c,d). Rewrite the product using the definition of multiplication on pairs, apply toInt_mk three times, expand the resulting Nat expressions with toNat_add and toNat_mul, then invoke push_cast followed by the ring tactic to obtain equality in Int.
why it matters
The result is invoked directly in the proofs of distributivity (add_mul', mul_add'), associativity (mul_assoc'), commutativity (mul_comm'), and the zero-divisor law (mul_eq_zero). Together with the addition counterpart it realizes the transfer principle that reduces all ring identities on LogicInt to the corresponding statements in Int. This step is required to embed the constructed integers into the model used for the phi-ladder and the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.