This file isolates the numerical argument used after the truncated Golod--Shafarevich coefficient inequality. A zero-extended backwards shift makes every coefficient statement safe in ℕ. Abel summation turns the coefficient inequalities into positivity of the Golod--Shafarevich polynomial on [0, 1), while eventual stabilization handles the endpoint t = 1 separately.
The final theorem is deliberately assumption-level: it consumes only a monotone bounded dimension sequence, the truncated inequalities, relator depths, and positivity of the generator count.
The zero-extended backwards shift used in a truncated coefficient inequality.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
namespace ClassFieldTower.ProPdef backshift (A : ℕ → ℕ) (N k : ℕ) : ℕSurrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
namespace ClassFieldTower.ProPtheorem backshift_add (A : ℕ → ℕ) (n k : ℕ) :
backshift A (n + k) k = A nSurrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
namespace ClassFieldTower.ProPtheorem backshift_lt (A : ℕ → ℕ) {n k : ℕ} (h : n < k) :
backshift A n k = 0A uniformly bounded sequence has a summable weighted series on [0, 1).
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
namespace ClassFieldTower.ProP
section Abel
variable (A : ℕ → ℕ) (C : ℕ)theorem weighted_summable
(hAC : ∀ n, A n ≤ C) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t < 1) :
Summable (fun n : ℕ ↦ (A n : ℝ) * t ^ n) := by
apply Summable.of_nonneg_of_le (f := fun n : ℕ ↦ (C : ℝ) * t ^ n)
· intro n
positivity
· intro n
exact mul_le_mul_of_nonneg_right (by exact_mod_cast hAC n) (pow_nonneg ht0 n)
· exact (summable_geometric_of_lt_one ht0 ht1).mul_left (C : ℝ)Abel summation for a zero-extended backwards shift.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
namespace ClassFieldTower.ProP
section Abel
variable (A : ℕ → ℕ) (C : ℕ)theorem weighted_backshift_hasSum
(hAC : ∀ n, A n ≤ C) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t < 1) (k : ℕ) :
HasSum (fun n : ℕ ↦ (backshift A n k : ℝ) * t ^ n)
(t ^ k * ∑' n : ℕ, (A n : ℝ) * t ^ n) := by
let f : ℕ → ℝ := fun n ↦ (backshift A n k : ℝ) * t ^ n
have hprefix : ∑ i ∈ Finset.range k, f i = 0 := by
apply Finset.sum_eq_zero
intro i hi
simp [f, backshift, Nat.not_le.mpr (Finset.mem_range.mp hi)]
rw [← hasSum_nat_add_iff' k]
rw [hprefix, sub_zero]
have hsum :=
(weighted_summable A C hAC ht0 ht1).hasSum.mul_left (t ^ k)
have hfun : (fun n ↦ f (n + k)) =
fun n ↦ t ^ k * ((A n : ℝ) * t ^ n) := by
funext n
simp only [f, backshift_add]
rw [pow_add]
ring
rw [hfun]
exact hsumThe sum of a weighted backwards shift is the correspondingly shifted generating series.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
namespace ClassFieldTower.ProP
section Abel
variable (A : ℕ → ℕ) (C : ℕ)theorem tsum_weighted_backshift
(hAC : ∀ n, A n ≤ C) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t < 1) (k : ℕ) :
∑' n : ℕ, (backshift A n k : ℝ) * t ^ n =
t ^ k * ∑' n : ℕ, (A n : ℝ) * t ^ nThe Nat-safe truncated coefficient inequalities force positivity of the Golod--Shafarevich polynomial at every real t in [0, 1), provided the dimension sequence is uniformly bounded and nonzero in degree zero.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
namespace ClassFieldTower.ProPtheorem gsPolynomial_pos_of_truncated
{d r : ℕ} (ν : Fin r → ℕ) (A : ℕ → ℕ)
(hbound : ∃ C, ∀ n, A n ≤ C)
(hA0 : 0 < A 0)
(hineq : ∀ N,
1 + d * backshift A N 1 ≤
A N + ∑ i : Fin r, backshift A N (ν i))
{t : ℝ} (ht0 : 0 ≤ t) (ht1 : t < 1) :
0 < 1 - d * t + ∑ i : Fin r, t ^ ν iA backwards shift of a monotone sequence is bounded by the unshifted term.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
namespace ClassFieldTower.ProPtheorem backshift_le_of_monotone {A : ℕ → ℕ} (hA : Monotone A) (N k : ℕ) :
backshift A N k ≤ A NThe t = 1 boundary calculation. Eventual stabilization supplies a coefficient where the constant term in the truncated inequality forces d ≤ r.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
namespace ClassFieldTower.ProPtheorem generator_le_relation_of_stable_truncated
{d r : ℕ} (ν : Fin r → ℕ) (A : ℕ → ℕ)
(hmono : Monotone A) (hA0 : 0 < A 0)
(hstable : ∃ M, ∀ n, M ≤ n → A n = A M)
(hineq : ∀ N,
1 + d * backshift A N 1 ≤
A N + ∑ i : Fin r, backshift A N (ν i)) :
d ≤ rAssumption-level numerical endpoint for the truncated Golod--Shafarevich argument.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped BigOperators
namespace ClassFieldTower.ProPtheorem square_generator_lt_four_relations_of_truncated
{d r : ℕ} (ν : Fin r → ℕ) (A : ℕ → ℕ)
(hmono : Monotone A) (hbound : ∃ C, ∀ n, A n ≤ C)
(hineq : ∀ N,
1 + d * backshift A N 1 ≤
A N + ∑ i : Fin r, backshift A N (ν i))
(hdepth : ∀ i, 2 ≤ ν i) (hd : 0 < d) :
d ^ 2 < 4 * r