Rational cutoff certificate for oneSmallCutoffRow_28

Proved

D1Bound5.oneSmallCutoffRow_28_valid

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

diophantine-tuplesnumber-theory

The cutoff row satisfies the required rational arithmetic conditions: the cutoff and anchor-norm bounds, the rational square-root enclosures, positivity of the coefficient bounds, all thirteen strict overlap comparisons, and the ordinary-tail comparison at the stated cutoff.

Preamble

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.Ring.Equiv
import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Prod
import Mathlib.Data.Int.Interval
import Mathlib.Data.Int.Sqrt
import Mathlib.Data.List.Range
import Mathlib.Tactic.IntervalCases
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Definitions.Def_D1Bound5_Coordinates_Definitions
import Definitions.Def_D1Bound5_OneSmallCutoffArithmetic_Definitions_001

Formal statement

section
namespace D1Bound5
open QuadInt



namespace OneSmallCutoffRow



























end OneSmallCutoffRow

set_option maxRecDepth 100000
set_option maxHeartbeats 0



















































































































theorem _root_.D1Bound5.oneSmallCutoffRow_28_valid : oneSmallCutoffRow_28.Valid := by sorry

























































































































end D1Bound5
end

Source

D1Bound5/OneSmallCutoffArithmetic.lean, lines 270-271, SHA-256 d65ab45ed304589ddbe969477a809953ce44ed6ceae42c0145a3b1e641e229f4. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph