Alphabeta Math
DefinitionDefinition: AI-adaptedProof: AI-generatedverified 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.

Finite sums and finite products of natural numbers, ∑k<nak and ∏k<nak in N

Definition

Let a:N→N, written ak for a(k), with addition and multiplication of natural numbers as in Addition of natural numbers and Multiplication of natural numbers. Finite sums and finite products of a inside N are defined by recursion on the upper index, which is legitimate by the recursion theorem (The recursion theorem).

That theorem produces a function of one variable, so the running index has to be carried inside the value. Apply it to the set A=N×N, the starting element (0,0) and the function f(k,s)=(σ(k), s+ak): there is a unique g:N→N×N with

g(0)=(0,0),g(σ(n))=f(g(n))(n∈N).

Write g(n)=(π1(g(n)), Sn) for its two coordinates.

The first coordinate is the index itself, and that is an induction, not an observation (The principle of mathematical induction). Indeed π1(g(0))=0; and if π1(g(n))=n then g(σ(n))=f(π1(g(n)),Sn)=(σ(π1(g(n))), Sn+aπ1(g(n)))=(σ(n), Sn+an), so π1(g(σ(n)))=σ(n). Only now may the second coordinates of the two displayed clauses be read off, and doing so gives

S0=0,Sσ(n)=Sn+an.

S is moreover the unique function N→N with those two properties: if S′ also has them then n↦(n,Sn′) satisfies the two clauses defining g, hence equals g by the uniqueness clause of The recursion theorem, so S′=S. We write

∑k<nak:=Sn.

The same construction with starting element (0,1) and f(k,p)=(σ(k), p⋅ak), with the same induction on the first coordinate and the same uniqueness argument, gives the unique P:N→N with

P0=1,Pσ(n)=Pn⋅an,

and we write ∏k<nak:=Pn.

The empty sum is 0 and the empty product is 1, by the base clause of the recursion and by nothing else: no convention is imported from anywhere.

Notation. We abbreviate ∑k=0nak:=∑k<n+1ak and likewise for products, using σ(n)=n+1. Only finitely many values of a enter ∑k<nak, so the notation is also used for a list a0,…,an−1 of naturals given without reference to any extension to all of N: extend the list by ak=0 (respectively ak=1) for k≥n and apply the definition. Where the two kinds of finite sum have to be told apart, we write ∑N and ∏N for the ones defined here and ∑R, ∏R for those of Finite sums and finite products, by recursion; elsewhere the ambient set is fixed by the terms being summed.

Truncated difference, fixed here for the whole page. For m,n∈N we write n−m for the unique j∈N with m+j=n when m≤n, and for 0 when n<m. Existence in the first case is the definition of ≤ (Order on the natural numbers) and uniqueness is commutativity with cancellation (Addition is commutative, Addition is cancellative). The two cases are exhaustive and mutually exclusive, since exactly one of m<n, m=n, n<m holds (Trichotomy of the order on N), so the notation names a single natural number for every m and n. Every use of n−m on this page is this operation; no negative number is ever formed, and where a statement is true only under m≤n that hypothesis is written out.

Remarks

  • Why a second finite sum is needed at all. Finite sums and finite products, by recursion defines ∑k<nak for a sequence of reals, and its value is a real number. Every count on this page is a natural number, so the sum rule, the row sums of Pascal's triangle, the condition ∑iki=n on a multinomial coefficient and the stars-and-bars count all need a sum that stays in N. The two notions are related, not rival: the bridge ι(∑k<nNak)=∑k<nRι(ak) is proved in the next item, and it is what lets an identity between counts be read inside R and back.

  • The monoid version, later. The same recursion is carried out in an arbitrary monoid in The product g0g1⋯gn−1 of a finite list in a monoid, by recursion, with the empty product (n=0) equal to the identity ↗, which comes later in the reading order; (N,+,0) and (N,⋅,1) are instances of it, and the agreement is immediate because the recursion clauses are identical. That pointer is orientation only: nothing here depends on it, and the notion defined above is complete as it stands.

  • 0 is an index. ∑k<n runs over k=0,1,…,n−1, so ∑k<1ak=a0 and ∑k<0ak=0. A claim about ∑k<nak must be checked at n=0, where it is a claim about 0, and a claim about ∏k<nak at n=0, where it is a claim about 1.

Depends on

Used by

Dependency tree · two levels

33 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