def SG_C₅ : NNReal

Equations

• SG_C₅ = 2 ^ 49

noncomputable def SG_C₄ : NNReal

Equations

• SG_C₄ = 4 + 16 * (SG_C₅ + 2)

noncomputable def SG_C₃ : NNReal

Equations

• SG_C₃ = 4 * NNReal.sqrt (SG_C₄ + 1)

noncomputable def SG_C₂ : NNReal

Equations

• SG_C₂ = SG_C₃ + 16

noncomputable def SG_C : NNReal

Equations

• SG_C = SG_C₂ + 1

noncomputable def ST_C₄ : NNReal

Equations

• ST_C₄ = SG_C + 2

noncomputable def ST_C₃ : NNReal

Equations

• ST_C₃ = (ST_C₄ + 73) ^ (1 / 4)

noncomputable def ST_C₂ : NNReal

Equations

• ST_C₂ = NNReal.sqrt (2 * (ST_C₃ + NNReal.sqrt 2 / 4))

noncomputable def ST_C : NNReal

Equations

• ST_C = ST_C₂ + 1

noncomputable def SG_eps₃ (α : ℝ) : ℝ

Equations

• SG_eps₃ α = min (min (11 / 439) (15 / 136 * α)) (α / 4 / (↑(full_C (α / 4)) * 9212 / 45))

noncomputable def SG_eps₂ (α : ℝ) : ℝ

Equations

• SG_eps₂ α = 2 / 3 * SG_eps₃ α

noncomputable def SG_eps (α : ℝ) : ℝ

Equations

• SG_eps α = 13 / 30 * SG_eps₂ α

noncomputable def ST_prime_field_eps₃ (α : ℝ) : ℝ

Equations

• ST_prime_field_eps₃ α = 12 / 13 * SG_eps α

noncomputable def ST_prime_field_eps₂ (α : ℝ) : ℝ

Equations

• ST_prime_field_eps₂ α = ST_prime_field_eps₃ α / 4

noncomputable def ST_prime_field_eps (α : ℝ) : ℝ

Equations

• ST_prime_field_eps α = ST_prime_field_eps₂ α / 3

theorem ntlSGeps (β : ℝ) : SG_eps₃ β < 45 / 1756

theorem ntlSGeps' (β : ℝ) : SG_eps₃ β ≤ 15 / 136 * β

theorem full_C_neq_zero (x : ℝ) : full_C x ≠ 0

theorem pos_SGeps₃ (β : ℝ) (h : 0 < β) : 0 < SG_eps₃ β

theorem pos_ST_prime_field_eps (α : ℝ) (h : 0 < α) : 0 < ST_prime_field_eps α

theorem one_le_SG_C₃ : 1 ≤ SG_C₃

theorem SG_C₃_pos : 0 < SG_C₃

theorem one_le_ST_C₃ : 1 ≤ ST_C₃

theorem ST_C₃_pos : 0 < ST_C₃

theorem ST_C_pos : 0 < ST_C

theorem lemma1 (β : ℝ) : 1 / 2 + 2 * ST_prime_field_eps β ≤ 1 - 4 * ST_prime_field_eps₂ β

theorem lemma2 (β : ℝ) : 4 * ST_prime_field_eps₂ β ≤ 1

theorem lemma3 (β : ℝ) : ST_prime_field_eps₂ β + 6 * ST_prime_field_eps β ≤ 1 - 4 * ST_prime_field_eps₂ β

theorem lemma4 (β : ℝ) : 1 ≤ 3 / 2 - SG_eps β

theorem lemma5 (β : ℝ) : 1 + (2⁻¹ - SG_eps β) ≠ 0

theorem lemma6 (β : ℝ) : 1 + 4 * ST_prime_field_eps β ≤ 3 / 2 - SG_eps β

theorem lemma7 (β : ℝ) : 1 / 2 + SG_eps β ≤ 1 + (-(SG_eps β * 2) - ST_prime_field_eps β * 4)

theorem lemma8 (β : ℝ) : 0 ≤ 1 / 2 - SG_eps₂ β - SG_eps β - 4 * ST_prime_field_eps β

theorem lemma9 (β : ℝ) (h : 0 < β) : 0 ≤ ST_prime_field_eps β

theorem lemma10 (β : ℝ) (h : 0 < β) : 0 ≤ SG_eps₃ β

theorem lemma11 (β : ℝ) (h : 0 < β) : β / 4 < β / 2 - 439 / 45 * β * SG_eps₃ β

theorem lemma12 (β : ℝ) (h : 0 < β) : 0 < β / 2 - 439 / 45 * β * SG_eps₃ β

theorem lemma13 (β : ℝ) : ST_prime_field_eps β * 6 + SG_eps₂ β + SG_eps β ≤ 1 / 2 - 439 / 45 * SG_eps₃ β

theorem lemma14 (β : ℝ) : 0 ≤ 1 / 2 - 439 / 45 * SG_eps₃ β

theorem lemma15 (β : ℝ) (h : 0 < β) : 0 ≤ 1 / 2 + 8 * ST_prime_field_eps β + SG_eps₂ β + SG_eps β

theorem lemma16 (β : ℝ) : 0 ≤ 1 / 2 - 113 / 30 * SG_eps₃ β

theorem final_theorem (β : ℝ) (h : 0 < β) (n : ℕ+) (p : ℕ) [instpprime : Fact (Nat.Prime p)] (h₁ : ↑↑n ≤ ↑p ^ (2 - β)) (h₂ : SG_C₅ * (1 / 4) ≤ ↑↑n ^ (ST_prime_field_eps β * 6 + SG_eps₂ β + SG_eps β)) : (2 ^ 110 * (256 * ↑↑n ^ (8 * ST_prime_field_eps β + 2 * SG_eps₃ β)) ^ 42) ^ full_C (β / 2 - 439 / 45 * β * SG_eps₃ β) < ↑p ^ min (β / 2 - 17 / 15 * (2 - β) * SG_eps₃ β) (β / 2 - 113 / 30 * β * SG_eps₃ β) / 2