Retained mixed four first term lt

Proved

D1Bound5.retained_mixed_four_first_term_lt

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

diophantine-tuplesnumber-theory

With A≥1 and B≥3, the first summand of the actual four-anchor form is below one percent after the retained five-entry growth has been established.

Preamble

import Mathlib.Data.Real.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.GCongr
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring

Formal statement

section
namespace D1Bound5


theorem _root_.D1Bound5.retained_mixed_four_first_term_lt
    (A B S T C D Z : ℝ) (hA : 1 ≤ A) (hB : 3 ≤ B)
    (hS : 0 < S) (hT : 0 < T) (hZ : 0 < Z)
    (hC : 16*B*S*T < C)
    (hD : A^2*C^5/S^2 < D)
    (hroot : (3999/4000 : ℝ)*C*D < Z^2) :
    13*B*S^2*T^3/Z < (1/100 : ℝ) := by sorry



end D1Bound5
end

Source

D1Bound5/RetainedMixedFourScalar.lean, lines 5-45, SHA-256 a4ae2cd4aa93ee653bdc1acf1660c5bb84963f8e3f72e7896314845810407848. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph