add_assoc'
plain-language theorem explainer
Associativity of addition holds on the recovered real numbers obtained as the Cauchy completion of logic-derived rationals. Researchers verifying the algebraic layer of the Recognition Science foundation would cite this to confirm that ring identities transport correctly from Mathlib. The proof reduces the claim via the equality transfer map and concludes with the ring tactic.
Claim. For all recovered reals $x, y, z$, $(x + y) + z = x + (y + z)$.
background
The module recovers the real numbers from the law-of-logic rationals by completing the rationals using Mathlib's Bourbaki construction. LogicReal wraps the completed reals to avoid polluting global instances, with addition and other operations defined by transport along the canonical equivalence to Mathlib's reals. This builds directly on the parallel associativity results for the integer and rational layers, each of which rests on its own equality transfer principle that equates statements in the recovered type with the corresponding statement after transport.
proof idea
The proof applies the equality transfer lemma to rewrite the goal as an identity on the underlying real line. It then uses simp to unfold the transported addition and invokes the ring tactic to discharge the associativity identity.
why it matters
This theorem completes the transfer of the ring axioms to the recovered reals and is referenced by the corresponding associativity statements in the integer and rational recoveries. It forms part of the systematic recovery of arithmetic from the law of logic, ensuring the real line inherits its algebraic structure before the construction proceeds to physical constants and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.