toInt_neg
plain-language theorem explainer
The canonical map from logic-constructed integers to standard integers preserves negation. Researchers formalizing arithmetic from logical primitives cite this when verifying that the quotient yields a group homomorphism. The proof reduces via quotient induction on a representative pair, rewrites both sides with the defining property on constructors, and concludes by ring arithmetic.
Claim. Let $Z_ℓ$ be the Grothendieck completion of the logic naturals and let $ι : Z_ℓ → ℤ$ be the canonical map. Then $ι(-a) = -ι(a)$ for every $a ∈ Z_ℓ$.
background
LogicInt is the quotient of LogicNat × LogicNat by the setoid equivalence, forming integers as formal differences. The constructor mk(a, b) denotes the class of a − b. The map toInt is the lift of the core function sending mk a b to (toNat a : Int) − toNat b, as stated by the upstream theorem toInt_mk. The result sits inside the module that builds integers directly from logic naturals after the arithmetic foundations.
proof idea
Quotient.inductionOn reduces to a representative pair p = (a, b). Both sides are rewritten by toInt_mk to obtain toNat b − toNat a and the negation of toNat a − toNat b. Equality follows by ring simplification in Int.
why it matters
The lemma is invoked to prove additive inverses in add_left_neg' and to define negation on rationals in toRat_neg. It confirms that the embedding respects the additive group structure, advancing the integer and rational layers required for the Recognition Science forcing chain from T0 to T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.