fromRat
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not supply a computable implementation of the map.
- Does not define addition or multiplication on LogicRat.
- Does not extend the embedding beyond rationals.
- Assumes the input rational has positive denominator by construction.
formal statement (Lean)
226noncomputable def fromRat (q : ℚ) : LogicRat :=
proof body
Definition body.
227 let n : LogicInt := fromInt q.num
228 let d : LogicInt := fromInt q.den
229 mk n d (by
230 intro h
231 have : toInt d = toInt 0 := congrArg toInt h
232 rw [toInt_zero] at this
233 have : toInt (fromInt q.den) = 0 := this
234 rw [toInt_fromInt] at this
235 have hpos : (0 : Int) < q.den := by exact_mod_cast q.den_pos
236 have : (q.den : Int) = 0 := this
237 have hne : (q.den : Int) ≠ 0 := ne_of_gt hpos
238 exact hne this)
239