LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-02 (claude-opus-5)

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.

Discreteness: $σ (n)$ is the immediate successor

Statement

For all $m, n \in N$ : $m < n ⟺ σ (m) \leq n$ (Order on the natural numbers). Consequently there is no $k$ with $n < k < σ (n)$ : the successor $σ (n)$ is the immediate successor of $n$ .

Facts & Assumptions

Given: The order $m \leq n ⟺ \exists j (m + j = n)$ , with $m < n$ meaning $m \leq n$ and $m \neq n$ (Order on the natural numbers), and addition with $m + 0 = m$ , $m + σ (n) = σ (m + n)$ (Addition of natural numbers).

[L1]

Every nonzero natural is a successor: $j \neq 0 \Rightarrow j = σ (i)$ (Every nonzero natural number is a successor).

[L2]

$σ (m) + i = σ (m + i)$ (the left successor law, Left successor law for addition) and $m + σ (i) = σ (m + i)$ (the addition recursion).

[L3]

Cancellation: $x + k = y + k \Rightarrow x = y$ (Addition is cancellative).

[L4]

$σ (x) \neq 0$ for every $x$ (Peano axiom P1) (The von Neumann naturals form a Peano system).

[L5]

Addition is commutative: $x + y = y + x$ (Addition is commutative).

Proof

technique · direct

1.1givenL1L2

Forward: if $m < n$ then $m \leq n$ and $m \neq n$ , so $m + j = n$ for some $j$ , with $j \neq 0$ since $j = 0$ would give $m = n$ ; then $j = σ (i)$ [L1] and $n = m + σ (i) = σ (m + i) = σ (m) + i$ [L2], hence $σ (m) \leq n$ .

1.2givenL2L3L4L5

Backward: if $σ (m) \leq n$ then $σ (m) + i = n$ , so $n = σ (m) + i = σ (m + i) = m + σ (i)$ [L2], hence $m \leq n$ ; and $m \neq n$ , since $m = n$ would give $m + σ (i) = m = m + 0$ , so $σ (i) + m = 0 + m$ by [L5] and $σ (i) = 0$ by [L3], contradicting [L4]; therefore $m < n$ .

2.1step 1.1step 1.2∎

No $k$ satisfies $n < k < σ (n)$ : if $n < k$ then $σ (n) \leq k$ by the equivalence, so $k \geq σ (n)$ , contradicting $k < σ (n)$ ; thus $σ (n)$ is the immediate successor.

Discreteness: $σ (n)$ is the immediate successor

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

Discreteness: σ(n)σ(n) is the immediate successor

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

Discreteness: $σ (n)$ is the immediate successor