toRat_one
plain-language theorem explainer
The canonical map from the logic-constructed rationals to the standard rationals preserves the multiplicative unit. Researchers constructing arithmetic from logical primitives inside a proof assistant would cite this when verifying that the embedding respects ring structure. The argument is a direct term reduction that unfolds the quotient representative for one and invokes the corresponding integer result before normalizing.
Claim. Let $Q_ℓ$ be the field of fractions of the integers $Z_ℓ$ obtained from logic. The recovery map $φ: Q_ℓ → ℚ$ satisfies $φ(1) = 1$.
background
LogicRat is the quotient of PreRat pairs by the setoid equivalence, yielding the field of fractions of LogicInt. The map toRat is the induced lift of the core function sending a representative pair (a, b) to (toInt a) / (toInt b) in the standard rationals. The constructor mk forms an element of LogicRat from a pair of LogicInt values with nonzero second component.
proof idea
Term-mode proof that reduces the claim on the unit representative via the lemma toRat_mk, substitutes the integer identity from toInt_one, and finishes by norm_num on the resulting rational expression.
why it matters
This result supplies the multiplicative identity preservation needed for the ring axioms in the constructed rationals, directly feeding the proofs of mul_one' and one_mul'. It belongs to the early foundation layer that lets the Recognition Science framework treat the embedded rationals as a faithful model before moving to the forcing chain and physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.