toRat_mk
plain-language theorem explainer
The recovery map from logic rationals to standard rationals commutes with the constructor that forms a rational from a numerator-denominator pair of logic integers. Researchers building faithful embeddings of discrete logic structures into classical number fields cite this for the transport API. The proof is a direct reflexivity after the definitions of mk and toRat are unfolded.
Claim. For $a, b$ in the logic integers with $b$ nonzero, the rational recovery of the constructed logic rational equals the ratio of the recovered integers: $toRat(mk(a, b, h_b)) = (toInt(a) : ℚ) / toInt(b)$.
background
LogicInt is the Grothendieck completion of LogicNat under addition, constructed as the quotient of pairs of naturals. LogicRat is the corresponding quotient of pairs of LogicInt values with nonzero second component, using the constructor mk. The map toRat is the induced lift from this quotient to Mathlib's ℚ, while toInt recovers integers from LogicInt. This sits in the foundation layer that builds rationals directly from the logic primitives before any Recognition Science structures such as the phi-ladder or J-cost are introduced.
proof idea
One-line reflexivity proof. It follows immediately once mk is expanded to Quotient.mk' and toRat to Quotient.lift, with the core function toRatCore returning the ratio of the lifted integers.
why it matters
This lemma is invoked by the round-trip theorem fromRat_toRat and by the homomorphism theorems toRat_add, toRat_mul, toRat_neg, toRat_one and toRat_zero. It completes the definition of the transport map between LogicRat and ℚ, supplying the concrete equality needed to lift arithmetic operations from the logic side. In the broader Recognition Science chain it anchors the rational layer that later supports the eight-tick octave and mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.