Alphabeta Math
CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29
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.

∑k<n+1(nk)=2n, and ∑k<n+1(−1)kι ⁣(nk)=0 for n≥1

Statement

  1. The row sum. For every n∈N, in N, ∑k<n+1(nk)=2 n.
  2. The alternating row sum. For every n≥1, in R, ∑k<n+1(−1)k ι(nk)=0.

Clause 2 is false at n=0, where the sum has the single term (−1)0ι(00)=1. The hypothesis n≥1 is therefore part of the statement, and this page's companion records the version that drops it as a false statement.

Facts & Assumptions

Given: A natural n, a finite set A with ∣A∣=n, and ι the canonical natural (The canonical natural ι(n)=n⋅1F of a field).

[L1]

The binomial theorem: (x+y)n=∑k<σ(n)ι(nk)xky n−k for reals x, y (The binomial theorem in R: (x+y)n=∑k<n+1ι ⁣(nk) xky n−k).

[L2]

∣P(A)∣=2 n (∣P(A)∣=2∣A∣ for finite A), and ∣[A]k∣=(nk), with [A]k=∅ for k>n (The set [A]k of k-element subsets and the binomial coefficient (nk):=∣[n]k∣).

[L4]

ι is additive, multiplicative and injective, and ι(∑k<NNak)=∑k<NRι(ak) (clauses 0, 6 and 7 of Laws of finite sums and products in N, and ι(∑k<nak)=∑k<nι(ak)).

[L5]

Powers: ι(mj)=ι(m)j (Exponentiation of natural numbers, mn, and its agreement with the integer power in R, clause (d)); a0=1 and aσ(j)=aja, so 1j=1 and 0j=0 for j≥1 (Integer powers am, Multiplication by zero: 0⋅a=0, Field).

[L6]

Real finite sums: the recursion clauses and the scaling clause (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

Proof

technique · direct
1.1

Clause 1, by counting. Every S⊆A satisfies ∣S∣≤n by [L7], so P(A) is the union of the sets [A]k for k∈σ(n)={0,1,…,n}; these are pairwise disjoint, since S determines ∣S∣. By [L3] and [L2], 2 n=∣P(A)∣=∑k∈σ(n)∣[A]k∣=∑k<σ(n)(nk), the last equality being the bridge for an index set that is a natural number.

L2L3L7
1.2

Clause 2. Apply [L1] with x=−1 and y=1. The left-hand side is (−1+1)n=0 n, which is 0 because n≥1 ([L5]). The right-hand side is ∑k<σ(n)ι(nk)(−1)k1 n−k=∑k<σ(n)(−1)kι(nk), using 1j=1 from [L5]. Hence the alternating sum is 0.

L1L5
2.1

Clause 1 again, from the binomial theorem, as a check that the two routes agree. Taking x=y=1 in [L1] gives (1+1)n=∑k<σ(n)ι(nk), and the right-hand side is ι(∑k<σ(n)N(nk)) by the bridge clause of [L4], while the left-hand side is ι(2)n=ι(2 n) by [L5]. Since ι is injective, ∑k<σ(n)N(nk)=2 n, which is step 1.1.

step 1.1L1L4L5
2.2

The hypothesis of clause 2 is not removable. At n=0 the sum is ∑k<1(−1)kι(0k)=(−1)0ι(00)=1⋅1=1≠0, by [L6], (00)=1 and a0=1. What fails in the argument of step 1.2 is exactly one thing: (−1+1)0=00=1 rather than 0.

step 1.2L2L5L6
3.1

Clause 1 is step 1.1, confirmed by step 2.1; clause 2 is step 1.2, and step 2.2 shows why it carries the hypothesis n≥1.

step 1.1step 1.2step 2.1step 2.2∎

Remarks

  • Two proofs of the same identity, deliberately. The counting proof is a statement about natural numbers and uses no embedding at all, while the analytic proof goes through R and comes back by the injectivity of ι. Recording both is what makes the agreement of the two readings visible rather than assumed.

  • Where the hypothesis of clause 2 is spent. In 0n=0, and nowhere else. The convention 00=1 is not a defect here: it is what makes the binomial theorem hold at n=0, and the price is that the alternating sum identity acquires a hypothesis. Both facts are consequences of the same convention.

  • The alternating sum is stated in R because (−1)k is not a natural number. The unsigned row sum, by contrast, is an identity between counts and is stated in N.

Depends on

Used by

Dependency tree · two levels

61 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