mul_one'
plain-language theorem explainer
The theorem establishes that multiplication by the constructed unit leaves every element of LogicInt unchanged. Researchers verifying ring axioms in the logic-derived integers before lifting to rationals and reals would cite it. The proof is a one-line wrapper that transfers the claim via the embedding toInt and finishes by ring simplification on the standard integers.
Claim. For every $a$ in the Grothendieck completion of LogicNat, $a$ multiplied by the unit element equals $a$.
background
LogicInt is the quotient of pairs of LogicNat under the equivalence that identifies (a,b) with (c,d) when a+d = b+c, yielding the integers via Grothendieck completion. The transfer principle eq_iff_toInt_eq asserts that an equality holds in LogicInt precisely when the images under the canonical map toInt agree in the ordinary integers. Upstream lemmas establish that toInt preserves multiplication and sends the constructed unit to the integer 1.
proof idea
One-line wrapper that rewrites the goal with eq_iff_toInt_eq, replaces the product and unit by their images under toInt_mul and toInt_one, then applies ring to obtain the identity in the target integers.
why it matters
This identity completes the multiplicative unit axiom for LogicInt and is invoked verbatim by the corresponding mul_one' statements in the rationals and reals layers. It supplies a basic ring property required for the arithmetic hierarchy that later hosts the Recognition Science constants and the phi-ladder mass formula. No scaffolding remains; the result is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.