Depths n + 5 leave a strict negative Golod--Shafarevich margin at t = 5/12. This numerical file does not assert that the required Frobenius elements or their deep lifts have already been constructed.
The depth required of the nth extra Frobenius relation.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawindef sawinFrobeniusDepth (n : ℕ) : ℕThe geometric upper bound for the nth extra relation weight.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawindef sawinFrobeniusCost (n : ℕ) : ℝThe full countable cost is strictly smaller than the initial margin.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawintheorem sawinFrobeniusCost_hasSum :
HasSum sawinFrobeniusCost (3125 / 145152 : ℝ)Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawintheorem sawinFrobeniusCost_summable : Summable sawinFrobeniusCostSurrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawintheorem sawinFrobeniusCost_tsum :
∑' n : ℕ, sawinFrobeniusCost n = (3125 / 145152 : ℝ)Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawintheorem sawinFrobeniusCost_tsum_lt_margin :
(∑' n : ℕ, sawinFrobeniusCost n) < (1 / 24 : ℝ)Any greater depth consumes at most the scheduled geometric weight.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawintheorem sawinFrobeniusWeight_le_cost (depth : ℕ → ℕ)
(hdepth : ∀ n : ℕ, sawinFrobeniusDepth n ≤ depth n) (n : ℕ) :
(5 / 12 : ℝ) ^ depth n ≤ sawinFrobeniusCost nSurrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawintheorem sawinFrobeniusWeight_summable (depth : ℕ → ℕ)
(hdepth : ∀ n : ℕ, sawinFrobeniusDepth n ≤ depth n) :
Summable (fun n : ℕ ↦ (5 / 12 : ℝ) ^ depth n) := by
apply Summable.of_nonneg_of_le
(fun n ↦ pow_nonneg (by norm_num) (depth n))
(sawinFrobeniusWeight_le_cost depth hdepth)
sawinFrobeniusCost_summableSurrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawintheorem sawinFrobeniusWeight_tsum_le (depth : ℕ → ℕ)
(hdepth : ∀ n : ℕ, sawinFrobeniusDepth n ≤ depth n) :
(∑' n : ℕ, (5 / 12 : ℝ) ^ depth n) ≤ (3125 / 145152 : ℝ)A relation rank at most six still leaves a strict negative margin with all of the scheduled extra relations included.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawintheorem sawinGsPolynomial_with_frobenius_budget (r : ℕ) (hr : r ≤ 6)
(depth : ℕ → ℕ)
(hdepth : ∀ n : ℕ, sawinFrobeniusDepth n ≤ depth n) :
(1 : ℝ) - 5 * (5 / 12) + r * (5 / 12) ^ 2 +
(∑' n : ℕ, (5 / 12 : ℝ) ^ depth n) ≤ -2923 / 145152Every finite selection of the scheduled relations obeys the same budget.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawintheorem sawinFrobeniusWeight_sum_le (depth : ℕ → ℕ)
(hdepth : ∀ n : ℕ, sawinFrobeniusDepth n ≤ depth n) (s : Finset ℕ) :
(∑ n ∈ s, (5 / 12 : ℝ) ^ depth n) ≤ (3125 / 145152 : ℝ)The weighted polynomial stays strictly negative after any finite selection.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawintheorem sawinGsPolynomial_with_finite_frobenius_budget (r : ℕ) (hr : r ≤ 6)
(depth : ℕ → ℕ)
(hdepth : ∀ n : ℕ, sawinFrobeniusDepth n ≤ depth n) (s : Finset ℕ) :
(1 : ℝ) - 5 * (5 / 12) + r * (5 / 12) ^ 2 +
(∑ n ∈ s, (5 / 12 : ℝ) ^ depth n) ≤ -2923 / 145152The exact finite-prefix inequality needed by the countable GS criterion.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Sawintheorem sawinGsPolynomial_frobenius_prefix_nonpos (r : ℕ) (hr : r ≤ 6) (N : ℕ) :
(1 : ℝ) - 5 * (5 / 12) + (∑ _i : Fin r, (5 / 12 : ℝ) ^ 2) +
(∑ i : Fin N, (5 / 12 : ℝ) ^ sawinFrobeniusDepth i) ≤ 0