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

Distributivity and the successor law for multiplication

Statement

For all a,b,c,n∈Na, b, c, n \in \mathbb{N}: (left distributivity) a⋅(b+c)=a⋅b+a⋅ca \cdot (b + c) = a \cdot b + a \cdot c; and (successor-left law) σ(a)⋅n=a⋅n+n\sigma(a) \cdot n = a \cdot n + n.

Facts & Assumptions

Given: multiplication m⋅0=0m \cdot 0 = 0, m⋅σ(n)=m⋅n+mm \cdot \sigma(n) = m \cdot n + m and addition m+0=mm + 0 = m, m+σ(k)=σ(m+k)m + \sigma(k) = \sigma(m + k) (Multiplication of natural numbers, Addition of natural numbers); in particular the addition recursion a+σ(k)=σ(a+k)a + \sigma(k) = \sigma(a + k) is available.

[L1]

Addition is associative (Addition is associative) and commutative (Addition is commutative).

[L2]

The induction principle (The principle of mathematical induction).

Proof

technique · induction on $c$ for distributivity, with a second induction on $n$ for the successor law
1.1

Base c=0c = 0: a⋅(b+0)=a⋅b=a⋅b+0=a⋅b+a⋅0a \cdot (b + 0) = a \cdot b = a \cdot b + 0 = a \cdot b + a \cdot 0, using b+0=bb + 0 = b and a⋅0=0a \cdot 0 = 0.

base
1.2

Inductive hypothesis: a⋅(b+c)=a⋅b+a⋅ca \cdot (b + c) = a \cdot b + a \cdot c.

ih
1.3

Successor-left law σ(a)⋅n=a⋅n+n\sigma(a) \cdot n = a \cdot n + n, by a second induction on nn: base n=0n = 0 gives σ(a)⋅0=0=a⋅0+0\sigma(a) \cdot 0 = 0 = a \cdot 0 + 0; assuming σ(a)⋅n=a⋅n+n\sigma(a) \cdot n = a \cdot n + n, the step gives σ(a)⋅σ(n)=σ(a)⋅n+σ(a)=(a⋅n+n)+σ(a)=a⋅n+(n+σ(a))=a⋅n+σ(n+a)=a⋅n+σ(a+n)=a⋅n+(a+σ(n))=(a⋅n+a)+σ(n)=a⋅σ(n)+σ(n)\sigma(a) \cdot \sigma(n) = \sigma(a) \cdot n + \sigma(a) = (a \cdot n + n) + \sigma(a) = a \cdot n + (n + \sigma(a)) = a \cdot n + \sigma(n + a) = a \cdot n + \sigma(a + n) = a \cdot n + (a + \sigma(n)) = (a \cdot n + a) + \sigma(n) = a \cdot \sigma(n) + \sigma(n), using associativity and commutativity [L1] and a+σ(k)=σ(a+k)a + \sigma(k) = \sigma(a + k).

L1given
2.1

Step: a⋅(b+σ(c))=a⋅σ(b+c)=a⋅(b+c)+a=(a⋅b+a⋅c)+a=a⋅b+(a⋅c+a)=a⋅b+a⋅σ(c)a \cdot (b + \sigma(c)) = a \cdot \sigma(b + c) = a \cdot (b + c) + a = (a \cdot b + a \cdot c) + a = a \cdot b + (a \cdot c + a) = a \cdot b + a \cdot \sigma(c), using b+σ(c)=σ(b+c)b + \sigma(c) = \sigma(b + c), the multiplication recursion, the hypothesis, associativity [L1], and a⋅σ(c)=a⋅c+aa \cdot \sigma(c) = a \cdot c + a.

step 1.2L1
3.1

By induction [L2], a⋅(b+c)=a⋅b+a⋅ca \cdot (b + c) = a \cdot b + a \cdot c for all cc (hence all a,b,ca, b, c) and σ(a)⋅n=a⋅n+n\sigma(a) \cdot n = a \cdot n + n for all a,na, n.

step 2.1step 1.3discharge-induction∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 21 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