Section 4

In this file we formalise section 4 of the paper. Currently, we formalise section 4.3 onwards, taking as assumptions the bounds in the earlier parts of the paper.

structure baseAssumptions (d : ℕ) (a : ℕ → ℝ) : Prop

A structure containing the basic assumptions for each vector.

• nonneg (i : ℕ) : 0 ≤ a i
• zero : a 0 = 0
• sum_bound : ∑ i ∈ Finset.Iic d, ↑i * a i ≤ 1

theorem baseAssumptions.sum_restrict_bound {d : ℕ} {a : ℕ → ℝ} (ha : baseAssumptions d a) : ∑ i ∈ Finset.Icc 1 d, ↑i * a i ≤ 1

def Bound4Point3 (d : ℕ) (ε : ℝ) (a b : ℕ → ℝ) : Prop

A statement of equation 4.3 from the paper, formulated for a, b. We explicitly take a, b as inputs to simplify symmetry arguments in the conclusion.

Equations

• Bound4Point3 d ε a b = (0.66 - ε ^ 2 ≤ ∑ i ∈ Finset.Iic d, (a i + b i))

theorem Bound4Point3.symm {d : ℕ} {ε : ℝ} {a b : ℕ → ℝ} (h43ab : Bound4Point3 d ε a b) : Bound4Point3 d ε b a

The bound 4.3 is symmetric in a, b

def Bound4Point4 (d : ℕ) (δ ε : ℝ) (a b c : ℕ → ℝ) : Prop

A statement of equation 4.4 from the paper, formulated for a, b, c. We explicitly take a, b, c as inputs to simplify symmetry arguments in the conclusion.

Equations

• Bound4Point4 d δ ε a b c = (∑ i ∈ Finset.Iic d, (a i + b i + c i) ≤ 1 + δ - ε)

theorem Bound4Point4.left_comm {d : ℕ} {δ ε : ℝ} {a b c : ℕ → ℝ} (h44 : Bound4Point4 d δ ε a b c) : Bound4Point4 d δ ε b a c

theorem Bound4Point4.right_comm {d : ℕ} {δ ε : ℝ} {a b c : ℕ → ℝ} (h44 : Bound4Point4 d δ ε a b c) : Bound4Point4 d δ ε a c b

theorem Bound4Point4.rotate {d : ℕ} {δ ε : ℝ} {a b c : ℕ → ℝ} (h44 : Bound4Point4 d δ ε a b c) : Bound4Point4 d δ ε b c a

structure Bound4Point5 (d : ℕ) (δ ε : ℝ) (a : ℕ → ℝ) : Prop

A statement of equation 4.5 from the paper, formulated for a.

We will at some point show that 4.5 can be safely assumed in context, after we've assumed 1.2 and 4.4

• lower : 0.32 - δ ≤ ∑ i ∈ Finset.Iic d, a i
• upper : ∑ i ∈ Finset.Iic d, a i ≤ 0.34 + δ - ε / 2

def FourierBound (d : ℕ) (δ ν : ℝ) (a b : ℕ → ℝ) : Prop

A statement of the Fourier bound. Note that this is not saying the bound holds, but defining what it means for the bound to hold. In Section4.lean, we will take this as an assumption to many statements in order to deduce bounds on ν. Elsewhere we will show that the bound holds, and thus its proof can be fed in to those lemmas which have it as an assumption.

Equations

• FourierBound d δ ν a b = (ν < 1 / 2 * (1 + δ + ∑ i ∈ Finset.Iic d, max (a i) (b i) - sSup {x : ℝ | ∃ i ∈ Set.Ioc 1 d, max (a i) (b i) = x}))

theorem FourierBound.special {d : ℕ} {δ ν : ℝ} {a b : ℕ → ℝ} (hfab : FourierBound d δ ν a b) (j : ℕ) (hj : j ∈ Set.Ioc 1 d) : ν < 1 / 2 * (1 + δ + ∑ i ∈ Finset.Iic d, max (a i) (b i) - max (a j) (b j))

From the Fourier bound, we can deduce bounds for each j ∈ (1, d].

theorem FourierBound.special' {d : ℕ} {δ ν : ℝ} {a b : ℕ → ℝ} (hfab : FourierBound d δ ν a b) (j : ℕ) (hj : j ∈ Set.Ioc 1 d) : ν < 1 / 2 * (1 + δ + ∑ i ∈ Finset.Iic d with i ≠ j, max (a i) (b i))

theorem FourierBound.two {d : ℕ} {δ ν : ℝ} {a b : ℕ → ℝ} (hfab : FourierBound d δ ν a b) (hd : 2 ≤ d) : ν < 1 / 2 * (1 + δ + ∑ i ∈ Finset.Iic d, max (a i) (b i) - max (a 2) (b 2))

theorem FourierBound.three {d : ℕ} {δ ν : ℝ} {a b : ℕ → ℝ} (hfab : FourierBound d δ ν a b) (hd : 3 ≤ d) : ν < 1 / 2 * (1 + δ + ∑ i ∈ Finset.Iic d, max (a i) (b i) - max (a 3) (b 3))

theorem FourierBound.symm {d : ℕ} {δ ν : ℝ} {a b : ℕ → ℝ} (hfab : FourierBound d δ ν a b) : FourierBound d δ ν b a

def DeterminantBound (d : ℕ) (δ ν : ℝ) (a b : ℕ → ℝ) : Prop

A statement of the Determinant bound. Note that this is not saying the bound holds, but defining what it means for the bound to hold. In Section4.lean, we will take this as an assumption to many statements in order to deduce bounds on ν. Elsewhere we will show that the bound holds, and thus its proof can be fed in to those lemmas which have it as an assumption.

Equations

• DeterminantBound d δ ν a b = (ν < sInf {x : ℝ | ∃ (p : ℕ) (q : ℕ) (_ : p ∈ Set.Ioc 1 d) (_ : q ∈ Set.Ioc 1 d), 1 + δ - a p - b q + min (a p / ↑q) (b q / ↑p) = x})

theorem determinantBound_set_finite {d : ℕ} {δ : ℝ} {a b : ℕ → ℝ} : {x : ℝ | ∃ (p : ℕ) (q : ℕ) (_ : p ∈ Set.Ioc 1 d) (_ : q ∈ Set.Ioc 1 d), 1 + δ - a p - b q + min (a p / ↑q) (b q / ↑p) = x}.Finite

theorem DeterminantBound.symm {d : ℕ} {δ ν : ℝ} {a b : ℕ → ℝ} (hdab : DeterminantBound d δ ν a b) : DeterminantBound d δ ν b a

theorem DeterminantBound.application {d : ℕ} {δ ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (hd : 4 ≤ d) (M : ℝ) (hM : M = sSup {x : ℝ | ∃ i ∈ Set.Icc 4 d, max (b i) (c i) = x}) : ν < 1 + δ - a 3 - M + min (a 3 / 4) (M / 3)

A particular application of the determinant bound used in subcase 2.1

def ThueBound (d : ℕ) (δ ν : ℝ) (a b : ℕ → ℝ) : Prop

A statement of the Thue bound. Note that this is not saying the bound holds, but defining what it means for the bound to hold. In Section4.lean, we will take this as an assumption to many statements in order to deduce bounds on ν. Elsewhere we will show that the bound holds, and thus its proof can be fed in to those lemmas which have it as an assumption.

Equations

• ThueBound d δ ν a b = (ν < 1 + δ - sSup {x : ℝ | ∃ p ∈ Set.Ioc 1 d, ∑ i ∈ Finset.Iic d with p ∣ i, (a i + b i) = x})

theorem ThueBound.symm {d : ℕ} {δ ν : ℝ} {a b : ℕ → ℝ} (htab : ThueBound d δ ν a b) : ThueBound d δ ν b a

theorem ThueBound.special {d : ℕ} {δ ν : ℝ} {a b : ℕ → ℝ} (htab : ThueBound d δ ν a b) (p : ℕ) (hp : p ∈ Set.Ioc 1 d) : ν < 1 + δ - ∑ i ∈ Finset.Iic d with p ∣ i, (a i + b i)

theorem ThueBound.very_special {d : ℕ} {δ ν : ℝ} {a b : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (htab : ThueBound d δ ν a b) (p : ℕ) (hp : p ∈ Set.Ioc 1 d) : ν < 1 + δ - (a p + b p)

theorem ThueBound.special_two {d : ℕ} {δ ν : ℝ} {a b : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (htab : ThueBound d δ ν a b) (hd : 4 ≤ d) : ν < 1 + δ - (a 2 + a 4 + (b 2 + b 4))

def S (a b c : ℕ → ℝ) (i : ℕ) : ℝ

We define S i to be a i + b i + c i.

Equations

• S a b c i = a i + b i + c i

theorem s_apply (a b c : ℕ → ℝ) (i : ℕ) : S a b c i = a i + b i + c i

theorem s_nonneg {d : ℕ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (i : ℕ) : 0 ≤ S a b c i

theorem s_zero {d : ℕ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) : S a b c 0 = 0

theorem s_rotate {a b c : ℕ → ℝ} : S b c a = S a b c

theorem s_left_comm {a b c : ℕ → ℝ} : S b a c = S a b c

theorem s_right_comm {a b c : ℕ → ℝ} : S a c b = S a b c

theorem Bound4Point4.s_version {d : ℕ} {δ ε : ℝ} {a b c : ℕ → ℝ} (h44 : Bound4Point4 d δ ε a b c) : ∑ i ∈ Finset.Iic d, S a b c i ≤ 1 + δ - ε

def GeometryBound (d : ℕ) (ε ν : ℝ) (a b c : ℕ → ℝ) : Prop

A statement of the Geometry bound. Note that this is not saying the bound holds, but defining what it means for the bound to hold. In Section4.lean, we will take this as an assumption to many statements in order to deduce bounds on ν. Elsewhere we will show that the bound holds, and thus its proof can be fed in to those lemmas which have it as an assumption.

Equations

• One or more equations did not get rendered due to their size.

theorem geometryBound_set_finite {d : ℕ} {a b c : ℕ → ℝ} : {x : ℝ | ∃ I ⊆ Finset.Icc 1 d, ∃ I' ⊆ Finset.Icc 1 d, ∃ I'' ⊆ Finset.Icc 1 d, max 1 (∑ i ∈ I, ↑i * a i + ∑ i ∈ I', ↑i * b i + ∑ i ∈ I'', ↑i * c i) - (∑ i ∈ I, a i + ∑ i ∈ I', b i + ∑ i ∈ I'', c i) = x}.Finite

The set that we are taking the infimum over in the geometry bound is a finite set.

theorem GeometryBound.special {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (h44 : Bound4Point4 d δ ε a b c) (hg : GeometryBound d ε ν a b c) (Ia Ib Ic : Finset ℕ) (hIa : Ia ⊆ Finset.Icc 1 d) (hIb : Ib ⊆ Finset.Icc 1 d) (hIc : Ic ⊆ Finset.Icc 1 d) : ν < δ + (max 1 (∑ i ∈ Ia, ↑i * a i + ∑ i ∈ Ib, ↑i * b i + ∑ i ∈ Ic, ↑i * c i) - (∑ i ∈ Ia, a i + ∑ i ∈ Ib, b i + ∑ i ∈ Ic, c i))

theorem GeometryBound.special_s {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (h44 : Bound4Point4 d δ ε a b c) (hg : GeometryBound d ε ν a b c) (I : Finset ℕ) (hI : I ⊆ Finset.Icc 1 d) : ν < δ + (max 1 (∑ i ∈ I, ↑i * S a b c i) - ∑ i ∈ I, S a b c i)

theorem GeometryBound.left_comm {d : ℕ} {ε ν : ℝ} {a b c : ℕ → ℝ} (hg : GeometryBound d ε ν a b c) : GeometryBound d ε ν b a c

theorem GeometryBound.right_comm {d : ℕ} {ε ν : ℝ} {a b c : ℕ → ℝ} (hg : GeometryBound d ε ν a b c) : GeometryBound d ε ν a c b

theorem GeometryBound.rotate {d : ℕ} {ε ν : ℝ} {a b c : ℕ → ℝ} (hg : GeometryBound d ε ν a b c) : GeometryBound d ε ν b c a

def δ_ (d : ℕ) (f : ℕ → ℝ) : ℝ

Define δ_ f to be 1 / 3 - ∑ i ≤ d, f i.

Equations

• δ_ d f = 1 / 3 - ∑ i ∈ Finset.Iic d, f i

theorem sum_eq_δ_ (d : ℕ) (f : ℕ → ℝ) : ∑ i ∈ Finset.Iic d, f i = 1 / 3 - δ_ d f

4.7

theorem bound_4_point_8 {d : ℕ} {ε : ℝ} {a b : ℕ → ℝ} (h43 : Bound4Point3 d ε a b) : δ_ d a + δ_ d b ≤ 2 / 300 + ε ^ 2

theorem bound_4_point_9_lower {d : ℕ} {δ ε : ℝ} (hε : 0 < ε) (f : ℕ → ℝ) (h45 : Bound4Point5 d δ ε f) : -2 / 300 - δ ≤ δ_ d f

theorem bound_4_point_9_upper {d : ℕ} {δ ε : ℝ} (hε : 0 < ε) (f : ℕ → ℝ) (h45 : Bound4Point5 d δ ε f) : δ_ d f ≤ 1 / 75 + δ + ε

def delta_s (d : ℕ) (a b c : ℕ → ℝ) : ℝ

Define δₛ to be the sum of the δ_ values for a, b, c.

Equations

• delta_s d a b c = δ_ d a + δ_ d b + δ_ d c

theorem δₛ_eq {d : ℕ} {a b c : ℕ → ℝ} : delta_s d a b c = δ_ d a + δ_ d b + δ_ d c

theorem bound_4_point_10_lower {d : ℕ} {δ ε : ℝ} {a b c : ℕ → ℝ} (hε : 0 < ε) (h44 : Bound4Point4 d δ ε a b c) : -δ < delta_s d a b c

theorem sum_s {d : ℕ} {a b c : ℕ → ℝ} : ∑ i ∈ Finset.Iic d, S a b c i = 1 - delta_s d a b c

theorem bound_4_point_10_upper {d : ℕ} {ε : ℝ} {a b c : ℕ → ℝ} (hε : 0 < ε) (hε₁ : ε ≤ 2 / 3) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) : delta_s d a b c ≤ 1e-2 + ε

theorem bound_4_point_11_2 {d : ℕ} {a : ℕ → ℝ} (h : baseAssumptions d a) (hd : 1 ≤ d) : ∑ i ∈ Finset.Icc 2 d, (↑i - 1) * a i ≤ 2 / 3 + δ_ d a

theorem bound_4_point_11_3 {d : ℕ} {a : ℕ → ℝ} (ha : baseAssumptions d a) (hd : 2 ≤ d) : ∑ i ∈ Finset.Icc 3 d, (↑i - 2) * a i ≤ 1 / 3 + a 1 + 2 * δ_ d a

theorem bound_4_point_11_4 {d : ℕ} {a : ℕ → ℝ} (ha : baseAssumptions d a) (hd : 3 ≤ d) : ∑ i ∈ Finset.Icc 4 d, (↑i - 3) * a i ≤ 2 * a 1 + a 2 + 3 * δ_ d a

theorem bound_4_point_12 {d : ℕ} {δ ν : ℝ} {a b : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (htab : ThueBound d δ ν a b) (j : ℕ) (hj : j ∈ Set.Ioc 1 d) (hν : 0.66 < ν) : a j + b j < 0.34 + δ

theorem bound_4_point_13 {d : ℕ} {δ ν : ℝ} {a b : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (htab : ThueBound d δ ν a b) (hd : 4 ≤ d) (hν : 0.66 < ν) : a 2 + a 4 + (b 2 + b 4) < 0.34 + δ

theorem bound_4_point_14_general {d : ℕ} {δ ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (j : ℕ) (hj : j ∈ Set.Ioc 1 d) (hν : 0.66 < ν) : S a b c j < 0.51 + 1.5 * δ

theorem bound_4_point_14_two_four {d : ℕ} {δ ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hd : 4 ≤ d) (hν : 0.66 < ν) : S a b c 2 + S a b c 4 < 0.51 + 1.5 * δ

theorem sum_s_2 {d : ℕ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (hd : 1 ≤ d) : ∑ i ∈ Finset.Icc 2 d, (↑i - 1) * S a b c i ≤ 2 + delta_s d a b c

theorem sum_s_3 {d : ℕ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (hd : 2 ≤ d) : ∑ i ∈ Finset.Icc 3 d, (↑i - 2) * S a b c i ≤ 1 + S a b c 1 + 2 * delta_s d a b c

theorem sum_s_4 {d : ℕ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (hd : 3 ≤ d) : ∑ i ∈ Finset.Icc 4 d, (↑i - 3) * S a b c i ≤ 2 * S a b c 1 + S a b c 2 + 3 * delta_s d a b c

theorem bound_4_point_15 {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h44 : Bound4Point4 d δ ε a b c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hδ : δ ≤ 6e-2) (hν : 0.66 < ν) (hd : 2 ≤ d) : S a b c 1 + S a b c 2 ≤ 0.34 + δ

def SubSums (j : ℕ) (a b c : ℕ → ℝ) : Set ℝ

4.16

Equations

• SubSums j a b c = {a j, b j, c j, a j + b j, a j + c j, b j + c j, a j + b j + c j}

theorem GeometryBound.subSums {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (h44 : Bound4Point4 d δ ε a b c) (hg : GeometryBound d ε ν a b c) {τ : ℝ} (j : ℕ) (hj : j ∈ Set.Icc 3 d) (hτ : τ ∈ SubSums j a b c) : ν < δ + (max 1 (S a b c 1 + 2 * S a b c 2 + ↑j * τ) - (S a b c 1 + S a b c 2 + τ)) ∧ ν < δ + (max 1 (S a b c 1 + ↑j * τ) - (S a b c 1 + τ))

theorem bound_4_point_17 {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (h44 : Bound4Point4 d δ ε a b c) (hg : GeometryBound d ε ν a b c) (τ : ℝ) {j : ℕ} (hτ : τ ∈ SubSums j a b c) (hν : 0.66 < ν) (hj : j ∈ Set.Icc 3 d) : τ ∉ Set.Icc (0.34 - S a b c 1 - S a b c 2 + δ) ((0.66 - S a b c 2 - δ) / (↑j - 1))

theorem bound_4_point_17_3 {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (h44 : Bound4Point4 d δ ε a b c) (hg : GeometryBound d ε ν a b c) (τ : ℝ) (hτ : τ ∈ SubSums 3 a b c) (hν : 0.66 < ν) (hd : 3 ≤ d) : τ ∉ Set.Icc (0.34 - S a b c 1 - S a b c 2 + δ) (0.33 - 1 / 2 * S a b c 2 - 1 / 2 * δ)

theorem bound_4_point_18_aux {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (h44 : Bound4Point4 d δ ε a b c) (hg : GeometryBound d ε ν a b c) (τ : ℝ) (hτ : τ ∈ SubSums 3 a b c) (hν : 0.66 < ν) (hd : 3 ≤ d) : τ ∉ Set.Icc (0.34 - S a b c 1 + δ) (0.33 - 1 / 2 * δ)

theorem bound_4_point_18 {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (h44 : Bound4Point4 d δ ε a b c) (hg : GeometryBound d ε ν a b c) (τ : ℝ) (hτ : τ ∈ SubSums 3 a b c) (hd : 3 ≤ d) (hν : 0.66 < ν) : τ ∉ Set.Icc (0.34 - S a b c 1 - S a b c 2 + δ) (0.33 - 1 / 2 * S a b c 2 - 1 / 2 * δ) ∪ Set.Icc (0.34 - S a b c 1 + δ) (0.33 - 1 / 2 * δ)

theorem bound_4_point_19_first {d : ℕ} {a : ℕ → ℝ} (ha : baseAssumptions d a) (hd : 3 ≤ d) : 1 / 3 - 4 * δ_ d a - 3 * a 1 - 2 * a 2 ≤ a 3

theorem bound_4_point_19_second {d : ℕ} {a : ℕ → ℝ} (ha : baseAssumptions d a) (hd : 4 ≤ d) : 1 / 3 - 5 / 2 * δ_ d a - 2 * a 1 - 3 / 2 * a 2 - 1 / 2 * a 4 ≤ a 3

theorem bound_4_point_20 {d : ℕ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (hd : 3 ≤ d) : 1 - 4 * delta_s d a b c - 3 * S a b c 1 - 2 * S a b c 2 ≤ S a b c 3

theorem bound_4_point_21 {d : ℕ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (hd : 4 ≤ d) : 1 - 5 / 2 * delta_s d a b c - 2 * S a b c 1 - 3 / 2 * S a b c 2 - 1 / 2 * S a b c 4 ≤ S a b c 3

theorem bound_4_point_22 {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h44 : Bound4Point4 d δ ε a b c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hν : 0.66 < ν) (hs₂ : 0.3 ≤ S a b c 2) (hδ : δ ≤ 6e-2) (hd : 2 ≤ d) : S a b c 1 ≤ 4e-2 + δ

theorem case_1_helper {d : ℕ} {δ ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hν : 0.66 < ν) (hs₂ : 0.3 ≤ S a b c 2) (hd : 4 ≤ d) : S a b c 4 < 0.21 + 3 / 2 * δ

theorem subcase_1_point_1 {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) (h44 : Bound4Point4 d δ ε a b c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 4 ≤ d) (hν : 0.66 < ν) (hδ : δ ≤ 3e-3) (hcb : c 3 ≤ b 3) (hs₂ : 0.3 ≤ S a b c 2) (hε : ε ≤ 1 / 10000) (hε₀ : 0 < ε) (hb₃ : b 3 ≤ 0.34 - S a b c 1 - S a b c 2 + δ) : False

theorem bound_4_point_23 {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (h44 : Bound4Point4 d δ ε a b c) (hg : GeometryBound d ε ν a b c) (hd : 3 ≤ d) (hν : 0.66 < ν) (hb₃ : 0.34 - S a b c 1 - S a b c 2 + δ < b 3) : 0.33 - 1 / 2 * S a b c 2 - 1 / 2 * δ < b 3

theorem b4_bound {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h44 : Bound4Point4 d δ ε a b c) (h45b : Bound4Point5 d δ ε b) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 4 ≤ d) (hν : 0.66 < ν) (hb₃ : 0.34 - S a b c 1 - S a b c 2 + δ < b 3) (hε₀ : 0 < ε) (hδ : δ ≤ 3e-3) (hε : ε ≤ 1 / 10000) : b 4 < (0.66 - S a b c 2 - δ) / 3

theorem b5_bound {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h44 : Bound4Point4 d δ ε a b c) (h45b : Bound4Point5 d δ ε b) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 5 ≤ d) (hν : 0.66 < ν) (hb₃ : 0.34 - S a b c 1 - S a b c 2 + δ < b 3) (hε₀ : 0 < ε) (hδ : δ ≤ 3e-3) (hε : ε ≤ 1 / 10000) : b 5 < (0.66 - S a b c 2 - δ) / 4

theorem b6_bound {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h44 : Bound4Point4 d δ ε a b c) (h45b : Bound4Point5 d δ ε b) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 6 ≤ d) (hν : 0.66 < ν) (hb₃ : 0.34 - S a b c 1 - S a b c 2 + δ < b 3) (hε₀ : 0 < ε) (hδ : δ ≤ 3e-3) (hε : ε ≤ 1 / 10000) : b 6 < (0.66 - S a b c 2 - δ) / 5

theorem a4_bound {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h44 : Bound4Point4 d δ ε a b c) (h45a : Bound4Point5 d δ ε a) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 4 ≤ d) (hν : 0.66 < ν) (hb₃ : 0.34 - S a b c 1 - S a b c 2 + δ < b 3) (hε₀ : 0 < ε) (hδ : δ ≤ 3e-3) (hε : ε ≤ 1 / 10000) (hba : b 3 ≤ a 3) : a 4 < (0.66 - S a b c 2 - δ) / 3

theorem a5_bound {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h44 : Bound4Point4 d δ ε a b c) (h45a : Bound4Point5 d δ ε a) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 5 ≤ d) (hν : 0.66 < ν) (hb₃ : 0.34 - S a b c 1 - S a b c 2 + δ < b 3) (hε₀ : 0 < ε) (hδ : δ ≤ 3e-3) (hε : ε ≤ 1 / 10000) (hba : b 3 ≤ a 3) : a 5 < (0.66 - S a b c 2 - δ) / 4

theorem a6_bound {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h44 : Bound4Point4 d δ ε a b c) (h45a : Bound4Point5 d δ ε a) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 6 ≤ d) (hν : 0.66 < ν) (hb₃ : 0.34 - S a b c 1 - S a b c 2 + δ < b 3) (hε₀ : 0 < ε) (hδ : δ ≤ 3e-3) (hε : ε ≤ 1 / 10000) (hba : b 3 ≤ a 3) : a 6 < (0.66 - S a b c 2 - δ) / 5

theorem self_improve_bounds {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h44 : Bound4Point4 d δ ε a b c) (h45a : Bound4Point5 d δ ε a) (h45b : Bound4Point5 d δ ε b) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 6 ≤ d) (hν : 0.66 < ν) (hb₃ : 0.34 - S a b c 1 - S a b c 2 + δ < b 3) (hε₀ : 0 < ε) (hδ : δ ≤ 3e-3) (hε : ε ≤ 1 / 10000) (hba : b 3 ≤ a 3) : max (a 4) (b 4) < 0.34 - S a b c 1 - S a b c 2 + δ ∧ max (a 5) (b 5) < 0.34 - S a b c 1 - S a b c 2 + δ ∧ max (a 6) (b 6) < 0.34 - S a b c 1 - S a b c 2 + δ

theorem test {α : Type u_1} [AddCommMonoid α] {a b : ℕ} {f : ℕ → α} (hab : a ≤ b) : ∑ i ∈ Finset.Iic a, f i + ∑ i ∈ Finset.Icc (a + 1) b, f i = ∑ i ∈ Finset.Iic b, f i

theorem apply_fourier {d : ℕ} {δ ν : ℝ} {a b : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hfab : FourierBound d δ ν a b) (hd : 6 ≤ d) : 2 * ν - 1 - δ < 2 / 3 - (δ_ d a + δ_ d b) - ∑ i ∈ Finset.Iic 6with i ≠ 2, min (a i) (b i) - (a 2 + b 2)

theorem two_bound {d : ℕ} {a : ℕ → ℝ} (ha : baseAssumptions d a) (hd : 6 ≤ d) : 4 / 15 - 1 / 5 * ∑ i ∈ Finset.Iic 6with i ≠ 2, (7 - ↑i) * a i - 7 / 5 * δ_ d a ≤ a 2

theorem summation_range_eq : {x ∈ Finset.Iic 6 | x ≠ 2} = {0, 1, 3, 4, 5, 6}

theorem bound_4_point_24 {d : ℕ} {δ ν : ℝ} {a b : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hfab : FourierBound d δ ν a b) (hd : 6 ≤ d) (hba : b 3 ≤ a 3) : 2 * ν - 1 - δ < 2 / 15 + 2 / 5 * (δ_ d a + δ_ d b) + 1 / 5 * (6 * max (a 1) (b 1) + min (a 1) (b 1) + 4 * a 3 - b 3 + 3 * max (a 4) (b 4) + 2 * max (a 5) (b 5) + max (a 6) (b 6))

theorem subcase_1_point_2_aux {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (h44 : Bound4Point4 d δ ε a b c) (htab : ThueBound d δ ν a b) (hg : GeometryBound d ε ν a b c) (hd : 3 ≤ d) (hν : 0.66 < ν) (hb₃ : 0.34 - S a b c 1 - S a b c 2 + δ < b 3) : 4 * a 3 - b 3 ≤ 5 / 2 * S a b c 2 - 0.29 + 13 / 2 * δ

theorem subcase_1_point_2 {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h44 : Bound4Point4 d δ ε a b c) (h45a : Bound4Point5 d δ ε a) (h45b : Bound4Point5 d δ ε b) (hfab : FourierBound d δ ν a b) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 6 ≤ d) (hν : 0.66 < ν) (hba : b 3 ≤ a 3) (hs₂ : 0.3 ≤ S a b c 2) (hb₃ : 0.34 - S a b c 1 - S a b c 2 + δ < b 3) (hε₀ : 0 < ε) (hδ : δ ≤ 3e-3) (hε : ε ≤ 1 / 10000) : False

theorem case_1 {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) (h44 : Bound4Point4 d δ ε a b c) (h45a : Bound4Point5 d δ ε a) (h45b : Bound4Point5 d δ ε b) (hfab : FourierBound d δ ν a b) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 6 ≤ d) (hν : 0.66 < ν) (hs₂ : 0.3 ≤ S a b c 2) (hδ : δ ≤ 3e-3) (hε₀ : 0 < ε) (hε : ε ≤ 1 / 10000) (hcb : c 3 ≤ b 3) (hba : b 3 ≤ a 3) : False

theorem bound_4_point_25 {d : ℕ} {δ ν : ℝ} {a b : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (htab : ThueBound d δ ν a b) (hd : 3 ≤ d) (hν : 0.66 < ν) (h : b 3 ≤ a 3) : b 3 < 0.17 + 1 / 2 * δ

theorem bound_4_point_26_aux {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (h44 : Bound4Point4 d δ ε a b c) (htab : ThueBound d δ ν a b) (hg : GeometryBound d ε ν a b c) (hd : 3 ≤ d) (hν : 0.66 < ν) (hs₂ : S a b c 2 < 0.3) (hδ : δ ≤ 1e-2) (hba : b 3 ≤ a 3) (hcb : c 3 ≤ b 3) : b 3 < 0.34 - S a b c 1 - S a b c 2 + δ ∧ c 3 < 0.34 - S a b c 1 - S a b c 2 + δ

theorem bound_4_point_26 {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h44 : Bound4Point4 d δ ε a b c) (htab : ThueBound d δ ν a b) (hg : GeometryBound d ε ν a b c) (hd : 3 ≤ d) (hν : 0.66 < ν) (hs₂ : S a b c 2 < 0.3) (hδ : δ ≤ 1e-2) (hba : b 3 ≤ a 3) (hcb : c 3 ≤ b 3) : 0.32 - 4 * delta_s d a b c - S a b c 1 - 2 * δ ≤ a 3

theorem case_2_subcase_1_large_sum {d : ℕ} {δ ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (hd : 4 ≤ d) (hν : 0.66 < ν) (hδ : δ ≤ 15e-3) (h : 0.32 ≤ a 3) (hmax : ∃ i ∈ Set.Icc 4 d, 3 / 4 * 9e-2 < max (b i) (c i)) : False

theorem GeometryBound.s21_application_basic {d : ℕ} {ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (hg : GeometryBound d ε ν a b c) (hd : 4 ≤ d) : ν < ε + a 3 + b 3 + min (b 4) (c 4) + ∑ i ∈ Finset.Icc 5 d, (b i + c i) + max 0 (∑ i ∈ Finset.Icc 1 d, ↑i * a i + (b 1 + c 1) + 2 * (b 2 + c 2) - 3 * (a 3 - c 3) + 4 * max (b 4) (c 4) - 1)

theorem min_le_half_add {x y : ℝ} : min x y ≤ (x + y) / 2

theorem case_2_subcase_1_subsubcase_1 {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43bc : Bound4Point3 d ε b c) (htab : ThueBound d δ ν a b) (hd : 5 ≤ d) (hν : 0.66 < ν) (h₅ : b 5 + c 5 ≤ 0.135) (hε₀ : 0 ≤ ε) (hε : ε ≤ 1 / 10000) (hδ : δ ≤ 5e-3) (h : ∑ i ∈ Finset.Iic d, (↑i - 1) * (b i + c i) ≤ 4 / 3 + (δ_ d b + δ_ d c)) : a 3 + b 3 + min (b 4) (c 4) + ∑ i ∈ Finset.Icc 5 d, (b i + c i) < 0.645

theorem case_2_subcase_1_subsubcase_2 {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (htac : ThueBound d δ ν a c) (hd : 4 ≤ d) (hν : 0.66 < ν) (hs₂ : S a b c 2 < 0.3) (h₄ : max (b 4) (c 4) ≤ 3 / 4 * 9e-2) (hε₀ : 0 < ε) (hδ : δ ≤ 5e-3) (h : 0.32 ≤ a 3) : a 3 + b 3 + min (b 4) (c 4) + ∑ i ∈ Finset.Icc 5 d, (b i + c i) + (∑ i ∈ Finset.Icc 1 d, ↑i * a i + (b 1 + c 1) + 2 * (b 2 + c 2) - 3 * (a 3 - c 3) + 4 * max (b 4) (c 4) - 1) < 0.61

theorem case_2_subcase_1 {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43bc : Bound4Point3 d ε b c) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (hg : GeometryBound d ε ν a b c) (hd : 5 ≤ d) (hν : 0.66 < ν) (hs₂ : S a b c 2 < 0.3) (hδ : δ ≤ 5e-3) (hε₀ : 0 < ε) (hε : ε ≤ 1 / 10000) (h : 0.32 ≤ a 3) : False

theorem case_2_subcase_2 {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) (h44 : Bound4Point4 d δ ε a b c) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 5 ≤ d) (hν : 0.66 < ν) (hs₂ : S a b c 2 < 0.3) (hδ : δ ≤ 5e-3) (hε₀ : 0 < ε) (hε : ε ≤ 1 / 10000) (h : b 3 + c 3 < 0.33 - 1 / 2 * S a b c 2 - 1 / 2 * δ) : False

theorem case_2_subcase_3 {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) (h44 : Bound4Point4 d δ ε a b c) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 5 ≤ d) (hν : 0.66 < ν) (hs₂ : S a b c 2 < 0.3) (hδ : δ ≤ 3e-3) (hε₀ : 0 < ε) (hε : ε ≤ 1 / 10000) (hba : b 3 ≤ a 3) (hcb : c 3 ≤ b 3) (h : 0.73 < 4 * S a b c 1 + 3 * S a b c 2) : False

theorem case_2_subcase_4 {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) (h44 : Bound4Point4 d δ ε a b c) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 5 ≤ d) (hν : 0.66 < ν) (hs₂ : S a b c 2 < 0.3) (hδ : δ ≤ 4e-3) (hε₀ : 0 < ε) (hε : ε ≤ 1 / 100000) (hba : b 3 ≤ a 3) (hcb : c 3 ≤ b 3) (h : 4 * S a b c 1 + S a b c 2 < 0.35) : False

theorem case_2_subcase_5 {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) (h44 : Bound4Point4 d δ ε a b c) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 5 ≤ d) (hν : 0.66 < ν) (hs₂ : S a b c 2 < 0.3) (hδ : δ ≤ 3e-3) (hε₀ : 0 < ε) (hε : ε ≤ 1 / 100000) (hba : b 3 ≤ a 3) (hcb : c 3 ≤ b 3) (h : S a b c 2 ∈ Set.Icc 7e-2 0.199) : False

theorem case_2_subcase_6_end_ab {d : ℕ} {δ ε ν : ℝ} {a b : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (h45a : Bound4Point5 d δ ε a) (h45b : Bound4Point5 d δ ε b) (hfab : FourierBound d δ ν a b) (hd : 5 ≤ d) (hδ : δ ≤ 1e-3) (hε₀ : 0 < ε) (hε : ε ≤ 1 / 100000) (hba : b 3 ≤ a 3) : ν ≤ 0.78451 + 1 / 3 * (max (a 2) (b 2) - a 3) - 1 / 2 * b 3

theorem case_2_subcase_6_end_ec {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h45a : Bound4Point5 d δ ε a) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (hfab : FourierBound d δ ν a b) (hfac : FourierBound d δ ν a c) (hfbc : FourierBound d δ ν b c) (hd : 5 ≤ d) (hν : 0.66 < ν) (hδ : δ ≤ 1e-3) (hε₀ : 0 < ε) (hε : ε ≤ 1 / 100000) (hba : b 3 ≤ a 3) (hcb : c 3 ≤ b 3) (hbc3' : 0.33 - 1 / 2 * δ ≤ b 3 + c 3) (hs2 : S a b c 2 ≤ 7e-2) : False

theorem case_2_subcase_6 {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) (h44 : Bound4Point4 d δ ε a b c) (h45a : Bound4Point5 d δ ε a) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (hfab : FourierBound d δ ν a b) (hfac : FourierBound d δ ν a c) (hfbc : FourierBound d δ ν b c) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 5 ≤ d) (hν : 0.66 < ν) (hs₂ : S a b c 2 < 0.3) (hδ : δ ≤ 1e-3) (hε₀ : 0 < ε) (hε : ε ≤ 1 / 100000) (hba : b 3 ≤ a 3) (hcb : c 3 ≤ b 3) (h : 25e-3 < 2 * S a b c 1 - S a b c 2) : False

theorem case_2 {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) (h44 : Bound4Point4 d δ ε a b c) (h45a : Bound4Point5 d δ ε a) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (hfab : FourierBound d δ ν a b) (hfac : FourierBound d δ ν a c) (hfbc : FourierBound d δ ν b c) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 5 ≤ d) (hν : 0.66 < ν) (hs₂ : S a b c 2 < 0.3) (hδ : δ ≤ 1e-3) (hε₀ : 0 < ε) (hε : ε ≤ 1 / 100000) (hba : b 3 ≤ a 3) (hcb : c 3 ≤ b 3) : False

theorem thm_4_point_3_asymm {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) (h44 : Bound4Point4 d δ ε a b c) (h45a : Bound4Point5 d δ ε a) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (hfab : FourierBound d δ ν a b) (hfac : FourierBound d δ ν a c) (hfbc : FourierBound d δ ν b c) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 6 ≤ d) (hδ : δ ≤ 1e-3) (hε₀ : 0 < ε) (hε : ε ≤ 1 / 100000) (hba : b 3 ≤ a 3) (hcb : c 3 ≤ b 3) : ν ≤ 0.66

theorem thm_4_point_3 {d : ℕ} {δ ε ν : ℝ} {a b c : ℕ → ℝ} (ha : baseAssumptions d a) (hb : baseAssumptions d b) (hc : baseAssumptions d c) (h43ab : Bound4Point3 d ε a b) (h43ac : Bound4Point3 d ε a c) (h43bc : Bound4Point3 d ε b c) (h44 : Bound4Point4 d δ ε a b c) (h45a : Bound4Point5 d δ ε a) (h45b : Bound4Point5 d δ ε b) (h45c : Bound4Point5 d δ ε c) (hfab : FourierBound d δ ν a b) (hfac : FourierBound d δ ν a c) (hfbc : FourierBound d δ ν b c) (hdab : DeterminantBound d δ ν a b) (hdac : DeterminantBound d δ ν a c) (hdbc : DeterminantBound d δ ν b c) (htab : ThueBound d δ ν a b) (htac : ThueBound d δ ν a c) (htbc : ThueBound d δ ν b c) (hg : GeometryBound d ε ν a b c) (hd : 6 ≤ d) (hδ : δ ≤ 1e-3) (hε₀ : 0 < ε) (hε : ε ≤ 1 / 100000) : ν ≤ 0.66