LogicRat
plain-language theorem explainer
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.
Claim. Let 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.