ratRel
The field-of-fractions equivalence on pre-rationals identifies pairs with proportional numerators and denominators. Researchers building the rationals from integers would cite this predicate when forming the quotient. The implementation reduces directly to the cross-multiplication equality check on the pair components.
claimFor pre-rationals $p = (a, b)$ and $q = (c, d)$ with $b, d$ nonzero, the relation holds precisely when $a d = c b$.
background
Pre-rational is the structure of a numerator-denominator pair drawn from LogicInt with the explicit nonzero-denominator hypothesis. The module constructs the rationals directly from the integers obtained via logic, using this relation as the first step toward the quotient type. The upstream PreRat structure supplies the pair components that enter the cross-multiplication test.
proof idea
The definition is a direct functional assignment returning the proposition that the cross products are equal. No lemmas or tactics are invoked; it is the primitive predicate for the equivalence.
why it matters in Recognition Science
This equivalence supplies the relation that turns PreRat into a setoid, enabling the quotient that yields LogicRat as the field of fractions of LogicInt. It is invoked by the subsequent reflexivity, symmetry, and transitivity theorems and by the distributivity law add_mul'. In the Recognition framework it furnishes the rational arithmetic required for later constructions.
scope and limits
- Does not establish reflexivity, symmetry, or transitivity of the relation.
- Does not construct the quotient type LogicRat itself.
- Does not admit zero denominators or define division.
- Does not extend the construction beyond rationals to reals or completions.
formal statement (Lean)
47def ratRel : PreRat → PreRat → Prop :=
proof body
Definition body.
48 fun p q => p.num * q.den = q.num * p.den
49