ratRel
plain-language theorem explainer
This definition supplies the cross-multiplication equivalence on pairs drawn from LogicInt that will become the rationals. It is cited by any construction of the field of fractions over the integers obtained from logic. The definition is a direct one-line encoding of the standard fraction equality test.
Claim. For pre-rationals \(p = (a, b)\) and \(q = (c, d)\) with \(b \neq 0\) and \(d \neq 0\), the relation \(p \sim q\) holds if and only if \(a \cdot d = c \cdot b\).
background
PreRat is the structure of pairs (num, den) where both components are LogicInt and den is nonzero. The module builds the rationals as the field of fractions of LogicInt. The upstream PreRat definition supplies the carrier type on which the relation acts.
The local setting is the step-by-step derivation of rational numbers directly from logical integers, prior to any physical interpretation.
proof idea
The definition is a direct functional encoding of the cross-multiplication condition.
why it matters
The relation supplies the equivalence used to form the setoid instance on PreRat and thereby the type LogicRat. It is invoked by the reflexivity, symmetry and transitivity theorems as well as by the ring law add_mul'. In the Recognition Science framework it provides the rational numbers required for later constructions such as the phi-ladder and the mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.