mul_assoc'
plain-language theorem explainer
Multiplication is associative on the recovered real numbers LogicReal built from the law-of-logic rationals. Foundation-layer work in Recognition Science cites this when confirming that ring structure survives the Bourbaki completion step. The argument reduces the claim to the standard reals via the equality transport theorem and discharges it with the ring tactic.
Claim. For all recovered reals $x, y, z$ in the Cauchy completion of the logic-derived rationals, $(x · y) · z = x · (y · z)$.
background
The module recovers the reals by completing the recovered rationals LogicRat, which are equivalent to the standard rationals via the prior layer. LogicReal is a wrapper around Mathlib's Bourbaki completion of ℚ; the maps toReal and fromReal transport statements to and from the standard real line so that algebra can be pulled back without polluting global instances. The local setting is a transport-first API: every algebraic identity on LogicReal is proved by moving to the completed reals and reading the result back.
proof idea
One-line wrapper that applies the equality transport theorem eq_iff_toReal_eq to rewrite the goal as an identity on the underlying Bourbaki reals, then uses simp to unfold the pulled-back multiplication and the ring tactic to finish.
why it matters
This result completes the transport of the multiplicative associativity axiom through the logic-to-reals chain, matching the parallel mul_assoc' theorems already established for LogicInt and LogicRat. It feeds the algebraic structure needed for later foundation developments that rely on a ring of recovered reals. In the Recognition Science setting it ensures no new defects are introduced when moving from the rational layer to the completed reals used in the phi-ladder and forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.