LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-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.

$\sum_{j < m + 1} (- 1)^{j} ι (\binom{t}{j}) = (- 1)^{m} ι (\binom{t - 1}{m})$ for every $t \geq 1$ and every $m$

Statement

Let $t \in N$ with $t \geq 1$ and let $m \in N$ . Then, in $R$ ,

$\sum_{j < m + 1} (- 1)^{j} ι (\binom{t}{j}) = (- 1)^{m} ι (\binom{t - 1}{m}),$

where $ι$ is the canonical natural (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field), the binomial coefficients are the counts of The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ , and $t - 1$ is the truncated difference of Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ , which for $t \geq 1$ is the ordinary one, so that $(t - 1) + 1 = t$ .

The hypothesis $t \geq 1$ is part of the statement. At $t = 0$ and $m = 1$ the left-hand side is $ι (\binom{0}{0}) - ι (\binom{0}{1}) = 1$ , while the truncated difference gives $t - 1 = 0$ and the right-hand side is $- ι (\binom{0}{1}) = 0$ .

Two readings worth recording. At $m = 0$ both sides are $1$ , since $(\binom{t}{0}) = (\binom{t - 1}{0}) = 1$ . For $m \geq t$ both sides are $0$ : the terms of the left-hand side with $j > t$ vanish and the remaining sum is the full alternating row sum of $t$ , which vanishes because $t \geq 1$ , while $(\binom{t - 1}{m}) = 0$ because $m > t - 1$ .

Facts & Assumptions

Given: Naturals $t \geq 1$ and $m$ ; the abbreviation $s : = t - 1$ , so that $s + 1 = t$ (Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ , Order on the natural numbers); the real finite sum of Finite sums and finite products, by recursion; and integer powers (Integer powers $a^{m}$ ) in the ordered field $R$ (Ordered field, Field).

[L1]

Induction: a property holding at $0$ and inherited by successors holds at every natural (The principle of mathematical induction).

[L2]

Recursion clauses of the real finite sum: $\sum_{j < 0} u_{j} = 0$ and $\sum_{j < p + 1} u_{j} = \sum_{j < p} u_{j} + u_{p}$ (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L3]

Pascal's rule, with no restriction relating the two indices: $(\binom{n + 1}{k + 1}) = (\binom{n}{k}) + (\binom{n}{k + 1})$ for all $n, k \in N$ (Pascal's rule $(\binom{n + 1}{k + 1}) = (\binom{n}{k}) + (\binom{n}{k + 1})$ , and the hockey-stick identity $\sum_{i \leq n} (\binom{i}{k}) = (\binom{n + 1}{k + 1})$ , clause 1).

[L4]

$(\binom{n}{0}) = 1$ for every $n$ (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ); $ι (1) = 1$ and $ι$ is additive (Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ , clause 0, The canonical natural $ι (n) = n \cdot 1_{F}$ of a field).

[L5]

Powers of $- 1$ : $(- 1)^{0} = 1$ and $(- 1)^{p + 1} = (- 1)^{p} \cdot (- 1) = - (- 1)^{p}$ (Integer powers $a^{m}$ ).

Proof

technique · induction

1.1

Fix $t \geq 1$ and write $s : = t - 1$ , so that $s + 1 = t$ ; the claim is proved by induction on $m$ , for this fixed $t$ .

given

1.2

Base case $m = 0$ . By [L2] the left-hand side is the single term $(- 1)^{0} ι (\binom{t}{0})$ , which is $1$ by [L4] and [L5]; and the right-hand side is $(- 1)^{0} ι (\binom{s}{0}) = 1$ for the same reason.

baseL2L4L5

1.3

Inductive hypothesis: fix $m$ and assume $\sum_{j < m + 1} (- 1)^{j} ι (\binom{t}{j}) = (- 1)^{m} ι (\binom{s}{m})$ .

1.4

Pascal's rule at $n = s$ and $k = m$ , together with $s + 1 = t$ , gives $(\binom{t}{m + 1}) = (\binom{s}{m}) + (\binom{s}{m + 1})$ , hence $ι (\binom{t}{m + 1}) = ι (\binom{s}{m}) + ι (\binom{s}{m + 1})$ by the additivity of $ι$ .

L3L4

2.1

By the recursion clause of [L2] and the hypothesis of step 1.3, $\sum_{j < m + 2} (- 1)^{j} ι (\binom{t}{j}) = (- 1)^{m} ι (\binom{s}{m}) + (- 1)^{m + 1} ι (\binom{t}{m + 1})$ .

step 1.3L2

3.1

Substituting step 1.4 into step 2.1 and using $(- 1)^{m + 1} = - (- 1)^{m}$ from [L5]: $(- 1)^{m} ι (\binom{s}{m}) + (- 1)^{m + 1} (ι (\binom{s}{m}) + ι (\binom{s}{m + 1})) = (- 1)^{m} ι (\binom{s}{m}) - (- 1)^{m} ι (\binom{s}{m}) + (- 1)^{m + 1} ι (\binom{s}{m + 1}) = (- 1)^{m + 1} ι (\binom{s}{m + 1})$ .

step 1.4step 2.1L5algebra

4.1

So the claim holds at $m + 1$ whenever it holds at $m$ , and it holds at $m = 0$ ; by [L1] it holds for every $m \in N$ , for the fixed $t \geq 1$ , which was arbitrary.

step 1.2step 1.3step 3.1L1discharge-induction∎

Remarks

Where $t \geq 1$ is spent. In exactly one place: the identity $s + 1 = t$ , which is what lets Pascal's rule be applied with upper index $s + 1$ . Under the truncated difference the equation $s + 1 = t$ fails at $t = 0$ , where $s = 0$ and $s + 1 = 1$ , and the statement fails there too.
Why not the full alternating row sum. The published corollary of the binomial theorem gives the sum over the whole row, and only for $t \geq 1$ . A truncation of that row is a different quantity, and the identity above is what says how far a truncation misses: by exactly one binomial coefficient of the row above, with the sign of the last term kept.

Depends on

Used by

Dependency tree · two levels

51 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

Binomial coefficient (Wikipedia) (standard reference, not scraped)
Pascal's rule (Wikipedia) (standard reference, not scraped)
Inclusion-exclusion principle (Wikipedia) (standard reference, not scraped)
Indicator Functions and Inclusion-Exclusion (University of South Carolina notes) (standard reference, not scraped)

∑j<m+1(−1)j ι(tj)=(−1)m ι(t−1m)∑j<m+1​(−1)jι(jt​)=(−1)mι(mt−1​) for every t≥1t≥1 and every mm