toRat_neg
plain-language theorem explainer
The canonical embedding from LogicRat to the standard rationals preserves negation. Foundation proofs in Recognition Science cite this when lifting additive inverses from LogicInt to the rational field. The argument proceeds by Quotient.inductionOn on a representative pair, reduces via toRat_mk and toInt_neg, then clears the denominator with field_simp after invoking eq_iff_toInt_eq and toInt_zero.
Claim. Let $L$ be the field of fractions of the logic integers and let $i:L→ℚ$ be the canonical embedding. Then $i(-q)=-i(q)$ for every $q∈L$.
background
LogicRat is the quotient of PreRat pairs by the setoid ratRel, forming the field of fractions of LogicInt. The map toRat recovers the standard rational by applying toInt to numerator and denominator. The module RationalsFromLogic builds this structure on top of IntegersFromLogic, whose transfer principle eq_iff_toInt_eq equates equality statements in LogicInt with equality of their integer images.
proof idea
Quotient.inductionOn reduces to a pair (a,b) with b nonzero. Both sides are rewritten by toRat_mk; toInt_neg is applied to the negated numerator. eq_iff_toInt_eq together with toInt_zero produces a contradiction if the denominator image is zero. field_simp clears the nonzero denominator and norm_num finishes the equality.
why it matters
add_left_neg' invokes this to obtain the additive inverse property in LogicRat. costAt_neg_eq and toRat_neg in HilbertPolyaCandidate use it to establish J-cost reciprocity at the index level. The lemma completes transfer of ring operations from LogicInt, supporting the Recognition Composition Law on rational arguments in the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.