one_mul'
plain-language theorem explainer
one_mul' establishes the left unit law for multiplication in the integers obtained as the Grothendieck completion of logic naturals. Developers of the arithmetic hierarchy in Recognition Science cite it when confirming that LogicInt carries a ring structure compatible with later extensions. The proof is a one-line wrapper that transfers the claim to ordinary integers via the toInt embedding and closes with ring normalization.
Claim. For any element $a$ of the Grothendieck completion of logic natural numbers, $1 · a = a$.
background
LogicInt is the Grothendieck completion of LogicNat under addition, realized as the quotient of pairs of logic naturals by the equivalence that identifies pairs with the same difference. The module IntegersFromLogic builds the ring operations on this quotient after importing ArithmeticFromLogic. The transfer theorem eq_iff_toInt_eq equates equality in LogicInt with equality after the toInt map, while toInt_mul and toInt_one record that the map preserves multiplication and sends the unit to 1.
proof idea
The proof is a one-line wrapper. It rewrites the goal with eq_iff_toInt_eq, substitutes via toInt_mul and toInt_one to reach the standard integer identity, and finishes with the ring tactic.
why it matters
This supplies the multiplicative left-unit property for LogicInt and is invoked by the one_mul' theorems in RationalsFromLogic and RealsFromLogic. It belongs to the foundation layer that supplies the arithmetic needed for the Recognition Composition Law and the forcing chain from T0 to T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.