mul_one'
plain-language theorem explainer
The multiplicative identity holds for every recovered real constructed from the law of logic. Foundation developers cite this result when transporting ring identities across the logic-to-reals pipeline. The proof reduces the claim to the standard real line via equality transport and finishes by simplification.
Claim. For every recovered real number $x$, multiplication by the multiplicative unit satisfies $x · 1 = x$.
background
The module recovers the real numbers by completing the logic-derived rationals. LogicReal is a wrapper around Mathlib's Bourbaki completion of ℚ, using the equivalence LogicRat ≃ ℚ to obtain a copy of the standard reals while avoiding global instance pollution. Transport maps toReal and fromReal identify the wrapper with the usual real line, so algebraic statements on LogicReal reduce to their Mathlib counterparts.
proof idea
One-line wrapper that rewrites the goal with the equality-transport lemma eq_iff_toReal_eq, reducing it to the corresponding identity on the underlying Bourbaki real, which simplification then discharges.
why it matters
This result completes the ring axioms on the recovered reals, mirroring the mul_one' theorems already established for LogicInt and LogicRat. It ensures every basic arithmetic identity lifts uniformly through the construction described in the module documentation, supplying the algebraic substrate required for later Recognition Science steps that define constants and physical structures on the real line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.