Nonvanishing of square-diagram Schur values at constant sequences

The Jacobi–Trudi determinant for the square diagram at constant power-sum sequences m (resp. −m) is nonzero. The positive case is proved here by a row-normalized product identity; the negated case is stated as SquareBinomialDetPos and proved by the Lindström–Gessel–Viennot argument of LGVStrict.lean.

The hard core

@[reducible, inline]

abbrev RS.SquareBinomialDetPos : Prop

The negated case: the Jacobi–Trudi determinant for squareDiagram s evaluated at the constant negative sequence −m is nonzero whenever s ≤ m.

Equivalently (by sign extraction), the binomial Toeplitz determinant det [C(m, s+j−i)]_{0 ≤ i,j < s} is nonzero for m ≥ s.

Proved as squareBinomialDetPos in LGVStrict.lean, by a Lindström–Gessel–Viennot lattice-path count whose non-intersecting-path formula is manifestly positive.

Equations

• RS.SquareBinomialDetPos = ∀ (s m : ℕ), 1 ≤ s → s ≤ m → (RS.diagramSchur (RS.squareDiagram s) fun (x : ℕ) => -↑m) ≠ 0

Combinatorial tools

Positive case: the row-normalized product identity

Positive case: nonvanishing

theorem RS.diagramSchur_square_const_pos (s m : ℕ) (hm : s ≤ m) : ∃ (N : ℕ) (D : ℕ), 0 < N ∧ 0 < D ∧ (↑D * diagramSchur (squareDiagram s) fun (x : ℕ) => ↑m) = ↑N

The square-diagram Schur value at the constant sequence m is a positive rational.

theorem RS.diagramSchur_square_const_ne_zero (s m : ℕ) (hm : s ≤ m) : (diagramSchur (squareDiagram s) fun (x : ℕ) => ↑m) ≠ 0

The square-diagram Schur value at the constant sequence m does not vanish.

Negative case

theorem RS.diagramSchur_square_neg_const_ne_zero (H : SquareBinomialDetPos) (s m : ℕ) (hm : s ≤ m) : (diagramSchur (squareDiagram s) fun (x : ℕ) => -↑m) ≠ 0

The square-diagram Schur value at the negated constant sequence −m does not vanish.