LemmaStatement: Literature-sourcedProof: 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.

Left successor law for addition

Statement

For all $m, n \in N$ : $σ (m) + n = σ (m + n)$ . (The recursion defines addition on the second argument; this is the matching law for adding on the first.)

Facts & Assumptions

Given: Addition with $m + 0 = m$ and $m + σ (k) = σ (m + k)$ (Addition of natural numbers).

[L1]

Induction principle (The principle of mathematical induction).

Proof

technique · induction

1.1base

Base $n = 0$ : $σ (m) + 0 = σ (m)$ by $x + 0 = x$ , and $σ (m + 0) = σ (m)$ by $m + 0 = m$ , so $σ (m) + 0 = σ (m + 0)$ .

1.2ih

Inductive hypothesis: $σ (m) + n = σ (m + n)$ .

2.1step 1.2given

Step: $σ (m) + σ (n) = σ (σ (m) + n) = σ (σ (m + n)) = σ (m + σ (n))$ , applying $x + σ (k) = σ (x + k)$ at the outer sum, then the hypothesis, then $m + σ (n) = σ (m + n)$ backward inside $σ$ .

3.1step 1.1step 2.1discharge-induction∎

By induction [L1], $σ (m) + n = σ (m + n)$ for all $n$ , and since $m$ was arbitrary, for all $m, n \in N$ .

Left successor law for addition

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources