Retained mixed four start scalar gap

Proved

D1Bound5.retained_mixed_four_start_scalar_gap

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

diophantine-tuplesnumber-theory

Mixed retained-start scalar contradiction: the actual nonzero four-anchor form forces the seventh-power terminal gap. Its assumptions are the concrete form estimate and previously obtained fifth-power growth, not the conclusion.

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_start_scalar_gap
    (A B S T C D Z L : ℝ) (hA : 1 ≤ A) (hB : 3 ≤ B)
    (hS : 0 < S) (hT : 0 < T) (hSC : S ≤ C) (hTC : T ≤ C)
    (hC1000 : 1000 < C) (hZ : 0 < Z)
    (hC : 16*B*S*T < C)
    (hD : A^2*C^5/S^2 < D)
    (hrootlo : (3999/4000 : ℝ)*C*D < Z^2)
    (hroothi : Z^2 ≤ C*D+1)
    (hL : 1 ≤ L)
    (hupper : L < 13*B*S^2*T^3/Z + (49/50 : ℝ)*S*T^2*Z/(A*C^4)) :
    A^2*C^7/(S^2*T^4) < D := by sorry

end D1Bound5
end

Source

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

View graph