LeanPool.RamanujanTauMissesPrimes.Solution

noncomputable def Nat.radical (n : ℕ) : ℕ

The radical of n: the product of its distinct prime factors (and 0 when n = 0).

Equations

• n.radical = if n = 0 then 0 else ∏ p ∈ n.primeFactors, p

structure RamanujanTau : Type

An axiomatic Ramanujan tau function: a function ℕ+ → ℤ satisfying Hecke multiplicativity, the Hecke recurrence at prime powers, the parity criterion, Deligne's bound and the non-unit property.

• τ : ℕ+ → ℤ

  The underlying function ℕ+ → ℤ.

• hecke_mult (m n : ℕ+) : (↑m).Coprime ↑n → self.τ (m * n) = self.τ m * self.τ n
• hecke_rec (p : ℕ+) : Nat.Prime ↑p → ∀ (m : ℕ), 2 ≤ m → self.τ (p ^ m) = self.τ p * self.τ (p ^ (m - 1)) - ↑↑p ^ 11 * self.τ (p ^ (m - 2))
• parity (n : ℕ+) : ¬2 ∣ self.τ n ↔ Odd ↑n ∧ IsSquare ↑n
• deligne_bound (p : ℕ+) : Nat.Prime ↑p → |↑(self.τ p)| ≤ 2 * ↑↑p ^ (11 / 2)
• non_unit (n : ℕ+) : 2 ≤ ↑n → self.τ n ≠ 1 ∧ self.τ n ≠ -1

noncomputable def tauPrimeSet (R : RamanujanTau) (X : ℝ) : Set ℕ

The set of positive primes ℓ ≤ X such that |τ n| = ℓ for some n ≥ 1.

Equations

• tauPrimeSet R X = {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (n : ℕ+), (R.τ n).natAbs = ℓ}

noncomputable def S (R : RamanujanTau) (X : ℝ) : ℕ

S X is the number of primes ℓ ≤ X taken (in absolute value) by τ.

Equations

• S R X = (tauPrimeSet R X).ncard

noncomputable def E2Set (X : ℝ) : Set (ℕ+ × ℤ)

The pairs (x, y) ∈ ℕ+ × ℤ with x > X ^ (2/11) and 1 ≤ |x ^ 11 - y ^ 2| ≤ X.

Equations

• E2Set X = {p : ℕ+ × ℤ | ↑↑p.1 > X ^ (2 / 11) ∧ 1 ≤ |↑↑p.1 ^ 11 - p.2 ^ 2| ∧ |↑↑↑p.1 ^ 11 - ↑p.2 ^ 2| ≤ X}

noncomputable def E2 (X : ℝ) : ℕ

E2 X is the cardinality of E2Set X.

Equations

• E2 X = (E2Set X).ncard

noncomputable def E4Set (X : ℝ) : Set (ℕ+ × ℤ)

The pairs (x, u) ∈ ℕ+ × ℤ with x > X ^ (1/11) and 1 ≤ |u ^ 2 - 5 * x ^ 22| ≤ 4 * X.

Equations

• E4Set X = {p : ℕ+ × ℤ | ↑↑p.1 > X ^ (1 / 11) ∧ 1 ≤ |p.2 ^ 2 - 5 * ↑↑p.1 ^ 22| ∧ |↑p.2 ^ 2 - 5 * ↑↑↑p.1 ^ 22| ≤ 4 * X}

noncomputable def E4 (X : ℝ) : ℕ

E4 X is the cardinality of E4Set X.

Equations

• E4 X = (E4Set X).ncard

def ABC : Prop

The ABC conjecture: for every ε > 0 there is K > 0 with c ≤ K * rad (a * b * c) ^ (1 + ε) for all coprime positive a + b = c.

Equations

• ABC = ∀ (ε : ℝ), 0 < ε → ∃ (K : ℝ), 0 < K ∧ ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → a.Coprime b → a + b = c → ↑c ≤ K * ↑(a * b * c).radical ^ (1 + ε)

def oddPrimesSigned : Set ℤ

The set of signed odd primes {±ℓ : ℓ an odd prime}.

Equations

• oddPrimesSigned = {z : ℤ | ∃ (p : ℕ), Nat.Prime p ∧ p ≠ 2 ∧ (z = ↑p ∨ z = -↑p)}

def X2k (R : RamanujanTau) (k : ℕ) : Set ℤ

X2k R k = {τ (p ^ (2 * k)) : p a positive prime}.

Equations

• X2k R k = {z : ℤ | ∃ (p : ℕ+), Nat.Prime ↑p ∧ z = R.τ (p ^ (2 * k))}

def Proposition54 (R : RamanujanTau) : Prop

The (sharper, N ^ (1/2)) form of Xiong's Proposition 5.4 used as a hypothesis.

Equations

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

noncomputable def tauWitness (R : RamanujanTau) (k ℓ : ℕ) : ℤ

A choice of value τ (p ^ (2 * k)) whose absolute value is ℓ, when such a prime p exists; otherwise 0.

Equations

• tauWitness R k ℓ = if h : ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ then R.τ (h.choose ^ (2 * k)) else 0

theorem tauWitness_natAbs (R : RamanujanTau) (k ℓ : ℕ) (hw : ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ) : (tauWitness R k ℓ).natAbs = ℓ

theorem tauWitness_mem_oddPrimesSigned (R : RamanujanTau) (k ℓ : ℕ) (hprime : Nat.Prime ℓ) (hne2 : ℓ ≠ 2) (hw : ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ) : tauWitness R k ℓ ∈ oddPrimesSigned

theorem tauWitness_mem_X2k (R : RamanujanTau) (k ℓ : ℕ) (hw : ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ) : tauWitness R k ℓ ∈ X2k R k

theorem tauWitness_abs_le (R : RamanujanTau) (k ℓ : ℕ) (X : ℝ) (hle : ↑ℓ ≤ X) (hw : ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ) : |↑(tauWitness R k ℓ)| ≤ X

theorem int_abs_le_subset_Icc (X : ℝ) : {z : ℤ | |↑z| ≤ X} ⊆ Set.Icc (-⌈X⌉) ⌈X⌉

theorem target_set_finite (R : RamanujanTau) (k : ℕ) (X : ℝ) (_hX : 0 < X) : (oddPrimesSigned ∩ X2k R k ∩ {z : ℤ | |↑z| ≤ X}).Finite

theorem tauWitness_injOn (R : RamanujanTau) (k : ℕ) (X : ℝ) : Set.InjOn (tauWitness R k) {ℓ : ℕ | Nat.Prime ℓ ∧ ℓ ≠ 2 ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ}

theorem per_k_odd_prime_ncard_le (R : RamanujanTau) (k : ℕ) (X : ℝ) (hX : 0 < X) : {ℓ : ℕ | Nat.Prime ℓ ∧ ℓ ≠ 2 ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ}.ncard ≤ (oddPrimesSigned ∩ X2k R k ∩ {z : ℤ | |↑z| ≤ X}).ncard

theorem even_prime_subset_singleton (R : RamanujanTau) (X : ℝ) : {ℓ : ℕ | Nat.Prime ℓ ∧ ℓ = 2 ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ∃ (k : ℕ), 3 ≤ k ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ} ⊆ {2}

theorem even_prime_ncard_le (R : RamanujanTau) (X : ℝ) (_hX : 0 < X) : {ℓ : ℕ | Nat.Prime ℓ ∧ ℓ = 2 ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ∃ (k : ℕ), 3 ≤ k ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ}.ncard ≤ 1

theorem natAbs_ne_zero_of_eq_prime {n : ℤ} {ℓ : ℕ} (hprime : Nat.Prime ℓ) (heq : n.natAbs = ℓ) : n.natAbs ≠ 0

theorem k_le_K_of_prime_witness (R : RamanujanTau) (X : ℝ) (K : ℕ) (hvanish : ∀ (k : ℕ), K < k → ∀ (p : ℕ+), Nat.Prime ↑p → (R.τ (p ^ (2 * k))).natAbs ≠ 0 → ¬↑(R.τ (p ^ (2 * k))).natAbs ≤ X) (ℓ : ℕ) (hprime : Nat.Prime ℓ) (hle : ↑ℓ ≤ X) (p : ℕ+) (hp : Nat.Prime ↑p) (k : ℕ) (_hk3 : 3 ≤ k) (heq : (R.τ (p ^ (2 * k))).natAbs = ℓ) : k ≤ K

theorem target_subset_finite_union (R : RamanujanTau) (X : ℝ) (_hX : 0 < X) (K : ℕ) (_hK : 3 ≤ K) (hvanish : ∀ (k : ℕ), K < k → ∀ (p : ℕ+), Nat.Prime ↑p → (R.τ (p ^ (2 * k))).natAbs ≠ 0 → ¬↑(R.τ (p ^ (2 * k))).natAbs ≤ X) : {ℓ : ℕ | Nat.Prime ℓ ∧ ℓ ≠ 2 ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ∃ (k : ℕ), 3 ≤ k ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ} ⊆ ⋃ k ∈ Finset.Icc 3 K, {ℓ : ℕ | Nat.Prime ℓ ∧ ℓ ≠ 2 ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ}

theorem biUnion_per_k_finite (R : RamanujanTau) (X : ℝ) (K : ℕ) : (⋃ k ∈ Finset.Icc 3 K, {ℓ : ℕ | Nat.Prime ℓ ∧ ℓ ≠ 2 ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ}).Finite

theorem target_ncard_le_sum_nat (R : RamanujanTau) (X : ℝ) (hX : 0 < X) (K : ℕ) (hK : 3 ≤ K) (hvanish : ∀ (k : ℕ), K < k → ∀ (p : ℕ+), Nat.Prime ↑p → (R.τ (p ^ (2 * k))).natAbs ≠ 0 → ¬↑(R.τ (p ^ (2 * k))).natAbs ≤ X) : {ℓ : ℕ | Nat.Prime ℓ ∧ ℓ ≠ 2 ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ∃ (k : ℕ), 3 ≤ k ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ}.ncard ≤ ∑ k ∈ Finset.Icc 3 K, (oddPrimesSigned ∩ X2k R k ∩ {z : ℤ | |↑z| ≤ X}).ncard

theorem odd_prime_ncard_le_sum (R : RamanujanTau) (X : ℝ) (hX : 0 < X) (K : ℕ) (hK : 3 ≤ K) (hvanish : ∀ (k : ℕ), K < k → ∀ (p : ℕ+), Nat.Prime ↑p → (R.τ (p ^ (2 * k))).natAbs ≠ 0 → ¬↑(R.τ (p ^ (2 * k))).natAbs ≤ X) : ↑{ℓ : ℕ | Nat.Prime ℓ ∧ ℓ ≠ 2 ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ∃ (k : ℕ), 3 ≤ k ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ}.ncard ≤ ∑ k ∈ Finset.Icc 3 K, ↑(oddPrimesSigned ∩ X2k R k ∩ {z : ℤ | |↑z| ≤ X}).ncard

theorem target_eq_union (R : RamanujanTau) (X : ℝ) : {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ∃ (k : ℕ), 3 ≤ k ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ} = {ℓ : ℕ | Nat.Prime ℓ ∧ ℓ = 2 ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ∃ (k : ℕ), 3 ≤ k ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ} ∪ {ℓ : ℕ | Nat.Prime ℓ ∧ ℓ ≠ 2 ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ∃ (k : ℕ), 3 ≤ k ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ}

theorem target_ncard_split (R : RamanujanTau) (X : ℝ) (_hX : 0 < X) : {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ∃ (k : ℕ), 3 ≤ k ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ}.ncard ≤ {ℓ : ℕ | Nat.Prime ℓ ∧ ℓ = 2 ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ∃ (k : ℕ), 3 ≤ k ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ}.ncard + {ℓ : ℕ | Nat.Prime ℓ ∧ ℓ ≠ 2 ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ∃ (k : ℕ), 3 ≤ k ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ}.ncard

theorem target_ncard_le_sum (R : RamanujanTau) (X : ℝ) (hX : 0 < X) (K : ℕ) (hK : 3 ≤ K) (hvanish : ∀ (k : ℕ), K < k → ∀ (p : ℕ+), Nat.Prime ↑p → (R.τ (p ^ (2 * k))).natAbs ≠ 0 → ¬↑(R.τ (p ^ (2 * k))).natAbs ≤ X) : ↑{ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ∃ (k : ℕ), 3 ≤ k ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ}.ncard ≤ 1 + ∑ k ∈ Finset.Icc 3 K, ↑(oddPrimesSigned ∩ X2k R k ∩ {z : ℤ | |↑z| ≤ X}).ncard

theorem nat_gt_floor_imp_ge (a : ℝ) (k : ℕ) (hk : ⌊a⌋₊ < k) : ↑k ≥ a

theorem tau_mem_X2k (R : RamanujanTau) (k : ℕ) (p : ℕ+) (hp : Nat.Prime ↑p) : R.τ (p ^ (2 * k)) ∈ X2k R k

theorem not_abs_le_of_mem_empty_inter (R : RamanujanTau) (k : ℕ) (X : ℝ) (z : ℤ) (hmem : z ∈ X2k R k) (hempty : X2k R k ∩ {z : ℤ | |↑z| ≤ X} = ∅) : ¬|↑z| ≤ X

theorem natAbs_cast_eq_abs_cast (n : ℤ) : ↑n.natAbs = |↑n|

theorem not_le_of_empty_inter (R : RamanujanTau) (k : ℕ) (X : ℝ) (hempty : X2k R k ∩ {z : ℤ | |↑z| ≤ X} = ∅) (p : ℕ+) (hp : Nat.Prime ↑p) (_hne : (R.τ (p ^ (2 * k))).natAbs ≠ 0) : ¬↑(R.τ (p ^ (2 * k))).natAbs ≤ X

theorem vanishing_large_k (R : RamanujanTau) (h54_part2 : ∃ (c₅ : ℝ), 0 < c₅ ∧ ∀ (N : ℝ), c₅ < N → ∀ (k : ℕ), ↑k ≥ Real.log N / (2 * Real.log 2) → X2k R k ∩ {z : ℤ | |↑z| ≤ N} = ∅) : ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → ∀ (k : ℕ), ⌊Real.log X / (2 * Real.log 2)⌋₊ < k → ∀ (p : ℕ+), Nat.Prime ↑p → (R.τ (p ^ (2 * k))).natAbs ≠ 0 → ¬↑(R.τ (p ^ (2 * k))).natAbs ≤ X

theorem six_mul_log_two_le_log (X : ℝ) (hX : 64 < X) : 6 * Real.log 2 ≤ Real.log X

theorem log_div_two_log_two_gt_three (X : ℝ) (hX : 64 < X) : 3 ≤ Real.log X / (2 * Real.log 2)

theorem rpow_half_nonneg {X : ℝ} (hX : 0 < X) : 0 ≤ X ^ (1 / 2)

theorem triple_inter_empty_of_X2k_inter_empty (R : RamanujanTau) (k : ℕ) (X : ℝ) (h : X2k R k ∩ {z : ℤ | |↑z| ≤ X} = ∅) : oddPrimesSigned ∩ X2k R k ∩ {z : ℤ | |↑z| ≤ X} = ∅

theorem per_k_ncard_le_rpow_half (R : RamanujanTau) (h54 : Proposition54 R) : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → ∀ k ∈ Finset.Icc 3 ⌊Real.log X / (2 * Real.log 2)⌋₊, ↑(oddPrimesSigned ∩ X2k R k ∩ {z : ℤ | |↑z| ≤ X}).ncard ≤ C * X ^ (1 / 2)

theorem sum_const_le_floor_mul (a : ℝ) (ha : 0 ≤ a) (c : ℝ) (hc : 0 ≤ c) : ∑ _k ∈ Finset.Icc 3 ⌊a⌋₊, c ≤ a * c

theorem sum_per_k_bound (R : RamanujanTau) (h54 : Proposition54 R) : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → ∑ k ∈ Finset.Icc 3 ⌊Real.log X / (2 * Real.log 2)⌋₊, ↑(oddPrimesSigned ∩ X2k R k ∩ {z : ℤ | |↑z| ≤ X}).ncard ≤ C * (Real.log X / (2 * Real.log 2) * X ^ (1 / 2))

theorem floor_log_ge_three (X : ℝ) (hX : 64 < X) : 3 ≤ ⌊Real.log X / (2 * Real.log 2)⌋₊

theorem one_le_sqrt_mul_log (X : ℝ) (hX : Real.exp 1 < X) : 1 ≤ X ^ (1 / 2) * Real.log X

theorem log_div_mul_eq (X : ℝ) (hX : 0 < X) : Real.log X / (2 * Real.log 2) * X ^ (1 / 2) = 1 / (2 * Real.log 2) * (X ^ (1 / 2) * Real.log X)

theorem final_arithmetic_bound (A : ℝ) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → 1 + A * (Real.log X / (2 * Real.log 2) * X ^ (1 / 2)) ≤ C * (X ^ (1 / 2) * Real.log X)

theorem k_ge3_contribution (R : RamanujanTau) (h54 : Proposition54 R) : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → ↑{ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ∃ (k : ℕ), 3 ≤ k ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ}.ncard ≤ C * (X ^ (1 / 2) * Real.log X)

theorem tau_one_zero_or_one (R : RamanujanTau) : R.τ 1 = 0 ∨ R.τ 1 = 1

theorem tau_one_ne_zero (R : RamanujanTau) : R.τ 1 ≠ 0

theorem tau_one_eq_one (R : RamanujanTau) : R.τ 1 = 1

theorem ordCompl_ge_two_of_not_isPrimePow (n : ℕ) (hn : 2 ≤ n) (hnp : ¬IsPrimePow n) (p : ℕ) (hp : Nat.Prime p) (_hpn : p ∣ n) : 2 ≤ n / p ^ n.factorization p

theorem ordProj_ge_two (n p : ℕ) (hp : Nat.Prime p) (hn : n ≠ 0) (hpn : p ∣ n) : 2 ≤ p ^ n.factorization p

theorem ordProj_coprime_ordCompl (n p : ℕ) (hp : Nat.Prime p) (hn : n ≠ 0) (hpn : p ∣ n) : (p ^ n.factorization p).Coprime (n / p ^ n.factorization p)

theorem lift_to_pnat_factorization (n : ℕ+) (hn : 2 ≤ ↑n) (hnp : ¬IsPrimePow ↑n) (p : ℕ) (hp : Nat.Prime p) (hpn : p ∣ ↑n) : ∃ (u : ℕ+) (v : ℕ+), ↑u * ↑v = ↑n ∧ (↑u).Coprime ↑v ∧ 2 ≤ ↑u ∧ 2 ≤ ↑v

theorem exists_coprime_factorization_of_not_isPrimePow (n : ℕ+) (hn : 2 ≤ ↑n) (hnp : ¬IsPrimePow ↑n) : ∃ (u : ℕ+) (v : ℕ+), ↑u * ↑v = ↑n ∧ (↑u).Coprime ↑v ∧ 2 ≤ ↑u ∧ 2 ≤ ↑v

theorem natAbs_tau_eq_one_of_coprime_factor (R : RamanujanTau) (u v : ℕ+) (hcop : (↑u).Coprime ↑v) (ℓ : ℕ) (hℓ : Nat.Prime ℓ) (hτ : (R.τ (u * v)).natAbs = ℓ) : (R.τ u).natAbs = 1 ∨ (R.τ v).natAbs = 1

theorem tau_prime_imp_prime_power (R : RamanujanTau) (n : ℕ+) (hn : 2 ≤ ↑n) (ℓ : ℕ) (hℓ : Nat.Prime ℓ) (hτ : (R.τ n).natAbs = ℓ) : IsPrimePow ↑n

theorem tau_not_two_dvd_of_odd_prime (R : RamanujanTau) (n : ℕ+) (ℓ : ℕ) (hℓ : Nat.Prime ℓ) (hℓ_odd : ℓ ≠ 2) (hτ : (R.τ n).natAbs = ℓ) : ¬2 ∣ R.τ n

theorem tau_odd_prime_imp_odd_square (R : RamanujanTau) (n : ℕ+) (ℓ : ℕ) (hℓ : Nat.Prime ℓ) (hℓ_odd : ℓ ≠ 2) (hτ : (R.τ n).natAbs = ℓ) : Odd ↑n ∧ IsSquare ↑n

theorem prime_pow_sq_even_exp_via_factorization (p a m : ℕ) (hp : Nat.Prime p) (_ha : 0 < a) (hm : p ^ a = m ^ 2) : a = 2 * m.factorization p

theorem prime_pow_sq_even_exp (p a : ℕ) (hp : Nat.Prime p) (ha : 0 < a) (hsq : IsSquare (p ^ a)) : ∃ (k : ℕ), a = 2 * k

theorem prime_power_odd_square_form (n : ℕ+) (hn : 2 ≤ ↑n) (hpp : IsPrimePow ↑n) (hodd : Odd ↑n) (hsq : IsSquare ↑n) : ∃ (p : ℕ+), Nat.Prime ↑p ∧ ∃ (k : ℕ), 1 ≤ k ∧ ↑n = ↑p ^ (2 * k)

theorem witness_ge_two (R : RamanujanTau) (n : ℕ+) (ℓ : ℕ) (hℓ : Nat.Prime ℓ) (hτ : (R.τ n).natAbs = ℓ) : 2 ≤ ↑n

theorem tau_eq_of_pnat_eq_pow (R : RamanujanTau) (n p : ℕ+) (k : ℕ) (heq : ↑n = ↑p ^ (2 * k)) : R.τ n = R.τ (p ^ (2 * k))

theorem S_set_subset_union (R : RamanujanTau) (X : ℝ) (_hX : 1 < X) : tauPrimeSet R X ⊆ {2} ∪ {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ} ∪ {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 4)).natAbs = ℓ} ∪ {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ∃ (k : ℕ), 3 ≤ k ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ}

theorem nat_bounded_by_real_finite (X : ℝ) : {n : ℕ | ↑n ≤ X}.Finite

theorem A_sets_finite (R : RamanujanTau) (X : ℝ) : ({ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ} ∪ {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 4)).natAbs = ℓ} ∪ {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ∃ (k : ℕ), 3 ≤ k ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ}).Finite

theorem full_union_finite (R : RamanujanTau) (X : ℝ) : ({2} ∪ {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ} ∪ {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 4)).natAbs = ℓ} ∪ {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ∃ (k : ℕ), 3 ≤ k ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ}).Finite

theorem ncard_four_union_le_nat (A B C D : Set ℕ) (a : ℕ) (hA : A = {a}) : (A ∪ B ∪ C ∪ D).ncard ≤ 1 + B.ncard + C.ncard + D.ncard

theorem ncard_four_union_le (R : RamanujanTau) (X : ℝ) : ↑({2} ∪ {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ} ∪ {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 4)).natAbs = ℓ} ∪ {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ∃ (k : ℕ), 3 ≤ k ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ}).ncard ≤ 1 + ↑{ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ}.ncard + ↑{ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 4)).natAbs = ℓ}.ncard + ↑{ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ∃ (k : ℕ), 3 ≤ k ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ}.ncard

theorem S_decomposition (R : RamanujanTau) (X : ℝ) (hX : 1 < X) : ↑(S R X) ≤ 1 + ↑{ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ}.ncard + ↑{ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 4)).natAbs = ℓ}.ncard + ↑{ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ∃ (k : ℕ), 3 ≤ k ∧ (R.τ (p ^ (2 * k))).natAbs = ℓ}.ncard

theorem L_subset_union (R : RamanujanTau) (X : ℝ) : {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ} ⊆ {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ ∧ ↑↑p > X ^ (2 / 11)} ∪ {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ ∧ ↑↑p ≤ X ^ (2 / 11)}

theorem bounded_nat_set_finite (X : ℝ) : {ℓ : ℕ | ↑ℓ ≤ X}.Finite

theorem L_union_finite (R : RamanujanTau) (X : ℝ) : ({ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ ∧ ↑↑p > X ^ (2 / 11)} ∪ {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ ∧ ↑↑p ≤ X ^ (2 / 11)}).Finite

theorem ell_split_large_small (R : RamanujanTau) (X : ℝ) : ↑{ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ}.ncard ≤ ↑{ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ ∧ ↑↑p > X ^ (2 / 11)}.ncard + ↑{ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ ∧ ↑↑p ≤ X ^ (2 / 11)}.ncard

theorem bounded_nat_set_finite_real (B : ℝ) : {n : ℕ | ↑n ≤ B}.Finite

theorem pnat_bounded_finite (B : ℝ) : {p : ℕ+ | ↑↑p ≤ B}.Finite

theorem bounded_pnat_int_subset (S : Set (ℕ+ × ℤ)) (N M : ℕ) (hS : ∀ p ∈ S, ↑p.1 ≤ N ∧ |p.2| ≤ ↑M) : S ⊆ {q : ℕ+ | ↑↑q ≤ ↑N} ×ˢ Set.Icc (-↑M) ↑M

theorem bounded_pnat_int_set_finite (S : Set (ℕ+ × ℤ)) (N M : ℕ) (hS : ∀ p ∈ S, ↑p.1 ≤ N ∧ |p.2| ≤ ↑M) : S.Finite

theorem real_bound_to_nat_bound (p : ℕ+ × ℤ) (B : ℝ) (hB : ↑↑p.1 ≤ B) : ↑p.1 ≤ ⌈B⌉₊

theorem abc_specialize_half (habc : ABC) : ∃ (K : ℝ), 0 < K ∧ ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → a.Coprime b → a + b = c → ↑c ≤ K * ↑(a * b * c).radical ^ (3 / 2)

theorem E2_ysq_le_x11_add_X_int_step (X : ℝ) (p : ℕ+ × ℤ) (h3 : |↑↑↑p.1 ^ 11 - ↑p.2 ^ 2| ≤ X) : ↑p.2 ^ 2 - ↑↑p.1 ^ 11 ≤ X

theorem E2_ysq_le_x11_add_X_helper (X : ℝ) (p : ℕ+ × ℤ) (h3 : |↑↑↑p.1 ^ 11 - ↑p.2 ^ 2| ≤ X) : ↑p.2 ^ 2 ≤ ↑↑p.1 ^ 11 + X

theorem E2_ysq_le_x11_add_X (X : ℝ) (p : ℕ+ × ℤ) (hp : p ∈ E2Set X) : ↑p.2 ^ 2 ≤ ↑↑p.1 ^ 11 + X

theorem int_diff_toNat_le_floor (z n : ℤ) (X : ℝ) (_hX : 0 ≤ X) (hnn : 0 ≤ z - n) (hle : ↑z - ↑n ≤ X) : (z - n).toNat ≤ ⌊X⌋₊

theorem intLe_add_floor_of_toNat_le (z n : ℤ) (X : ℝ) (hnn : 0 ≤ z - n) (h : (z - n).toNat ≤ ⌊X⌋₊) : z ≤ n + ↑⌊X⌋₊

theorem intLe_int_add_floor_of_cast_le (z n : ℤ) (X : ℝ) (hX : 0 ≤ X) (h : ↑z ≤ ↑n + X) : z ≤ n + ↑⌊X⌋₊

theorem E2_X_nonneg (X : ℝ) (p : ℕ+ × ℤ) (hp : p ∈ E2Set X) : 0 ≤ X

theorem E2_ysq_le_x11_add_floor (X : ℝ) (p : ℕ+ × ℤ) (hp : p ∈ E2Set X) : p.2 ^ 2 ≤ ↑↑p.1 ^ 11 + ↑⌊X⌋₊

theorem E2_y_sq_le (X : ℝ) (N : ℕ) (p : ℕ+ × ℤ) (hp : p ∈ E2Set X) (hxN : ↑p.1 ≤ N) : p.2 ^ 2 ≤ ↑(N ^ 11 + ⌊X⌋₊)

theorem int_abs_le_of_sq_le (y : ℤ) (M : ℕ) (h : y ^ 2 ≤ ↑M) : |y| ≤ ↑M

theorem E2_y_bound (X : ℝ) (N : ℕ) (p : ℕ+ × ℤ) (hp : p ∈ E2Set X) (hxN : ↑p.1 ≤ N) : |p.2| ≤ ↑(N ^ 11 + ⌊X⌋₊ + 1)

theorem rpow_pow_eleven_eq_sq (X : ℝ) (hX : 0 ≤ X) : (X ^ (2 / 11)) ^ 11 = X ^ 2

theorem E2_x11_gt_Xsq (X : ℝ) (hX : 2 < X) (x : ℕ+) (hx : ↑↑x > X ^ (2 / 11)) : ↑↑x ^ 11 > X ^ 2

theorem E2_y_ne_zero (X : ℝ) (hX : 2 < X) (p : ℕ+ × ℤ) (hp : p ∈ E2Set X) : p.2 ≠ 0

theorem E2_ysq_lt_2x11 (X : ℝ) (hX : 2 < X) (p : ℕ+ × ℤ) (hp : p ∈ E2Set X) : ↑p.2 ^ 2 < 2 * ↑↑p.1 ^ 11

theorem prime_factor_dvd_of_dvd_pow (m n k : ℕ) (_hk : 0 < k) (h : m ∣ n ^ k) (p : ℕ) (hp : p ∈ m.primeFactors) : p ∣ n

theorem radical_dvd_of_dvd_pow (m n k : ℕ) (hk : 0 < k) (h : m ∣ n ^ k) : m.radical ∣ n

theorem gcd_quotients_coprime (M N : ℕ) (hM : 0 < M) (_hN : 0 < N) : have g := M.gcd N; (M / g).Coprime (N / g)

theorem coprime_of_coprime_sub (a c : ℕ) (hac : a.Coprime c) (hle : a ≤ c) : a.Coprime (c - a)

theorem mul_div_cancel_of_dvd (g M : ℕ) (h : g ∣ M) : g * (M / g) = M

theorem mul_sub_div_eq (g M N : ℕ) (hgM : g ∣ M) (hgN : g ∣ N) (_hle : M ≤ N) : g * (N / g - M / g) = N - M

theorem sub_eq_gcd_mul_sub_div (M N : ℕ) (hM : 0 < M) (hle : M ≤ N) : N - M = M.gcd N * (N / M.gcd N - M / M.gcd N)

theorem sub_div_gcd (M N : ℕ) (hM : 0 < M) (hle : M ≤ N) : (N - M) / M.gcd N = N / M.gcd N - M / M.gcd N

theorem gcd_coprime_setup (M N : ℕ) (hM : 0 < M) (hN : 0 < N) (hle : M ≤ N) (hd : 0 < N - M) : have g := M.gcd N; have a := M / g; have c := N / g; have b := c - a; 0 < g ∧ 0 < a ∧ 0 < c ∧ 0 < b ∧ a.Coprime b ∧ a + b = c ∧ N = g * c ∧ M = g * a ∧ g ∣ N - M ∧ (N - M) / g = b

theorem primeFactors_mem_one_le (n p : ℕ) (hp : p ∈ n.primeFactors) : 1 ≤ p

theorem one_le_prod_primeFactors (n : ℕ) : 1 ≤ ∏ p ∈ n.primeFactors, p

theorem radical_mul_le_aux (m n : ℕ) (_hm : 0 < m) (_hn : 0 < n) : ∏ p ∈ (m * n).primeFactors, p ≤ (∏ p ∈ m.primeFactors, p) * ∏ p ∈ n.primeFactors, p

theorem radical_mul_le_pos (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : (m * n).radical ≤ m.radical * n.radical

theorem radical_mul_le (a b : ℕ) : (a * b).radical ≤ a.radical * b.radical

theorem rpow_three_halves_mono (a b : ℝ) (ha : 0 ≤ a) (hab : a ≤ b) : a ^ (3 / 2) ≤ b ^ (3 / 2)

theorem mul_K_t_mono_left (K : ℝ) (hK : 0 < K) (g d : ℕ) (h_g_le_d : g ≤ d) (t : ℝ) (ht : 0 ≤ t) : ↑g * (K * t) ≤ ↑d * (K * t)

theorem radical_le_self (n : ℕ) (hn : 0 < n) : n.radical ≤ n

theorem radical_abc_bound (x : ℕ) (hx : 0 < x) (y_abs : ℕ) (hy : 0 < y_abs) (d : ℕ) (hd : 0 < d) (hsum : y_abs ^ 2 + d = x ^ 11) : have g := (y_abs ^ 2).gcd (x ^ 11); have a := y_abs ^ 2 / g; have c := x ^ 11 / g; have b := c - a; ↑(a * b * c).radical ≤ ↑y_abs * ↑d * ↑x

theorem assemble_abc_bound_chain (K : ℝ) (hK : 0 < K) (x : ℕ) (_hx : 0 < x) (y_abs : ℕ) (_hy : 0 < y_abs) (d : ℕ) (_hd : 0 < d) (g : ℕ) (_hg : 0 < g) (c : ℕ) (_hc : 0 < c) (a : ℕ) (_ha : 0 < a) (b : ℕ) (_hb : 0 < b) (h_x11_eq : ↑x ^ 11 = ↑g * ↑c) (h_abc : ↑c ≤ K * ↑(a * b * c).radical ^ (3 / 2)) (h_rad_mono : ↑(a * b * c).radical ^ (3 / 2) ≤ (↑y_abs * ↑d * ↑x) ^ (3 / 2)) (h_gd_mono : ↑g * (K * (↑d * ↑x * ↑y_abs) ^ (3 / 2)) ≤ ↑d * (K * (↑d * ↑x * ↑y_abs) ^ (3 / 2))) : ↑x ^ 11 ≤ ↑d * K * (↑d * ↑x * ↑y_abs) ^ (3 / 2)

theorem assemble_abc_bound (K : ℝ) (hK : 0 < K) (x : ℕ) (hx : 0 < x) (y_abs : ℕ) (hy : 0 < y_abs) (d : ℕ) (hd : 0 < d) (_hsum : y_abs ^ 2 + d = x ^ 11) (g : ℕ) (hg : 0 < g) (c : ℕ) (hc : 0 < c) (a : ℕ) (ha : 0 < a) (b : ℕ) (hb : 0 < b) (hcop : a.Coprime b) (hab : a + b = c) (hNgc : x ^ 11 = g * c) (_hMga : y_abs ^ 2 = g * a) (hdgb : d = g * b) (hK_abc : ∀ (a' b' c' : ℕ), 0 < a' → 0 < b' → 0 < c' → a'.Coprime b' → a' + b' = c' → ↑c' ≤ K * ↑(a' * b' * c').radical ^ (3 / 2)) (hrad : ↑(a * b * c).radical ≤ ↑y_abs * ↑d * ↑x) : ↑x ^ 11 ≤ ↑d * K * (↑d * ↑x * ↑y_abs) ^ (3 / 2)

theorem abc_gcd_bound_nat (K : ℝ) (hK : 0 < K) (hK_abc : ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → a.Coprime b → a + b = c → ↑c ≤ K * ↑(a * b * c).radical ^ (3 / 2)) (x : ℕ) (hx : 0 < x) (y_abs : ℕ) (hy : 0 < y_abs) (d : ℕ) (hd : 0 < d) (hsum : y_abs ^ 2 + d = x ^ 11) : ↑x ^ 11 ≤ ↑d * K * (↑d * ↑x * ↑y_abs) ^ (3 / 2)

theorem int_eq_from_diff (x : ℕ) (y : ℤ) (d : ℕ) (hd_eq : ↑d = ↑x ^ 11 - y ^ 2) : y ^ 2 + ↑d = ↑x ^ 11

theorem nat_eq_from_int_eq (x : ℕ) (y : ℤ) (d : ℕ) (hint : y ^ 2 + ↑d = ↑x ^ 11) : y.natAbs ^ 2 + d = x ^ 11

theorem cast_to_nat_setup (x : ℕ) (_hx : 0 < x) (y : ℤ) (hy : y ≠ 0) (d : ℕ) (_hd : 0 < d) (hd_eq : ↑d = ↑x ^ 11 - y ^ 2) (_hge : y ^ 2 ≤ ↑x ^ 11) : y.natAbs ^ 2 + d = x ^ 11 ∧ 0 < y.natAbs

theorem E2_abc_applied_case1 (K : ℝ) (hK : 0 < K) (hK_abc : ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → a.Coprime b → a + b = c → ↑c ≤ K * ↑(a * b * c).radical ^ (3 / 2)) (x : ℕ) (hx : 0 < x) (y : ℤ) (hy : y ≠ 0) (d : ℕ) (hd : 0 < d) (hd_eq : ↑d = ↑x ^ 11 - y ^ 2) (hge : y ^ 2 ≤ ↑x ^ 11) : ↑x ^ 11 ≤ ↑d * K * (↑d * ↑x * |↑y|) ^ (3 / 2)

theorem x11_le_natAbs_sq (x : ℕ) (y : ℤ) (hlt : ↑x ^ 11 < y ^ 2) : x ^ 11 ≤ y.natAbs ^ 2

theorem d_eq_natAbs_diff (x : ℕ) (y : ℤ) (d : ℕ) (hd_eq : ↑d = y ^ 2 - ↑x ^ 11) (hlt : ↑x ^ 11 < y ^ 2) : d = y.natAbs ^ 2 - x ^ 11

theorem a_dvd_x11 (x : ℕ) (y : ℤ) : have g := (y.natAbs ^ 2).gcd (x ^ 11); have a := x ^ 11 / g; a ∣ x ^ 11

theorem c_dvd_yabs2 (x : ℕ) (y : ℤ) : have g := (y.natAbs ^ 2).gcd (x ^ 11); have c := y.natAbs ^ 2 / g; c ∣ y.natAbs ^ 2

theorem radical_triple_le (a b c : ℕ) : (a * b * c).radical ≤ a.radical * b.radical * c.radical

theorem mul_radical_bounds (a b c x d yabs : ℕ) (ha : a.radical ≤ x) (hb : b.radical ≤ d) (hc : c.radical ≤ yabs) : a.radical * b.radical * c.radical ≤ x * d * yabs

theorem radical_abc_le_dxy (a b c x d yabs : ℕ) (ha : a.radical ≤ x) (hb : b.radical ≤ d) (hc : c.radical ≤ yabs) : ↑(a * b * c).radical ≤ ↑d * ↑x * ↑yabs

theorem radical_dvd_implies_le (m n : ℕ) (hn : 0 < n) (h : m.radical ∣ n) : m.radical ≤ n

theorem radical_bound_case2 (x : ℕ) (hx : 0 < x) (y : ℤ) (hy : y ≠ 0) (d : ℕ) (hd : 0 < d) (hd_nat : d = y.natAbs ^ 2 - x ^ 11) (_hlt : ↑x ^ 11 < y ^ 2) : have g := (y.natAbs ^ 2).gcd (x ^ 11); have a := x ^ 11 / g; have b := d / g; have c := y.natAbs ^ 2 / g; ↑(a * b * c).radical ≤ ↑d * ↑x * ↑y.natAbs

theorem yabs_sq_le_g_mul_K_rad (K : ℝ) (_hK : 0 < K) (g c yabs : ℕ) (_hg : 0 < g) (_hc : 0 < c) (_hyabs : 0 < yabs) (h_gc : yabs ^ 2 = g * c) (rad : ℕ) (h_abc_bound : ↑c ≤ K * ↑rad ^ (3 / 2)) : ↑yabs ^ 2 ≤ ↑g * (K * ↑rad ^ (3 / 2))

theorem assemble_case2_bound (K : ℝ) (hK : 0 < K) (g c d x yabs : ℕ) (hg : 0 < g) (hc : 0 < c) (_hd : 0 < d) (_hx : 0 < x) (hyabs : 0 < yabs) (h_gc : yabs ^ 2 = g * c) (h_abc_bound : ↑c ≤ K * ↑(x ^ 11 / g * (d / g) * c).radical ^ (3 / 2)) (h_rad : ↑(x ^ 11 / g * (d / g) * c).radical ≤ ↑d * ↑x * ↑yabs) (h_g_le_d : g ≤ d) : ↑yabs ^ 2 ≤ ↑d * K * (↑d * ↑x * ↑yabs) ^ (3 / 2)

theorem E2_abc_applied_case2 (K : ℝ) (hK : 0 < K) (hK_abc : ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → a.Coprime b → a + b = c → ↑c ≤ K * ↑(a * b * c).radical ^ (3 / 2)) (x : ℕ) (hx : 0 < x) (y : ℤ) (hy : y ≠ 0) (d : ℕ) (hd : 0 < d) (hd_eq : ↑d = y ^ 2 - ↑x ^ 11) (hlt : ↑x ^ 11 < y ^ 2) : ↑y ^ 2 ≤ ↑d * K * (↑d * ↑x * |↑y|) ^ (3 / 2)

theorem E2_abc_case_A_d_eq (x : ℕ) (y : ℤ) (d : ℕ) (hd_eq : ↑d = |↑x ^ 11 - y ^ 2|) (hge : y ^ 2 ≤ ↑x ^ 11) : ↑d = ↑x ^ 11 - y ^ 2

theorem E2_abc_case_A_cast_le (x : ℕ) (y : ℤ) (hge : y ^ 2 ≤ ↑x ^ 11) : ↑y ^ 2 ≤ ↑x ^ 11

theorem E2_abc_case_A (K : ℝ) (_hK : 0 < K) (x : ℕ) (_hx : 0 < x) (y : ℤ) (_hy : y ≠ 0) (d : ℕ) (_hd : 0 < d) (hd_eq : ↑d = |↑x ^ 11 - y ^ 2|) (h1 : y ^ 2 ≤ ↑x ^ 11 → ↑d = ↑x ^ 11 - y ^ 2 → ↑x ^ 11 ≤ ↑d * K * (↑d * ↑x * |↑y|) ^ (3 / 2)) (hge : y ^ 2 ≤ ↑x ^ 11) : max (↑x ^ 11) (↑y ^ 2) ≤ ↑d * K * (↑d * ↑x * |↑y|) ^ (3 / 2)

theorem d_eq_ysq_sub_x11 (x : ℕ) (y : ℤ) (d : ℕ) (hd_eq : ↑d = |↑x ^ 11 - y ^ 2|) (hlt : ↑x ^ 11 < y ^ 2) : ↑d = y ^ 2 - ↑x ^ 11

theorem x11_le_y2_real (x : ℕ) (y : ℤ) (hlt : ↑x ^ 11 < y ^ 2) : ↑↑x ^ 11 ≤ ↑y ^ 2

theorem E2_abc_case_B (K : ℝ) (_hK : 0 < K) (x : ℕ) (_hx : 0 < x) (y : ℤ) (_hy : y ≠ 0) (d : ℕ) (_hd : 0 < d) (hd_eq : ↑d = |↑x ^ 11 - y ^ 2|) (h2 : ↑x ^ 11 < y ^ 2 → ↑d = y ^ 2 - ↑x ^ 11 → ↑y ^ 2 ≤ ↑d * K * (↑d * ↑x * |↑y|) ^ (3 / 2)) (hlt : ↑x ^ 11 < y ^ 2) : max (↑x ^ 11) (↑y ^ 2) ≤ ↑d * K * (↑d * ↑x * |↑y|) ^ (3 / 2)

theorem E2_abc_applied_from_cases (K : ℝ) (hK : 0 < K) (_hK_abc : ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → a.Coprime b → a + b = c → ↑c ≤ K * ↑(a * b * c).radical ^ (3 / 2)) (x : ℕ) (hx : 0 < x) (y : ℤ) (hy : y ≠ 0) (d : ℕ) (hd : 0 < d) (hd_eq : ↑d = |↑x ^ 11 - y ^ 2|) (h1 : y ^ 2 ≤ ↑x ^ 11 → ↑d = ↑x ^ 11 - y ^ 2 → ↑x ^ 11 ≤ ↑d * K * (↑d * ↑x * |↑y|) ^ (3 / 2)) (h2 : ↑x ^ 11 < y ^ 2 → ↑d = y ^ 2 - ↑x ^ 11 → ↑y ^ 2 ≤ ↑d * K * (↑d * ↑x * |↑y|) ^ (3 / 2)) : max (↑x ^ 11) (↑y ^ 2) ≤ ↑d * K * (↑d * ↑x * |↑y|) ^ (3 / 2)

theorem E2_abc_applied (K : ℝ) (hK : 0 < K) (hK_abc : ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → a.Coprime b → a + b = c → ↑c ≤ K * ↑(a * b * c).radical ^ (3 / 2)) (x : ℕ) (hx : 0 < x) (y : ℤ) (hy : y ≠ 0) (d : ℕ) (hd : 0 < d) (hd_eq : ↑d = |↑x ^ 11 - y ^ 2|) : max (↑x ^ 11) (↑y ^ 2) ≤ ↑d * K * (↑d * ↑x * |↑y|) ^ (3 / 2)

theorem rpow_mul_distrib (d x y_abs : ℝ) (hd : 0 < d) (hx : 1 ≤ x) (hy : 0 < y_abs) : (d * x * y_abs) ^ (3 / 2) = d ^ (3 / 2) * x ^ (3 / 2) * y_abs ^ (3 / 2)

theorem d_mul_d_rpow (d : ℝ) (hd : 0 < d) : d * d ^ (3 / 2) = d ^ (5 / 2)

theorem expand_abc_rhs_eq (K : ℝ) (_hK : 0 < K) (x : ℝ) (hx : 1 ≤ x) (y_abs : ℝ) (hy : 0 < y_abs) (d : ℝ) (hd_pos : 0 < d) : d * K * (d * x * y_abs) ^ (3 / 2) = K * d ^ (5 / 2) * x ^ (3 / 2) * y_abs ^ (3 / 2)

theorem expand_abc_rhs (K : ℝ) (hK : 0 < K) (x : ℝ) (hx : 1 ≤ x) (y_abs : ℝ) (hy : 0 < y_abs) (d : ℝ) (hd_pos : 0 < d) (habc : x ^ 11 ≤ d * K * (d * x * y_abs) ^ (3 / 2)) : x ^ 11 ≤ K * d ^ (5 / 2) * x ^ (3 / 2) * y_abs ^ (3 / 2)

theorem rpow_three_fourths_strict_mono (x : ℝ) (_hx : 1 ≤ x) (y_abs : ℝ) (_hy : 0 < y_abs) (hysq : y_abs ^ 2 < 2 * x ^ 11) : (y_abs ^ 2) ^ (3 / 4) < (2 * x ^ 11) ^ (3 / 4)

theorem lhs_simplify (y_abs : ℝ) (hy : 0 < y_abs) : (y_abs ^ 2) ^ (3 / 4) = y_abs ^ (3 / 2)

theorem rhs_simplify (x : ℝ) (hx : 1 ≤ x) : (2 * x ^ 11) ^ (3 / 4) = 2 ^ (3 / 4) * x ^ (33 / 4)

theorem bound_y_three_halves (x : ℝ) (hx : 1 ≤ x) (y_abs : ℝ) (hy : 0 < y_abs) (hysq : y_abs ^ 2 < 2 * x ^ 11) : y_abs ^ (3 / 2) < 2 ^ (3 / 4) * x ^ (33 / 4)

theorem coeff_pos (K : ℝ) (hK : 0 < K) (x : ℝ) (hx : 1 ≤ x) (d : ℝ) (hd_pos : 0 < d) : 0 < K * d ^ (5 / 2) * x ^ (3 / 2)

theorem rpow_combine_x (x : ℝ) (hx : 0 < x) : x ^ (3 / 2) * x ^ (33 / 4) = x ^ (39 / 4)

theorem rearrange_rhs (K : ℝ) (_hK : 0 < K) (x : ℝ) (hx : 1 ≤ x) (d : ℝ) (_hd_pos : 0 < d) : K * d ^ (5 / 2) * x ^ (3 / 2) * (2 ^ (3 / 4) * x ^ (33 / 4)) = 2 ^ (3 / 4) * K * d ^ (5 / 2) * x ^ (39 / 4)

theorem substitute_y_combine_x (K : ℝ) (hK : 0 < K) (x : ℝ) (hx : 1 ≤ x) (y_abs : ℝ) (_hy : 0 < y_abs) (d : ℝ) (hd_pos : 0 < d) (h_expanded : x ^ 11 ≤ K * d ^ (5 / 2) * x ^ (3 / 2) * y_abs ^ (3 / 2)) (h_ybound : y_abs ^ (3 / 2) < 2 ^ (3 / 4) * x ^ (33 / 4)) : x ^ 11 ≤ 2 ^ (3 / 4) * K * d ^ (5 / 2) * x ^ (39 / 4)

theorem rpow_div_le_of_rpow_le (x : ℝ) (hx_pos : 0 < x) (a b B : ℝ) (h : x ^ a ≤ B * x ^ b) : x ^ a / x ^ b ≤ B

theorem rpow_sub_eq_div (x : ℝ) (hx_pos : 0 < x) (a b : ℝ) : x ^ (a - b) = x ^ a / x ^ b

theorem rpow_cancel_general (x : ℝ) (hx : 1 ≤ x) (a b B : ℝ) (_hB : 0 < B) (h : x ^ a ≤ B * x ^ b) : x ^ (a - b) ≤ B

theorem divide_x_power (C : ℝ) (hC : 0 < C) (x : ℝ) (hx : 1 ≤ x) (h : x ^ 11 ≤ C * x ^ (39 / 4)) : x ^ (5 / 4) ≤ C

theorem cancel_x_powers (K : ℝ) (hK : 0 < K) (x : ℝ) (hx : 1 ≤ x) (y_abs : ℝ) (hy : 0 < y_abs) (d : ℝ) (hd_pos : 0 < d) (h_expanded : x ^ 11 ≤ K * d ^ (5 / 2) * x ^ (3 / 2) * y_abs ^ (3 / 2)) (h_ybound : y_abs ^ (3 / 2) < 2 ^ (3 / 4) * x ^ (33 / 4)) : x ^ (5 / 4) ≤ 2 ^ (3 / 4) * K * d ^ (5 / 2)

theorem x_fifth_fourth_le (K : ℝ) (hK : 0 < K) (x : ℝ) (hx : 1 ≤ x) (y_abs : ℝ) (hy : 0 < y_abs) (d : ℝ) (hd_pos : 0 < d) (hysq : y_abs ^ 2 < 2 * x ^ 11) (habc : x ^ 11 ≤ d * K * (d * x * y_abs) ^ (3 / 2)) : x ^ (5 / 4) ≤ 2 ^ (3 / 4) * K * d ^ (5 / 2)

theorem rpow_five_fourths_pow_four (x : ℝ) (hx : 0 ≤ x) : (x ^ (5 / 4)) ^ 4 = x ^ 5

theorem two_rpow_three_fourths_pow_four : (2 ^ (3 / 4)) ^ 4 = 8

theorem rpow_five_halves_pow_four (d : ℝ) (hd : 0 ≤ d) : (d ^ (5 / 2)) ^ 4 = d ^ 10

theorem rhs_fourth_power (K : ℝ) (_hK : 0 < K) (d : ℝ) (hd : 0 < d) : (2 ^ (3 / 4) * K * d ^ (5 / 2)) ^ 4 = 8 * K ^ 4 * d ^ 10

theorem pow_four_mono (a b : ℝ) (ha : 0 ≤ a) (hab : a ≤ b) : a ^ 4 ≤ b ^ 4

theorem rpow_five_fourths_nonneg (x : ℝ) (hx : 0 ≤ x) : 0 ≤ x ^ (5 / 4)

theorem raise_to_fourth (K : ℝ) (hK : 0 < K) (x : ℝ) (hx : 1 ≤ x) (d : ℝ) (hd_pos : 0 < d) (h : x ^ (5 / 4) ≤ 2 ^ (3 / 4) * K * d ^ (5 / 2)) : x ^ 5 ≤ 8 * K ^ 4 * d ^ 10

theorem d_pow_le_X_pow (K : ℝ) (hK : 0 < K) (X : ℝ) (_hX : 0 < X) (d : ℝ) (hd_pos : 0 < d) (hd_le : d ≤ X) : 8 * K ^ 4 * d ^ 10 ≤ 8 * K ^ 4 * X ^ 10

theorem E2_case1_bound (K : ℝ) (hK : 0 < K) (X : ℝ) (hX : 0 < X) (x : ℝ) (hx : 1 ≤ x) (y_abs : ℝ) (hy : 0 < y_abs) (d : ℝ) (hd_pos : 0 < d) (hd_le : d ≤ X) (hysq : y_abs ^ 2 < 2 * x ^ 11) (habc : x ^ 11 ≤ d * K * (d * x * y_abs) ^ (3 / 2)) : x ^ 5 ≤ 8 * K ^ 4 * X ^ 10

theorem expand_case2_rhs (K : ℝ) (hK : 0 < K) (x : ℝ) (hx : 1 ≤ x) (y_abs : ℝ) (hy : 0 < y_abs) (d : ℝ) (hd_pos : 0 < d) (habc : y_abs ^ 2 ≤ d * K * (d * x * y_abs) ^ (3 / 2)) : y_abs ^ 2 ≤ K * d ^ (5 / 2) * x ^ (3 / 2) * y_abs ^ (3 / 2)

theorem rpow_half_le_of_sq_le_mul_three_halves (y : ℝ) (hy : 0 < y) (A : ℝ) (h : y ^ 2 ≤ A * y ^ (3 / 2)) : y ^ (1 / 2) ≤ A

theorem div_y_three_halves (K : ℝ) (_hK : 0 < K) (x : ℝ) (_hx : 1 ≤ x) (y_abs : ℝ) (hy : 0 < y_abs) (d : ℝ) (_hd_pos : 0 < d) (h : y_abs ^ 2 ≤ K * d ^ (5 / 2) * x ^ (3 / 2) * y_abs ^ (3 / 2)) : y_abs ^ (1 / 2) ≤ K * d ^ (5 / 2) * x ^ (3 / 2)

theorem rpow_quarter_preserves_lt (x : ℝ) (hx : 1 ≤ x) (y_abs : ℝ) (_hy : 0 < y_abs) (hx11_lt_y2 : x ^ 11 < y_abs ^ 2) : (x ^ 11) ^ (1 / 4) < (y_abs ^ 2) ^ (1 / 4)

theorem rpow_nat_pow_quarter_lhs (x : ℝ) (hx : 0 ≤ x) : (x ^ 11) ^ (1 / 4) = x ^ (11 / 4)

theorem rpow_nat_pow_quarter_rhs (y : ℝ) (hy : 0 ≤ y) : (y ^ 2) ^ (1 / 4) = y ^ (1 / 2)

theorem x_pow_lt_y_half (x : ℝ) (hx : 1 ≤ x) (y_abs : ℝ) (hy : 0 < y_abs) (hx11_lt_y2 : x ^ 11 < y_abs ^ 2) : x ^ (11 / 4) < y_abs ^ (1 / 2)

theorem combine_and_cancel_x (K : ℝ) (hK : 0 < K) (x : ℝ) (hx : 1 ≤ x) (d : ℝ) (hd_pos : 0 < d) (h : x ^ (11 / 4) ≤ K * d ^ (5 / 2) * x ^ (3 / 2)) : x ^ (5 / 4) ≤ K * d ^ (5 / 2)

theorem scale_up_by_two_pow (K : ℝ) (hK : 0 < K) (x : ℝ) (_hx : 1 ≤ x) (d : ℝ) (hd_pos : 0 < d) (h : x ^ (5 / 4) ≤ K * d ^ (5 / 2)) : x ^ (5 / 4) ≤ 2 ^ (3 / 4) * K * d ^ (5 / 2)

theorem case2_x_fifth_fourth_le (K : ℝ) (hK : 0 < K) (x : ℝ) (hx : 1 ≤ x) (y_abs : ℝ) (hy : 0 < y_abs) (d : ℝ) (hd_pos : 0 < d) (hx11_lt_y2 : x ^ 11 < y_abs ^ 2) (habc : y_abs ^ 2 ≤ d * K * (d * x * y_abs) ^ (3 / 2)) : x ^ (5 / 4) ≤ 2 ^ (3 / 4) * K * d ^ (5 / 2)

theorem E2_case2_bound (K : ℝ) (hK : 0 < K) (X : ℝ) (hX : 0 < X) (x : ℝ) (hx : 1 ≤ x) (y_abs : ℝ) (hy : 0 < y_abs) (d : ℝ) (hd_pos : 0 < d) (hd_le : d ≤ X) (hx11_lt_y2 : x ^ 11 < y_abs ^ 2) (_hysq_le : y_abs ^ 2 ≤ x ^ 11 + d) (habc : y_abs ^ 2 ≤ d * K * (d * x * y_abs) ^ (3 / 2)) : x ^ 5 ≤ 8 * K ^ 4 * X ^ 10

theorem E2_x_fifth_le_of_max_bound (K : ℝ) (hK : 0 < K) (X : ℝ) (hX : 0 < X) (x : ℝ) (hx : 1 ≤ x) (y_abs : ℝ) (hy : 0 < y_abs) (d : ℝ) (hd_pos : 0 < d) (hd_le : d ≤ X) (hysq_lt : y_abs ^ 2 < 2 * x ^ 11) (hysq_le_d : y_abs ^ 2 ≤ x ^ 11 + d) (hmax : max (x ^ 11) (y_abs ^ 2) ≤ d * K * (d * x * y_abs) ^ (3 / 2)) : x ^ 5 ≤ 8 * K ^ 4 * X ^ 10

theorem E2_x_fifth_le (K : ℝ) (hK : 0 < K) (hK_abc : ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → a.Coprime b → a + b = c → ↑c ≤ K * ↑(a * b * c).radical ^ (3 / 2)) (X : ℝ) (hX : 2 < X) (p : ℕ+ × ℤ) (hp : p ∈ E2Set X) : ↑↑p.1 ^ 5 ≤ 8 * K ^ 4 * X ^ 10

theorem fifth_root_bound (x C : ℝ) (hx : 0 ≤ x) (hC : 0 ≤ C) (h : x ^ 5 ≤ C) : x ≤ C ^ (1 / 5)

theorem E2_x_bound_real (K : ℝ) (hK : 0 < K) (hK_abc : ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → a.Coprime b → a + b = c → ↑c ≤ K * ↑(a * b * c).radical ^ (3 / 2)) (X : ℝ) (hX : 2 < X) (p : ℕ+ × ℤ) (hp : p ∈ E2Set X) : ↑↑p.1 ≤ (8 * K ^ 4 * X ^ 10) ^ (1 / 5)

theorem E2_set_bounded_of_abc (habc : ABC) : ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → ∃ (N : ℕ) (M : ℕ), ∀ p ∈ E2Set X, ↑p.1 ≤ N ∧ |p.2| ≤ ↑M

theorem E2_set_finite_of_abc (habc : ABC) : ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → (E2Set X).Finite

theorem tau_sq_formula (R : RamanujanTau) (p : ℕ+) (hp : Nat.Prime ↑p) : R.τ (p ^ 2) = R.τ p ^ 2 - ↑↑p ^ 11

theorem p11_minus_tau_sq (R : RamanujanTau) (p : ℕ+) (hp : Nat.Prime ↑p) : ↑↑p ^ 11 - R.τ p ^ 2 = -R.τ (p ^ 2)

theorem E2_cond2 (R : RamanujanTau) (p : ℕ+) (hp : Nat.Prime ↑p) (ℓ : ℕ) (hℓ : Nat.Prime ℓ) (hτ : (R.τ (p ^ 2)).natAbs = ℓ) : 1 ≤ |↑↑p ^ 11 - R.τ p ^ 2|

theorem E2_cond3 (R : RamanujanTau) (X : ℝ) (p : ℕ+) (hp : Nat.Prime ↑p) (ℓ : ℕ) (hℓX : ↑ℓ ≤ X) (hτ : (R.τ (p ^ 2)).natAbs = ℓ) : |↑↑↑p ^ 11 - ↑(R.τ p) ^ 2| ≤ X

theorem witness_in_E2_set (R : RamanujanTau) (X : ℝ) (p : ℕ+) (hp : Nat.Prime ↑p) (hpX : ↑↑p > X ^ (2 / 11)) (ℓ : ℕ) (hℓ : Nat.Prime ℓ) (hℓX : ↑ℓ ≤ X) (hτ : (R.τ (p ^ 2)).natAbs = ℓ) : (p, R.τ p) ∈ E2Set X

noncomputable def witnessPE2 (R : RamanujanTau) (X : ℝ) (ℓ : ℕ) : ℕ+

A choice of prime p exhibiting ℓ as |τ (p ^ 2)| with p > X ^ (2/11), when one exists; otherwise 1.

Equations

• witnessPE2 R X ℓ = if h : ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ ∧ ↑↑p > X ^ (2 / 11) then h.choose else 1

theorem witnessP_E2_spec (R : RamanujanTau) (X : ℝ) (ℓ : ℕ) (h : ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ ∧ ↑↑p > X ^ (2 / 11)) : Nat.Prime ↑(witnessPE2 R X ℓ) ∧ (R.τ (witnessPE2 R X ℓ ^ 2)).natAbs = ℓ ∧ ↑↑(witnessPE2 R X ℓ) > X ^ (2 / 11)

noncomputable def witnessMapE2 (R : RamanujanTau) (X : ℝ) (ℓ : ℕ) : ℕ+ × ℤ

The map sending ℓ to (witnessPE2 R X ℓ, τ (witnessPE2 R X ℓ ^ 2)).

Equations

• witnessMapE2 R X ℓ = (witnessPE2 R X ℓ, R.τ (witnessPE2 R X ℓ))

theorem witnessMap_E2_mapsTo (R : RamanujanTau) (X : ℝ) (ℓ : ℕ) : ℓ ∈ {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ ∧ ↑↑p > X ^ (2 / 11)} → witnessMapE2 R X ℓ ∈ E2Set X

theorem witnessMap_E2_injOn (R : RamanujanTau) (X : ℝ) : Set.InjOn (witnessMapE2 R X) {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ ∧ ↑↑p > X ^ (2 / 11)}

theorem L_large_ncard_le_E2 (R : RamanujanTau) (X : ℝ) (hfin : (E2Set X).Finite) : {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ ∧ ↑↑p > X ^ (2 / 11)}.ncard ≤ E2 X

theorem large_ell_bound (R : RamanujanTau) (habc : ABC) : ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → ↑{ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ ∧ ↑↑p > X ^ (2 / 11)}.ncard ≤ ↑(E2 X)

theorem target_subset_image_k1 (R : RamanujanTau) (X : ℝ) : {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ ∧ ↑↑p ≤ X ^ (2 / 11)} ⊆ (fun (p : ℕ+) => (R.τ (p ^ 2)).natAbs) '' {p : ℕ+ | Nat.Prime ↑p ∧ ↑↑p ≤ X ^ (2 / 11)}

theorem natLe_floor_of_cast_le (B : ℝ) (x : ℕ) (hx : ↑x ≤ B) : x ≤ ⌊B⌋₊

theorem pnat_bounded_finite_k1 (B : ℝ) : {p : ℕ+ | ↑↑p ≤ B}.Finite

theorem pnat_bounded_finite_nat (M : ℕ) : {p : ℕ+ | ↑p ≤ M}.Finite

theorem witness_set_subset_bounded (X : ℝ) : {p : ℕ+ | Nat.Prime ↑p ∧ ↑↑p ≤ X ^ (2 / 11)} ⊆ {p : ℕ+ | ↑p ≤ ⌊X ^ (2 / 11)⌋₊}

theorem witness_set_finite_k1 (X : ℝ) : {p : ℕ+ | Nat.Prime ↑p ∧ ↑↑p ≤ X ^ (2 / 11)}.Finite

theorem ncard_Icc_one_M (M : ℕ) : (↑(Finset.Icc 1 M)).ncard = M

theorem pnat_val_mapsTo_Icc (M : ℕ) (a : ℕ+) : a ∈ {p : ℕ+ | ↑p ≤ M} → ↑a ∈ ↑(Finset.Icc 1 M)

theorem pnat_bounded_ncard_le (M : ℕ) : {p : ℕ+ | ↑p ≤ M}.ncard ≤ M

theorem witness_set_ncard_le_k1 (X : ℝ) (_hX : 1 ≤ X) : {p : ℕ+ | Nat.Prime ↑p ∧ ↑↑p ≤ X ^ (2 / 11)}.ncard ≤ ⌊X ^ (2 / 11)⌋₊

theorem floor_rpow_le_k1 (X : ℝ) (hX : 1 ≤ X) : ↑⌊X ^ (2 / 11)⌋₊ ≤ X ^ (2 / 11)

theorem small_ell_bound (R : RamanujanTau) (X : ℝ) : 1 ≤ X → ↑{ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ ∧ ↑↑p ≤ X ^ (2 / 11)}.ncard ≤ X ^ (2 / 11)

theorem rpow_le_rpow_of_le_exp {X a b : ℝ} (hX : 1 ≤ X) (hab : a ≤ b) : X ^ a ≤ X ^ b

theorem k1_contribution_abc (R : RamanujanTau) (habc : ABC) : ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → ↑{ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 2)).natAbs = ℓ}.ncard ≤ ↑(E2 X) + X ^ (13 / 22)

theorem target_subset_image (R : RamanujanTau) (X : ℝ) : {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ↑↑p ≤ X ^ (1 / 11) ∧ (R.τ (p ^ 4)).natAbs = ℓ} ⊆ (fun (p : ℕ+) => (R.τ (p ^ 4)).natAbs) '' {p : ℕ+ | Nat.Prime ↑p ∧ ↑↑p ≤ X ^ (1 / 11)}

theorem witness_set_finite (X : ℝ) : {p : ℕ+ | Nat.Prime ↑p ∧ ↑↑p ≤ X ^ (1 / 11)}.Finite

theorem witness_set_ncard_le (X : ℝ) (_hX : 1 < X) : {p : ℕ+ | Nat.Prime ↑p ∧ ↑↑p ≤ X ^ (1 / 11)}.ncard ≤ ⌊X ^ (1 / 11)⌋₊

theorem floor_rpow_le (X : ℝ) (hX : 0 < X) : ↑⌊X ^ (1 / 11)⌋₊ ≤ X ^ (1 / 11)

theorem small_primes_k2_bound (R : RamanujanTau) : ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → ↑{ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ↑↑p ≤ X ^ (1 / 11) ∧ (R.τ (p ^ 4)).natAbs = ℓ}.ncard ≤ X ^ (1 / 11)

theorem hecke_u_identity (R : RamanujanTau) (p : ℕ+) (hp : Nat.Prime ↑p) : have u := 2 * R.τ p ^ 2 - 3 * ↑↑p ^ 11; u ^ 2 - 5 * ↑↑p ^ 22 = 4 * R.τ (p ^ 4)

theorem E4_set_D_bounds (X : ℝ) (p : ℕ+ × ℤ) (hp : p ∈ E4Set X) : 1 ≤ |↑p.2 ^ 2 - 5 * ↑↑↑p.1 ^ 22| ∧ |↑p.2 ^ 2 - 5 * ↑↑↑p.1 ^ 22| ≤ 4 * X

theorem rpow_11_strict_mono {a b : ℝ} (ha : 0 ≤ a) (hab : a < b) : a ^ 11 < b ^ 11

theorem rpow_one_div_11_pow_11 (X : ℝ) (hX : 0 ≤ X) : (X ^ (1 / 11)) ^ 11 = X

theorem x11_gt_X_of_x_gt (X : ℝ) (hX : 1 < X) (x : ℕ+) (hx : ↑↑x > X ^ (1 / 11)) : ↑↑x ^ 11 > X

theorem E4_x11_pow_gt_X (X : ℝ) (hX : 4 < X) (x : ℕ+) (hx : ↑↑x > X ^ (1 / 11)) : ↑↑x ^ 11 > X

theorem sq_lt_sq_of_pos_lt (a b : ℝ) (ha : 0 < a) (hab : a < b) : a ^ 2 < b ^ 2

theorem x22_gt_X2_of_x11_gt (X : ℝ) (hX : 0 < X) (x : ℕ+) (h : ↑↑x ^ 11 > X) : ↑↑x ^ 22 > X ^ 2

theorem x22_gt_X_sq (X : ℝ) (hX : 4 < X) (x : ℕ+) (hx : ↑↑x > X ^ (1 / 11)) : ↑↑x ^ 22 > X ^ 2

theorem x22_gt_four_mul_X (X : ℝ) (hX : 4 < X) (x : ℕ+) (hx : ↑↑x > X ^ (1 / 11)) : ↑↑x ^ 22 > 4 * X

theorem five_x22_sub_4X_pos (X : ℝ) (hX : 4 < X) (x : ℕ+) (hx : ↑↑x > X ^ (1 / 11)) : 5 * ↑↑x ^ 22 - 4 * X > 0

theorem sqrt_sub_eq_div (a b : ℝ) (ha : 0 < a) (hb : 0 ≤ b) (_hab : b < a) : √a - √b = (a - b) / (√a + √b)

theorem five_x22_sub_4X_ge_four_x22 (X : ℝ) (hX : 4 < X) (x : ℕ+) (hx : ↑↑x > X ^ (1 / 11)) : 5 * ↑↑x ^ 22 - 4 * X > 4 * ↑↑x ^ 22

theorem sqrt_five_x22_sub_gt_two_x11 (X : ℝ) (hX : 4 < X) (x : ℕ+) (hx : ↑↑x > X ^ (1 / 11)) : √(5 * ↑↑x ^ 22 - 4 * X) > 2 * ↑↑x ^ 11

theorem sqrt_five_x22_add_gt_two_x11 (X : ℝ) (hX : 4 < X) (x : ℕ+) (hx : ↑↑x > X ^ (1 / 11)) : √(5 * ↑↑x ^ 22 + 4 * X) > 2 * ↑↑x ^ 11

theorem denom_gt_four_x11 (X : ℝ) (hX : 4 < X) (x : ℕ+) (hx : ↑↑x > X ^ (1 / 11)) : √(5 * ↑↑x ^ 22 + 4 * X) + √(5 * ↑↑x ^ 22 - 4 * X) > 4 * ↑↑x ^ 11

theorem E4_interval_length_lt_two (X : ℝ) (hX : 4 < X) (x : ℕ+) (hx : ↑↑x > X ^ (1 / 11)) : √(5 * ↑↑x ^ 22 + 4 * X) - √(5 * ↑↑x ^ 22 - 4 * X) < 2

theorem pos_int_subset_Icc (a b : ℝ) : {u : ℤ | 0 < u ∧ a ≤ ↑u ∧ ↑u ≤ b} ⊆ Set.Icc ⌈a⌉ ⌊b⌋

theorem pos_int_in_interval_finite (a b : ℝ) : {u : ℤ | 0 < u ∧ a ≤ ↑u ∧ ↑u ≤ b}.Finite

theorem no_three_pos_ints_in_short_interval (a b : ℝ) (hlen : b - a < 2) (u₁ u₂ u₃ : ℤ) (_h1pos : 0 < u₁) (_h2pos : 0 < u₂) (_h3pos : 0 < u₃) (h1a : a ≤ ↑u₁) (_h1b : ↑u₁ ≤ b) (_h2a : a ≤ ↑u₂) (_h2b : ↑u₂ ≤ b) (_h3a : a ≤ ↑u₃) (h3b : ↑u₃ ≤ b) (h12 : u₁ < u₂) (h23 : u₂ < u₃) : False

theorem exists_three_mem_of_three_le_ncard {S : Set ℤ} (_hfin : S.Finite) (hcard : 3 ≤ S.ncard) : ∃ a ∈ S, ∃ b ∈ S, ∃ c ∈ S, a ≠ b ∧ a ≠ c ∧ b ≠ c

theorem exists_strict_order_of_three_distinct_case_lt (a b c : ℤ) (hab : a < b) (hac : a ≠ c) (hbc : b ≠ c) : ∃ (u₁ : ℤ) (u₂ : ℤ) (u₃ : ℤ), {u₁, u₂, u₃} ⊆ {a, b, c} ∧ u₁ < u₂ ∧ u₂ < u₃

theorem exists_strict_order_of_three_distinct (a b c : ℤ) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) : ∃ (u₁ : ℤ) (u₂ : ℤ) (u₃ : ℤ), {u₁, u₂, u₃} ⊆ {a, b, c} ∧ u₁ < u₂ ∧ u₂ < u₃

theorem ncard_le_two_of_no_three_ordered {S : Set ℤ} (hfin : S.Finite) (h : ∀ u₁ ∈ S, ∀ u₂ ∈ S, ∀ u₃ ∈ S, u₁ < u₂ → u₂ < u₃ → False) : S.ncard ≤ 2

theorem ncard_pos_int_in_interval_lt_two (a b : ℝ) (hlen : b - a < 2) : {u : ℤ | 0 < u ∧ a ≤ ↑u ∧ ↑u ≤ b}.ncard ≤ 2

theorem E4_pos_fiber_subset_sqrt (X : ℝ) (_hX : 4 < X) (x : ℕ+) (_hx : ↑↑x > X ^ (1 / 11)) : {u : ℤ | 0 < u ∧ ↑u ^ 2 ≥ 5 * ↑↑x ^ 22 - 4 * X ∧ ↑u ^ 2 ≤ 5 * ↑↑x ^ 22 + 4 * X} ⊆ {u : ℤ | 0 < u ∧ √(5 * ↑↑x ^ 22 - 4 * X) ≤ ↑u ∧ ↑u ≤ √(5 * ↑↑x ^ 22 + 4 * X)}

theorem E4_pos_sqrt_fiber_finite (X : ℝ) (_hX : 4 < X) (x : ℕ+) (_hx : ↑↑x > X ^ (1 / 11)) : {u : ℤ | 0 < u ∧ √(5 * ↑↑x ^ 22 - 4 * X) ≤ ↑u ∧ ↑u ≤ √(5 * ↑↑x ^ 22 + 4 * X)}.Finite

theorem E4_pos_fiber_ncard_via_sqrt (X : ℝ) (hX : 4 < X) (x : ℕ+) (hx : ↑↑x > X ^ (1 / 11)) : {u : ℤ | 0 < u ∧ ↑u ^ 2 ≥ 5 * ↑↑x ^ 22 - 4 * X ∧ ↑u ^ 2 ≤ 5 * ↑↑x ^ 22 + 4 * X}.ncard ≤ {u : ℤ | 0 < u ∧ √(5 * ↑↑x ^ 22 - 4 * X) ≤ ↑u ∧ ↑u ≤ √(5 * ↑↑x ^ 22 + 4 * X)}.ncard

theorem E4_pos_fiber_ncard_le_two (X : ℝ) (hX : 4 < X) (x : ℕ+) (hx : ↑↑x > X ^ (1 / 11)) : {u : ℤ | 0 < u ∧ ↑u ^ 2 ≥ 5 * ↑↑x ^ 22 - 4 * X ∧ ↑u ^ 2 ≤ 5 * ↑↑x ^ 22 + 4 * X}.ncard ≤ 2

theorem neg_maps_to_pos (X : ℝ) (x : ℕ+) (u : ℤ) : u ∈ neg_fiber✝ X x → -u ∈ pos_fiber✝ X x

theorem pos_fiber_subset_Icc (X : ℝ) (x : ℕ+) : pos_fiber✝ X x ⊆ Set.Icc 1 ⌈√(5 * ↑↑x ^ 22 + 4 * X)⌉

theorem pos_fiber_finite (X : ℝ) (x : ℕ+) : (pos_fiber✝ X x).Finite

theorem E4_neg_fiber_ncard_le_pos_fiber (X : ℝ) (x : ℕ+) : {u : ℤ | u < 0 ∧ ↑u ^ 2 ≥ 5 * ↑↑x ^ 22 - 4 * X ∧ ↑u ^ 2 ≤ 5 * ↑↑x ^ 22 + 4 * X}.ncard ≤ {u : ℤ | 0 < u ∧ ↑u ^ 2 ≥ 5 * ↑↑x ^ 22 - 4 * X ∧ ↑u ^ 2 ≤ 5 * ↑↑x ^ 22 + 4 * X}.ncard

theorem E4_neg_fiber_ncard_le_two (X : ℝ) (hX : 4 < X) (x : ℕ+) (hx : ↑↑x > X ^ (1 / 11)) : {u : ℤ | u < 0 ∧ ↑u ^ 2 ≥ 5 * ↑↑x ^ 22 - 4 * X ∧ ↑u ^ 2 ≤ 5 * ↑↑x ^ 22 + 4 * X}.ncard ≤ 2

theorem u_sq_le_of_abs_le (x : ℕ+) (u : ℤ) (X : ℝ) (habs_le : |↑u ^ 2 - 5 * ↑↑↑x ^ 22| ≤ 4 * X) : ↑u ^ 2 ≤ 5 * ↑↑x ^ 22 + 4 * X

theorem u_sq_ge_of_abs_le (x : ℕ+) (u : ℤ) (X : ℝ) (habs_le : |↑u ^ 2 - 5 * ↑↑↑x ^ 22| ≤ 4 * X) : 5 * ↑↑x ^ 22 - 4 * X ≤ ↑u ^ 2

theorem u_sq_in_interval (X : ℝ) (x : ℕ+) (u : ℤ) (h : |↑u ^ 2 - 5 * ↑↑↑x ^ 22| ≤ 4 * X) : 5 * ↑↑x ^ 22 - 4 * X ≤ ↑u ^ 2 ∧ ↑u ^ 2 ≤ 5 * ↑↑x ^ 22 + 4 * X

theorem u_ne_zero_of_fiber (X : ℝ) (_hX : 4 < X) (_x : ℕ+) (_hx : ↑↑_x > X ^ (1 / 11)) (u : ℤ) (hu_lb : 5 * ↑↑_x ^ 22 - 4 * X ≤ ↑u ^ 2) (h5pos : 5 * ↑↑_x ^ 22 - 4 * X > 0) : u ≠ 0

theorem E4_fiber_subset_pos_neg (X : ℝ) (hX : 4 < X) (x : ℕ+) (hx : ↑↑x > X ^ (1 / 11)) : {u : ℤ | (x, u) ∈ E4Set X} ⊆ {u : ℤ | 0 < u ∧ ↑u ^ 2 ≥ 5 * ↑↑x ^ 22 - 4 * X ∧ ↑u ^ 2 ≤ 5 * ↑↑x ^ 22 + 4 * X} ∪ {u : ℤ | u < 0 ∧ ↑u ^ 2 ≥ 5 * ↑↑x ^ 22 - 4 * X ∧ ↑u ^ 2 ≤ 5 * ↑↑x ^ 22 + 4 * X}

theorem int_mem_Icc_ceil_sqrt_of_sq_le (y : ℤ) (M : ℝ) (hM : 0 ≤ M) (hy : ↑y ^ 2 ≤ M) : y ∈ Set.Icc (-⌈√M⌉) ⌈√M⌉

theorem E4_pos_neg_fiber_finite (X : ℝ) (hX : 4 < X) (x : ℕ+) (_hx : ↑↑x > X ^ (1 / 11)) : ({u : ℤ | 0 < u ∧ ↑u ^ 2 ≥ 5 * ↑↑x ^ 22 - 4 * X ∧ ↑u ^ 2 ≤ 5 * ↑↑x ^ 22 + 4 * X} ∪ {u : ℤ | u < 0 ∧ ↑u ^ 2 ≥ 5 * ↑↑x ^ 22 - 4 * X ∧ ↑u ^ 2 ≤ 5 * ↑↑x ^ 22 + 4 * X}).Finite

theorem E4_fiber_ncard_le_four (X : ℝ) (hX : 4 < X) (x : ℕ+) (hx : ↑↑x > X ^ (1 / 11)) : {u : ℤ | (x, u) ∈ E4Set X}.ncard ≤ 4

theorem E4_fiber_empty_of_le (X : ℝ) (x : ℕ+) (hx : ¬↑↑x > X ^ (1 / 11)) : {u : ℤ | (x, u) ∈ E4Set X} = ∅

theorem denom_pos_E4 (ε : ℝ) (hε : 0 < ε) (hε_bound : ε ≤ 1 / 24) : 0 < 10 - 12 * ε

theorem exponent_bound_E4 (η ε : ℝ) (hη : 0 < η) (hε : 0 < ε) (hε_η : ε ≤ η) (hε_bound : ε ≤ 1 / 24) : (2 + ε) / (10 - 12 * ε) ≤ 1 / 5 + η

theorem five_x22_gt_four_X_of_x_gt (X : ℝ) (hX : 1 < X) (x : ℕ+) (hx : ↑↑x > X ^ (1 / 11)) : 5 * ↑↑x ^ 22 > 4 * X

theorem product_upper_bound (x : ℕ+) (X : ℝ) (hX : 1 < X) (Y : ℝ) (_hY : 0 ≤ Y) (h_Y : Y ≤ √2 * ↑↑x ^ (11 / 2)) : ↑↑x * Y * X ≤ √2 * ↑↑x ^ (13 / 2) * X

theorem rpow_triple_mul_distrib (a b c e : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) : (a * b * c) ^ e = a ^ e * b ^ e * c ^ e

theorem pnat_rpow_mul (x : ℕ+) (p q : ℝ) : ↑↑x ^ (p * q) = (↑↑x ^ p) ^ q

theorem rpow_product_expand (x : ℕ+) (X : ℝ) (hX : 1 < X) (ε : ℝ) (_hε : 0 < ε) : (√2 * ↑↑x ^ (13 / 2) * X) ^ (1 + ε) = √2 ^ (1 + ε) * ↑↑x ^ (13 / 2 * (1 + ε)) * X ^ (1 + ε)

theorem combine_X_powers (K : ℝ) (x : ℕ+) (X : ℝ) (hX : 1 < X) (ε : ℝ) (_hε : 0 < ε) : K * X * (√2 ^ (1 + ε) * ↑↑x ^ (13 / 2 * (1 + ε)) * X ^ (1 + ε)) = K * √2 ^ (1 + ε) * ↑↑x ^ (13 / 2 * (1 + ε)) * X ^ (2 + ε)

theorem substitute_Y_bound (K : ℝ) (hK : 0 < K) (ε : ℝ) (hε : 0 < ε) (x : ℕ+) (X : ℝ) (hX : 1 < X) (Y : ℝ) (hY : 0 ≤ Y) (h_x11 : ↑↑x ^ 11 ≤ K * X * (↑↑x * Y * X) ^ (1 + ε)) (h_Y : Y ≤ √2 * ↑↑x ^ (11 / 2)) : ↑↑x ^ 11 ≤ K * √2 ^ (1 + ε) * ↑↑x ^ (13 / 2 * (1 + ε)) * X ^ (2 + ε)

theorem cancel_common_rpow_factor (K : ℝ) (_hK : 0 < K) (ε : ℝ) (_hε : 0 < ε) (_hε' : ε < 9 / 13) (x : ℕ+) (X : ℝ) (_hX : 1 < X) (h : ↑↑x ^ (13 / 2 * (1 + ε)) * ↑↑x ^ ((9 - 13 * ε) / 2) ≤ ↑↑x ^ (13 / 2 * (1 + ε)) * (K * √2 ^ (1 + ε) * X ^ (2 + ε))) : ↑↑x ^ ((9 - 13 * ε) / 2) ≤ K * √2 ^ (1 + ε) * X ^ (2 + ε)

theorem exponent_sum_eq_11 (ε : ℝ) : 13 / 2 * (1 + ε) + (9 - 13 * ε) / 2 = 11

theorem lhs_eq_x_pow_11 (ε : ℝ) (_hε : 0 < ε) (_hε' : ε < 9 / 13) (x : ℕ+) (hx : 0 < ↑↑x) : ↑↑x ^ (13 / 2 * (1 + ε)) * ↑↑x ^ ((9 - 13 * ε) / 2) = ↑↑x ^ 11

theorem nat_pow_eq_rpow (x : ℕ+) : ↑↑x ^ 11 = ↑↑x ^ 11

theorem rhs_rearrange (K ε : ℝ) (x : ℕ+) (X : ℝ) : K * √2 ^ (1 + ε) * ↑↑x ^ (13 / 2 * (1 + ε)) * X ^ (2 + ε) = ↑↑x ^ (13 / 2 * (1 + ε)) * (K * √2 ^ (1 + ε) * X ^ (2 + ε))

theorem rewrite_hypothesis (K : ℝ) (_hK : 0 < K) (ε : ℝ) (hε : 0 < ε) (hε' : ε < 9 / 13) (x : ℕ+) (X : ℝ) (_hX : 1 < X) (h : ↑↑x ^ 11 ≤ K * √2 ^ (1 + ε) * ↑↑x ^ (13 / 2 * (1 + ε)) * X ^ (2 + ε)) : ↑↑x ^ (13 / 2 * (1 + ε)) * ↑↑x ^ ((9 - 13 * ε) / 2) ≤ ↑↑x ^ (13 / 2 * (1 + ε)) * (K * √2 ^ (1 + ε) * X ^ (2 + ε))

theorem isolate_x_power (K : ℝ) (hK : 0 < K) (ε : ℝ) (hε : 0 < ε) (hε' : ε < 9 / 13) (x : ℕ+) (X : ℝ) (hX : 1 < X) (h : ↑↑x ^ 11 ≤ K * √2 ^ (1 + ε) * ↑↑x ^ (13 / 2 * (1 + ε)) * X ^ (2 + ε)) : ↑↑x ^ ((9 - 13 * ε) / 2) ≤ K * √2 ^ (1 + ε) * X ^ (2 + ε)

theorem denom_pos_general (ε : ℝ) (_hε : 0 < ε) (hε' : ε < 9 / 13) : 0 < 9 - 13 * ε

theorem exponent_cancel (ε : ℝ) (_hε : 0 < ε) (hε' : ε < 9 / 13) : (9 - 13 * ε) / 2 * (2 / (9 - 13 * ε)) = 1

theorem X_exponent_eq (ε : ℝ) (_hε : 0 < ε) (_hε' : ε < 9 / 13) : (2 + ε) * (2 / (9 - 13 * ε)) = (4 + 2 * ε) / (9 - 13 * ε)

theorem raise_to_reciprocal_power (K : ℝ) (hK : 0 < K) (ε : ℝ) (hε : 0 < ε) (hε' : ε < 9 / 13) (x : ℕ+) (X : ℝ) (hX : 1 < X) (h : ↑↑x ^ ((9 - 13 * ε) / 2) ≤ K * √2 ^ (1 + ε) * X ^ (2 + ε)) : ↑↑x ≤ (K * √2 ^ (1 + ε)) ^ (2 / (9 - 13 * ε)) * X ^ ((4 + 2 * ε) / (9 - 13 * ε))

theorem u_ne_zero_of_E4 (X : ℝ) (hX : 1 < X) (p : ℕ+ × ℤ) (hp : p ∈ E4Set X) : p.2 ≠ 0

theorem x_pow11_gt_X (x : ℕ+) (X : ℝ) (hX : 1 < X) (hx_lower : ↑↑x > X ^ (1 / 11)) : ↑↑x ^ 11 > X

theorem x11_gt_one (x : ℕ+) (X : ℝ) (hX : 1 < X) (hx11_gt : ↑↑x ^ 11 > X) : ↑↑x ^ 11 > 1

theorem x22_gt_X (x : ℕ+) (X : ℝ) (hX : 1 < X) (hx11_gt : ↑↑x ^ 11 > X) : ↑↑x ^ 22 > X

theorem four_X_le_four_x22 (x : ℕ+) (X : ℝ) (hX : 1 < X) (hx11_gt : ↑↑x ^ 11 > X) : 4 * X < 4 * ↑↑x ^ 22

theorem u_sq_lt_nine_x22 (x : ℕ+) (u : ℤ) (X : ℝ) (hu_sq : ↑u ^ 2 ≤ 5 * ↑↑x ^ 22 + 4 * X) (h4X : 4 * X < 4 * ↑↑x ^ 22) : ↑u ^ 2 < 9 * ↑↑x ^ 22

theorem natAbs_le_of_sq_lt (x : ℕ+) (u : ℤ) (hu_sq : ↑u ^ 2 < 9 * ↑↑x ^ 22) : ↑u.natAbs ≤ 3 * ↑↑x ^ 11

theorem u_bound_from_E4 (x : ℕ+) (u : ℤ) (X : ℝ) (hX : 1 < X) (hx_lower : ↑↑x > X ^ (1 / 11)) (habs_le : |↑u ^ 2 - 5 * ↑↑↑x ^ 22| ≤ 4 * X) : ↑u.natAbs ≤ 3 * ↑↑x ^ 11

theorem radical_pow (n k : ℕ) (hn : 0 < n) (hk : 0 < k) : (n ^ k).radical = n.radical

theorem radical_prime (p : ℕ) (hp : Nat.Prime p) : p.radical = p

theorem radical_factors_le (U x D : ℕ) (hU : 0 < U) (hx : 0 < x) (hD : 0 < D) : U.radical * D.radical * (Nat.radical 5 * x.radical) ≤ U * D * (5 * x)

theorem radical_chain_bound (U x D : ℕ) (hU : 0 < U) (hx : 0 < x) (_hD : 0 < D) : (U ^ 2 * D * (5 * x ^ 22)).radical ≤ U.radical * D.radical * (Nat.radical 5 * x.radical)

theorem radical_E4_bound_nat (U x D : ℕ) (hU : 0 < U) (hx : 0 < x) (hD : 0 < D) : (U ^ 2 * D * (5 * x ^ 22)).radical ≤ U * D * (5 * x)

theorem radical_E4_bound (U x D : ℕ) (hU : 0 < U) (hx : 0 < x) (hD : 0 < D) : ↑(U ^ 2 * D * (5 * x ^ 22)).radical ≤ ↑U * ↑D * (5 * ↑x)

theorem radical_E4_bound' (U x D : ℕ) (hU : 0 < U) (hx : 0 < x) (hD : 0 < D) : ↑(5 * x ^ 22 * D * U ^ 2).radical ≤ 5 * ↑x * ↑D * ↑U

theorem radical_dvd_le (d n : ℕ) (hd : 0 < d) (hn : 0 < n) (hdvd : d ∣ n) : d.radical ≤ n.radical

theorem coprime_of_div_gcd (a b : ℕ) (h : 0 < a.gcd b) : (a / a.gcd b).Coprime (b / a.gcd b)

theorem gcd_reduction_coprime (a b : ℕ) (ha : 0 < a) : (a / a.gcd b).Coprime (b / a.gcd b)

theorem gcd_reduction_pos_a_div (a b : ℕ) (ha : 0 < a) : 0 < a / a.gcd b

theorem gcd_reduction_pos_b_div (a b : ℕ) (hb : 0 < b) : 0 < b / a.gcd b

theorem gcd_dvd_add (a b : ℕ) : a.gcd b ∣ a + b

theorem gcd_pos_of_sum_pos (a b c : ℕ) (hc : 0 < c) (hsum : a + b = c) : 0 < a.gcd b

theorem gcd_reduction_pos_c_div (a b c : ℕ) (hc : 0 < c) (hsum : a + b = c) : 0 < c / a.gcd b

theorem gcd_reduction_dvd_c (a b c : ℕ) (hsum : a + b = c) : a.gcd b ∣ c

theorem gcd_reduction_mul_div_cancel (a b c : ℕ) (hsum : a + b = c) : a.gcd b * (c / a.gcd b) = c

theorem abc_eq_gcd_cubed_mul (a b c : ℕ) (_ha : 0 < a) (_hb : 0 < b) (_hc : 0 < c) (hsum : a + b = c) : a * b * c = a.gcd b ^ 3 * (a / a.gcd b * (b / a.gcd b) * (c / a.gcd b))

theorem gcd_reduction_product_dvd (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hsum : a + b = c) : a / a.gcd b * (b / a.gcd b) * (c / a.gcd b) ∣ a * b * c

theorem gcd_reduction (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hsum : a + b = c) : have g := a.gcd b; (a / g).Coprime (b / g) ∧ a / g + b / g = c / g ∧ 0 < a / g ∧ 0 < b / g ∧ 0 < c / g ∧ g ∣ c ∧ g * (c / g) = c ∧ a / g * (b / g) * (c / g) ∣ a * b * c

theorem abc_triple_to_bound (K : ℝ) (hK : 0 < K) (ε : ℝ) (hε : 0 < ε) (habc_ineq : ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → a.Coprime b → a + b = c → ↑c ≤ K * ↑(a * b * c).radical ^ (1 + ε)) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hsum : a + b = c) (g_bound : ℝ) (hg_bound : ↑(a.gcd b) ≤ g_bound) (rad_bound : ℝ) (hrad : ↑(a * b * c).radical ≤ rad_bound) (hrad_nn : 0 ≤ rad_bound) : ↑c ≤ g_bound * K * rad_bound ^ (1 + ε)

theorem abc_E4_sum_eq (x : ℕ+) (u : ℤ) (hD_pos : u ^ 2 - 5 * ↑↑x ^ 22 > 0) : 5 * ↑x ^ 22 + (u ^ 2 - 5 * ↑↑x ^ 22).natAbs = u.natAbs ^ 2

theorem D_pos_of_hD_pos (x : ℕ+) (u : ℤ) (hD_pos : u ^ 2 - 5 * ↑↑x ^ 22 > 0) : 0 < (u ^ 2 - 5 * ↑↑x ^ 22).natAbs

theorem gcd_le_D (x : ℕ+) (u : ℤ) (hD_pos : u ^ 2 - 5 * ↑↑x ^ 22 > 0) : ↑((5 * ↑x ^ 22).gcd (u ^ 2 - 5 * ↑↑x ^ 22).natAbs) ≤ ↑(u ^ 2 - 5 * ↑↑x ^ 22).natAbs

theorem int_ineq_from_sub_pos (x : ℕ+) (u : ℤ) (hD_pos : u ^ 2 - 5 * ↑↑x ^ 22 > 0) : 5 * ↑↑x ^ 22 < u ^ 2

theorem cast_int_ineq_to_real (x : ℕ+) (u : ℤ) (h : 5 * ↑↑x ^ 22 < u ^ 2) : 5 * ↑↑x ^ 22 < ↑u ^ 2

theorem natAbs_sq_real (u : ℤ) : ↑u.natAbs ^ 2 = ↑u ^ 2

theorem five_x22_lt_U_sq (x : ℕ+) (u : ℤ) (hD_pos : u ^ 2 - 5 * ↑↑x ^ 22 > 0) : 5 * ↑↑x ^ 22 < ↑u.natAbs ^ 2

theorem radical_E4_bound_reorder (U x D : ℕ) (hU : 0 < U) (hx : 0 < x) (hD : 0 < D) : ↑(5 * x ^ 22 * D * U ^ 2).radical ≤ ↑U * ↑D * (5 * ↑x)

theorem abc_E4_case_pos (K : ℝ) (hK : 0 < K) (ε : ℝ) (hε : 0 < ε) (habc_ineq : ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → a.Coprime b → a + b = c → ↑c ≤ K * ↑(a * b * c).radical ^ (1 + ε)) (x : ℕ+) (u : ℤ) (hu_ne : u ≠ 0) (hD_pos : u ^ 2 - 5 * ↑↑x ^ 22 > 0) : have D := ↑(u ^ 2 - 5 * ↑↑x ^ 22).natAbs; 5 * ↑↑x ^ 22 ≤ D * K * (↑u.natAbs * D * (5 * ↑↑x)) ^ (1 + ε)

theorem E4_neg_abc_sum_int (x : ℕ+) (u : ℤ) (habs_pos : 1 ≤ |u ^ 2 - 5 * ↑↑x ^ 22|) (hD_neg : u ^ 2 - 5 * ↑↑x ^ 22 ≤ 0) : ↑u.natAbs ^ 2 + ↑(u ^ 2 - 5 * ↑↑x ^ 22).natAbs = 5 * ↑↑x ^ 22

theorem E4_neg_abc_sum (x : ℕ+) (u : ℤ) (habs_pos : 1 ≤ |u ^ 2 - 5 * ↑↑x ^ 22|) (hD_neg : u ^ 2 - 5 * ↑↑x ^ 22 ≤ 0) : u.natAbs ^ 2 + (u ^ 2 - 5 * ↑↑x ^ 22).natAbs = 5 * ↑x ^ 22

theorem E4_neg_D_natAbs_pos (u : ℤ) (x : ℕ+) (habs_pos : 1 ≤ |u ^ 2 - 5 * ↑↑x ^ 22|) (hD_neg : u ^ 2 - 5 * ↑↑x ^ 22 ≤ 0) : 0 < (u ^ 2 - 5 * ↑↑x ^ 22).natAbs

theorem natAbs_pos_of_ne_zero (y : ℤ) (hy : y ≠ 0) : 0 < y.natAbs

theorem E4_neg_gcd_le_D (x : ℕ+) (u : ℤ) (habs_pos : 1 ≤ |u ^ 2 - 5 * ↑↑x ^ 22|) (_hD_neg : u ^ 2 - 5 * ↑↑x ^ 22 ≤ 0) : ↑((u.natAbs ^ 2).gcd (u ^ 2 - 5 * ↑↑x ^ 22).natAbs) ≤ ↑(u ^ 2 - 5 * ↑↑x ^ 22).natAbs

theorem abc_E4_case_neg (K : ℝ) (hK : 0 < K) (ε : ℝ) (hε : 0 < ε) (habc_ineq : ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → a.Coprime b → a + b = c → ↑c ≤ K * ↑(a * b * c).radical ^ (1 + ε)) (x : ℕ+) (u : ℤ) (hu_ne : u ≠ 0) (habs_pos : 1 ≤ |u ^ 2 - 5 * ↑↑x ^ 22|) (hD_neg : u ^ 2 - 5 * ↑↑x ^ 22 ≤ 0) : have D := ↑(u ^ 2 - 5 * ↑↑x ^ 22).natAbs; 5 * ↑↑x ^ 22 ≤ D * K * (5 * ↑↑x * D * ↑u.natAbs) ^ (1 + ε)

theorem natAbs_D_eq_abs_cast (x : ℕ+) (u : ℤ) : ↑(u ^ 2 - 5 * ↑↑x ^ 22).natAbs = |↑u ^ 2 - 5 * ↑↑↑x ^ 22|

theorem combine_pos_case (K : ℝ) (hK : 0 < K) (ε : ℝ) (hε : 0 < ε) (habc_ineq : ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → a.Coprime b → a + b = c → ↑c ≤ K * ↑(a * b * c).radical ^ (1 + ε)) (x : ℕ+) (u : ℤ) (hu_ne : u ≠ 0) (habs_pos : 1 ≤ |u ^ 2 - 5 * ↑↑x ^ 22|) (hsgn : u ^ 2 - 5 * ↑↑x ^ 22 > 0) : 5 * ↑↑x ^ 22 ≤ |↑u ^ 2 - 5 * ↑↑↑x ^ 22| * K * (5 * ↑↑x * ↑u.natAbs * |↑u ^ 2 - 5 * ↑↑↑x ^ 22|) ^ (1 + ε)

theorem combine_neg_case (K : ℝ) (hK : 0 < K) (ε : ℝ) (hε : 0 < ε) (habc_ineq : ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → a.Coprime b → a + b = c → ↑c ≤ K * ↑(a * b * c).radical ^ (1 + ε)) (x : ℕ+) (u : ℤ) (hu_ne : u ≠ 0) (habs_pos : 1 ≤ |u ^ 2 - 5 * ↑↑x ^ 22|) (hsgn : u ^ 2 - 5 * ↑↑x ^ 22 ≤ 0) : 5 * ↑↑x ^ 22 ≤ |↑u ^ 2 - 5 * ↑↑↑x ^ 22| * K * (5 * ↑↑x * ↑u.natAbs * |↑u ^ 2 - 5 * ↑↑↑x ^ 22|) ^ (1 + ε)

theorem abc_gives_5x22_bound (K : ℝ) (hK : 0 < K) (ε : ℝ) (hε : 0 < ε) (habc_ineq : ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → a.Coprime b → a + b = c → ↑c ≤ K * ↑(a * b * c).radical ^ (1 + ε)) (x : ℕ+) (u : ℤ) (X : ℝ) (_hX : 1 < X) (hu_ne : u ≠ 0) (habs_pos : 1 ≤ |u ^ 2 - 5 * ↑↑x ^ 22|) (_habs_le : |↑u ^ 2 - 5 * ↑↑↑x ^ 22| ≤ 4 * X) : 5 * ↑↑x ^ 22 ≤ |↑u ^ 2 - 5 * ↑↑↑x ^ 22| * K * (5 * ↑↑x * ↑u.natAbs * |↑u ^ 2 - 5 * ↑↑↑x ^ 22|) ^ (1 + ε)

theorem product_bound_E4 (x : ℕ+) (u : ℤ) (D : ℝ) (hD : 0 ≤ D) (hu_bound : ↑u.natAbs ≤ 3 * ↑↑x ^ 11) : 5 * ↑↑x * ↑u.natAbs * D ≤ 15 * ↑↑x ^ 12 * D

theorem product_nonneg_E4 (x : ℕ+) (u : ℤ) (D : ℝ) (hD : 0 ≤ D) : 0 ≤ 5 * ↑↑x * ↑u.natAbs * D

theorem rpow_product_bound (x : ℕ+) (u : ℤ) (D ε : ℝ) (hε : 0 < ε) (hD : 0 ≤ D) (hu_bound : ↑u.natAbs ≤ 3 * ↑↑x ^ 11) : (5 * ↑↑x * ↑u.natAbs * D) ^ (1 + ε) ≤ (15 * ↑↑x ^ 12 * D) ^ (1 + ε)

theorem combine_D_powers (D ε : ℝ) (hD : 0 < D) : D * D ^ (1 + ε) = D ^ (2 + ε)

theorem pnat_cast_nonneg (x : ℕ+) : 0 ≤ ↑↑x

theorem pnat_pow_rpow_eq (x : ℕ+) (ε : ℝ) : (↑↑x ^ 12) ^ (1 + ε) = ↑↑x ^ (12 * (1 + ε))

theorem expand_rhs (K ε : ℝ) (_hε : 0 < ε) (x : ℕ+) (D : ℝ) (hD_pos : 0 < D) : D * K * (15 * ↑↑x ^ 12 * D) ^ (1 + ε) = K * 15 ^ (1 + ε) * ↑↑x ^ (12 * (1 + ε)) * D ^ (2 + ε)

theorem nat_pow_div_rpow_eq (x : ℝ) (hx : 0 < x) (e : ℝ) : x ^ 22 / x ^ e = x ^ (22 - e)

theorem div_ineq_of_mul_le (a b c : ℝ) (hc : 0 < c) (h : 5 * a ≤ b * c) : a / c ≤ b / 5

theorem divide_and_simplify (K : ℝ) (_hK : 0 < K) (ε : ℝ) (_hε : 0 < ε) (_hε_bound : ε ≤ 1 / 24) (x : ℕ+) (D : ℝ) (_hD_pos : 0 < D) (h : 5 * ↑↑x ^ 22 ≤ K * 15 ^ (1 + ε) * ↑↑x ^ (12 * (1 + ε)) * D ^ (2 + ε)) : ↑↑x ^ (10 - 12 * ε) ≤ K * 15 ^ (1 + ε) / 5 * D ^ (2 + ε)

theorem rearrange_to_target (K : ℝ) (hK : 0 < K) (ε : ℝ) (hε : 0 < ε) (hε_bound : ε ≤ 1 / 24) (x : ℕ+) (D : ℝ) (hD_pos : 0 < D) (h : 5 * ↑↑x ^ 22 ≤ D * K * (15 * ↑↑x ^ 12 * D) ^ (1 + ε)) : ↑↑x ^ (10 - 12 * ε) ≤ K * 15 ^ (1 + ε) / 5 * D ^ (2 + ε)

theorem combine_h5x22_with_bound (K : ℝ) (hK : 0 < K) (ε : ℝ) (hε : 0 < ε) (x : ℕ+) (u : ℤ) (D : ℝ) (hD_pos : 0 < D) (hu_bound : ↑u.natAbs ≤ 3 * ↑↑x ^ 11) (h5x22 : 5 * ↑↑x ^ 22 ≤ D * K * (5 * ↑↑x * ↑u.natAbs * D) ^ (1 + ε)) : 5 * ↑↑x ^ 22 ≤ D * K * (15 * ↑↑x ^ 12 * D) ^ (1 + ε)

theorem E4_algebraic_cleanup (K : ℝ) (hK : 0 < K) (ε : ℝ) (hε : 0 < ε) (hε_bound : ε ≤ 1 / 24) (x : ℕ+) (u : ℤ) (D : ℝ) (hD_pos : 0 < D) (_hD_ge_one : 1 ≤ D) (hu_bound : ↑u.natAbs ≤ 3 * ↑↑x ^ 11) (h5x22 : 5 * ↑↑x ^ 22 ≤ D * K * (5 * ↑↑x * ↑u.natAbs * D) ^ (1 + ε)) : ↑↑x ^ (10 - 12 * ε) ≤ K * 15 ^ (1 + ε) / 5 * D ^ (2 + ε)

theorem exponent_cleanup_E4 (K : ℝ) (hK : 0 < K) (ε : ℝ) (hε : 0 < ε) (hε_bound : ε ≤ 1 / 24) : ∃ (K₂ : ℝ), 0 < K₂ ∧ ∃ (X₁ : ℝ), 0 < X₁ ∧ ∀ (X : ℝ), X₁ < X → ∀ (x : ℕ+) (u : ℤ), ↑↑x > X ^ (1 / 11) → 1 ≤ |u ^ 2 - 5 * ↑↑x ^ 22| → |↑u ^ 2 - 5 * ↑↑↑x ^ 22| ≤ 4 * X → 5 * ↑↑x ^ 22 ≤ |↑u ^ 2 - 5 * ↑↑↑x ^ 22| * K * (5 * ↑↑x * ↑u.natAbs * |↑u ^ 2 - 5 * ↑↑↑x ^ 22|) ^ (1 + ε) → ↑↑x ^ (10 - 12 * ε) ≤ K₂ * |↑u ^ 2 - 5 * ↑↑↑x ^ 22| ^ (2 + ε)

theorem abc_core_E4 (habc : ABC) (ε : ℝ) (hε : 0 < ε) (hε_bound : ε ≤ 1 / 24) : ∃ (K₂ : ℝ), 0 < K₂ ∧ ∃ (X₁ : ℝ), 0 < X₁ ∧ ∀ (X : ℝ), X₁ < X → ∀ p ∈ E4Set X, ↑↑p.1 ^ (10 - 12 * ε) ≤ K₂ * |↑p.2 ^ 2 - 5 * ↑↑↑p.1 ^ 22| ^ (2 + ε)

theorem x_from_power_bound_E4 (ε : ℝ) (hε : 0 < ε) (hε_bound : ε ≤ 1 / 24) (K₂ : ℝ) (hK₂ : 0 < K₂) : ∃ (K₃ : ℝ), 0 < K₃ ∧ ∀ (X : ℝ), 1 < X → ∀ p ∈ E4Set X, ↑↑p.1 ^ (10 - 12 * ε) ≤ K₂ * |↑p.2 ^ 2 - 5 * ↑↑↑p.1 ^ 22| ^ (2 + ε) → ↑↑p.1 ≤ K₃ * X ^ ((2 + ε) / (10 - 12 * ε))

theorem rpow_le_rpow_of_le_exp' {X a b : ℝ} (hX : 1 ≤ X) (hab : a ≤ b) : X ^ a ≤ X ^ b

theorem x_bound_in_E4 (habc : ABC) (η : ℝ) (hη : 0 < η) : ∃ (K₄ : ℝ), 0 < K₄ ∧ ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → ∀ p ∈ E4Set X, ↑↑p.1 ≤ K₄ * X ^ (1 / 5 + η)

theorem cast_coercion_eq (p₁ : ℕ+) : 5 * ↑↑↑p₁ ^ 22 = 5 * ↑↑p₁ ^ 22

theorem abs_bound_to_upper_bound (u : ℤ) (p₁ : ℕ+) (X : ℝ) (h : |↑u ^ 2 - 5 * ↑↑↑p₁ ^ 22| ≤ 4 * X) : ↑u ^ 2 ≤ 5 * ↑↑p₁ ^ 22 + 4 * X

theorem u_sq_le_of_mem_E4 (X : ℝ) (p : ℕ+ × ℤ) (hmem : p ∈ E4Set X) : ↑p.2 ^ 2 ≤ 5 * ↑↑p.1 ^ 22 + 4 * X

theorem u_sq_le_bound (X : ℝ) (p : ℕ+ × ℤ) (hmem : p ∈ E4Set X) (N : ℕ) (hN : ↑p.1 ≤ N) : ↑p.2 ^ 2 ≤ 5 * ↑N ^ 22 + 4 * X

theorem cast_abs_le_sqrt_of_sq_le (u : ℤ) (B : ℝ) (hB : ↑u ^ 2 ≤ B) : ↑|u| ≤ √B

theorem abs_le_ceil_of_cast_le_sqrt (u : ℤ) (B : ℝ) (h : ↑|u| ≤ √B) : |u| ≤ ↑⌈√B⌉₊

theorem abs_le_ceil_sqrt_of_sq_le (u : ℤ) (B : ℝ) (hB : ↑u ^ 2 ≤ B) : |u| ≤ ↑⌈√B⌉₊

theorem u_bound_from_E4_membership (X : ℝ) (p : ℕ+ × ℤ) (hmem : p ∈ E4Set X) (N : ℕ) (hN : ↑p.1 ≤ N) : |p.2| ≤ ↑⌈√(5 * ↑N ^ 22 + 4 * X)⌉₊

theorem E4_set_bounded_of_abc (habc : ABC) : ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → ∃ (N : ℕ) (M : ℕ), ∀ p ∈ E4Set X, ↑p.1 ≤ N ∧ |p.2| ≤ ↑M

theorem E4_set_finite_of_abc (habc : ABC) : ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → (E4Set X).Finite

theorem witness_in_E4_set (R : RamanujanTau) (X : ℝ) (p : ℕ+) (hp : Nat.Prime ↑p) (hp_large : ↑↑p > X ^ (1 / 11)) (ℓ : ℕ) (hℓ_prime : Nat.Prime ℓ) (hℓ_le : ↑ℓ ≤ X) (hℓ_eq : (R.τ (p ^ 4)).natAbs = ℓ) : (p, 2 * R.τ p ^ 2 - 3 * ↑↑p ^ 11) ∈ E4Set X

theorem ncard_witness_le_E4 (R : RamanujanTau) (X : ℝ) (hfin : (E4Set X).Finite) : {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ↑↑p > X ^ (1 / 11) ∧ (R.τ (p ^ 4)).natAbs = ℓ}.ncard ≤ E4 X

theorem large_primes_k2_bound (R : RamanujanTau) (habc : ABC) : ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → ↑{ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ↑↑p > X ^ (1 / 11) ∧ (R.τ (p ^ 4)).natAbs = ℓ}.ncard ≤ ↑(E4 X)

theorem k2_set_split (R : RamanujanTau) (X : ℝ) : {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 4)).natAbs = ℓ} ⊆ {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ↑↑p ≤ X ^ (1 / 11) ∧ (R.τ (p ^ 4)).natAbs = ℓ} ∪ {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ ↑↑p > X ^ (1 / 11) ∧ (R.τ (p ^ 4)).natAbs = ℓ}

theorem k2_target_set_finite (R : RamanujanTau) (X : ℝ) : {ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 4)).natAbs = ℓ}.Finite

theorem k2_contribution_abc (R : RamanujanTau) (habc : ABC) : ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → ↑{ℓ : ℕ | Nat.Prime ℓ ∧ ↑ℓ ≤ X ∧ ∃ (p : ℕ+), Nat.Prime ↑p ∧ (R.τ (p ^ 4)).natAbs = ℓ}.ncard ≤ ↑(E4 X) + X ^ (6 / 11)

theorem reduction_lemma_core (R : RamanujanTau) (habc : ABC) (h54 : Proposition54 R) : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → ↑(S R X) ≤ C * (X ^ (1 / 2) * Real.log X + X ^ (13 / 22) + X ^ (6 / 11) + ↑(E2 X) + ↑(E4 X))

theorem reduction_lemma (R : RamanujanTau) (habc : ABC) (h54 : Proposition54 R) : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → ↑(S R X) ≤ C * (X ^ (1 / 2) * Real.log X + X ^ (13 / 22) + X ^ (6 / 11) + ↑(E2 X) + ↑(E4 X))

theorem E2Helpers.eventually_rpow_ge_const {C a b : ℝ} (_hC : 0 < C) (hab : a < b) : ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → C ≤ X ^ (b - a)

theorem E2Helpers.rpow_diff_mul_rpow_le {C a b X : ℝ} (hX : 0 < X) (h : C ≤ X ^ (b - a)) : C * X ^ a ≤ X ^ b

theorem E2Helpers.E2_caseA_mem (X : ℝ) (x : ℕ+) (y : ℤ) (h_abs_le : |↑↑↑x ^ 11 - ↑y ^ 2| ≤ X) (h_sign : y ^ 2 ≤ ↑↑x ^ 11 - 1) : y ∈ {y : ℤ | y ^ 2 ≤ ↑↑x ^ 11 - 1 ∧ ↑(↑↑x ^ 11 - y ^ 2) ≤ X}

theorem E2Helpers.E2_caseB_mem (X : ℝ) (x : ℕ+) (y : ℤ) (h_abs_le : |↑↑↑x ^ 11 - ↑y ^ 2| ≤ X) (h_sign : ↑↑x ^ 11 + 1 ≤ y ^ 2) : y ∈ {y : ℤ | ↑↑x ^ 11 + 1 ≤ y ^ 2 ∧ ↑(y ^ 2 - ↑↑x ^ 11) ≤ X}

theorem E2Helpers.E2_fiber_subset_union (X : ℝ) (_hX : 2 < X) (x : ℕ+) (_hx : ↑↑x > X ^ (2 / 11)) : {y : ℤ | (x, y) ∈ E2Set X} ⊆ {y : ℤ | y ^ 2 ≤ ↑↑x ^ 11 - 1 ∧ ↑(↑↑x ^ 11 - y ^ 2) ≤ X} ∪ {y : ℤ | ↑↑x ^ 11 + 1 ≤ y ^ 2 ∧ ↑(y ^ 2 - ↑↑x ^ 11) ≤ X}

theorem E2Helpers.sq_le_imp_mem_Icc (x : ℕ+) (y : ℤ) (hy : y ^ 2 ≤ ↑↑x ^ 11 - 1) : y ∈ Set.Icc (-↑↑x ^ 11) (↑↑x ^ 11)

theorem E2Helpers.E2_caseA_finite (X : ℝ) (_hX : 2 < X) (x : ℕ+) (_hx : ↑↑x > X ^ (2 / 11)) : {y : ℤ | y ^ 2 ≤ ↑↑x ^ 11 - 1 ∧ ↑(↑↑x ^ 11 - y ^ 2) ≤ X}.Finite

theorem E2Helpers.nonneg_int_short_interval_finite (a b : ℝ) (_hab : a ≤ b) : {n : ℤ | 0 ≤ n ∧ a ≤ ↑n ∧ ↑n ≤ b}.Finite

theorem E2Helpers.int_eq_of_cast_in_short_interval (n₁ n₂ : ℤ) (a b : ℝ) (hlen : b - a < 1) (ha1 : a ≤ ↑n₁) (hb1 : ↑n₁ ≤ b) (ha2 : a ≤ ↑n₂) (hb2 : ↑n₂ ≤ b) : n₁ = n₂

theorem E2Helpers.ncard_nonneg_int_in_short_interval (a b : ℝ) (hab : a ≤ b) (hlen : b - a < 1) (_ha : 0 ≤ a) : {n : ℤ | 0 ≤ n ∧ a ≤ ↑n ∧ ↑n ≤ b}.ncard ≤ 1

theorem E2Helpers.rpow_two_eleven_eq_sq (X : ℝ) (hX : 0 < X) : (X ^ (2 / 11)) ^ 11 = X ^ 2

theorem E2Helpers.pow_eleven_strict_mono (X : ℝ) (hX : 0 < X) (x : ℕ+) (hx : ↑↑x > X ^ (2 / 11)) : (X ^ (2 / 11)) ^ 11 < ↑↑x ^ 11

theorem E2Helpers.x11_gt_X_sq (X : ℝ) (hX : 2 < X) (x : ℕ+) (hx : ↑↑x > X ^ (2 / 11)) : ↑↑x ^ 11 > X ^ 2

theorem E2Helpers.x11_sub_X_pos (X : ℝ) (hX : 2 < X) (x : ℕ+) (hx : ↑↑x > X ^ (2 / 11)) : ↑↑x ^ 11 - X > 0

theorem E2Helpers.x11_sub_one_pos (X : ℝ) (hX : 2 < X) (x : ℕ+) (hx : ↑↑x > X ^ (2 / 11)) : ↑↑x ^ 11 - 1 > 0

theorem E2Helpers.sqrt_x11_sub_one_gt_one (X : ℝ) (hX : 2 < X) (x : ℕ+) (hx : ↑↑x > X ^ (2 / 11)) : √(↑↑x ^ 11 - 1) > 1

theorem E2Helpers.x11_sub_X_gt_X_mul_X_sub_one (X : ℝ) (hX : 2 < X) (x : ℕ+) (hx : ↑↑x > X ^ (2 / 11)) : ↑↑x ^ 11 - X > X * (X - 1)

theorem E2Helpers.sqrt_x11_sub_X_gt (X : ℝ) (hX : 2 < X) (x : ℕ+) (hx : ↑↑x > X ^ (2 / 11)) : √(↑↑x ^ 11 - X) > √(X * (X - 1))

theorem E2Helpers.sq_sub_two_lt_mul (X : ℝ) (hX : 2 < X) : (X - 2) ^ 2 < X * (X - 1)

theorem E2Helpers.one_plus_sqrt_gt_X_sub_one (X : ℝ) (hX : 2 < X) : 1 + √(X * (X - 1)) > X - 1

theorem E2Helpers.denom_gt_X_sub_one (X : ℝ) (hX : 2 < X) (x : ℕ+) (hx : ↑↑x > X ^ (2 / 11)) : √(↑↑x ^ 11 - 1) + √(↑↑x ^ 11 - X) > X - 1

theorem E2Helpers.interval_length_lt_one (X : ℝ) (hX : 2 < X) (x : ℕ+) (hx : ↑↑x > X ^ (2 / 11)) : √(↑↑x ^ 11 - 1) - √(↑↑x ^ 11 - X) < 1

theorem E2Helpers.pair_ncard_le_two (n : ℕ) : {↑n, -↑n}.ncard ≤ 2

theorem E2Helpers.subset_natAbs_eq_ncard_le_two (n : ℕ) (T : Set ℤ) (_hfin : T.Finite) (hT : ∀ y ∈ T, y.natAbs = n) : T.ncard ≤ 2

theorem E2Helpers.ncard_le_two_of_natAbs_image_le_one (S : Set ℤ) (hfin : S.Finite) (himg : (Int.natAbs '' S).ncard ≤ 1) : S.ncard ≤ 2

theorem E2Helpers.natAbs_cast_sq_eq (y : ℤ) : ↑↑y.natAbs ^ 2 = ↑(y ^ 2)

theorem E2Helpers.natAbs_sq_le_cast_real (x : ℕ+) (y : ℤ) (hy_sq : y ^ 2 ≤ ↑↑x ^ 11 - 1) : ↑↑y.natAbs ^ 2 ≤ ↑↑x ^ 11 - 1

theorem E2Helpers.upper_bound_from_sq_le (x : ℕ+) (y : ℤ) (X : ℝ) (hX : 2 < X) (hx : ↑↑x > X ^ (2 / 11)) (hy_sq : y ^ 2 ≤ ↑↑x ^ 11 - 1) : ↑↑y.natAbs ≤ √(↑↑x ^ 11 - 1)

theorem E2Helpers.natAbs_cast_sq_eq' (y : ℤ) : ↑↑y.natAbs ^ 2 = ↑y ^ 2

theorem E2Helpers.rearrange_diff_le (x : ℕ+) (y : ℤ) (X : ℝ) (hy_diff : ↑(↑↑x ^ 11 - y ^ 2) ≤ X) : ↑↑x ^ 11 - X ≤ ↑↑y.natAbs ^ 2

theorem E2Helpers.lower_bound_from_diff_le (x : ℕ+) (y : ℤ) (X : ℝ) (_hX : 2 < X) (_hx : ↑↑x > X ^ (2 / 11)) (hy_diff : ↑(↑↑x ^ 11 - y ^ 2) ≤ X) : √(↑↑x ^ 11 - X) ≤ ↑↑y.natAbs

theorem E2Helpers.natAbs_image_subset_nonneg_interval (X : ℝ) (hX : 2 < X) (x : ℕ+) (hx : ↑↑x > X ^ (2 / 11)) : Nat.cast '' Int.natAbs '' {y : ℤ | y ^ 2 ≤ ↑↑x ^ 11 - 1 ∧ ↑(↑↑x ^ 11 - y ^ 2) ≤ X} ⊆ {n : ℤ | 0 ≤ n ∧ √(↑↑x ^ 11 - X) ≤ ↑n ∧ ↑n ≤ √(↑↑x ^ 11 - 1)}

theorem E2Helpers.E2_caseA_abs_image_ncard (X : ℝ) (hX : 2 < X) (x : ℕ+) (hx : ↑↑x > X ^ (2 / 11)) : (Int.natAbs '' {y : ℤ | y ^ 2 ≤ ↑↑x ^ 11 - 1 ∧ ↑(↑↑x ^ 11 - y ^ 2) ≤ X}).ncard ≤ 1

theorem E2Helpers.E2_caseA_ncard (X : ℝ) (hX : 2 < X) (x : ℕ+) (hx : ↑↑x > X ^ (2 / 11)) : {y : ℤ | y ^ 2 ≤ ↑↑x ^ 11 - 1 ∧ ↑(↑↑x ^ 11 - y ^ 2) ≤ X}.ncard ≤ 2

theorem E2Helpers.int_abs_le_ceil_sqrt (y : ℤ) (M : ℝ) (_hM : 0 ≤ M) (hy : ↑y ^ 2 ≤ M) : |y| ≤ ⌈√M⌉

theorem E2Helpers.int_mem_Icc_ceil_sqrt_of_sq_le (y : ℤ) (M : ℝ) (_hM : 0 ≤ M) (hy : ↑y ^ 2 ≤ M) : y ∈ Set.Icc (-⌈√M⌉) ⌈√M⌉

theorem E2Helpers.y_sq_le_x11_add_X_from_set (X : ℝ) (x : ℕ+) (y : ℤ) (h : ↑(y ^ 2 - ↑↑x ^ 11) ≤ X) : ↑y ^ 2 ≤ ↑↑x ^ 11 + X

theorem E2Helpers.E2_caseB_subset_Icc (X : ℝ) (hX : 2 < X) (x : ℕ+) (_hx : ↑↑x > X ^ (2 / 11)) : {y : ℤ | ↑↑x ^ 11 + 1 ≤ y ^ 2 ∧ ↑(y ^ 2 - ↑↑x ^ 11) ≤ X} ⊆ Set.Icc (-⌈√(↑↑x ^ 11 + X)⌉) ⌈√(↑↑x ^ 11 + X)⌉

theorem E2Helpers.E2_caseB_finite (X : ℝ) (hX : 2 < X) (x : ℕ+) (hx : ↑↑x > X ^ (2 / 11)) : {y : ℤ | ↑↑x ^ 11 + 1 ≤ y ^ 2 ∧ ↑(y ^ 2 - ↑↑x ^ 11) ≤ X}.Finite

theorem E2Helpers.sqrt_x11_add_one_gt_X (X : ℝ) (_hX_pos : 0 < X) (x_pow : ℝ) (hx_pow : x_pow > X ^ 2) : X < √(x_pow + 1)

theorem E2Helpers.sq_lt_xpow_add_X (X : ℝ) (_hX_pos : 0 < X) (x_pow : ℝ) (hx_pow : x_pow > X ^ 2) : X ^ 2 < x_pow + X

theorem E2Helpers.sqrt_x11_add_X_gt_X (X : ℝ) (hX_pos : 0 < X) (x_pow : ℝ) (hx_pow : x_pow > X ^ 2) : X < √(x_pow + X)

theorem E2Helpers.denom_gt_two_X (X : ℝ) (hX : 2 < X) (x : ℕ+) (hx : ↑↑x > X ^ (2 / 11)) : √(↑↑x ^ 11 + X) + √(↑↑x ^ 11 + 1) > 2 * X

theorem E2Helpers.X_sub_one_div_two_X_lt_one (X : ℝ) (hX : 2 < X) : (X - 1) / (2 * X) < 1

theorem E2Helpers.caseB_interval_length_lt_one (X : ℝ) (hX : 2 < X) (x : ℕ+) (hx : ↑↑x > X ^ (2 / 11)) : √(↑↑x ^ 11 + X) - √(↑↑x ^ 11 + 1) < 1

theorem E2Helpers.caseB_lower_bound_cast_ineq (x : ℕ+) (y : ℤ) (h : ↑↑x ^ 11 + 1 ≤ y ^ 2) : ↑↑x ^ 11 + 1 ≤ ↑y.natAbs ^ 2

theorem E2Helpers.caseB_lower_bound (x : ℕ+) (y : ℤ) (hy_lower : ↑↑x ^ 11 + 1 ≤ y ^ 2) : √(↑↑x ^ 11 + 1) ≤ ↑y.natAbs

theorem E2Helpers.caseB_upper_bound (X : ℝ) (x : ℕ+) (y : ℤ) (_hy_lower : ↑↑x ^ 11 + 1 ≤ y ^ 2) (hy_upper : ↑(y ^ 2 - ↑↑x ^ 11) ≤ X) : ↑y.natAbs ≤ √(↑↑x ^ 11 + X)

theorem E2Helpers.caseB_natAbs_bounds (X : ℝ) (x : ℕ+) (y : ℤ) (hy_lower : ↑↑x ^ 11 + 1 ≤ y ^ 2) (hy_upper : ↑(y ^ 2 - ↑↑x ^ 11) ≤ X) : √(↑↑x ^ 11 + 1) ≤ ↑y.natAbs ∧ ↑y.natAbs ≤ √(↑↑x ^ 11 + X)

theorem E2Helpers.caseB_natAbs_image_subset (X : ℝ) (_hX : 2 < X) (x : ℕ+) (_hx : ↑↑x > X ^ (2 / 11)) : Int.natAbs '' {y : ℤ | ↑↑x ^ 11 + 1 ≤ y ^ 2 ∧ ↑(y ^ 2 - ↑↑x ^ 11) ≤ X} ⊆ {n : ℕ | √(↑↑x ^ 11 + 1) ≤ ↑n ∧ ↑n ≤ √(↑↑x ^ 11 + X)}

theorem E2Helpers.nat_image_subset_int_set (a b : ℝ) : Nat.cast '' {n : ℕ | a ≤ ↑n ∧ ↑n ≤ b} ⊆ {n : ℤ | 0 ≤ n ∧ a ≤ ↑n ∧ ↑n ≤ b}

theorem E2Helpers.ncard_nat_in_short_interval (a b : ℝ) (hab : a ≤ b) (hlen : b - a < 1) (ha : 0 ≤ a) : {n : ℕ | a ≤ ↑n ∧ ↑n ≤ b}.ncard ≤ 1

theorem E2Helpers.caseB_nat_interval_subset_Iic (X : ℝ) (x : ℕ+) : {n : ℕ | √(↑↑x ^ 11 + 1) ≤ ↑n ∧ ↑n ≤ √(↑↑x ^ 11 + X)} ⊆ {n : ℕ | n ≤ ⌈√(↑↑x ^ 11 + X)⌉₊}

theorem E2Helpers.caseB_nat_interval_finite (X : ℝ) (_hX : 2 < X) (x : ℕ+) (_hx : ↑↑x > X ^ (2 / 11)) : {n : ℕ | √(↑↑x ^ 11 + 1) ≤ ↑n ∧ ↑n ≤ √(↑↑x ^ 11 + X)}.Finite

theorem E2Helpers.E2_caseB_abs_image_ncard (X : ℝ) (hX : 2 < X) (x : ℕ+) (hx : ↑↑x > X ^ (2 / 11)) : (Int.natAbs '' {y : ℤ | ↑↑x ^ 11 + 1 ≤ y ^ 2 ∧ ↑(y ^ 2 - ↑↑x ^ 11) ≤ X}).ncard ≤ 1

theorem E2Helpers.E2_caseB_finite_and_abs_image (X : ℝ) (hX : 2 < X) (x : ℕ+) (hx : ↑↑x > X ^ (2 / 11)) : have S := {y : ℤ | ↑↑x ^ 11 + 1 ≤ y ^ 2 ∧ ↑(y ^ 2 - ↑↑x ^ 11) ≤ X}; S.Finite ∧ (Int.natAbs '' S).ncard ≤ 1

theorem E2Helpers.E2_caseB_ncard (X : ℝ) (hX : 2 < X) (x : ℕ+) (hx : ↑↑x > X ^ (2 / 11)) : {y : ℤ | ↑↑x ^ 11 + 1 ≤ y ^ 2 ∧ ↑(y ^ 2 - ↑↑x ^ 11) ≤ X}.ncard ≤ 2

theorem E2Helpers.E2_cases_finite (X : ℝ) (hX : 2 < X) (x : ℕ+) (hx : ↑↑x > X ^ (2 / 11)) : ({y : ℤ | y ^ 2 ≤ ↑↑x ^ 11 - 1 ∧ ↑(↑↑x ^ 11 - y ^ 2) ≤ X} ∪ {y : ℤ | ↑↑x ^ 11 + 1 ≤ y ^ 2 ∧ ↑(y ^ 2 - ↑↑x ^ 11) ≤ X}).Finite

theorem E2Helpers.E2_fiber_bound (X : ℝ) (hX : 2 < X) (x : ℕ+) (hx : ↑↑x > X ^ (2 / 11)) : {y : ℤ | (x, y) ∈ E2Set X}.ncard ≤ 4

theorem E2Helpers.E2XBoundHelpers.X_lt_X_sq (X : ℝ) (hX : 1 < X) : X < X ^ 2

theorem E2Helpers.E2XBoundHelpers.x11_pow_gt_X (x : ℕ+) (X : ℝ) (hX : 1 < X) (hx_lower : ↑↑x > X ^ (2 / 11)) : ↑↑x ^ 11 > X

theorem E2Helpers.E2XBoundHelpers.y_ne_zero_of_E2 (x : ℕ+) (y : ℤ) (X : ℝ) (hX : 1 < X) (hx_lower : ↑↑x > X ^ (2 / 11)) (habs_pos : 1 ≤ |↑↑x ^ 11 - y ^ 2|) (habs_le : |↑↑↑x ^ 11 - ↑y ^ 2| ≤ X) : y ≠ 0

theorem E2Helpers.E2XBoundHelpers.radical_abc_bound (x Y B : ℕ) (hx : 0 < x) (hY : 0 < Y) (hB : 0 < B) : ↑(Y ^ 2 * B * x ^ 11).radical ≤ ↑Y * ↑B * ↑x

theorem E2Helpers.E2XBoundHelpers.radical_abc_bound'_nat (x Y B : ℕ) (hx : 0 < x) (hY : 0 < Y) (hB : 0 < B) : (x ^ 11 * B * Y ^ 2).radical ≤ x * B * Y

theorem E2Helpers.E2XBoundHelpers.radical_abc_bound' (x Y B : ℕ) (hx : 0 < x) (hY : 0 < Y) (hB : 0 < B) : ↑(x ^ 11 * B * Y ^ 2).radical ≤ ↑x * ↑B * ↑Y

theorem E2Helpers.E2XBoundHelpers.abc_triple_sum_case1 (x : ℕ+) (y : ℤ) (hge : ↑↑x ^ 11 ≥ y ^ 2) : y.natAbs ^ 2 + (↑↑x ^ 11 - y ^ 2).natAbs = ↑x ^ 11

theorem E2Helpers.E2XBoundHelpers.natAbs_pos_of_ne_zero (y : ℤ) (hy : y ≠ 0) : 0 < y.natAbs

theorem E2Helpers.E2XBoundHelpers.B_nat_pos (x : ℕ+) (y : ℤ) (habs_pos : 1 ≤ |↑↑x ^ 11 - y ^ 2|) : 0 < (↑↑x ^ 11 - y ^ 2).natAbs

theorem E2Helpers.E2XBoundHelpers.natAbs_cast_le_X (x : ℕ+) (y : ℤ) (X : ℝ) (habs_le : |↑↑↑x ^ 11 - ↑y ^ 2| ≤ X) (_hge : ↑↑x ^ 11 ≥ y ^ 2) : ↑(↑↑x ^ 11 - y ^ 2).natAbs ≤ X

theorem E2Helpers.E2XBoundHelpers.gcd_le_natAbs (x : ℕ+) (y : ℤ) (hpos : 0 < (↑↑x ^ 11 - y ^ 2).natAbs) : (y.natAbs ^ 2).gcd (↑↑x ^ 11 - y ^ 2).natAbs ≤ (↑↑x ^ 11 - y ^ 2).natAbs

theorem E2Helpers.E2XBoundHelpers.gcd_le_X_case1 (x : ℕ+) (y : ℤ) (X : ℝ) (habs_pos : 1 ≤ |↑↑x ^ 11 - y ^ 2|) (habs_le : |↑↑↑x ^ 11 - ↑y ^ 2| ≤ X) (hge : ↑↑x ^ 11 ≥ y ^ 2) : ↑((y.natAbs ^ 2).gcd (↑↑x ^ 11 - y ^ 2).natAbs) ≤ X

theorem E2Helpers.E2XBoundHelpers.rad_bound_le_case1 (x : ℕ+) (y : ℤ) (X : ℝ) (habs_le : |↑↑↑x ^ 11 - ↑y ^ 2| ≤ X) (_hge : ↑↑x ^ 11 ≥ y ^ 2) : ↑y.natAbs * ↑(↑↑x ^ 11 - y ^ 2).natAbs * ↑↑x ≤ ↑↑x * ↑y.natAbs * X

theorem E2Helpers.E2XBoundHelpers.chain_bound_case1 (K : ℝ) (hK : 0 < K) (ε : ℝ) (hε : 0 < ε) (x : ℕ+) (y : ℤ) (X : ℝ) (hX : 1 < X) (h_abc : ↑↑x ^ 11 ≤ X * K * (↑y.natAbs * ↑(↑↑x ^ 11 - y ^ 2).natAbs * ↑↑x) ^ (1 + ε)) (h_rad_le : ↑y.natAbs * ↑(↑↑x ^ 11 - y ^ 2).natAbs * ↑↑x ≤ ↑↑x * ↑y.natAbs * X) : ↑↑x ^ 11 ≤ K * X * (↑↑x * ↑y.natAbs * X) ^ (1 + ε)

theorem E2Helpers.E2XBoundHelpers.abc_case_x11_ge_y2 (K : ℝ) (hK : 0 < K) (ε : ℝ) (hε : 0 < ε) (habc_ineq : ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → a.Coprime b → a + b = c → ↑c ≤ K * ↑(a * b * c).radical ^ (1 + ε)) (x : ℕ+) (y : ℤ) (X : ℝ) (hX : 1 < X) (hy_ne : y ≠ 0) (habs_pos : 1 ≤ |↑↑x ^ 11 - y ^ 2|) (habs_le : |↑↑↑x ^ 11 - ↑y ^ 2| ≤ X) (hge : ↑↑x ^ 11 ≥ y ^ 2) : ↑↑x ^ 11 ≤ K * X * (↑↑x * ↑y.natAbs * X) ^ (1 + ε)

theorem E2Helpers.E2XBoundHelpers.x11_le_natAbs_sq (x : ℕ+) (y : ℤ) (hlt : ↑↑x ^ 11 < y ^ 2) : ↑x ^ 11 ≤ y.natAbs ^ 2

theorem E2Helpers.E2XBoundHelpers.B_pos_of_x11_lt_y2 (x : ℕ+) (y : ℤ) (hlt : ↑↑x ^ 11 < y ^ 2) : 0 < y.natAbs ^ 2 - ↑x ^ 11

theorem E2Helpers.E2XBoundHelpers.abc_sum_eq_of_x11_lt_y2 (x : ℕ+) (y : ℤ) (hlt : ↑↑x ^ 11 < y ^ 2) : ↑x ^ 11 + (y.natAbs ^ 2 - ↑x ^ 11) = y.natAbs ^ 2

theorem E2Helpers.E2XBoundHelpers.gcd_le_B (x : ℕ+) (y : ℤ) (hlt : ↑↑x ^ 11 < y ^ 2) : ↑((↑x ^ 11).gcd (y.natAbs ^ 2 - ↑x ^ 11)) ≤ ↑(y.natAbs ^ 2 - ↑x ^ 11)

theorem E2Helpers.E2XBoundHelpers.abs_int_sub_eq_reverse (x : ℕ+) (y : ℤ) (hlt : ↑↑x ^ 11 < y ^ 2) : |↑↑x ^ 11 - y ^ 2| = y ^ 2 - ↑↑x ^ 11

theorem E2Helpers.E2XBoundHelpers.abs_eq_reverse_sub_real (x : ℕ+) (y : ℤ) (hlt : ↑↑x ^ 11 < y ^ 2) : |↑↑↑x ^ 11 - ↑y ^ 2| = ↑(y ^ 2 - ↑↑x ^ 11)

theorem E2Helpers.E2XBoundHelpers.B_cast_le_X (x : ℕ+) (y : ℤ) (X : ℝ) (habs_le : |↑↑↑x ^ 11 - ↑y ^ 2| ≤ X) (hlt : ↑↑x ^ 11 < y ^ 2) : ↑(y.natAbs ^ 2 - ↑x ^ 11) ≤ X

theorem E2Helpers.E2XBoundHelpers.rad_bound_le (x : ℕ+) (y : ℤ) (X : ℝ) (habs_le : |↑↑↑x ^ 11 - ↑y ^ 2| ≤ X) (hlt : ↑↑x ^ 11 < y ^ 2) : ↑↑x * ↑(y.natAbs ^ 2 - ↑x ^ 11) * ↑y.natAbs ≤ ↑↑x * ↑y.natAbs * X

theorem E2Helpers.E2XBoundHelpers.x11_le_y2_real (x : ℕ+) (y : ℤ) (hlt : ↑↑x ^ 11 < y ^ 2) : ↑↑x ^ 11 ≤ ↑(y.natAbs ^ 2)

theorem E2Helpers.E2XBoundHelpers.rad_bound_nonneg (x : ℕ+) (y : ℤ) (X : ℝ) (hX : 1 < X) : 0 ≤ ↑↑x * ↑y.natAbs * X

theorem E2Helpers.E2XBoundHelpers.abc_case_x11_lt_y2 (K : ℝ) (hK : 0 < K) (ε : ℝ) (hε : 0 < ε) (habc_ineq : ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → a.Coprime b → a + b = c → ↑c ≤ K * ↑(a * b * c).radical ^ (1 + ε)) (x : ℕ+) (y : ℤ) (X : ℝ) (hX : 1 < X) (hy_ne : y ≠ 0) (_habs_pos : 1 ≤ |↑↑x ^ 11 - y ^ 2|) (habs_le : |↑↑↑x ^ 11 - ↑y ^ 2| ≤ X) (hlt : ↑↑x ^ 11 < y ^ 2) : ↑↑x ^ 11 ≤ K * X * (↑↑x * ↑y.natAbs * X) ^ (1 + ε)

theorem E2Helpers.E2XBoundHelpers.abc_gives_x11_bound (K : ℝ) (hK : 0 < K) (ε : ℝ) (hε : 0 < ε) (habc_ineq : ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → a.Coprime b → a + b = c → ↑c ≤ K * ↑(a * b * c).radical ^ (1 + ε)) (x : ℕ+) (y : ℤ) (X : ℝ) (hX : 1 < X) (hx_lower : ↑↑x > X ^ (2 / 11)) (habs_pos : 1 ≤ |↑↑x ^ 11 - y ^ 2|) (habs_le : |↑↑↑x ^ 11 - ↑y ^ 2| ≤ X) : ↑↑x ^ 11 ≤ K * X * (↑↑x * ↑y.natAbs * X) ^ (1 + ε)

theorem E2Helpers.E2XBoundHelpers.y_sq_le_x11_add_X (x : ℕ+) (y : ℤ) (X : ℝ) (habs_le : |↑↑↑x ^ 11 - ↑y ^ 2| ≤ X) : ↑y ^ 2 ≤ ↑↑x ^ 11 + X

theorem E2Helpers.E2XBoundHelpers.natAbs_y_sq_le_two_mul_x11 (x : ℕ+) (y : ℤ) (X : ℝ) (hX : 1 < X) (hx_lower : ↑↑x > X ^ (2 / 11)) (habs_le : |↑↑↑x ^ 11 - ↑y ^ 2| ≤ X) : ↑y.natAbs ^ 2 ≤ 2 * ↑↑x ^ 11

theorem E2Helpers.E2XBoundHelpers.sqrt_two_mul_x11_eq (x : ℕ+) : √(2 * ↑↑x ^ 11) = √2 * ↑↑x ^ (11 / 2)

theorem E2Helpers.E2XBoundHelpers.natAbs_le_sqrt_of_sq_le (y : ℤ) (b : ℝ) (_hb : 0 ≤ b) (h : ↑y.natAbs ^ 2 ≤ b) : ↑y.natAbs ≤ √b

theorem E2Helpers.E2XBoundHelpers.Y_bound_from_E2 (x : ℕ+) (y : ℤ) (X : ℝ) (hX : 1 < X) (hx_lower : ↑↑x > X ^ (2 / 11)) (_habs_pos : 1 ≤ |↑↑x ^ 11 - y ^ 2|) (habs_le : |↑↑↑x ^ 11 - ↑y ^ 2| ≤ X) : ↑y.natAbs ≤ √2 * ↑↑x ^ (11 / 2)

theorem E2Helpers.E2XBoundHelpers.combine_bounds_to_x_bound (K : ℝ) (hK : 0 < K) (ε : ℝ) (hε : 0 < ε) (hε' : ε < 9 / 13) (x : ℕ+) (X : ℝ) (hX : 1 < X) (Y : ℝ) (hY : 0 ≤ Y) (h_x11 : ↑↑x ^ 11 ≤ K * X * (↑↑x * Y * X) ^ (1 + ε)) (h_Y : Y ≤ √2 * ↑↑x ^ (11 / 2)) : ↑↑x ≤ (K * √2 ^ (1 + ε)) ^ (2 / (9 - 13 * ε)) * X ^ ((4 + 2 * ε) / (9 - 13 * ε))

theorem E2Helpers.E2XBoundHelpers.cx_pos (K : ℝ) (hK : 0 < K) (ε : ℝ) (_hε : 0 < ε) (_hε' : ε < 9 / 13) : 0 < (K * √2 ^ (1 + ε)) ^ (2 / (9 - 13 * ε))

theorem E2Helpers.E2XBoundHelpers.E2_x_bound_from_abc (habc : ABC) (ε : ℝ) (hε : 0 < ε) (hε' : ε < 9 / 13) : ∃ (Cx : ℝ), 0 < Cx ∧ ∃ (X₁ : ℝ), 0 < X₁ ∧ ∀ (X : ℝ), X₁ < X → ∀ p ∈ E2Set X, ↑↑p.1 ≤ Cx * X ^ ((4 + 2 * ε) / (9 - 13 * ε))

theorem E2Helpers.E2_x_bound_from_abc (habc : ABC) (ε : ℝ) (hε : 0 < ε) (hε' : ε < 9 / 13) : ∃ (Cx : ℝ), 0 < Cx ∧ ∃ (X₁ : ℝ), 0 < X₁ ∧ ∀ (X : ℝ), X₁ < X → ∀ p ∈ E2Set X, ↑↑p.1 ≤ Cx * X ^ ((4 + 2 * ε) / (9 - 13 * ε))

theorem E2Helpers.exponent_comparison_strict (η ε : ℝ) (hη : 0 < η) (hε1 : 0 < ε) (hε2 : ε ≤ η / 4) (hε3 : ε ≤ 1 / 10) : (4 + 2 * ε) / (9 - 13 * ε) < 4 / 9 + η

theorem E2Helpers.E2NcardHelpers.pnat_bounded_finite (B : ℝ) (_hB : 0 < B) : {x : ℕ+ | ↑↑x ≤ B}.Finite

theorem E2Helpers.E2NcardHelpers.y_sq_le_real_of_E2_cond (x : ℕ+) (y : ℤ) (X : ℝ) (h2 : |↑↑↑x ^ 11 - ↑y ^ 2| ≤ X) : ↑y ^ 2 ≤ ↑↑x ^ 11 + X

theorem E2Helpers.E2NcardHelpers.pnatLe_ceil_of_le (x : ℕ+) (B : ℝ) (_hB : 0 < B) (hx : ↑↑x ≤ B) : ↑x ≤ ⌈B⌉₊

theorem E2Helpers.E2NcardHelpers.y_sq_le_ceil_pow_add (x : ℕ+) (y : ℤ) (X B : ℝ) (hB : 0 < B) (hx_le_B : ↑↑x ≤ B) (hy_sq : ↑y ^ 2 ≤ ↑↑x ^ 11 + X) : ↑y ^ 2 ≤ ↑⌈B⌉₊ ^ 11 + X

theorem E2Helpers.E2NcardHelpers.E2_set_subset_bounded_prod (X B : ℝ) (hX : 2 < X) (hB : 0 < B) (hxbound : ∀ p ∈ E2Set X, ↑↑p.1 ≤ B) : E2Set X ⊆ {x : ℕ+ | ↑↑x ≤ B} ×ˢ Set.Icc (-⌈√(↑⌈B⌉₊ ^ 11 + X)⌉) ⌈√(↑⌈B⌉₊ ^ 11 + X)⌉

theorem E2Helpers.E2NcardHelpers.E2_set_finite (X B : ℝ) (hX : 2 < X) (hB : 0 < B) (hxbound : ∀ p ∈ E2Set X, ↑↑p.1 ≤ B) : (E2Set X).Finite

theorem E2Helpers.E2NcardHelpers.E2_fst_gt_of_mem_image (X : ℝ) (hfin : (E2Set X).Finite) (x : ℕ+) (hx : x ∈ Finset.image Prod.fst hfin.toFinset) : ↑↑x > X ^ (2 / 11)

theorem E2Helpers.E2NcardHelpers.E2_fiber_finite (X : ℝ) (hfin : (E2Set X).Finite) (x : ℕ+) : {y : ℤ | (x, y) ∈ E2Set X}.Finite

theorem E2Helpers.E2NcardHelpers.E2_filter_eq_image (X : ℝ) (hfin : (E2Set X).Finite) (x : ℕ+) (hfib : {y : ℤ | (x, y) ∈ E2Set X}.Finite) : {a ∈ hfin.toFinset | a.1 = x} = Finset.image (fun (y : ℤ) => (x, y)) hfib.toFinset

theorem E2Helpers.E2NcardHelpers.E2_filter_card_le_fiber_ncard (X : ℝ) (hfin : (E2Set X).Finite) (x : ℕ+) : {a ∈ hfin.toFinset | a.1 = x}.card ≤ {y : ℤ | (x, y) ∈ E2Set X}.ncard

theorem E2Helpers.E2NcardHelpers.E2_finset_fiber_card_le (X : ℝ) (_hX : 2 < X) (hfin : (E2Set X).Finite) (hfiber : ∀ (x : ℕ+), ↑↑x > X ^ (2 / 11) → {y : ℤ | (x, y) ∈ E2Set X}.ncard ≤ 4) (x : ℕ+) (hx : x ∈ Finset.image Prod.fst hfin.toFinset) : {a ∈ hfin.toFinset | a.1 = x}.card ≤ 4

theorem E2Helpers.E2NcardHelpers.pnat_image_val_card_eq (s : Finset ℕ+) : (Finset.image (fun (x : ℕ+) => ↑x) s).card = s.card

theorem E2Helpers.E2NcardHelpers.pnat_nat_image_subset_Icc (X B : ℝ) (_hB : 0 < B) (hfin : (E2Set X).Finite) (hxbound : ∀ p ∈ E2Set X, ↑↑p.1 ≤ B) : Finset.image (fun (x : ℕ+) => ↑x) (Finset.image Prod.fst hfin.toFinset) ⊆ Finset.Icc 1 ⌊B⌋₊

theorem E2Helpers.E2NcardHelpers.Icc_card_le_floor_add_one (B : ℝ) : (Finset.Icc 1 ⌊B⌋₊).card ≤ ⌊B⌋₊ + 1

theorem E2Helpers.E2NcardHelpers.E2_fst_image_card_le (X B : ℝ) (hB : 0 < B) (hfin : (E2Set X).Finite) (hxbound : ∀ p ∈ E2Set X, ↑↑p.1 ≤ B) : (Finset.image Prod.fst hfin.toFinset).card ≤ ⌊B⌋₊ + 1

theorem E2Helpers.E2NcardHelpers.E2_ncard_le_nat (X B : ℝ) (hX : 2 < X) (hB : 0 < B) (hfin : (E2Set X).Finite) (hfiber : ∀ (x : ℕ+), ↑↑x > X ^ (2 / 11) → {y : ℤ | (x, y) ∈ E2Set X}.ncard ≤ 4) (hxbound : ∀ p ∈ E2Set X, ↑↑p.1 ≤ B) : E2 X ≤ 4 * (⌊B⌋₊ + 1)

theorem E2Helpers.E2NcardHelpers.E2_ncard_le_via_fibers (X B : ℝ) (hX : 2 < X) (hB : 0 < B) (hfiber : ∀ (x : ℕ+), ↑↑x > X ^ (2 / 11) → {y : ℤ | (x, y) ∈ E2Set X}.ncard ≤ 4) (hxbound : ∀ p ∈ E2Set X, ↑↑p.1 ≤ B) : ↑(E2 X) ≤ 4 * (B + 1)

theorem E2Helpers.E2_ncard_le_via_fibers (X B : ℝ) (hX : 2 < X) (hB : 0 < B) (hfiber : ∀ (x : ℕ+), ↑↑x > X ^ (2 / 11) → {y : ℤ | (x, y) ∈ E2Set X}.ncard ≤ 4) (hxbound : ∀ p ∈ E2Set X, ↑↑p.1 ≤ B) : ↑(E2 X) ≤ 4 * (B + 1)

theorem abc_bound_E2_core (habc : ABC) (η : ℝ) (hη : 0 < η) : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → ↑(E2 X) ≤ C * X ^ (4 / 9 + η)

theorem abc_bound_E2 (habc : ABC) (η : ℝ) (hη : 0 < η) : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → ↑(E2 X) ≤ C * X ^ (4 / 9 + η)

theorem E4Helpers.u_fiber_bound : ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → ∀ (x : ℕ+), {u : ℤ | (x, u) ∈ E4Set X}.ncard ≤ 10

theorem E4Helpers.E4_fiber_ncard_le (X : ℝ) (hX : 4 < X) (x : ℕ+) : {u : ℤ | (x, u) ∈ E4Set X}.ncard ≤ 4

theorem E4Helpers.pnat_bounded_finite (B : ℝ) (_hB : 0 < B) : {x : ℕ+ | ↑↑x ≤ B}.Finite

theorem E4Helpers.pow22_le_of_le (x : ℕ+) (B : ℝ) (hxB : ↑↑x ≤ B) : ↑↑x ^ 22 ≤ B ^ 22

theorem E4Helpers.u_sq_le_of_E4 (X B : ℝ) (hx : ∀ p ∈ E4Set X, ↑↑p.1 ≤ B) (p : ℕ+ × ℤ) (hp : p ∈ E4Set X) : ↑p.2 ^ 2 ≤ 5 * B ^ 22 + 4 * X

theorem E4Helpers.bound_nonneg_of_E4 (X B : ℝ) (hx : ∀ p ∈ E4Set X, ↑↑p.1 ≤ B) (p : ℕ+ × ℤ) (hp : p ∈ E4Set X) : 0 ≤ 5 * B ^ 22 + 4 * X

theorem E4Helpers.u_in_Icc_of_E4 (X B : ℝ) (hx : ∀ p ∈ E4Set X, ↑↑p.1 ≤ B) (p : ℕ+ × ℤ) (hp : p ∈ E4Set X) : p.2 ∈ Set.Icc (-⌈√(5 * B ^ 22 + 4 * X)⌉) ⌈√(5 * B ^ 22 + 4 * X)⌉

theorem E4Helpers.E4_set_subset_prod (X B : ℝ) (hx : ∀ p ∈ E4Set X, ↑↑p.1 ≤ B) : E4Set X ⊆ {x : ℕ+ | ↑↑x ≤ B} ×ˢ Set.Icc (-⌈√(5 * B ^ 22 + 4 * X)⌉) ⌈√(5 * B ^ 22 + 4 * X)⌉

theorem E4Helpers.E4_set_finite_of_bounded (X B : ℝ) (hB : 0 < B) (_hX : 4 < X) (hx : ∀ p ∈ E4Set X, ↑↑p.1 ≤ B) : (E4Set X).Finite

theorem E4Helpers.E4_fiber_finite (X : ℝ) (hfin : (E4Set X).Finite) (x : ℕ+) : {u : ℤ | (x, u) ∈ E4Set X}.Finite

theorem E4Helpers.E4_filter_image_subset_fiber (X : ℝ) (hfin : (E4Set X).Finite) (x : ℕ+) : Finset.image Prod.snd ({a ∈ hfin.toFinset | a.1 = x}) ⊆ ⋯.toFinset

theorem E4Helpers.E4_snd_injOn_filter (X : ℝ) (hfin : (E4Set X).Finite) (x : ℕ+) : Set.InjOn Prod.snd ↑({a ∈ hfin.toFinset | a.1 = x})

theorem E4Helpers.E4_filter_card_le_fiber_ncard (X : ℝ) (hfin : (E4Set X).Finite) (x : ℕ+) : {a ∈ hfin.toFinset | a.1 = x}.card ≤ {u : ℤ | (x, u) ∈ E4Set X}.ncard

theorem E4Helpers.E4_finset_fiber_card_le (X : ℝ) (hX : 4 < X) (hfin : (E4Set X).Finite) (x : ℕ+) : {a ∈ hfin.toFinset | a.1 = x}.card ≤ 4

theorem E4Helpers.pnat_image_val_card_eq (s : Finset ℕ+) : (Finset.image (fun (x : ℕ+) => ↑x) s).card = s.card

theorem E4Helpers.pnat_finset_card_le_floor_add_one (s : Finset ℕ+) (B : ℝ) (hs : ∀ x ∈ s, ↑↑x ≤ B) : s.card ≤ ⌊B⌋₊ + 1

theorem E4Helpers.E4_fst_image_card_le (X B : ℝ) (_hB : 0 < B) (hfin : (E4Set X).Finite) (hx : ∀ p ∈ E4Set X, ↑↑p.1 ≤ B) : (Finset.image Prod.fst hfin.toFinset).card ≤ ⌊B⌋₊ + 1

theorem E4Helpers.E4_ncard_le_mul_floor (X B : ℝ) (hB : 0 < B) (hX : 4 < X) (hfin : (E4Set X).Finite) (hx : ∀ p ∈ E4Set X, ↑↑p.1 ≤ B) : E4 X ≤ 4 * (⌊B⌋₊ + 1)

theorem E4Helpers.E4_real_bound_from_nat (X B : ℝ) (hB : 0 < B) (h : E4 X ≤ 4 * (⌊B⌋₊ + 1)) : ↑(E4 X) ≤ 4 * (B + 1)

theorem E4Helpers.absorb_additive_const (η K₄ : ℝ) (hη : 0 < η) (_hK₄ : 0 < K₄) : ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → 4 * (K₄ * X ^ (1 / 5 + η) + 1) ≤ 4 * (K₄ + 1) * X ^ (1 / 5 + η)

theorem E4Helpers.E4_bound_from_x_and_fiber (η : ℝ) (hη : 0 < η) (K₄ : ℝ) (hK₄ : 0 < K₄) (X₀_x : ℝ) (hX₀_x : 0 < X₀_x) (hx_bound : ∀ (X : ℝ), X₀_x < X → ∀ p ∈ E4Set X, ↑↑p.1 ≤ K₄ * X ^ (1 / 5 + η)) (X₀_u : ℝ) (_hX₀_u : 0 < X₀_u) (_hu_bound : ∀ (X : ℝ), X₀_u < X → ∀ (x : ℕ+), {u : ℤ | (x, u) ∈ E4Set X}.ncard ≤ 10) : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → ↑(E4 X) ≤ C * X ^ (1 / 5 + η)

theorem abc_bound_E4_core (habc : ABC) (η : ℝ) (hη : 0 < η) : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → ↑(E4 X) ≤ C * X ^ (1 / 5 + η)

theorem abc_bound_E4 (habc : ABC) (η : ℝ) (hη : 0 < η) : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → ↑(E4 X) ≤ C * X ^ (1 / 5 + η)

theorem absorb_const_rpow {C a b : ℝ} (_hC : 0 < C) (hab : a < b) : ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → C * X ^ a ≤ X ^ b

theorem half_log_le_13_22 : ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → X ^ (1 / 2) * Real.log X ≤ X ^ (13 / 22)

theorem combine_five_bounds {S t₁ t₂ t₃ t₄ t₅ B C₁ : ℝ} (hS : S ≤ C₁ * (t₁ + t₂ + t₃ + t₄ + t₅)) (h1 : t₁ ≤ B) (h2 : t₂ ≤ B) (h3 : t₃ ≤ B) (h4 : t₄ ≤ B) (h5 : t₅ ≤ B) (hC₁ : 0 < C₁) : S ≤ 5 * C₁ * B

theorem main_theorem (R : RamanujanTau) (habc : ABC) (h54 : Proposition54 R) : ∃ (C : ℝ), 0 < C ∧ ∃ (X₀ : ℝ), 0 < X₀ ∧ ∀ (X : ℝ), X₀ < X → ↑(S R X) ≤ C * X ^ (13 / 22)