sound
plain-language theorem explainer
sound shows that the rational constructor mk respects cross-multiplication: if a d equals c b for nonzero b and d in LogicInt, then mk a b hb equals mk c d hd in LogicRat. Researchers building the logic-to-number embedding cite it when forming the field of fractions and when lifting integer arithmetic. The proof is a direct one-line wrapper that invokes Quotient.sound on the supplied equality hypothesis.
Claim. Let $a, b, c, d$ be elements of the Grothendieck integers with $b, d$ nonzero. If $a d = c b$, then the rational formed by numerator $a$ and denominator $b$ equals the rational formed by numerator $c$ and denominator $d$.
background
LogicInt is the quotient of LogicNat pairs under the integer equivalence, the Grothendieck completion under addition. LogicRat is the quotient of PreRat pairs under the rational equivalence, forming the field of fractions of LogicInt. The mk constructor packages a numerator-denominator pair together with a proof that the denominator is nonzero.
proof idea
The proof is a one-line wrapper that applies Quotient.sound. It then exhibits the required equality a * d = c * b directly from the hypothesis h.
why it matters
The result ensures the rational constructor is well-defined on equivalence classes, completing the passage from LogicInt to LogicRat. It is invoked by BWD3Model for SAT linear encodings and by the minimality-completeness theorem for virtue signatures. The declaration advances the foundation by supplying the multiplicative relation needed for later arithmetic and complexity constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.