fromRat
plain-language theorem explainer
The map embedding classical rationals into logic-native rationals is realized by sending q to the mk constructor on fromInt of its numerator and denominator, with a short non-zero check. Researchers transporting classical number theory results such as Erdős-Straus representations into the Recognition Science setting cite this definition to obtain the inverse leg of equivRat. The definition proceeds by direct construction that applies the integer embedding and verifies the denominator condition via recovery maps.
Claim. The function sending a rational $q$ to the logic rational formed by the pair $(fromInt(q.num), fromInt(q.den))$ in the field of fractions of LogicInt, with the proof that the denominator is nonzero.
background
LogicRat is the field of fractions of LogicInt, constructed as the quotient of PreRat pairs under the setoid ratRel. LogicInt itself is the Grothendieck completion of LogicNat under addition, with constructor mk forming equivalence classes [a, b]ₗ. The upstream fromInt embeds classical integers into LogicInt by cases on sign, with toInt as the recovery map satisfying toInt_fromInt and toInt_zero.
proof idea
The definition applies fromInt to q.num and q.den, then invokes mk with a proof term. The proof transports the zero-denominator assumption via toInt, rewrites with toInt_zero and toInt_fromInt, invokes q.den_pos via exact_mod_cast, and derives the contradiction ne_of_gt.
why it matters
This definition supplies the inverse leg of equivRat : LogicRat ≃ ℚ and is invoked by toRat_fromRat, fromRat_toRat, and eq_iff_toRat_eq. It is used downstream in box_phase_hit_gives_repr_logic and reprLogic_fromRat_of_classical to lift classical Erdős-Straus representations into the logic setting, closing the rational transport API that preserves the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.