toRatCore_respects
plain-language theorem explainer
toRatCore_respects establishes invariance of the candidate ratio map on PreRat pairs under the field-of-fractions equivalence, so the map descends to a well-defined function on the quotient LogicRat. A mathematician verifying the construction of rationals from logic primitives would cite it to justify the recovery map toRat. The proof reduces the equivalence hypothesis to cross-multiplication of integers via the transfer lemma and applies the standard rational equality criterion.
Claim. Let $p=(a,b)$ and $q=(c,d)$ be pre-rationals with $b,d$ nonzero. If $a·d=c·b$, then $(toInt a)/(toInt b)=(toInt c)/(toInt d)$ in $ℚ$.
background
PreRat is the structure of pairs (num, den) with num, den : LogicInt and den ≠ 0. The equivalence ≈ on PreRat holds when a·d = c·b. LogicRat is the quotient of PreRat by this setoid, forming the field of fractions of LogicInt. toRatCore sends each PreRat to the rational (toInt num)/(toInt den). The construction uses the upstream transfer theorem eq_iff_toInt_eq (an equation holds in LogicInt iff it holds after toInt), the multiplication preservation toInt_mul, and toInt_zero.
proof idea
The tactic proof intros the two PreRat pairs and the equivalence h. It proves the denominators map to nonzero rationals by contradiction, using eq_iff_toInt_eq and toInt_zero to reduce to the den_nonzero assumptions. It then derives the cross-multiplication toInt a · toInt d = toInt c · toInt b by applying congrArg toInt to the equality from h and rewriting with toInt_mul twice. The proof finishes by rewriting with div_eq_div_iff and casting the integer equality.
why it matters
The theorem justifies the lift in the definition of toRat : LogicRat → ℚ, the recovery map from logic-derived rationals to standard rationals. It completes the rational layer built on the integers from IntegersFromLogic and feeds the single downstream use in toRat. Within Recognition Science it ensures arithmetic recovered from the primitive distinction axioms matches classical ℚ, supporting later steps in the forcing chain toward physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.