Nonvanishing of the binomial Toeplitz determinant

The binomial Toeplitz determinant det [C(m, s+j−i)]_{s × s} is nonzero for 1 ≤ s ≤ m, discharging SquareBinomialDetPos of BinomialDet.lean.

The proof is the Lindström–Gessel–Viennot involution: the Leibniz expansion of the determinant is a signed count of tuples (σ, F) where F i is an (s + σ(i) − i)-subset of Fin m (the E-step heights of a lattice path). Crossing tuples cancel in pairs under the tail-swap involution at the first crossing; the noncrossing tuples all have σ = 1 and count with sign +1, and at least one exists.

1. Sign extraction

theorem RS.diagramSchur_neg_eq_sign_mul_binomDet (s m : ℕ) (hs : 1 ≤ s) (hm : s ≤ m) : (diagramSchur (squareDiagram s) fun (x : ℕ) => -↑m) = (-1) ^ s * (Matrix.of fun (i j : Fin s) => ↑(m.choose (s + ↑j - ↑i))).det

Sign extraction: diagramSchur(sq_s, -(m)) = (-1)^s * det[C(m, s+j-i)].

2. The LGV path model

For a permutation σ, the Leibniz term ∏ i C(m, s+σ(i)−i) counts tuples F : Fin s → Finset (Fin m) with (F i).card = s + σ(i) − i. Path i has x-coordinate x_i(h) = i + #{a ∈ F i | a < h} at height h.

3. Canonical crossing data

4. The tail-swap involution on families

5. Invariance of the canonical crossing data

6. The involution kills the crossing terms

7. Noncrossing families force the identity permutation

8. The signed count

9. Core nonvanishing

theorem RS.det_binomial_upper_ne_zero (s m : ℕ) : 1 ≤ s → ∀ (hm : s ≤ m), (Matrix.of fun (i j : Fin s) => ↑(m.choose (s + ↑j - ↑i))).det ≠ 0

The determinant det[C(m, s+j-i)] is nonzero for 1 ≤ s ≤ m.

10. Glue

theorem RS.squareBinomialDetPos : SquareBinomialDetPos

The binomial Toeplitz determinant is nonzero, discharging the hypothesis of the determinant development.