Absolute Value Multiplicativity and Elementary Natural Number Arithmetic

We formalize a small collection of foundational results concerning the absolute value function on real numbers and elementary arithmetic on natural numbers. The central result is the multiplicativity of absolute value: for all real numbers \(a\) and \(b\), we have \(|ab| = |a| \cdot |b|\). This property is treated as a hypothesis in our formalization, reflecting its role as a defining characteristic of the standard absolute value on \(\mathbb{R}\).

We also prove several elementary properties of natural numbers using only arithmetic decision procedures: (i) the only idempotent squares are 0 and 1, i.e., \(a^2 = a\) implies \(a \in \{0, 1\}\); (ii) not all natural numbers are even; and (iii) the standard arithmetic identities for addition and multiplication with 0 and 1. These results, while elementary, demonstrate the effectiveness of automated arithmetic reasoning within a formally verified framework.

The proofs are fully mechanized in Lean 4 via the Platonic kernel, with 6 theorems verified and 1 hypothesis (the multiplicativity axiom).

Keywords: absolute value, natural number arithmetic, idempotent squares, parity, formal verification

MSC 2020: 11A25, 26A06