mul_add'
plain-language theorem explainer
The theorem establishes left distributivity of multiplication over addition for the recovered real numbers LogicReal. Foundation-layer developers in the Recognition Science project cite it to confirm that algebraic operations lift consistently through the completion from the logic-derived rationals. The proof reduces the claim to the corresponding identity on Mathlib's reals via transport and then applies ring simplification.
Claim. For all $x, y, z$ in the Cauchy completion LogicReal of the logic-derived rationals, $x · (y + z) = x · y + x · z$.
background
LogicReal is the wrapper structure around Mathlib's Bourbaki completion of ℚ, built on the equivalence LogicRat ≃ ℚ recovered from the Law-of-Logic layer. The module recovers the reals by completing the logic-derived rationals while exposing a transport-first API: every operation on LogicReal is defined by pulling back the corresponding structure along the canonical map toReal to Mathlib's reals. This setup ensures downstream theorems reduce to existing real-number results and read back as recovered theorems.
proof idea
The proof is a term-mode wrapper. It first rewrites the goal using eq_iff_toReal_eq to transport the equality to Mathlib's reals, then applies simp to unfold the pulled-back definitions of multiplication and addition, and finally invokes the ring tactic to discharge the algebraic identity.
why it matters
This declaration mirrors the mul_add' theorems already established for LogicInt and LogicRat, ensuring the distributive law holds uniformly across the logic-to-reals recovery chain. It supports the module's goal of transporting algebraic structure from the completed rationals without global instance pollution. The result contributes to the foundation layer that underpins later Recognition Science constructions, though no specific open question is closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.