toRat_fromRat
plain-language theorem explainer
The theorem asserts that recovering any classical rational q after embedding it into logic-native rationals via the constructor yields q exactly. Foundation researchers establishing equivalences between classical and derived number systems cite it to confirm the right inverse of the embedding. The proof reduces the claim to the integer round-trip by unfolding the rational mk constructor and rewriting with the integer lemmas.
Claim. $forall q in mathbb{Q}, recover(embed(q)) = q$, where embed maps a classical rational to its logic-native counterpart by applying the integer embedding to numerator and denominator, and recover extracts the classical value from the resulting logic-native pair.
background
In the RationalsFromLogic module, logic-native rationals LogicRat arise as the quotient of pairs of LogicInt under the equivalence ratRel. The embedding fromRat takes a classical rational q, applies fromInt to its numerator and denominator, and forms the mk pair (with a nonzeroness proof). The recovery map toRat inverts this process. This relies on the integer construction where fromInt maps Int to LogicInt by cases on sign, and the round-trip theorem toInt_fromInt establishes that integers are recovered exactly, as stated: 'The inverse Int → LogicInt. Maps non-negative n ≥ 0 to [n, 0] and negative -n < 0 to `[0, n]'. The local setting is building the rationals from logic primitives to support later arithmetic and number-theoretic results.
proof idea
The term proof introduces q, rewrites the application of fromRat to its definition as mk (fromInt q.num) (fromInt q.den) with the appropriate proof, then applies toRat_mk to obtain the ratio of the recovered integers, substitutes the integer round-trips toInt_fromInt twice, and concludes with the exact_mod_cast of the classical num_div_den equality.
why it matters
This theorem supplies the right inverse for the equivalence equivRat : LogicRat ≃ ℚ, which is invoked in the proof of add_mul' to transport ring laws and in reprLogic_fromRat_of_classical to move Erdos-Straus representations into the logic setting. It closes the transport API for rationals in the foundation layer, enabling applications of the Recognition Composition Law to classical rationals. It supports the broader construction toward the phi-ladder and dimensional forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.