toRat_zero
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove that toRat is a ring homomorphism.
- Does not address preservation of order or positivity.
- Does not extend the result to real completions or other extensions.
- Does not establish uniqueness of the embedding among possible maps.
Lean usage
rw [toRat_zero]formal statement (Lean)
297theorem toRat_zero : toRat (0 : LogicRat) = 0 := by
proof body
Term-mode proof.
298 show toRat (mk 0 1 _) = 0
299 rw [toRat_mk, toInt_zero, toInt_one]
300 norm_num
301