Tail Disk 0 11 checked
ProvedD1Bound5.tailDisk_0_11_checkeddiophantine-tuplesnumber-theory
No external execution or native-evaluation axiom is used.
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.Tactic.IntervalCases import Mathlib.Tactic.Linarith import Mathlib.Tactic.LinearCombination import Mathlib.Tactic.Ring import Definitions.Def_D1Bound5_Coordinates_Definitions import Definitions.Def_D1Bound5_SmallTailAllData_Definitions import Definitions.Def_D1Bound5_SmallTailExplicit_Definitions
Formal statement
section namespace D1Bound5 open QuadInt set_option maxRecDepth 32768 set_option maxHeartbeats 6000000 theorem _root_.D1Bound5.tailDisk_0_11_checked : tailListBool tailDisk_0_11 = true := by sorry end D1Bound5 end
Source
D1Bound5/SmallTailAllData.lean, lines 168-170, SHA-256 b043adcb34167ee12d7125095cb2fb5aa023d0064768e88ccfe344b7e38716d1. Project: https://github.com/tomislav-math/d1-bound5-lean