setoid
The instance equips the type of pre-rationals with the standard field-of-fractions equivalence. Researchers building number systems from logical primitives cite it when forming the quotient that yields logic-rational numbers. The definition is a direct bundling of the cross-multiplication relation with its reflexivity, symmetry, and transitivity lemmas.
claimThe type of pre-rationals, consisting of pairs $(n,d)$ of logic-integers with $d$ nonzero, carries the equivalence relation $(n_1,d_1)sim(n_2,d_2)$ if and only if $n_1cdot d_2=n_2cdot d_1$, together with proofs that the relation is reflexive, symmetric, and transitive.
background
In the module that constructs rationals from logical primitives, a pre-rational is a pair of logic-integers (numerator and denominator) with nonzero denominator. The equivalence identifies two pairs precisely when their cross-products coincide, which is the standard construction for the field of fractions of the logic-integers. This construction follows the earlier Grothendieck completion that produced logic-integers from logic-naturals via an analogous setoid on pairs.
proof idea
The declaration is a one-line wrapper that applies the Setoid constructor to the pre-rational type, supplying the cross-multiplication relation together with the already-proved reflexivity, symmetry, and transitivity lemmas for that relation.
why it matters in Recognition Science
This setoid instance is required to define logic-rational numbers as the quotient of pre-rationals, which then serves as the field of fractions over logic-integers. It is invoked by the distributivity theorem for logic-rats and by geometric results such as indistinguishable equivalence. Within the Recognition Science framework the step supplies the rational numbers needed to express quantities on the phi-ladder before geometry and forcing-chain extensions are introduced.
scope and limits
- Does not derive the equivalence relation from more primitive axioms.
- Does not define arithmetic operations on the quotient.
- Does not link the construction to physical constants or the forcing chain.
Lean usage
def LogicRat : Type := Quotient setoidformal statement (Lean)
77instance setoid : Setoid PreRat := ⟨ratRel, ratRel_refl, ratRel_symm, ratRel_trans⟩
proof body
Definition body.
78
79/-! ## 2. The Type of Logic-Native Rationals -/
80
81/-- `LogicRat` is the field of fractions of `LogicInt`. -/