eq_iff_toRat_eq
plain-language theorem explainer
The theorem states that two elements of the logic-native rationals coincide exactly when their images under the recovery map to ordinary rationals agree. Foundation-layer work in Recognition Science cites it to move arithmetic identities from Mathlib's Rat back into the constructed LogicRat. The proof is a direct two-direction argument: one side applies the congruence property of toRat, while the converse applies fromRat to both sides and invokes the round-trip identity fromRat_toRat.
Claim. Let LogicRat be the quotient field of fractions of LogicInt. For any $a, b$ in LogicRat, $a = b$ if and only if the images under the canonical recovery map toRat : LogicRat → ℚ satisfy toRat($a$) = toRat($b$).
background
LogicRat is defined as the quotient of PreRat pairs (numerator and denominator from LogicInt) by the equivalence relation ratRel, yielding the field of fractions of LogicInt. The map toRat lifts a core function toRatCore to this quotient via Quotient.lift, while fromRat embeds ordinary rationals ℚ back into LogicRat by forming the corresponding mk pair. The upstream theorem fromRat_toRat establishes that applying fromRat after toRat recovers the original element, providing the key injectivity for the transport.
proof idea
The term-mode proof opens the biconditional with constructor. The forward direction is immediate from congrArg toRat. The converse assumes toRat a = toRat b, applies fromRat to both sides to obtain fromRat(toRat a) = fromRat(toRat b), then rewrites both sides via fromRat_toRat to conclude a = b.
why it matters
This transfer principle is invoked by the nine ring-operation theorems (add_assoc', add_comm', mul_assoc', etc.) that rewrite via eq_iff_toRat_eq and then apply ring. It closes the embedding of LogicRat into Mathlib's Rat, allowing the Recognition Science rationals to inherit field axioms without separate verification. The result sits inside the RationalsFromLogic module that supplies the arithmetic substrate for later steps in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.