Alphabeta Math
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.

Trichotomy of the order on N

Statement

For all m,n∈N exactly one of m<n, m=n, m>n holds. In particular the order (Order on the natural numbers) is total.

Facts & Assumptions

Given: The order on N, where m≤n means ∃k (m+k=n) and m<n means m≤n with m≠n (Order on the natural numbers), and addition with m+0=m, m+σ(n)=σ(m+n) (Addition of natural numbers).

[L1]
[L2]

Left successor law: σ(a)+k=σ(a+k) (Left successor law for addition).

[L3]

Addition is associative (Addition is associative).

[L4]

Every nonzero natural is a successor: n≠0⇒n=σ(a) for some a (Every nonzero natural number is a successor).

[L5]

σ(x)≠0 for every x (axiom P1 of The von Neumann naturals form a Peano system).

[L6]

Cancellation: x+k=y+k⇒x=y (Addition is cancellative).

[L7]

Addition is commutative (Addition is commutative).

Proof

technique · induction
1.1

At most one of the three holds where equality is involved: m<n forces m≠n and m>n forces n≠m, so m=n is incompatible with either strict relation.

given
1.2

The two strict relations are incompatible: if m<n and m>n then m+j=n and n+i=m with i,j≠0, so m+(j+i)=(m+j)+i=n+i=m=m+0; by commutativity [L7], (j+i)+m=0+m, so j+i=0 by cancellation [L6]; yet j=σ(a) [L4] gives, by the left successor law [L2], j+i=σ(a)+i=σ(a+i)≠0 [L5], a contradiction.

givenL2L3L4L5L6L7
1.3

For every n one has n<σ(n), since n+σ(0)=σ(n+0)=σ(n) by the recursion, with σ(0)≠0 [L5].

givenL5
1.4

Base case n=0: for arbitrary m, either m=0, giving m=n, or m≠0 so 0+m=m [L1] with m≠0 gives 0<m, that is n<m; so at least one of m<n, m=n, m>n holds.

baseL1L4
1.5

Inductive hypothesis: fix n and assume that for every m at least one of m<n, m=n, m>n holds.

ih
2.1

Successor step: for arbitrary m, apply the hypothesis; if m<n then n=m+k with k≠0, and the recursion gives m+σ(k)=σ(m+k)=σ(n), so σ(n)=m+σ(k) with σ(k)≠0 [L5], giving m<σ(n); if m=n then m+σ(0)=σ(m+0)=σ(m)=σ(n), so σ(n)=m+σ(0) with σ(0)≠0, giving m<σ(n); if m>n then m=n+i with i≠0, so i=σ(a) [L4], and the recursion gives n+σ(a)=σ(n+a) while the left successor law [L2] gives σ(n)+a=σ(n+a), so m=n+σ(a)=σ(n+a)=σ(n)+a, whence a=0 gives m=σ(n) and a≠0 gives σ(n)<m; in every case at least one of m<σ(n), m=σ(n), m>σ(n) holds.

step 1.5givenL2L4L5
3.1

By the induction principle with base 1.4, hypothesis 1.5, and step 2.1, comparability holds for all m,n, and with the incompatibilities 1.1 and 1.2 exactly one of m<n, m=n, m>n holds, so the order is total.

step 1.1step 1.2step 1.4step 2.1discharge-induction∎

Depends on

Used by

…and 10 more results.

Dependency tree · two levels

17 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