Subsum condition for the general case

def GeneralCase.redEmb1 {n : ℕ} : Fin 4 ↪ Fin (n + 6)

The embedding for the first subsum block reduction.

Equations

• GeneralCase.redEmb1 = { toFun := fun (i : Fin 4) => Fin.natAdd n (Fin.natAdd 2 i), inj' := ⋯ }

def GeneralCase.tailK (n : ℕ) (F : Finset ℕ) : ℕ

The sum of tup n F h's first n + 2 elements, not depending on h.

Equations

• GeneralCase.tailK n F = (GeneralCase.VW n F).v + (GeneralCase.VW n F).w + ∑ i ∈ Finset.range n, primeChain (100 * GeneralCase.Y F ^ 6) i

theorem GeneralCase.sum_redEmb1_compl {n : ℕ} {F : Finset ℕ} {h : ℕ} : ∑ i ∈ (Finset.map redEmb1 Finset.univ)ᶜ, (tup n F h i).natAbs = tailK n F

theorem GeneralCase.tailK_lower_bound {n : ℕ} {F : Finset ℕ} : 196 * Y F ^ 6 ≤ tailK n F

theorem GeneralCase.Y6_le_X {n : ℕ} {F : Finset ℕ} {h : ℕ} (hh : tailK n F < X F h) : 196 * Y F ^ 6 ≤ X F h

theorem GeneralCase.b₁_upper_bound {n : ℕ} {F : Finset ℕ} {h : ℕ} (hh : tailK n F < X F h) : ((↑(X F h) ^ 2 + 10 * ↑(Y F) ^ 3) ^ 2).natAbs ≤ 4 * X F h ^ 4

theorem GeneralCase.b₃_lower_bound {n : ℕ} {F : Finset ℕ} {h : ℕ} (hh : tailK n F < X F h) : 12 * Y F * X F h ^ 4 ≤ ((↑(X F h) - ↑(Y F)) ^ 5).natAbs

theorem GeneralCase.b₄_lower_bound {n : ℕ} {F : Finset ℕ} {h : ℕ} (hh : tailK n F < X F h) : 12 * Y F * X F h ^ 4 ≤ (-(↑(X F h) + ↑(Y F)) ^ 5).natAbs

theorem GeneralCase.X4_le_natAbs_b4 {n : ℕ} {F : Finset ℕ} {h : ℕ} (hh : tailK n F < X F h) {b₁ b₂ b₃ b₄ : SignType} (hl : b₄ < b₃) : X F h ^ 4 ≤ (↑b₁ * (↑(X F h) ^ 2 + 10 * ↑(Y F) ^ 3) ^ 2 + ↑b₂ * ((10 * ↑(Y F) - 1) * ↑(X F h) ^ 4) + ↑b₃ * (↑(X F h) - ↑(Y F)) ^ 5 + ↑b₄ * -(↑(X F h) + ↑(Y F)) ^ 5).natAbs

theorem GeneralCase.b₃_lower_bound_2 {F : Finset ℕ} {h : ℕ} : 5 * X F h ^ 4 ≤ (-2 * ↑(Y F) * (5 * ↑(X F h) ^ 4 + 10 * ↑(X F h) ^ 2 * ↑(Y F) ^ 2 + ↑(Y F) ^ 4)).natAbs

theorem GeneralCase.X4_le_natAbs_b3 {n : ℕ} {F : Finset ℕ} {h : ℕ} (hh : tailK n F < X F h) {b₁ b₂ b₃ : SignType} (hl : b₃ < b₂) : X F h ^ 4 ≤ (↑b₁ * (↑(X F h) ^ 2 + 10 * ↑(Y F) ^ 3) ^ 2 + ↑b₂ * ((10 * ↑(Y F) - 1) * ↑(X F h) ^ 4) + ↑b₃ * (-2 * ↑(Y F) * (5 * ↑(X F h) ^ 4 + 10 * ↑(X F h) ^ 2 * ↑(Y F) ^ 2 + ↑(Y F) ^ 4))).natAbs

theorem GeneralCase.X_le_natAbs_redEmb1 {n : ℕ} {F : Finset ℕ} {h : ℕ} (hh : tailK n F < X F h) {b₁ b₂ b₃ b₄ : SignType} (hb : b₁ ≠ b₂ ∨ b₂ ≠ b₃ ∨ b₃ ≠ b₄) : X F h ≤ (↑b₁ * (↑(X F h) ^ 2 + 10 * ↑(Y F) ^ 3) ^ 2 + ↑b₂ * ((10 * ↑(Y F) - 1) * ↑(X F h) ^ 4) + ↑b₃ * (↑(X F h) - ↑(Y F)) ^ 5 + ↑b₄ * -(↑(X F h) + ↑(Y F)) ^ 5).natAbs

theorem GeneralCase.eventually_X_gt {F : Finset ℕ} (K : Finset ℕ → ℕ) : ∀ᶠ (h : ℕ) in Filter.atTop, K F < X F h

theorem GeneralCase.isSubsumBlock_redEmb1 {n : ℕ} {F : Finset ℕ} : ∀ᶠ (h : ℕ) in Filter.atTop, IsSubsumBlock (tup n F h) (Finset.map redEmb1 Finset.univ)

theorem GeneralCase.tupReduce_tup {n : ℕ} {F : Finset ℕ} {h : ℕ} {c₁ : n + 2 = n + 6 - (Finset.map redEmb1 Finset.univ).card} : tupReduce (tup n F h) (Finset.map redEmb1 Finset.univ) c₁ = vwTup (VW n F)

theorem GeneralCase.strongSSC_tup {n : ℕ} {F : Finset ℕ} : ∀ᶠ (h : ℕ) in Filter.atTop, StrongSSC (tup n F h)

theorem GeneralCase.maxAbs_tup {n : ℕ} {F : Finset ℕ} : ∀ᶠ (h : ℕ) in Filter.atTop, maxAbs (tup n F h) = (X F h + Y F) ^ 5