Frontier table numeric

Proved

D1Bound5.frontier_table_numeric

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

diophantine-tuplesnumber-theory

All five frontier constants pass the exact rational endpoint check. This is only the scalar closing step; the determinant inequality is explicitly displayed here and supplied by the tuple assembly.

Preamble

import Mathlib.Data.Real.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.GCongr
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_FrontierScalarReduction_Definitions
import Definitions.Def_D1Bound5_FrontierTableNumeric_Definitions

Formal statement

section
namespace D1Bound5






theorem _root_.D1Bound5.frontier_table_numeric (alpha beta target tau : ℝ)
    (hrow : FrontierTableRow alpha beta target) (htau : (2/3 : ℝ) < tau)
    (hscalar : tau ≤ 2*frontierK alpha beta*tau^2+
      frontierL alpha beta*frontierP alpha beta*tau+frontierJ alpha beta) :
    target < tau := by sorry

end D1Bound5
end

Source

D1Bound5/FrontierTableNumeric.lean, lines 24-78, SHA-256 fdb5110fd7c01a02f52f2b7aca40f48eff76285798bc764522ee4ed8858163e4. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph