toRat
plain-language theorem explainer
The definition supplies the canonical projection from the logic-constructed rationals to the standard rationals of Mathlib. Researchers building transport between discrete logic structures and continuous number systems cite it for all subsequent arithmetic and embedding results. The definition is realized as the quotient lift of the core ratio map once invariance under the equivalence is established.
Claim. The function sending each equivalence class in the field of fractions of the logic integers to the corresponding element of $ℚ$, obtained by lifting the assignment of a pre-rational pair $(num, den)$ to the ratio of their integer values.
background
LogicRat is the field of fractions of LogicInt, constructed as the quotient of PreRat by the setoid equivalence relation. This yields a type whose elements are equivalence classes of pairs of logic integers with nonzero denominator, as described in the module documentation.
proof idea
The definition is a one-line wrapper that invokes the Quotient.lift constructor on the core map toRatCore, justified by the invariance theorem toRatCore_respects.
why it matters
This map is invoked by the equivalence equivRat between LogicRat and ℚ, by the round-trip theorems fromRat_toRat and toRat_fromRat, and by the arithmetic preservation results such as toRat_add. It also feeds the embedding of logic rationals into the complexes via toComplex_ofLogicRat. Within the Recognition framework it provides the bridge from the discrete logic layer to the continuous quantities required for later physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.