Cancellations in Alternating Sums

This file formalizes the theory of cancellations in alternating sums using sign-reversing bijections and involutions. The main results include:

• The negative hockey-stick identity for binomial coefficients
• Three versions of the cancellation principle (Lemmas sign_cancel1, sign_cancel2, sign_cancel3)
• The evaluation of q-binomial coefficients at q = -1
• The q-Lucas theorem for primitive roots of unity

Main definitions

• acceptableSets: A finset of subsets of Finset.range n with cardinality at most m
• partner: The symmetric difference of a set with {0}, used for sign-reversing
• setSign: The sign (-1)^|I| of a finite set I
• switch: Swap elements i and i+1 in a set when exactly one is present
• IsBlocky: A subset that is a union of consecutive pairs (blocks)
• IsRootOfUnity: An element ω satisfying ω^d = 1
• qBinomial: The q-binomial coefficient [n choose k]_q (local definition as Polynomial ℤ)

Main results

• negHockeyStick: The negative hockey-stick identity ∑ k ∈ Finset.range (m+1), (-1)^k * (n.choose k) = (-1)^m * (n-1).choose m
• sign_cancel1: Cancellation principle for sign-reversing bijections
• sign_cancel2: Cancellation principle for sign-reversing involutions without fixed points
• sign_cancel3: Cancellation principle for sign-reversing involutions with zero-sign fixed points
• qBinom_neg_one: Formula for q-binomial coefficients evaluated at q = -1
• qLucas: The q-Lucas theorem for primitive roots of unity
• qBinomial_eq_canonical: Bridge lemma connecting local qBinomial to AlgebraicCombinatorics.qBinomialPoly

Note on qBinomial: This file defines a local qBinomial as a Polynomial ℤ using the subset sum formula. This is equivalent to AlgebraicCombinatorics.qBinomialPoly in QBinomialBasic.lean. The theorem qBinomial_eq_canonical proves this equivalence. The local definition is in namespace AlgebraicCombinatorics.SignedCounting to avoid conflicts.

References

• Section on "Cancellations in alternating sums" from Algebraic Combinatorics notes
• Labels: prop.binom.nhs, lem.sign.cancel1, lem.sign.cancel2, lem.sign.cancel3, exe.sign.-1inom, def.root-of-unity.prim, thm.sign.q-lucas

Tags

alternating sums, sign-reversing involution, cancellation principle, q-binomial, hockey-stick identity, roots of unity, q-Lucas theorem

Acceptable Sets and Partners

We define acceptable sets (subsets of {0, 1, ..., n-1} with size at most m) and the partner operation (symmetric difference with {0}).

def AlgebraicCombinatorics.SignedCounting.acceptableSets (n m : ℕ) : Finset (Finset ℕ)

The finset of acceptable sets: subsets of Finset.range n with cardinality at most m.

Equations

• AlgebraicCombinatorics.SignedCounting.acceptableSets n m = {I ∈ (Finset.range n).powerset | I.card ≤ m}

def AlgebraicCombinatorics.SignedCounting.partner (I : Finset ℕ) : Finset ℕ

The partner of a finite set I is I △ {0} (symmetric difference with singleton 0). If 0 ∈ I, this removes 0; if 0 ∉ I, this adds 0.

Equations

• AlgebraicCombinatorics.SignedCounting.partner I = symmDiff I {0}

theorem AlgebraicCombinatorics.SignedCounting.partner_partner (I : Finset ℕ) : partner (partner I) = I

The partner operation is an involution.

theorem AlgebraicCombinatorics.SignedCounting.partner_card (I : Finset ℕ) : (partner I).card = I.card + 1 ∨ (partner I).card + 1 = I.card

The partner has size differing by 1 (when 0 is in range).

def AlgebraicCombinatorics.SignedCounting.setSign (I : Finset ℕ) : ℤ

The sign of a finite set is (-1)^|I|.

Equations

• AlgebraicCombinatorics.SignedCounting.setSign I = (-1) ^ I.card

@[simp]

theorem AlgebraicCombinatorics.SignedCounting.setSign_empty : setSign ∅ = 1

The sign of the empty set is 1.

@[simp]

theorem AlgebraicCombinatorics.SignedCounting.setSign_singleton (a : ℕ) : setSign {a} = -1

The sign of a singleton set is -1.

@[simp]

theorem AlgebraicCombinatorics.SignedCounting.partner_empty : partner ∅ = {0}

The partner of the empty set is {0}.

@[simp]

theorem AlgebraicCombinatorics.SignedCounting.partner_singleton_zero : partner {0} = ∅

The partner of {0} is the empty set.

theorem AlgebraicCombinatorics.SignedCounting.partner_sign (I : Finset ℕ) : setSign (partner I) = -setSign I

The partner has opposite sign.

The Negative Hockey-Stick Identity

The negative hockey-stick identity states: ∑_{k=0}^{m} (-1)^k * C(n,k) = (-1)^m * C(n-1,m)

This is Proposition \ref{prop.binom.nhs} in the source.

theorem AlgebraicCombinatorics.SignedCounting.negHockeyStick (n m : ℕ) (hn : 0 < n) : ∑ k ∈ Finset.range (m + 1), (-1) ^ k * ↑(n.choose k) = (-1) ^ m * ↑((n - 1).choose m)

Negative Hockey-Stick Identity (prop.binom.nhs)

For n : ℕ with n ≥ 1 and m : ℕ, we have ∑ k in range (m+1), (-1)^k * n.choose k = (-1)^m * (n-1).choose m

Note: We state this for natural numbers with n ≥ 1. The source states it for n ∈ ℂ, but by the polynomial identity principle, it suffices to prove it for positive integers. The hypothesis n ≥ 1 is necessary because natural number subtraction gives (0 - 1) = 0, which would make the RHS incorrect when n = 0 and m ≥ 1.

theorem AlgebraicCombinatorics.SignedCounting.negHockeyStick' (n m : ℕ) : ∑ k ∈ Finset.range (m + 1), (-1) ^ k * ↑((n + 1).choose k) = (-1) ^ m * ↑(n.choose m)

Negative Hockey-Stick Identity (variant without hypothesis)

Alternative formulation using (n + 1) to avoid the edge case. This is exactly Int.alternating_sum_range_choose_eq_choose from Mathlib.

Cancellation Principles

These lemmas formalize the idea that sign-reversing bijections/involutions cause addends to cancel in sums.

theorem AlgebraicCombinatorics.SignedCounting.sign_cancel1 {α : Type u_1} [DecidableEq α] {R : Type u_2} [AddCommGroup R] [NoZeroSMulDivisors ℕ R] (A X : Finset α) (hXA : X ⊆ A) (sign : α → R) (f : ↥X → ↥X) (hf_bij : Function.Bijective f) (hf_sign : ∀ (I : ↥X), sign ↑(f I) = -sign ↑I) : ∑ I ∈ A, sign I = ∑ I ∈ A \ X, sign I

Cancellation Principle, Take 1 (lem.sign.cancel1)

Let A be a finite set, X ⊆ A, and sign : A → R where R is an additive group with no 2-torsion (i.e., 2a = 0 → a = 0). If f : X → X is a bijection satisfying sign(f(I)) = -sign(I) for all I ∈ X, then ∑_{I ∈ A} sign(I) = ∑_{I ∈ A \ X} sign(I).

This version requires R to have no 2-torsion (e.g., R = ℤ, ℚ, ℝ).

theorem AlgebraicCombinatorics.SignedCounting.sign_cancel2 {α : Type u_1} [DecidableEq α] {R : Type u_2} [AddCommGroup R] (A X : Finset α) (hXA : X ⊆ A) (sign : α → R) (f : ↥X → ↥X) (hf_invol : ∀ (I : ↥X), f (f I) = I) (hf_no_fixed : ∀ (I : ↥X), f I ≠ I) (hf_sign : ∀ (I : ↥X), sign ↑(f I) = -sign ↑I) : ∑ I ∈ A, sign I = ∑ I ∈ A \ X, sign I

Cancellation Principle, Take 2 (lem.sign.cancel2)

Let A be a finite set, X ⊆ A, and sign : A → R for any additive abelian group R. If f : X → X is an involution with no fixed points satisfying sign(f(I)) = -sign(I) for all I ∈ X, then ∑_{I ∈ A} sign(I) = ∑_{I ∈ A \ X} sign(I).

This version works for any additive abelian group (no 2-torsion requirement).

theorem AlgebraicCombinatorics.SignedCounting.sign_cancel3 {α : Type u_1} [DecidableEq α] {R : Type u_2} [AddCommGroup R] (A X : Finset α) (hXA : X ⊆ A) (sign : α → R) (f : ↥X → ↥X) (hf_invol : ∀ (I : ↥X), f (f I) = I) (hf_sign : ∀ (I : ↥X), sign ↑(f I) = -sign ↑I) (hf_fixed_zero : ∀ (I : ↥X), f I = I → sign ↑I = 0) : ∑ I ∈ A, sign I = ∑ I ∈ A \ X, sign I

Cancellation Principle, Take 3 (lem.sign.cancel3)

Let A be a finite set, X ⊆ A, and sign : A → R for any additive abelian group R. If f : X → X is an involution satisfying sign(f(I)) = -sign(I) for all I ∈ X, and furthermore sign(I) = 0 for all fixed points I of f, then ∑_{I ∈ A} sign(I) = ∑_{I ∈ A \ X} sign(I).

This is the most general version, allowing fixed points as long as they have sign 0.

Switching Operation

The switching operation switch_{i,i+1} swaps elements i and i+1 in a set when exactly one of them is present.

def AlgebraicCombinatorics.SignedCounting.switch (i : ℕ) (S : Finset ℕ) : Finset ℕ

Switch i with i+1 in a set: if exactly one of {i, i+1} is in S, replace it with the other; otherwise leave S unchanged.

Equations

• AlgebraicCombinatorics.SignedCounting.switch i S = if (S ∩ {i, i + 1}).card = 1 then symmDiff S {i, i + 1} else S

@[simp]

theorem AlgebraicCombinatorics.SignedCounting.switch_empty (i : ℕ) : switch i ∅ = ∅

Switching the empty set gives the empty set.

theorem AlgebraicCombinatorics.SignedCounting.switch_switch (i : ℕ) (S : Finset ℕ) : switch i (switch i S) = S

The switch operation is an involution.

theorem AlgebraicCombinatorics.SignedCounting.switch_card (i : ℕ) (S : Finset ℕ) : (switch i S).card = S.card

Switching preserves cardinality.

q-Binomial Coefficients

We define q-binomial coefficients and study their properties. Note: As of this writing, q-binomial coefficients are not in Mathlib, so we define them here.

noncomputable def AlgebraicCombinatorics.SignedCounting.qFactorial (n : ℕ) : Polynomial ℤ

The q-factorial [n]_q! = [1]_q * [2]_q * ... * [n]_q where [k]_q = 1 + q + q^2 + ... + q^{k-1}. We define it as a polynomial in q.

Equations

• AlgebraicCombinatorics.SignedCounting.qFactorial n = ∏ k ∈ Finset.range n, ∑ i ∈ Finset.range (k + 1), Polynomial.X ^ i

noncomputable def AlgebraicCombinatorics.SignedCounting.qBinomial (n k : ℕ) : Polynomial ℤ

The q-binomial coefficient [n choose k]_q = [n]_q! / ([k]_q! * [n-k]_q!). This is well-defined as a polynomial (the division is exact).

We define it combinatorially using the sum over k-element subsets formula: [n choose k]_q = ∑_{S ⊆ [n], |S|=k} q^{sum(S) - (1+2+...+k)}

Note: This is a local definition as Polynomial ℤ, equivalent to AlgebraicCombinatorics.qBinomial n k X from QBinomialBasic.lean when the latter is evaluated as a polynomial. The equivalence follows from qBinomial_eq_sum_subsets. This definition uses 0-indexed sets {0, 1, ..., n-1} while QBinomialBasic uses 1-indexed sets {1, 2, ..., n} in its subset formula, but both are equivalent.

Equations

• AlgebraicCombinatorics.SignedCounting.qBinomial n k = ∑ S ∈ (Finset.range n).powerset with S.card = k, Polynomial.X ^ (S.sum id - (Finset.range k).sum id)

Roots of Unity and Primitive Roots of Unity

This section formalizes Definition \ref{def.root-of-unity.prim} from the source.

Definition (def.root-of-unity.prim): Let K be a field and d a positive integer.

(a) A d-th root of unity in K is an element ω of K satisfying ω^d = 1. In other words, a d-th root of unity in K is an element of K whose d-th power is 1.

(b) A primitive d-th root of unity in K is an element ω of K satisfying ω^d = 1 but ω^i ≠ 1 for each i ∈ {1, 2, ..., d-1}. In other words, a primitive d-th root of unity in K is an element of the multiplicative group K× whose order is exactly d.

Mathlib correspondence:

• Part (a) is captured by ω ∈ rootsOfUnity d K or equivalently ω ^ d = 1
• Part (b) is captured by IsPrimitiveRoot ω d from RingTheory.RootsOfUnity.PrimitiveRoots

Key property: For K = ℂ, the d-th roots of unity are the d complex numbers e^{2πi·0/d}, e^{2πi·1/d}, ..., e^{2πi·(d-1)/d} (vertices of a regular d-gon on the unit circle). The primitive d-th roots of unity are those e^{2πi·g/d} where gcd(g, d) = 1.

In particular:

• The 2nd roots of unity in ℂ are 1 and -1
• The only primitive 2nd root of unity is -1

def AlgebraicCombinatorics.SignedCounting.IsRootOfUnity {K : Type u_1} [CommRing K] (ω : K) (d : ℕ) : Prop

An element ω is a d-th root of unity if ω^d = 1. (def.root-of-unity.prim (a))

This is the condition for membership in rootsOfUnity d K when ω is a unit. For fields, we can state this directly without the unit requirement.

Equations

• AlgebraicCombinatorics.SignedCounting.IsRootOfUnity ω d = (ω ^ d = 1)

theorem AlgebraicCombinatorics.SignedCounting.IsRootOfUnity.pow_eq_one {K : Type u_1} [CommRing K] {ω : K} {d : ℕ} (h : IsRootOfUnity ω d) : ω ^ d = 1

A d-th root of unity satisfies ω^d = 1.

theorem AlgebraicCombinatorics.SignedCounting.isRootOfUnity_one {K : Type u_1} [CommRing K] (d : ℕ) : IsRootOfUnity 1 d

1 is always a d-th root of unity.

theorem AlgebraicCombinatorics.SignedCounting.IsPrimitiveRoot.isRootOfUnity {K : Type u_1} [CommRing K] {ω : K} {d : ℕ} (h : IsPrimitiveRoot ω d) : IsRootOfUnity ω d

Every primitive d-th root of unity is also a d-th root of unity.

theorem AlgebraicCombinatorics.SignedCounting.isPrimitiveRoot_iff_pow_eq_one_and_pow_ne_one {K : Type u_1} [CommRing K] {ω : K} {d : ℕ} (hd : 0 < d) : IsPrimitiveRoot ω d ↔ ω ^ d = 1 ∧ ∀ (i : ℕ), 0 < i → i < d → ω ^ i ≠ 1

Characterization of primitive roots (def.root-of-unity.prim (b))

An element ω is a primitive d-th root of unity if and only if:

• ω^d = 1, and
• ω^i ≠ 1 for all i with 0 < i < d.

This is the characterization given in the source definition.

theorem AlgebraicCombinatorics.SignedCounting.IsPrimitiveRoot.pow_ne_one' {K : Type u_1} [CommRing K] {ω : K} {d : ℕ} (h : IsPrimitiveRoot ω d) {i : ℕ} (hi : 0 < i) (hi' : i < d) : ω ^ i ≠ 1

A primitive d-th root of unity ω satisfies ω^i ≠ 1 for 0 < i < d.

theorem AlgebraicCombinatorics.SignedCounting.neg_one_isPrimitiveRoot_two {K : Type u_1} [CommRing K] (h : -1 ≠ 1) : IsPrimitiveRoot (-1) 2

-1 is a primitive 2nd root of unity in any integral domain where -1 ≠ 1.

theorem AlgebraicCombinatorics.SignedCounting.isPrimitiveRoot_two_iff {K : Type u_1} [CommRing K] [IsDomain K] (h : -1 ≠ 1) (ω : K) : IsPrimitiveRoot ω 2 ↔ ω = -1

In an integral domain where -1 ≠ 1, -1 is the unique primitive 2nd root of unity.

The 2nd roots of unity are 1 and -1, but only -1 is primitive.

Sum of Primitive Roots of Unity

A key property used in cancellation arguments: if ω is a primitive d-th root of unity with d > 1, then 1 + ω + ω² + ... + ω^{d-1} = 0.

This generalizes 1 + (-1) = 0 (the case d = 2) and allows cancellation in sums involving powers of ω.

Note: Mathlib provides IsPrimitiveRoot.geom_sum_eq_zero which proves exactly this.

theorem AlgebraicCombinatorics.SignedCounting.primitiveRoot_geom_sum_eq_zero {K : Type u_1} [CommRing K] [IsDomain K] {ω : K} {d : ℕ} (hω : IsPrimitiveRoot ω d) (hd : 1 < d) : ∑ i ∈ Finset.range d, ω ^ i = 0

Geometric sum of primitive roots (used in the discrete Fourier transform)

If ω is a primitive d-th root of unity with d > 1, then 1 + ω + ω² + ... + ω^{d-1} = 0.

This is the key identity that enables cancellation in sums involving roots of unity. It generalizes 1 + (-1) = 0 (the case d = 2).

This is IsPrimitiveRoot.geom_sum_eq_zero from Mathlib, included here for documentation.

The q-Lucas Theorem

The q-Lucas theorem relates q-binomial coefficients at primitive roots of unity to ordinary binomial coefficients.

Helper Lemmas for q-Lucas

theorem AlgebraicCombinatorics.SignedCounting.pow_mod_primitiveRoot {K : Type u_1} [CommRing K] {ω : K} {d : ℕ} (hω : IsPrimitiveRoot ω d) (n : ℕ) : ω ^ n = ω ^ (n % d)

For a primitive d-th root of unity ω, ω^n = ω^(n % d)

theorem AlgebraicCombinatorics.SignedCounting.qBinomial_eval_one (n k : ℕ) : Polynomial.eval 1 (qBinomial n k) = ↑(n.choose k)

q-binomial at q=1 gives ordinary binomial coefficient

theorem AlgebraicCombinatorics.SignedCounting.qBinomial_eq_zero_of_lt (n k : ℕ) (h : n < k) : qBinomial n k = 0

q-binomial is 0 when k > n

theorem AlgebraicCombinatorics.SignedCounting.qBinomial_zero_right (n : ℕ) : qBinomial n 0 = 1

q-binomial boundary case: [n choose 0]_q = 1

theorem AlgebraicCombinatorics.SignedCounting.qBinomial_self (n : ℕ) : qBinomial n n = 1

q-binomial boundary case: [n choose n]_q = 1

Bridge to Canonical q-Binomial Definition

The local qBinomial definition uses 0-indexed k-subsets of {0, 1, ..., n-1}, while the canonical AlgebraicCombinatorics.qBinomialPoly uses monotone functions. This section proves they are equal.

theorem AlgebraicCombinatorics.SignedCounting.qBinomial_eq_canonical (n k : ℕ) : qBinomial n k = qBinomialPoly n k

The local qBinomial equals the canonical qBinomialPoly from QBinomialBasic.lean.

This bridge lemma connects the subset-sum definition used in this file (which uses 0-indexed subsets of {0, 1, ..., n-1}) with the canonical monotone function definition in QBinomialBasic.lean.

The key bijection: for a k-subset S = {s₀ < s₁ < ... < sₖ₋₁} of {0,...,n-1}, define f(i) = sᵢ - i. This is a monotone function Fin k → Fin (n-k+1), and ∑ᵢ f(i) = ∑ᵢ sᵢ - ∑ᵢ i = S.sum id - (range k).sum id.

d-Cycle Infrastructure for q-Lucas

The key to proving the q-Lucas theorem is the d-cycle cancellation argument. For a primitive d-th root of unity ω, we have ∑_{j=0}^{d-1} ω^j = 0 (when d > 1). This allows us to cancel contributions from subsets that don't respect the "block structure" where blocks are consecutive intervals of size d.

def AlgebraicCombinatorics.SignedCounting.IsDBlocky (d n : ℕ) (S : Finset ℕ) : Prop

A subset S of [n] is d-blocky if for each complete d-block {id, id+1, ..., id+d-1} contained in [n], the set S either contains all elements or none of the elements.

Equations

• AlgebraicCombinatorics.SignedCounting.IsDBlocky d n S = (S ⊆ Finset.range n ∧ ∀ i < n / d, (∀ j < d, i * d + j ∈ S) ∨ ∀ j < d, i * d + j ∉ S)

instance AlgebraicCombinatorics.SignedCounting.decidableIsDBlocky (d n : ℕ) (S : Finset ℕ) : Decidable (IsDBlocky d n S)

Equations

• AlgebraicCombinatorics.SignedCounting.decidableIsDBlocky d n S = id inferInstance

def AlgebraicCombinatorics.SignedCounting.kSubsets (n k : ℕ) : Finset (Finset ℕ)

The set of k-element subsets of [n].

Equations

• AlgebraicCombinatorics.SignedCounting.kSubsets n k = Finset.powersetCard k (Finset.range n)

def AlgebraicCombinatorics.SignedCounting.blockySubsets (d n k : ℕ) : Finset (Finset ℕ)

The set of d-blocky k-element subsets of [n].

Equations

• AlgebraicCombinatorics.SignedCounting.blockySubsets d n k = {S ∈ AlgebraicCombinatorics.SignedCounting.kSubsets n k | AlgebraicCombinatorics.SignedCounting.IsDBlocky d n S}

theorem AlgebraicCombinatorics.SignedCounting.primitiveRoot_geom_sum_zero {K : Type u_1} [Field K] {ω : K} {d : ℕ} (hω : IsPrimitiveRoot ω d) (hd : 1 < d) : ∑ j ∈ Finset.range d, ω ^ j = 0

For d > 1, the sum ∑_{j=0}^{d-1} ω^j = 0 when ω is a primitive d-th root of unity.

def AlgebraicCombinatorics.SignedCounting.smallestSplitBlock (d n : ℕ) (S : Finset ℕ) : Option ℕ

For a subset S of [n], the smallest complete d-block index where S is "split" (i.e., contains some but not all elements). Returns none if S is d-blocky.

Equations

• AlgebraicCombinatorics.SignedCounting.smallestSplitBlock d n S = {i ∈ Finset.range (n / d) | have blockStart := i * d; (∃ j < d, blockStart + j ∈ S) ∧ ∃ j < d, blockStart + j ∉ S}.min

def AlgebraicCombinatorics.SignedCounting.smallestInBlock (d i : ℕ) (S : Finset ℕ) : Option ℕ

Given a split block at index i, find the smallest offset j such that i*d + j is in S.

Equations

• AlgebraicCombinatorics.SignedCounting.smallestInBlock d i S = {j ∈ Finset.range d | i * d + j ∈ S}.min

def AlgebraicCombinatorics.SignedCounting.dCycleSwitch (d n : ℕ) (S : Finset ℕ) : Finset ℕ

The d-cycle switch operation: for a non-d-blocky subset S with smallest split block i, find the smallest element in that block that's in S, and swap it with the next element (mod d). This operation has the property that applying it d times returns to the original set.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicCombinatorics.SignedCounting.orbit_sum_eq_zero {K : Type u_1} [Field K] {ω : K} {d : ℕ} (hω : IsPrimitiveRoot ω d) (hd : 1 < d) (baseSum j : ℕ) (hj_pos : 0 < j) (hj_lt : j < d) : have m := d / d.gcd j; ∑ k ∈ Finset.range m, ω ^ (baseSum + k * j) = 0

Key algebraic lemma for orbit sums: Given 0 < j < d, the sum ∑_{k=0}^{m-1} ω^(baseSum + k*j) = 0 where m = d/gcd(d,j).

This is the algebraic core of the d-cycle cancellation argument. For each non-blocky set S with smallest split block i, let j = |blockOffsets d i S|. The orbit of S under rotation in block i has size m = d/gcd(d,j), and this lemma shows that the sum of ω^(sum T) over the orbit is 0.

theorem AlgebraicCombinatorics.SignedCounting.orbit_sum_full_eq_zero {K : Type u_1} [Field K] {ω : K} {d : ℕ} (hω : IsPrimitiveRoot ω d) (hd : 1 < d) (baseSum j : ℕ) (hj_pos : 0 < j) (hj_lt : j < d) : ∑ k ∈ Finset.range d, ω ^ (baseSum + k * j) = 0

Orbit sum over full range d: Given 0 < j < d, the sum ∑_{k=0}^{d-1} ω^(baseSum + k*j) = 0.

This is a stronger version of orbit_sum_eq_zero that sums over the full range d instead of range m where m = d/gcd(d,j). The sum is still 0 because ω^j is a primitive (d/gcd(d,j))-th root of unity, and the geometric series formula applies.

This lemma is useful when we need to work with the full orbit of size d rather than the reduced orbit of size m. The algebraic cancellation still works because the sums repeat with period m, and each period sums to 0.

Rotation infrastructure for orbit cancellation

theorem AlgebraicCombinatorics.SignedCounting.rotateInBlock_injective (d i : ℕ) (hd : 0 < d) : Function.Injective (AlgebraicCombinatorics.SignedCounting.rotateInBlock✝ d i)

The rotation function is injective.

theorem AlgebraicCombinatorics.SignedCounting.rotateSetInBlockK_sum_pow {K : Type u_1} [Field K] {ω : K} {d : ℕ} (hω : IsPrimitiveRoot ω d) (hd : 0 < d) (i : ℕ) (S : Finset ℕ) (k : ℕ) : ω ^ (AlgebraicCombinatorics.SignedCounting.rotateSetInBlockK✝ d i k S).sum id = ω ^ (S.sum id + k * (AlgebraicCombinatorics.SignedCounting.blockOffsets✝ d i S).card)

KEY COMBINATORIAL LEMMA: rotation changes sum by j (mod d). Since ω^d = 1, this means ω^(sum(rotate^k(S))) = ω^(sum(S) + k*j).

The proof uses:

1. Each rotation changes the sum by j - d * (wraparounds) where j = |blockOffsets|
2. Since ω^d = 1, the -d * (wraparounds) term vanishes
3. So ω^(sum(rotate(S))) = ω^(sum(S) + j)
4. By induction, ω^(sum(rotate^k(S))) = ω^(sum(S) + k*j)

The key insight is that rotation preserves |blockOffsets|, so we can use induction.

theorem AlgebraicCombinatorics.SignedCounting.rotateSetInBlockK_subset (d n i : ℕ) (hd : 0 < d) (hi : i < n / d) (S : Finset ℕ) (hS : S ⊆ Finset.range n) (k : ℕ) : AlgebraicCombinatorics.SignedCounting.rotateSetInBlockK✝ d i k S ⊆ Finset.range n

Rotation k times preserves subset of [n]

theorem AlgebraicCombinatorics.SignedCounting.rotateSetInBlockK_card (d i : ℕ) (hd : 0 < d) (S : Finset ℕ) (k : ℕ) : (AlgebraicCombinatorics.SignedCounting.rotateSetInBlockK✝ d i k S).card = S.card

Rotation k times preserves cardinality

Commutativity of rotations in different blocks

Rotations in different blocks commute because they act on disjoint sets of elements. This is KEY for the correct approach to proving nonBlocky_contributions_cancel: instead of using single-block orbits, we should use equivalence classes under ALL rotations. Since rotations in different blocks commute, the equivalence class is a product of single-block orbits.

Multi-block equivalence classes (for correct proof approach)

The correct proof of nonBlocky_contributions_cancel uses equivalence classes under ALL rotations (not just single-block orbits). Two sets S and T are equivalent if T can be obtained from S by applying rotations in any combination of blocks.

Key insight: Since rotations in different blocks COMMUTE (proven above as rotateSetInBlockK_comm), the equivalence class of S is: { rotateSetInBlockK d i₁ k₁ (... (rotateSetInBlockK d iₘ kₘ S)...) } for all choices of k₁, ..., kₘ where i₁, ..., iₘ are the split blocks of S.

This equals the product of single-block orbits: ∏_{i : split block of S} {rotations in block i}

Why this fixes the proof:

1. The equivalence class is orbit-closed under rotation in ANY split block (by definition)
2. The sum over each equivalence class factors as: ∑{k₁} ∑{k₂} ... ∑{kₘ} ω^(sum of rotated set) = (∑{k₁} ω^(k₁ * j₁)) * ... * (∑_{kₘ} ω^(kₘ * jₘ)) * ω^(base)
3. Since S is non-blocky, at least one block i has 0 < jᵢ < d, so ∑_{k} ω^(k * jᵢ) = 0, making the whole product 0.

Current status: The commutativity lemmas are proven. The full multi-block equivalence infrastructure is outlined below. The main theorem nonBlocky_contributions_cancel is fully proven using single-block orbit arguments.

Periodicity and orbit infrastructure for orbit cancellation

theorem AlgebraicCombinatorics.SignedCounting.rotateInBlock_iterate_d (d i x : ℕ) (hd : 0 < d) : (AlgebraicCombinatorics.SignedCounting.rotateInBlock✝ d i)^[d] x = x

Key periodicity lemma: rotating d times in block i returns to identity. This is because each element in block i has offset (x - i*d) which cycles through 0, 1, ..., d-1 and back to 0 after d rotations.

theorem AlgebraicCombinatorics.SignedCounting.rotateSetInBlockK_d (d i : ℕ) (hd : 0 < d) (S : Finset ℕ) : AlgebraicCombinatorics.SignedCounting.rotateSetInBlockK✝ d i d S = S

Rotating a set d times returns to identity

theorem AlgebraicCombinatorics.SignedCounting.rotateSetInBlockK_injective (d i : ℕ) (hd : 0 < d) (S : Finset ℕ) (_hj_pos : 0 < (AlgebraicCombinatorics.SignedCounting.blockOffsets✝ d i S).card) (_hj_lt : (AlgebraicCombinatorics.SignedCounting.blockOffsets✝¹ d i S).card < d) : have j := (AlgebraicCombinatorics.SignedCounting.blockOffsets✝² d i S).card; have m := d / d.gcd j; ∀ (k1 k2 : ℕ), k1 < m → k2 < m → AlgebraicCombinatorics.SignedCounting.rotateSetInBlockK✝ d i k1 S = AlgebraicCombinatorics.SignedCounting.rotateSetInBlockK✝¹ d i k2 S → k1 = k2

Orbit injectivity: For k1, k2 < m = d/gcd(d,j) where j = |blockOffsets d i S|, if rotateSetInBlockK d i k1 S = rotateSetInBlockK d i k2 S, then k1 = k2.

This follows from the fact that the sums differ: sum(rotate^k(S)) ≡ sum(S) + kj (mod d), and kj takes distinct values mod d for k in range(m) since m = d/gcd(d,j).

theorem AlgebraicCombinatorics.SignedCounting.rotateSetInBlockK_fiber_card_uniform (d i : ℕ) (hd : 0 < d) (S : Finset ℕ) : ∃ (c : ℕ), c ∣ d ∧ ∀ T ∈ Finset.image (fun (k : ℕ) => AlgebraicCombinatorics.SignedCounting.rotateSetInBlockK✝ d i k S) (Finset.range d), {k ∈ Finset.range d | AlgebraicCombinatorics.SignedCounting.rotateSetInBlockK✝¹ d i k S = T}.card = c

The rotation orbit has uniform fiber cardinality.

For any set S and block i, the function k ↦ rotateSetInBlockK d i k S has period p | d (where p is the smallest positive integer with rotate^p(S) = S). Thus each element of the image appears d/p times in the sum over range d.

This lemma provides the uniform multiplicity needed for sum_image_eq_zero_of_uniform_multiplicity_primitiveRoot. The proof uses the orbit-stabilizer principle: the stabilizer of S under rotation is a subgroup of ℤ/dℤ, so its size divides d, and all orbit elements have the same stabilizer size.

Smallest split block infrastructure

These lemmas establish that rotation preserves the smallest split block, which is key to proving that orbits (defined using smallest split block) partition NonBlocky.

instance AlgebraicCombinatorics.SignedCounting.isSplitBlock_decidable (d n i : ℕ) (S : Finset ℕ) : Decidable (AlgebraicCombinatorics.SignedCounting.isSplitBlock✝ d n i S)

Decidability for isSplitBlock

Equations

• AlgebraicCombinatorics.SignedCounting.isSplitBlock_decidable d n i S = id inferInstance

theorem AlgebraicCombinatorics.SignedCounting.sum_nonBlocky_subset_eq_zero {K : Type u_1} [Field K] {ω : K} {d : ℕ} (hω : IsPrimitiveRoot ω d) (hd : 1 < d) (n k : ℕ) (_hnd : d ≤ n) (NonBlocky : Finset (Finset ℕ)) (hNB_def : NonBlocky = {S ∈ kSubsets n k | ¬IsDBlocky d n S}) (hrot_mem : ∀ S ∈ NonBlocky, ∀ i < n / d, ∀ (iter : ℕ), AlgebraicCombinatorics.SignedCounting.rotateSetInBlockK✝ d i iter S ∈ kSubsets n k) (hrot_nonblocky : ∀ S ∈ NonBlocky, ∀ rotBlock < n / d, ∀ (iter : ℕ), ¬IsDBlocky d n (AlgebraicCombinatorics.SignedCounting.rotateSetInBlockK✝¹ d rotBlock iter S)) (_horbit_sum_zero : ∀ S ∈ NonBlocky, ∀ i < n / d, AlgebraicCombinatorics.SignedCounting.isSplitBlock✝ d n i S → have j := (AlgebraicCombinatorics.SignedCounting.blockOffsets✝ d i S).card; have m := d / d.gcd j; ∑ k ∈ Finset.range m, ω ^ (AlgebraicCombinatorics.SignedCounting.rotateSetInBlockK✝² d i k S).sum id = 0) (A : Finset (Finset ℕ)) (hA_sub : A ⊆ NonBlocky) (hOrbitClosed : ∀ S ∈ A, ∀ (hne_S : (AlgebraicCombinatorics.SignedCounting.splitBlockIndices✝ d n S).Nonempty), have i_S := AlgebraicCombinatorics.SignedCounting.smallestSplitBlockIdx✝ d n S hne_S; ∀ (iter : ℕ), AlgebraicCombinatorics.SignedCounting.rotateSetInBlockK✝³ d i_S iter S ∈ A) : ∑ S ∈ A, ω ^ S.sum id = 0

Helper: For any orbit-closed subset of NonBlocky, the weighted sum is 0. This is the key lemma that allows the induction to work correctly. It's proved by strong induction on the cardinality of the subset.

The orbit-closure hypothesis ensures that when we pick an element S₀ ∈ A and compute its orbit O under rotation in the smallest split block, we have O ⊆ A. This avoids the problematic case where A is a proper subset of an orbit.

Key insight (2025-01 fix): The orbit-closure only needs to hold for the SMALLEST split block of each element. This is because:

1. All elements of an orbit O (under block i₀) have the same smallest split block i₀
2. If S ∉ O has smallest split block i_S ≠ i₀, rotating S in block i_S gives T with smallest split block i_S ≠ i₀, so T ∉ O
3. If S ∉ O has smallest split block i₀, then S differs from S₀ outside block i₀, which is impossible if O uses the full orbit (range d)

theorem AlgebraicCombinatorics.SignedCounting.nonBlocky_contributions_cancel {K : Type u_1} [Field K] {ω : K} {d : ℕ} (hω : IsPrimitiveRoot ω d) (hd : 1 < d) (n k : ℕ) : ∑ S ∈ kSubsets n k with ¬IsDBlocky d n S, ω ^ S.sum id = 0

Key lemma: For non-blocky subsets, contributions cancel in d-cycles. This is the heart of the q-Lucas theorem proof.

More precisely: partition non-blocky k-element subsets into equivalence classes where two sets are equivalent if they differ only by cyclic shifts within blocks. Each equivalence class has size m where 1 < m and m | d, and the sum of ω^(sum S) over each class is 0 because the sums form an arithmetic progression with common difference d/m, and ω^(d/m) is a primitive m-th root of unity.

Bijection between blocky subsets and component pairs

theorem AlgebraicCombinatorics.SignedCounting.blocky_subsets_count (d n k : ℕ) (hd : 0 < d) : (blockySubsets d n k).card = if k % d ≤ n % d then (n / d).choose (k / d) * (n % d).choose (k % d) else 0

Blocky subsets correspond to choosing which complete blocks to include, plus choosing elements from the partial block. The count depends on divisibility.

A blocky k-element subset S of [n] is uniquely determined by:

1. Which complete d-blocks are fully in S (a subset of {0, ..., n/d - 1} of size k/d)
2. Which elements of the partial block are in S (a subset of {0, ..., n%d - 1} of size k%d)

This gives a bijection with pairs from (Finset.range (n/d)).powersetCard (k/d) × (Finset.range (n%d)).powersetCard (k%d) which has cardinality (n/d).choose(k/d) * (n%d).choose(k%d).

When k%d > n%d, no such subsets exist (can't choose k%d elements from n%d available).

theorem AlgebraicCombinatorics.SignedCounting.blocky_sum_eq {K : Type u_1} [Field K] {ω : K} {d : ℕ} (hω : IsPrimitiveRoot ω d) (hd : 0 < d) (n k : ℕ) : ∑ S ∈ blockySubsets d n k, ω ^ (S.sum id - (Finset.range k).sum id) = ↑((n / d).choose (k / d)) * (Polynomial.aeval ω) (qBinomial (n % d) (k % d))

The sum of contributions from blocky subsets gives the product formula.

For blocky subsets, the contribution factors because:

1. Complete blocks contribute ddi + d*(d-1)/2 each, and since ω^d = 1, the ω^{ddi} part is always 1.
2. The partial block contributes independently.
3. The bijection with (block indices, partial elements) pairs allows factoring.

The Main Theorem

theorem AlgebraicCombinatorics.SignedCounting.qLucas {K : Type u_1} [Field K] (d : ℕ) (hd : 0 < d) (ω : K) (hω : IsPrimitiveRoot ω d) (n k : ℕ) : (Polynomial.aeval ω) (qBinomial n k) = ↑((n / d).choose (k / d)) * (Polynomial.aeval ω) (qBinomial (n % d) (k % d))

q-Lucas Theorem (thm.sign.q-lucas)

Let K be a field, d a positive integer, and ω a primitive d-th root of unity in K. For n, k : ℕ, write n = q * d + r and k = u * d + v where 0 ≤ r, v < d. Then: [n choose k]_ω = (q choose u) * [r choose v]_ω

This generalizes the formula for [n choose k]_{-1} (which is the case d = 2).

Proof idea: The proof uses a generalization of sign-reversing involutions to d-cycles. The key insight is that for a primitive d-th root of unity ω, we have ∑_{i=0}^{d-1} ω^i = 0 (when d > 1) This allows cancellation of terms that don't respect the "block structure" where blocks are consecutive intervals of size d: {0,...,d-1}, {d,...,2d-1}, etc.

A k-element subset S of {0,...,n-1} can be decomposed into:

1. Which "full blocks" it contains (choosing k/d blocks from n/d available blocks)
2. Which elements of the "partial block" {(n/d)*d, ..., n-1} it contains

For subsets that don't respect the block structure, we can define a d-cycle that permutes related subsets, and the sum of ω^(exponent) over each cycle is zero. The remaining terms correspond to "blocky" subsets, giving the product formula.

q-Binomial Coefficients at q = -1

We compute [n choose k]_{-1} using the q-Lucas theorem with d=2 and ω=-1. The result depends on the parities of n and k.

This is Exercise \ref{exe.sign.-1inom} in the source.

def AlgebraicCombinatorics.SignedCounting.IsBlocky (n : ℕ) (S : Finset ℕ) : Prop

A blocky subset of [n] (when n is even) is a union of blocks {0,1}, {2,3}, .... Each block is either fully included or fully excluded.

Equations

• AlgebraicCombinatorics.SignedCounting.IsBlocky n S = (S ⊆ Finset.range n ∧ ∀ (i : ℕ), 2 * i + 1 < n → (2 * i ∈ S ↔ 2 * i + 1 ∈ S))

theorem AlgebraicCombinatorics.SignedCounting.qBinom_neg_one (n k : ℕ) : Polynomial.eval (-1) (qBinomial n k) = ↑(if Even n ∧ Odd k then 0 else (n / 2).choose (k / 2))

q-Binomial at q = -1 (exe.sign.-1inom, eq.sol.sign.-1inom.res)

For n, k : ℕ, the q-binomial coefficient [n choose k]_{-1} equals:

• 0 if n is even and k is odd
• ⌊n/2⌋ choose ⌊k/2⌋ otherwise

The proof uses the q-Lucas theorem with d=2 and ω=-1: [n choose k]_{-1} = (n/2 choose k/2) * [n%2 choose k%2]_{-1}

The base cases are:

• [0 choose 0]_{-1} = 1
• [0 choose 1]_{-1} = 0
• [1 choose 0]_{-1} = 1
• [1 choose 1]_{-1} = 1

Therefore:

• If Even n ∧ Odd k: result is (n/2 choose k/2) * 0 = 0
• Otherwise: result is (n/2 choose k/2) * 1 = (n/2 choose k/2)

Application: Sum of Signs of Acceptable Sets

We formalize the key step in the combinatorial proof of the negative hockey-stick identity: the sum of signs of acceptable sets equals (-1)^m * C(n-1, m).

theorem AlgebraicCombinatorics.SignedCounting.acceptable_nonAcceptablePartner_iff (n m : ℕ) (hn : 0 < n) (I : Finset ℕ) (hI : I ∈ acceptableSets n m) : partner I ∉ acceptableSets n m ↔ 0 ∉ I ∧ I.card = m

The set of acceptable sets with non-acceptable partners consists exactly of m-element subsets of {0, ..., n-1} that do not contain 0.

Note: We require 0 < n because when n = 0, the partner of ∅ is {0} which is not in range 0, but ∅.card = 0 may not equal m.

theorem AlgebraicCombinatorics.SignedCounting.sum_signs_acceptable (n m : ℕ) (hn : 0 < n) : ∑ I ∈ acceptableSets n m, setSign I = (-1) ^ m * ↑((n - 1).choose m)

The sum of signs of all acceptable sets equals (-1)^m * C(n-1, m).