Cubed central binomial coefficients

DefinitionCubed central binomial coefficients#✓fully proved

For a natural number \(n\), \(a(n) = \binom{2n}{n}^3\).

def a (n : ℕ) : ℕ := (Nat.choose (2 * n) n) ^ 3

Used by 1

Used byDiagonal-coefficient property of the cubed central binomial coefficients

AbbreviationIndices for three variables#✓fully proved

Three polynomial variables are indexed by the set \(\{0, 1, 2\}\).

abbrev Vars := Fin 3

Used by 3

Used byDiagonal-coefficient property of the cubed central binomial coefficients · Product polynomial for the cubed central binomial coefficients · Exponent vector of \(x^n y^n z^n\)

DefinitionExponent vector of \(x^n y^n z^n\)#✓fully proved

For a natural number \(n\), the exponent vector assigning exponent \(n\) to each of the three variables \(x, y, z\), that is, the monomial \(x^n y^n z^n\).

noncomputable def xyzPowN (n : ℕ) : Finsupp Vars ℕ :=
  Finsupp.ofSupportFinite (fun _ : Vars => n) (Set.toFinite _)

Uses 1 · Used by 1

Statement usesIndices for three variables

Used byDiagonal-coefficient property of the cubed central binomial coefficients

DefinitionProduct polynomial for the cubed central binomial coefficients#✓fully proved

For a natural number \(n\), this is the polynomial \((1 + x + y + z)^{2n} (1 + x + y - z)^n (1 + x - y + z)^n\) in three variables \(x, y, z\) (indexed by \(0, 1, 2\)) with integer coefficients.

noncomputable def pPoly (n : ℕ) : P :=
  let X := MvPolynomial.X 0
  let Y := MvPolynomial.X 1
  let Z := MvPolynomial.X 2
  let p1 : P := 1 + X + Y + Z
  let p2 : P := 1 + X + Y - Z
  let p3 : P := 1 + X - Y + Z
  p1 ^ (2 * n) * p2 ^ n * p3 ^ n

Uses 1 · Used by 1

Statement usesIndices for three variables

Used byDiagonal-coefficient property of the cubed central binomial coefficients

DefinitionDiagonal-coefficient property of the cubed central binomial coefficients#✓fully proved

This is the proposition that for every natural number \(n\), the coefficient of \(x^n y^n z^n\) in the polynomial \((1 + x + y + z)^{2n} (1 + x + y - z)^n (1 + x - y + z)^n\) in three variables \(x, y, z\) with integer coefficients equals \(\binom{2n}{n}^3\).

def a_eq_coeff : Prop :=
  ∀ (n : ℕ), (a n : ℤ) = AddMonoidAlgebra.coeff (pPoly n) (xyzPowN n)

Uses 4 · Used by 1

Statement usesIndices for three variables · Cubed central binomial coefficients · Product polynomial for the cubed central binomial coefficients · Exponent vector of \(x^n y^n z^n\)

Used byCubed central binomial coefficients as diagonal coefficients

TheoremCubed central binomial coefficients as diagonal coefficients#●ready to prove

For every natural number \(n\), the coefficient of \(x^n y^n z^n\) in the polynomial \((1 + x + y + z)^{2n} (1 + x + y - z)^n (1 + x - y + z)^n\) in three variables \(x, y, z\) with integer coefficients equals \(\binom{2n}{n}^3\).

public theorem_wanted a_eq_coeff_holds : a_eq_coeff

Sources

• Formal proof of the A002897 diagonal-coefficient identity (methods of Tsoukalas et al. [arXiv/2605.22763]), https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/2897.wip.lean#L408.

Uses 1

Statement usesDiagonal-coefficient property of the cubed central binomial coefficients

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.