add_comm'
plain-language theorem explainer
Addition commutes on the rationals obtained as the field of fractions of the logic integers. Researchers constructing the Recognition Science number hierarchy cite this result to confirm that the quotient construction preserves the algebraic laws already verified for LogicInt. The proof is a one-line wrapper that invokes the transfer principle eq_iff_toRat_eq together with additivity of toRat and then normalizes via the ring tactic.
Claim. For all $a, b$ in the field of fractions of the logic integers, $a + b = b + a$.
background
LogicRat is the quotient of PreRat pairs by the setoid equivalence, forming the field of fractions of LogicInt. The module builds rationals directly from the integers derived from logic, importing the integers module for its base operations. Upstream results include the integers add_comm' (which states commutativity for LogicInt via its own transfer and toInt_add), the transfer theorem eq_iff_toRat_eq (equality of LogicRat elements is equivalent to equality of their images under toRat in Mathlib Rat), and toRat_add (the embedding preserves addition).
proof idea
The proof rewrites the goal with eq_iff_toRat_eq, replaces both sides by toRat_add, and finishes with ring. This reduces the statement to the known commutativity of addition in Mathlib Rat.
why it matters
The result propagates commutativity from LogicInt through the rationals into the reals construction, appearing as a dependency for both IntegersFromLogic.add_comm' and RealsFromLogic.add_comm'. It completes one link in the foundation chain that supplies the number systems used for the phi-ladder and Recognition Composition Law. No open scaffolding remains for this specific property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.