Bennett Polynomial Residue homogenize

Proved

D1Bound5.bennettPolynomialResidue_homogenize

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

diophantine-tuplesnumber-theory

Auxiliary result bennettPolynomialResidue_homogenize in the proof of the bound five for Diophantine D(1) sets in imaginary quadratic integer rings. The formal statement specifies its hypotheses and conclusion; a mathematical prose description remains to be supplied.

Preamble

import Lean.Elab.Tactic.Omega
import Mathlib.Algebra.Polynomial.BigOperators
import Mathlib.Algebra.Polynomial.Degree.Operations
import Mathlib.RingTheory.PowerSeries.Binomial
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_BennettClearedResidues_Definitions
import Definitions.Def_D1Bound5_BennettResiduePolynomials_Definitions

Formal statement

section
open Finset

namespace D1Bound5

variable {F : Type*} [Field F] [CharZero F]









section Nodes

variable {I : Type*} [DecidableEq I]





theorem _root_.D1Bound5.bennettPolynomialResidue_homogenize (s : Finset I) (a : I → F)
    (k : ℕ) (ν N : F) (i j : I) (hN : N ≠ 0) :
    N ^ k * (bennettPolynomialResidue s a k ν i j).eval N⁻¹ =
      (bennettClearedResidue s a k ν i j).eval N := by sorry

end Nodes

end D1Bound5
end

Source

D1Bound5/BennettResiduePolynomials.lean, lines 92-98, SHA-256 5264fd8f08d4a6fb748bab8f101f05ca183c3e4658b02954972b81e086f0144d. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph