Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28
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.

In a field, the additive multiple n1Fn \cdot 1_F is the canonical natural ι(n)\iota(n): the additive power of the group-power definition and the canonical natural are the same function, both being the unique one given by the recursion ι(0)=0F\iota(0) = 0_F, ι(σ(n))=ι(n)+1F\iota(\sigma(n)) = \iota(n) + 1_F

Statement

Let FF be a field (Field), which is a ring by Every field is a commutative ring with 101 \ne 0; it is an integral domain, and it is a commutative division ring. Two functions NF\mathbb{N} \to F are in play:

These are the same function: ι(n)=n1F\iota(n) = n \cdot 1_F for every nNn \in \mathbb{N}. In particular the notation n1Fn \cdot 1_F used by The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field and the notation n1Fn \cdot 1_F used by Powers gng^{n}: natural exponents in a monoid and integer exponents in a group, with g0=eg^{0} = e denote the same element of FF, and no second notion is in play.

Facts & Assumptions

Given: A field FF with 0F0_F and 1F1_F, the map ι:NF\iota : \mathbb{N} \to F of The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field, and the additive natural powers of Powers gng^{n}: natural exponents in a monoid and integer exponents in a group, with g0=eg^{0} = e in the group (F,+,0F)(F,+,0_F).

[L2]

ι(0)=0F\iota(0) = 0_F and ι(n+1)=ι(n)+1F\iota(n+1) = \iota(n) + 1_F for every nNn \in \mathbb{N} (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field).

[L3]

The additive natural powers satisfy 0a=0F0 \cdot a = 0_F and σ(n)a=na+a\sigma(n) \cdot a = n \cdot a + a for every nNn \in \mathbb{N} and every aFa \in F (Powers gng^{n}: natural exponents in a monoid and integer exponents in a group, with g0=eg^{0} = e).

[L4]

On N\mathbb{N}: m+0=mm + 0 = m and m+σ(n)=σ(m+n)m + \sigma(n) = \sigma(m+n), so n+1=σ(n)n + 1 = \sigma(n) (Addition of natural numbers, The natural numbers N\mathbb{N} (von Neumann)).

[L5]

The recursion theorem: for a set AA, an element aAa \in A and a function u:AAu : A \to A there is exactly one g:NAg : \mathbb{N} \to A with g(0)=ag(0) = a and g(σ(n))=u(g(n))g(\sigma(n)) = u(g(n)) (The recursion theorem).

Proof

technique · direct
1.1

Let u:FFu : F \to F be the function u(t)=t+1Fu(t) = t + 1_F, which is a function from FF to FF because addition is a binary operation on FF. By [L5] applied with A=FA = F, a=0Fa = 0_F and this uu, there is exactly one function g:NFg : \mathbb{N} \to F satisfying g(0)=0Fg(0) = 0_F and g(σ(n))=g(n)+1Fg(\sigma(n)) = g(n) + 1_F for every nNn \in \mathbb{N}.

L1L5
1.2

The map ι\iota satisfies those two equations: ι(0)=0F\iota(0) = 0_F by [L2], and ι(σ(n))=ι(n+1)=ι(n)+1F\iota(\sigma(n)) = \iota(n+1) = \iota(n) + 1_F by [L2] together with n+1=σ(n)n + 1 = \sigma(n).

L2L4
1.3

The map nn1Fn \mapsto n \cdot 1_F satisfies them too: 01F=0F0 \cdot 1_F = 0_F and σ(n)1F=n1F+1F\sigma(n)\cdot 1_F = n \cdot 1_F + 1_F, both by [L3] with a=1Fa = 1_F.

L3
2.1

By the uniqueness clause of step 1.1, the two functions of steps 1.2 and 1.3 are equal, so ι(n)=n1F\iota(n) = n \cdot 1_F for every nNn \in \mathbb{N}.

step 1.1step 1.2step 1.3L5

Remarks

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 57 results over 17 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