Bennett two taylor scalar mem

Proved

D1Bound5.bennett_two_taylor_scalar_mem

by tp · Oct 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-tuplesnumber-theory

The three binomial factors in the two-node Taylor expansion are integral after the uniform order-k power of four is included. Every integer is in S.

Preamble

import Mathlib.Algebra.BigOperators.NatAntidiagonal
import Mathlib.Combinatorics.Enumerative.Catalan.Basic
import Mathlib.RingTheory.Binomial
import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.NormNum

Formal statement

section
open Finset

namespace D1Bound5




theorem _root_.D1Bound5.bennett_two_taylor_scalar_mem
    {F : Type*} [Field F] [CharZero F] (S : Subring F)
    (k h p q u v : ℕ) (hh : h ≤ k) :
    (((4 : F) ^ k * Ring.choose ((k : F) + 1 / 2) h) *
      Ring.choose (-(p : F)) u * Ring.choose (-(q : F)) v) ∈ S := by sorry

end D1Bound5
end

Source

D1Bound5/BennettSubringSums.lean, lines 27-38, SHA-256 5c21c49f96a2c66d645b20532b67dda8cde35833f4e0f3fe6b545b7454d81ecf. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph