toInt_mul
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.
claimLet $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 in Recognition Science
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.
formal statement (Lean)
344theorem toInt_mul (a b : LogicInt) : toInt (a * b) = toInt a * toInt b := by
proof body
Term-mode proof.
345 induction a using Quotient.inductionOn with
346 | h p =>
347 induction b using Quotient.inductionOn with
348 | h q =>
349 rcases p with ⟨a, b⟩
350 rcases q with ⟨c, d⟩
351 show toInt (mk (a * c + b * d) (a * d + b * c)) = toInt (mk a b) * toInt (mk c d)
352 rw [toInt_mk, toInt_mk, toInt_mk]
353 rw [toNat_add, toNat_add, toNat_mul, toNat_mul, toNat_mul, toNat_mul]
354 push_cast
355 ring
356
357/-- Transfer principle: an equation in `LogicInt` holds iff it holds
358under `toInt`. The workhorse for proving ring identities on
359`LogicInt` by reduction to `Int`. -/