Bennett two coefficient rounding

Proved

D1Bound5.bennett_two_coefficient_rounding

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

diophantine-tuplesnumber-theory

The small loss from the degree-(k+1) numerator majorant fits strictly inside the manuscript's rounding of the exponential base to 42.

Preamble

import Lean.Elab.Tactic.Omega
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring

Formal statement

section
namespace D1Bound5








theorem _root_.D1Bound5.bennett_two_coefficient_rounding (T : ℝ) (hT : 1000 ≤ T) :
    ((1 + 7 / (5 * T)) / (1 - 1 / T)) *
      ((125 / 3 : ℝ) * (1 + 7 / (5 * T))) < 42 := by sorry



end D1Bound5
end

Source

D1Bound5/BennettTwoCoefficientConstants.lean, lines 71-99, SHA-256 034cf7aa6d3e853901a9f7bd5f2be74a2cd9af0c2f34f1de6a52a0f80541821b. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph