toRat_zero
plain-language theorem explainer
The recovery map from logic-derived rationals to standard rationals sends the zero element to the rational zero. Foundation-layer verifications in Recognition Science cite this when confirming that the constructed additive structure matches expected arithmetic. The proof is a short reduction that expresses zero via the mk constructor, applies the integer recovery maps for zero and one, and normalizes the resulting expression.
Claim. Let $LogicRat$ be the field of fractions of $LogicInt$. The recovery map $toRat : LogicRat → ℚ$ satisfies $toRat(0) = 0$.
background
LogicRat is the quotient of PreRat by the setoid equivalence relation, forming the field of fractions of LogicInt. The mk constructor produces an element from a numerator-denominator pair in LogicInt with nonzero denominator. Upstream results include toInt_zero, which recovers the standard zero from the logic integer zero via mk on naturals, and toInt_one, which does the same for one; toRat_mk lifts these integer maps to the rational level.
proof idea
The proof rewrites the zero element as mk 0 1, applies toRat_mk to obtain a ratio of toInt images, substitutes toInt_zero and toInt_one, then invokes norm_num to conclude the equality.
why it matters
This theorem supplies the zero case needed for add_zero', zero_add', and add_left_neg', which establish the additive group axioms on LogicRat. It forms a basic consistency check in the logic-to-rationals construction before downstream use in Hilbert-Polya candidate maps, aligning with the Recognition Science step of deriving standard arithmetic from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.