LogicRat defines the type of logic-native rationals as the quotient of PreRat pairs under the cross-multiplication equivalence. Researchers building number systems from primitive distinction axioms cite it as the carrier for rational arithmetic before transport to standard rationals. The definition is a direct application of the Quotient constructor to the setoid instance on PreRat.
claimLet PreRat be the set of pairs $(n,d)$ with $n,d$ logic-integers and $d$ nonzero. Let the equivalence relation on PreRat be given by $(n,d) sim (m,e)$ if and only if $n e = m d$. Then LogicRat is the quotient set PreRat under this relation.
background
PreRat is the structure of pairs of logic-integers with nonzero second component, serving as unreduced fractions. The setoid on PreRat is the instance generated by ratRel together with its reflexivity, symmetry, and transitivity proofs; this relation identifies pairs that represent the same rational value via cross-multiplication. The construction inherits the setoid structure already placed on logic-integers by the Grothendieck completion in IntegersFromLogic.setoid.
proof idea
The definition is a one-line wrapper that applies the Quotient type constructor directly to the setoid instance on PreRat.
why it matters in Recognition Science
LogicRat supplies the carrier for all lifted rational operations (addition, multiplication, negation) defined later in the same module and is the input type for the embedding ofLogicRat into LogicComplex. It realizes the field-of-fractions step that follows the integer construction, completing the recovery of standard rationals inside the Recognition Science foundation chain.
scope and limits
Does not prove that the lifted operations make LogicRat a field.
Does not supply an embedding into reals or complexes.
Does not address ordering or completeness properties.
Does not connect to the phi-ladder or physical constants.
formal statement (Lean)
82def LogicRat : Type := Quotient (setoid : Setoid PreRat)
proof body
Definition body.
83 84namespace LogicRat 85 86/-- Constructor: form a rational from a pair with non-zero denominator. -/
used by (40)
From the project-wide theorem graph. These declarations reference this one in their body.