ratRel_symm
plain-language theorem explainer
Symmetry of the field-of-fractions relation on pre-rationals follows immediately from equality symmetry on LogicInt. Researchers constructing the quotient field LogicRat from logic-native integers cite this when verifying the setoid axioms. The proof is a one-line wrapper that rewrites the goal to the symmetric equality and applies h.symm.
Claim. Let $p=(a,b)$ and $q=(c,d)$ be pre-rationals with $b,d$ nonzero. If $a d = c b$ then $c b = a d$.
background
PreRat is the structure of pairs (num, den) where both components are LogicInt and den is nonzero. The relation ratRel declares two such pairs equivalent precisely when their cross-products agree: p.num * q.den = q.num * p.den. This module builds the rationals directly on top of the integers constructed in IntegersFromLogic, supplying the raw material for the setoid quotient that yields LogicRat.
proof idea
The proof introduces p, q and the hypothesis h : ratRel p q. It rewrites the goal to the symmetric form q.num * p.den = p.num * q.den and closes with exact h.symm, using only the built-in symmetry of equality on LogicInt.
why it matters
ratRel_symm supplies the symmetry axiom required by the setoid instance on PreRat, which is the immediate parent that defines LogicRat as the field of fractions. This step closes the equivalence-relation package needed to embed the rationals into the Recognition Science foundation before lifting to the phi-ladder and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.