toRatCore
plain-language theorem explainer
The definition maps each PreRat pair of LogicInts (with nonzero denominator) to a rational by recovering the integers via toInt and dividing in ℚ. Researchers constructing number systems from logical primitives cite it as the core step before quotienting to LogicRat. It is implemented as a direct one-line functional definition applying toInt componentwise.
Claim. The map from pre-rationals to rationals sends a pair (num, den) with den ≠ 0 to (toInt num) / (toInt den) in ℚ, where toInt recovers the underlying integer from each LogicInt.
background
PreRat is the structure of pairs (num, den) where both components are LogicInt and den ≠ 0; it serves as the raw input for the field-of-fractions construction before identifying equivalent pairs. The upstream map toInt : LogicInt → Int is the recovery function defined by quotient lifting from its core implementation, sending non-negative logical integers to their natural values and negatives to the corresponding positive form. This definition appears in the module that builds rationals directly from the prior integers-from-logic construction.
proof idea
It is a one-line definition that applies toInt to the num and den fields of the input PreRat and performs division in ℚ.
why it matters
This definition supplies the core map lifted in the downstream toRat recovery function LogicRat → ℚ and in the respect theorem toRatCore_respects that shows the map is invariant under the equivalence relation. It forms part of the foundational layer that derives the rational numbers used in the Recognition Science forcing chain (T0–T8) and subsequent constants such as ħ = φ^{-5}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.