4.1 Cancellations in alternating sums
4.1.1 Acceptable sets, partners, and signs
The acceptable sets for parameters \(n, m \in \mathbb {N}\) are the subsets of \(\{ 0, 1, \ldots , n-1\} \) with cardinality at most \(m\):
- AlgebraicCombinatorics.SignedCounting.acceptableSets n m = {I ∈ (Finset.range n).powerset | I.card ≤ m}
The partner of a finite set \(I\) of natural numbers is the symmetric difference \(I' := I \bigtriangleup \{ 0\} \). If \(0 \in I\), then \(I' = I \setminus \{ 0\} \); if \(0 \notin I\), then \(I' = I \cup \{ 0\} \).
The sign of a finite set \(I\) of natural numbers is \(\operatorname {sign}(I) := (-1)^{|I|}\).
The partner operation is an involution: \((I')' = I\) for all finite sets \(I\).
By the self-cancellation property of symmetric difference: \((I \bigtriangleup \{ 0\} ) \bigtriangleup \{ 0\} = I\).
The partner reverses the sign: \(\operatorname {sign}(I') = -\operatorname {sign}(I)\) for all finite sets \(I\).
If \(0 \in I\), then \(|I'| = |I| - 1\); if \(0 \notin I\), then \(|I'| = |I| + 1\). In either case, \((-1)^{|I'|} = -(-1)^{|I|}\).
Let \(n\in \mathbb {C}\) and \(m\in \mathbb {N}\). Then,
The Lean proof delegates to Int.alternating_sum_range_choose_eq_choose from Mathlib.
The source gives a combinatorial proof using sign-reversing involutions. Both sides of the equality are polynomial functions in \(n\), so we can WLOG assume that \(n\) is a positive integer (by the polynomial identity trick). Set \([n] := \{ 1, 2, \ldots , n\} \). Define an acceptable set to be a subset of \([n]\) that has size \(\leq m\). Define the sign of a finite set \(I\) to be \((-1)^{|I|}\). Then
For each finite set \(I\), define the partner of \(I\) to be the set \(I' := I \bigtriangleup \{ 1\} \), where \(\bigtriangleup \) denotes symmetric difference. Each finite set \(I\) satisfies \(I'' = I\) and \(|I'| = |I| \pm 1\), so that \((-1)^{|I'|} = -(-1)^{|I|}\). If both \(I\) and \(I'\) are acceptable sets, then their contributions to the sum cancel each other.
Claim 1: Let \(I\) be an acceptable set. Then, the partner \(I'\) of \(I\) is non-acceptable if and only if \((1 \notin I \text{ and } |I| = m)\).
[Proof of Claim 1: If \(1 \notin I\) and \(|I| = m\), then \(I' = I \cup \{ 1\} \) has size \(|I| + 1 {\gt} m\), so it is non-acceptable. Conversely, if \(I'\) is non-acceptable, then \(1 \notin I\) (otherwise \(I' = I \setminus \{ 1\} \subseteq I\) would be acceptable) and \(|I| = m\) (otherwise \(|I| \leq m - 1\) would give \(|I'| = |I| + 1 \leq m\), making \(I'\) acceptable).]
The acceptable sets with non-acceptable partners are precisely the \(m\)-element subsets of \([n]\) that do not contain \(1\), i.e., the \(m\)-element subsets of \([n] \setminus \{ 1\} \). There are \(\binom {n-1}{m}\) such subsets, each with sign \((-1)^m\). Hence,
This proves Proposition 4.6.
Let \(n \geq 1\), \(m \in \mathbb {N}\), and let \(I\) be an acceptable set (i.e., \(I \subseteq \{ 0, \ldots , n-1\} \) with \(|I| \leq m\)). Then the partner \(I'\) of \(I\) is non-acceptable if and only if \(0 \notin I\) and \(|I| = m\).
By case analysis on whether \(0 \in I\) and the cardinality of \(I\), as outlined in Claim 1 in the proof of Proposition 4.6.
For \(n \geq 1\) and \(m \in \mathbb {N}\),
where \(\mathcal{A} = \mathcal{A}(n, m)\) is the set of acceptable sets (subsets of \(\{ 0, \ldots , n-1\} \) with size \(\leq m\)) and \(\operatorname {sign}(I) = (-1)^{|I|}\).
Partition \(\mathcal{A}\) into “moving” sets (those whose partner is also acceptable) and “fixed” sets (those whose partner is non-acceptable). The sum over moving sets is \(0\) by a sign-reversing involution argument: the partner pairs them up with opposite signs. The sum over fixed sets equals \((-1)^m \binom {n-1}{m}\), since by Theorem 4.7, the fixed sets are precisely the \(m\)-element subsets of \([n] \setminus \{ 0\} \), each contributing \((-1)^m\).
4.1.2 Cancellation principles
Let \(\mathcal{A}\) be a finite set. Let \(\mathcal{X}\) be a subset of \(\mathcal{A}\).
For each \(I \in \mathcal{A}\), let \(\operatorname {sign} I\) be an element of an additive abelian group \(R\) with no \(2\)-torsion (i.e., \(2a = 0\) implies \(a = 0\)). Let \(f : \mathcal{X} \to \mathcal{X}\) be a bijection with the property that
(Such a bijection \(f\) is called sign-reversing.) Then,
We have
Adding \(\sum _{I \in \mathcal{X}} \operatorname {sign} I\) to both sides, we obtain \(2 \cdot \sum _{I \in \mathcal{X}} \operatorname {sign} I = 0\). Since \(R\) has no \(2\)-torsion, \(\sum _{I \in \mathcal{X}} \operatorname {sign} I = 0\).
Now, \(\mathcal{X} \subseteq \mathcal{A}\); hence,
Let \(\mathcal{A}\) be a finite set. Let \(\mathcal{X}\) be a subset of \(\mathcal{A}\).
For each \(I \in \mathcal{A}\), let \(\operatorname {sign} I\) be an element of some additive abelian group. Let \(f : \mathcal{X} \to \mathcal{X}\) be an involution (i.e., a map satisfying \(f \circ f = \operatorname {id}\)) that has no fixed points. Assume that
Then,
All addends corresponding to the \(I \in \mathcal{X}\) cancel out from the sum \(\sum _{I \in \mathcal{A}} \operatorname {sign} I\) (because they come in pairs of addends with opposite signs). The Lean proof uses Mathlib’s Finset.sum_involution.
Let \(\mathcal{A}\) be a finite set. Let \(\mathcal{X}\) be a subset of \(\mathcal{A}\).
For each \(I \in \mathcal{A}\), let \(\operatorname {sign} I\) be an element of some additive abelian group. Let \(f : \mathcal{X} \to \mathcal{X}\) be an involution (i.e., a map satisfying \(f \circ f = \operatorname {id}\)). Assume that
Assume furthermore that
Then,
This is similar to Lemma 4.10, except that the addends corresponding to the \(I \in \mathcal{X}\) satisfying \(f(I) = I\) don’t cancel (but are already zero and thus can be removed right away). The Lean proof uses Mathlib’s Finset.sum_involution, which handles both the pairing and the fixed-point condition.
4.1.3 Switching operations and the \(q\)-binomial at \(q = -1\)
For \(i \in \mathbb {N}\), define the switch operation \(\operatorname {switch}_i\) on finite subsets \(S\) of \(\mathbb {N}\) by
In other words, if exactly one of \(i\) and \(i+1\) belongs to \(S\), then we replace it by the other; otherwise we leave \(S\) unchanged.
The switch operation \(\operatorname {switch}_i\) is an involution, i.e., \(\operatorname {switch}_i(\operatorname {switch}_i(S)) = S\) for all finite sets \(S\).
By case analysis: if exactly one of \(\{ i, i+1\} \) is in \(S\), then the symmetric difference \(S \bigtriangleup \{ i, i+1\} \) restores \(S\) after two applications. Otherwise the operation is the identity.
The switch operation preserves cardinality: \(|\operatorname {switch}_i(S)| = |S|\) for all finite sets \(S\).
When \(|S \cap \{ i, i+1\} | = 1\), the symmetric difference removes one element and adds another. Otherwise the set is unchanged.
4.1.4 Roots of unity
Let \(K\) be a field. Let \(d\) be a positive integer.
(a) A \(d\)-th root of unity in \(K\) means an element \(\omega \) of \(K\) satisfying \(\omega ^d = 1\).
(b) A primitive \(d\)-th root of unity in \(K\) means an element \(\omega \) of \(K\) satisfying \(\omega ^d = 1\) but \(\omega ^i \neq 1\) for each \(i \in \{ 1, 2, \ldots , d-1\} \). In other words, a primitive \(d\)-th root of unity in \(K\) means an element of the multiplicative group \(K^{\times }\) whose order is \(d\).
In any integral domain where \(-1 \neq 1\), the element \(-1\) is a primitive \(2\)nd root of unity.
We have \((-1)^2 = 1\) and \((-1)^1 = -1 \neq 1\).
If \(\omega \) is a primitive \(d\)-th root of unity with \(d {\gt} 1\), then
This is IsPrimitiveRoot.geom_sum_eq_zero from Mathlib.
4.1.5 The \(q\)-Lucas theorem
The \(q\)-binomial coefficient \(\binom {n}{k}_q\) is the polynomial in \(\mathbb {Z}[q]\) defined by
where \(\operatorname {sum}(S) = \sum _{x \in S} x\). This is the local definition used in the formalization; it agrees with Mathlib’s \(q\)-binomial coefficient (see Lemma 4.19).
- AlgebraicCombinatorics.SignedCounting.qBinomial n k = ∑ S ∈ (Finset.range n).powerset with S.card = k, Polynomial.X ^ (S.sum id - (Finset.range k).sum id)
The local \(q\)-binomial coefficient \(\binom {n}{k}_q\) (Definition 4.18) equals Mathlib’s \(q\)-binomial coefficient \(\binom {n}{k}_q\) (as a polynomial in \(\mathbb {Z}[q]\)).
Both definitions agree: they are sums over \(k\)-element subsets of \(\{ 0,\ldots ,n-1\} \), with monomials \(q^{(\operatorname {sum}(S) - k(k-1)/2)}\). The proof establishes the identity by showing the exponents coincide using the order embedding of \(S\) into \(\{ 0,\ldots ,n-1\} \).
For \(n, k \in \mathbb {N}\), \(\binom {n}{k}_q \big|_{q=1} = \binom {n}{k}\).
Each term evaluates to \(1\) at \(q = 1\), so the sum counts the number of \(k\)-element subsets of \([n]\), which is \(\binom {n}{k}\).
For \(n {\lt} k\), \(\binom {n}{k}_q = 0\).
There are no \(k\)-element subsets of \([n]\) when \(n {\lt} k\).
For all \(n \in \mathbb {N}\), \(\binom {n}{0}_q = 1\).
The only \(0\)-element subset is \(\varnothing \), contributing \(q^0 = 1\).
For all \(n \in \mathbb {N}\), \(\binom {n}{n}_q = 1\).
The only \(n\)-element subset of \([n]\) is \([n]\) itself, contributing \(q^0 = 1\).
A subset \(S \subseteq \{ 0, \ldots , n-1\} \) is \(d\)-blocky if \(S \subseteq \{ 0, \ldots , n-1\} \) and for each block index \(i \in \{ 0, \ldots , \lfloor n/d \rfloor - 1\} \), either all elements of \(\{ id, id+1, \ldots , id+d-1\} \) are in \(S\) or none are.
The set \(\binom {[n]}{k}\) of \(k\)-element subsets of \(\{ 0, \ldots , n-1\} \):
The set of \(d\)-blocky \(k\)-element subsets of \(\{ 0, \ldots , n-1\} \):
For \(d {\gt} 0\), the number of \(d\)-blocky \(k\)-element subsets of \(\{ 0, \ldots , n-1\} \) is
A \(d\)-blocky \(k\)-element subset is uniquely determined by the pair \((B, P)\) where \(B \subseteq \{ 0, \ldots , n/d - 1\} \) selects which complete \(d\)-blocks are fully included (giving \(|B| \cdot d\) elements) and \(P \subseteq \{ 0, \ldots , n \bmod d - 1\} \) selects which elements of the partial block are included (giving \(|P|\) elements). The constraint \(|S| = k\) forces \(|B| = k / d\) and \(|P| = k \bmod d\). If \(k \bmod d {\gt} n \bmod d\), no valid \(P\) exists.
Let \(K\) be a field. Let \(d\) be a positive integer. Let \(\omega \) be a primitive \(d\)-th root of unity in \(K\). Let \(n, k \in \mathbb {N}\). Let \(q\) and \(u\) be the quotients obtained when dividing \(n\) and \(k\) by \(d\) with remainder, and let \(r\) and \(v\) be the respective remainders. Then,
The proof splits into cases:
Case \(d = 1\): Then \(\omega = 1\), and both sides reduce to \(\binom {n}{k}\) by Lemma 4.20.
Case \(k {\gt} n\): Both sides are \(0\).
Case \(n {\lt} d\): Then \(n / d = 0\), \(n \bmod d = n\), and the formula reduces to \(\binom {n}{k}_\omega = \binom {0}{k/d} \cdot \binom {n}{k \bmod d}_\omega \).
Main case (\(d \geq 2\), \(k \leq n\), \(n \geq d\)): The proof has three steps:
Rewrite \(\binom {n}{k}_\omega \) as \(\sum _{S \in \mathcal{A}} \omega ^{(\operatorname {sum}(S) - \text{baseline})}\) where \(\mathcal{A}\) is the set of \(k\)-element subsets of \([n]\).
Split the sum into contributions from \(d\)-blocky subsets (those that consist of entire \(d\)-blocks) and non-\(d\)-blocky subsets.
Show that non-blocky contributions cancel (Lemma 4.29) and that the blocky contributions give the product formula (Lemma 4.31).
A subset \(S\) of \([n]\) is \(d\)-blocky if for each complete \(d\)-block \(\{ id, id+1, \ldots , id+d-1\} \) contained in \([n]\), either all elements of the block are in \(S\) or none are.
Let \(K\) be a field, \(d \geq 2\), and \(\omega \) a primitive \(d\)-th root of unity. For \(n, k \in \mathbb {N}\),
For each non-\(d\)-blocky set \(S\), there exists a “split block” \(i\): a block index where \(S\) contains some but not all elements of \(\{ id, id+1, \ldots , id+d-1\} \). Define the rotation operation that cyclically permutes elements within block \(i\) (replacing each element \(x\) in the block by \(id + (x - id + 1) \bmod d\)).
The non-blocky sets are partitioned into orbits under rotation in the smallest split block. Each orbit has size \(m = d / \gcd (d, j)\) where \(j = |S \cap \text{block}_i|\), and \(m {\gt} 1\) since \(0 {\lt} j {\lt} d\). The sum over each orbit is \(0\) by Lemma 4.30. Therefore the total sum is \(0\).
The Lean proof applies Lemma 4.41 to the full set of non-blocky subsets, verifying orbit-closure (rotation preserves membership via Lemmas 4.36 and 4.37).
Let \(K\) be a field, \(d \geq 2\), and \(\omega \) a primitive \(d\)-th root of unity. For \(0 {\lt} j {\lt} d\) and any \(b \in \mathbb {N}\), let \(m = d / \gcd (d, j)\). Then
Factor out \(\omega ^b\): \(\sum _{k=0}^{m-1} \omega ^{b + kj} = \omega ^b \sum _{k=0}^{m-1} (\omega ^j)^k\). Since \(0 {\lt} j {\lt} d\), we have \(\omega ^j \neq 1\) and \((\omega ^j)^m = 1\). The sum \(\sum _{k=0}^{m-1} (\omega ^j)^k\) can be evaluated using the geometric series formula \(\frac{(\omega ^j)^m - 1}{\omega ^j - 1} = 0\).
Let \(K\) be a field, \(d\) a positive integer, and \(\omega \) a primitive \(d\)-th root of unity. For \(n, k \in \mathbb {N}\),
A \(d\)-blocky \(k\)-element subset of \([n]\) decomposes into two independent parts: which complete \(d\)-blocks to include (choosing \(k/d\) blocks from \(n/d\) available) and which elements of the partial block \(\{ (n/d) \cdot d, \ldots , n-1\} \) to include (choosing \(k \bmod d\) elements from \(n \bmod d\) available).
The complete-block part contributes a factor of \(1\) (since \(\omega ^d = 1\)) and the partial-block part contributes \(\omega ^{(\text{sum of partial part})}\). The number of complete-block configurations is \(\binom {n/d}{k/d}\), and the partial-block sum gives \(\binom {n \bmod d}{k \bmod d}_{\omega }\).
The rotation function within block \(i\) is injective (for \(d {\gt} 0\)).
By case analysis on whether \(x\) and \(y\) are in block \(i\), and using injectivity of the modular arithmetic operation.
Rotating \(d\) times within block \(i\) returns to the identity: \((\operatorname {rotate}_i)^d(x) = x\) for all \(x\).
For \(x\) in block \(i\), after \(k\) rotations the offset becomes \((x - id + k) \bmod d\). After \(d\) rotations, the offset returns to its original value. For \(x\) outside block \(i\), the rotation is the identity.
For a primitive \(d\)-th root of unity \(\omega \),
The rotation changes \(\operatorname {sum}(S)\) by \(|\text{blockOffsets}(d, i, S)| \pmod{d}\) per iteration. Since \(\omega ^d = 1\), the congruence modulo \(d\) suffices.
For \(0 {\lt} j {\lt} d\) where \(j = |\text{blockOffsets}(d, i, S)|\) and \(m = d / \gcd (d, j)\), the map \(k \mapsto \operatorname {rotate}_i^k(S)\) is injective on \(\{ 0, 1, \ldots , m-1\} \).
If \(\operatorname {rotate}_i^{k_1}(S) = \operatorname {rotate}_i^{k_2}(S)\) with \(k_1 {\lt} k_2 {\lt} m\), then \(k_1 \cdot j \equiv k_2 \cdot j \pmod{d}\). By modular arithmetic cancellation, \(m \mid (k_2 - k_1)\), contradicting \(0 {\lt} k_2 - k_1 {\lt} m\).
Rotation preserves cardinality: for \(d {\gt} 0\), \(|\operatorname {rotate}_i^k(S)| = |S|\).
The rotation function \(\operatorname {rotate}_i\) is injective (Lemma 4.32), so the image of \(S\) under \(\operatorname {rotate}_i\) has the same cardinality. The result follows by induction on \(k\).
Rotation preserves the ambient set: for \(d {\gt} 0\) and \(i {\lt} n/d\), if \(S \subseteq \{ 0, \ldots , n-1\} \) then \(\operatorname {rotate}_i^k(S) \subseteq \{ 0, \ldots , n-1\} \).
Elements outside block \(i\) are unchanged. Elements inside block \(i\) stay within \(\{ id, \ldots , id+d-1\} \subseteq \{ 0, \ldots , n-1\} \) by the modular arithmetic of the rotation.
Rotating \(d\) times is the identity on sets: \(\operatorname {rotate}_i^d(S) = S\) for all sets \(S\).
Since \((\operatorname {rotate}_i)^d = \operatorname {id}\) on elements (Lemma 4.33), the image of \(S\) after \(d\) rotations equals \(S\).
Let \(\omega \) be a primitive \(d\)-th root of unity with \(d \geq 2\). For \(0 {\lt} j {\lt} d\) and any \(b \in \mathbb {N}\),
Since \(m = d / \gcd (d, j)\) divides \(d\), the sum over the full range \(\{ 0, \ldots , d-1\} \) is a sum of \(d/m\) copies of the orbit sum \(\sum _{k=0}^{m-1} \omega ^{b + kj}\), which is \(0\) by Lemma 4.30.
For \(d {\gt} 0\) and any set \(S\), the fibers of the map \(k \mapsto \operatorname {rotate}_i^k(S)\) on \(\{ 0, \ldots , d-1\} \) all have the same cardinality. That is, there exists \(c\) such that for every set \(T\) in the image, the number of \(k \in \{ 0, \ldots , d-1\} \) with \(\operatorname {rotate}_i^k(S) = T\) is exactly \(c\), and \(c \mid d\).
By the orbit-stabilizer theorem for the cyclic group \(\mathbb {Z}/d\) acting on sets via rotation. The stabilizer of \(S\) consists of those \(k\) with \(\operatorname {rotate}_i^k(S) = S\); all fibers have the same size as the stabilizer. The result follows from \(|\operatorname {orbit}| \cdot |\operatorname {stab}| = d\).
For any orbit-closed subset \(A\) of the non-blocky \(k\)-element subsets of \([n]\),
Here “orbit-closed” means that \(A\) is closed under rotation in the smallest split block of each element: for each \(S \in A\), the entire orbit of \(S\) under rotation in its smallest split block is contained in \(A\).
By strong induction on \(|A|\). If \(A\) is empty, the sum is \(0\). Otherwise, pick \(S_0 \in A\), let \(i_0\) be its smallest split block index, and let \(O\) be the orbit of \(S_0\) under rotation in block \(i_0\) (all \(d\) rotations). Since \(A\) is orbit-closed, \(O \subseteq A\). The sum over \(O\) is \(0\) by Lemma 4.39 and Lemma 4.40 (the sum over the image equals a constant times the sum over the fibers, which is zero). Then \(\sum _{S \in A} \omega ^{\operatorname {sum}(S)} = \sum _{S \in O}(\cdots ) + \sum _{S \in A \setminus O}(\cdots ) = 0 + 0\) by the inductive hypothesis on \(A \setminus O\) (which is orbit-closed and has strictly smaller cardinality).
4.1.6 The \(q\)-binomial at \(q = -1\)
Let \(n, k \in \mathbb {N}\). Then:
By Theorem 4.28 with \(d = 2\) and \(\omega = -1\) (which is a primitive \(2\)nd root of unity by Lemma 4.16):
The only possible remainders upon division by \(2\) are \(0\) and \(1\), and the base-case \((-1)\)-binomial coefficients are:
If \(n\) is even and \(k\) is odd, then \(n \bmod 2 = 0\) and \(k \bmod 2 = 1\), so \(\binom {n \bmod 2}{k \bmod 2}_{-1} = 0\) and the result is \(0\). Otherwise, \(\binom {n \bmod 2}{k \bmod 2}_{-1} = 1\) and the result is \(\binom {\lfloor n/2 \rfloor }{\lfloor k/2 \rfloor }\).
The Lean proof applies the \(q\)-Lucas theorem (Theorem 4.28) with \(d = 2\) over \(\mathbb {Q}\), then uses injectivity of \(\mathbb {Z} \hookrightarrow \mathbb {Q}\) to transfer the result back to \(\mathbb {Z}\).