ofLogicInt
plain-language theorem explainer
ofLogicInt supplies the canonical embedding of logical integers into their field of fractions by sending each n to the class of the pair (n,1). Developers extending the logical number system to rationals cite this map when lifting integer operations. The definition constructs the element directly via the mk constructor and discharges the nonzero-denominator obligation with a short reduction that invokes the recovery maps toInt_one and toInt_zero.
Claim. The map sending each logical integer $n$ to the rational class of the pair $(n,1)$, realizing the standard inclusion of the Grothendieck completion into its field of fractions.
background
LogicInt is the Grothendieck completion of LogicNat, formed as the quotient of pairs of logical naturals under the relation that equates $(a,b)$ with $(c,d)$ precisely when $a+d=b+c$. LogicRat is the field of fractions of this group, obtained as the quotient of PreRat pairs under the induced equivalence. The module therefore continues the construction begun in IntegersFromLogic, where the upstream theorems toInt_zero and toInt_one establish that the recovery map toInt sends the logical zero and unit to their integer counterparts.
proof idea
The definition is a direct application of the mk constructor to the pair consisting of the input integer and the unit 1. The accompanying proof assumes the denominator is zero, applies congrArg toInt to obtain toInt(1)=toInt(0), then rewrites via toInt_one and toInt_zero to reach the contradiction one_ne_zero.
why it matters
This embedding is the required interface that lets later definitions in the same module treat logical integers as a subring of the rationals. It completes the passage from the integer layer (itself the Grothendieck completion of LogicNat) to the rational layer inside the Recognition Science foundation. No downstream uses are recorded yet, and the declaration touches no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.