Integer Basics: Foundational Properties of Integer Arithmetic
Mathematics verified. Core theorems are machine-checked in Lean 4.
Prose and presentation may not have been human-reviewed.
Summary
We present formal proofs of six foundational theorems in integer arithmetic: commutativity of addition and multiplication over ℤ, absorption of zero under multiplication, non-negativity of squared differences, and the dichotomy that every natural number is either zero or positive. All results are machine-verified in the Lean 4 proof assistant.
Length
992 words
Claims
12 theorems
Status
Draft
Target
Archive-only