LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Zero and one under multiplication

Statement

For all $n \in N$ : $0 \cdot n = 0$ , $1 \cdot n = n$ , and $n \cdot 1 = n$ . Here $1 = σ (0)$ , and the clause $n \cdot 0 = 0$ is definitional.

Facts & Assumptions

Given: multiplication $m \cdot 0 = 0$ and $m \cdot σ (n) = m \cdot n + m$ (Multiplication of natural numbers), and addition with $m + 0 = m$ and $m + σ (k) = σ (m + k)$ (Addition of natural numbers).

[L1]

$0 + k = k$ for all $k \in N$ (Left identity for addition).

[L2]

The induction principle (The principle of mathematical induction).

Proof

technique · induction on $n$

1.1

Right unit $n \cdot 1 = n$ : $n \cdot 1 = n \cdot σ (0) = n \cdot 0 + n = 0 + n = n$ , using the multiplication recursion then [L1].

givenL1

1.2

Base of the left inductions: $0 \cdot 0 = 0$ and $1 \cdot 0 = 0$ by the clause $m \cdot 0 = 0$ .

base

1.3

Inductive hypothesis: $0 \cdot n = 0$ and $1 \cdot n = n$ .

2.1

Step: $0 \cdot σ (n) = 0 \cdot n + 0 = 0 + 0 = 0$ , using the hypothesis $0 \cdot n = 0$ and $0 + 0 = 0$ (the instance $k = 0$ of [L1]); and $1 \cdot σ (n) = 1 \cdot n + 1 = n + 1 = σ (n)$ , where $n + 1 = n + σ (0) = σ (n + 0) = σ (n)$ by the addition recursion $m + σ (k) = σ (m + k)$ and $n + 0 = n$ .

step 1.3givenL1

3.1

By induction [L2], $0 \cdot n = 0$ and $1 \cdot n = n$ for all $n$ ; together with step 1.1, $n \cdot 1 = n$ for all $n$ .

step 1.1step 2.1discharge-induction∎

Depends on

Used by

Dependency tree · two levels

10 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

T. Tao, Analysis I, 3rd ed., §2.1-2.3 (Peano axioms, recursion, arithmetic) (standard reference, not scraped)
Peano axioms (Wikipedia) (standard reference, not scraped)
W. Aitken, MATH 378 Ch. 1: The Peano Axioms (CSU San Marcos) (standard reference, not scraped)