Cleared Pole Numerator nat Degree

Proved

D1Bound5.clearedPoleNumerator_natDegree

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

diophantine-tuplesnumber-theory

Auxiliary result clearedPoleNumerator_natDegree 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.RingDivision
import Definitions.Def_D1Bound5_BennettResidueCoefficient_Definitions

Formal statement

section
open Finset Polynomial

namespace D1Bound5

section CommRing

variable {R ι : Type*} [CommRing R] [Nontrivial R]
variable [Fintype ι] [DecidableEq ι]





theorem _root_.D1Bound5.clearedPoleNumerator_natDegree (a : ι → R) (e : ι → ℕ)
    (i : ι) (j : Fin (e i + 1)) :
    (clearedPoleNumerator a e i j).natDegree =
      j.val + ∑ l ∈ (Finset.univ : Finset ι).erase i, (e l + 1) := by sorry







end CommRing

end D1Bound5
end

Source

D1Bound5/BennettResidueCoefficient.lean, lines 28-44, SHA-256 8c207032d119b0629e3cee3a36cfe0f7dd94d73784c8b28b8cba78efa262f829. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph