fromRat_toRat
plain-language theorem explainer
The theorem establishes that every logic-native rational recovers itself after transport to standard rationals and back, serving as the left inverse for the carrier equivalence. Researchers constructing custom number systems or verifying embeddings into Mathlib would cite it to confirm injectivity of the round-trip map. The proof proceeds by quotient induction on the representative pair, followed by rewriting via the toRat constructor and reduction through integer transfer lemmas to a cross-multiplication identity in the rationals.
Claim. Let $Q_ℓ$ be the field of fractions of the logic integers. For every $q ∈ Q_ℓ$, the composition of the recovery map from standard rationals with the embedding satisfies fromRat(toRat($q$)) = $q$.
background
LogicRat is the quotient of PreRat pairs by the equivalence ratRel, forming the field of fractions over LogicInt. LogicInt is itself the quotient of LogicNat pairs. The upstream transfer principle eq_iff_toInt_eq states that an equality between logic integers holds if and only if the images under toInt coincide in the standard integers; this is the workhorse for reducing ring identities on the custom structure to ordinary arithmetic. The module imports IntegersFromLogic to reuse its constructors mk, fromInt, toInt, and soundness theorem for quotients.
proof idea
The tactic proof introduces an arbitrary q and applies Quotient.inductionOn. It destructures the representative as a pair (a, b) with b nonzero, rewrites via toRat_mk, and invokes the soundness theorem. The remaining equality is transferred using eq_iff_toInt_eq together with toInt_mul and toInt_fromInt, then reduced to a cross-multiplication identity in ℚ by invoking div_eq_div_iff and the num_div_den property of standard rationals.
why it matters
This supplies the left inverse for the equivalence equivRat : LogicRat ≃ ℚ, which in turn enables transfer of ring operations such as add_mul' and the equality transfer eq_iff_toRat_eq. It completes the round-trip transport API in the foundation layer, ensuring the logic-native rationals can be used interchangeably with standard ones when building the phi-ladder and mass formulas. No open scaffolding remains here; the result is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.