Alphabeta Math
CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

Multiplication is a well-defined total operation

Statement

For each m∈Nm \in \mathbb{N} there is a unique function pm:N→Np_m : \mathbb{N} \to \mathbb{N} with pm(0)=0p_m(0) = 0 and pm(σ(n))=pm(n)+mp_m(\sigma(n)) = p_m(n) + m. Writing m⋅n:=pm(n)m \cdot n := p_m(n), multiplication ⋅:N×N→N\cdot : \mathbb{N} \times \mathbb{N} \to \mathbb{N} is a well-defined total binary operation satisfying m⋅0=0m \cdot 0 = 0 and m⋅σ(n)=m⋅n+mm \cdot \sigma(n) = m \cdot n + m.

Facts & Assumptions

Given: N\mathbb{N} with successor σ\sigma and addition ++ (Addition of natural numbers).

[L1]

The recursion theorem (The recursion theorem).

[L2]

For fixed mm, the map addm:x↦x+m\mathrm{add}_m : x \mapsto x + m is a function N→N\mathbb{N} \to \mathbb{N} (Addition of natural numbers).

[L3]

(N,0,σ)(\mathbb{N}, 0, \sigma) is a Peano system (The von Neumann naturals form a Peano system).

Proof

technique · direct
1.1

Fix m∈Nm \in \mathbb{N}; the map addm:N→N\mathrm{add}_m : \mathbb{N} \to \mathbb{N}, addm(x)=x+m\mathrm{add}_m(x) = x + m, is a well-defined function.

L2
2.1

Since (N,0,σ)(\mathbb{N}, 0, \sigma) is a Peano system [L3], apply the recursion theorem with A=NA = \mathbb{N}, a=0a = 0, f=addmf = \mathrm{add}_m: there is a unique pm:N→Np_m : \mathbb{N} \to \mathbb{N} with pm(0)=0p_m(0) = 0 and pm(σ(n))=addm(pm(n))=pm(n)+mp_m(\sigma(n)) = \mathrm{add}_m(p_m(n)) = p_m(n) + m.

L1L3step 1.1
3.1

Define m⋅n:=pm(n)m \cdot n := p_m(n); as pmp_m is total for each m∈Nm \in \mathbb{N}, the assignment (m,n)↦m⋅n(m,n) \mapsto m \cdot n is a well-defined function N×N→N\mathbb{N} \times \mathbb{N} \to \mathbb{N} with m⋅0=0m \cdot 0 = 0 and m⋅σ(n)=m⋅n+mm \cdot \sigma(n) = m \cdot n + m.

step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 19 results over 11 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources