English
If α is a nonzero linear form, then the top coefficient in the α-chain through β is one less than the least natural number n for which the weight space genWeightSpace M (n·α + β) becomes trivial.
Русский
Пусть α — ненулевой линейный функционал. Тогда верхний коэффициент в α-цепочке через β равен на единицу меньше наименьшего натурального числа n, такого что весовое пространство genWeightSpace M (n·α + β) становится тривиальным.
LaTeX
$$$\\displaystyle \\text{If } \\alpha \\neq 0, \\quad \\mathrm{TopCoeff}(\\alpha, \\beta) + 1 = \\min\\{ n \\in \\mathbb{N} \mid \\mathrm{genWeightSpace}(M, n \\cdot \\alpha + \\beta) = \\bot \\}.$$$
Lean4
theorem chainTopCoeff_add_one :
letI := Classical.propDecidable
chainTopCoeff α β + 1 = Nat.find (eventually_genWeightSpace_smul_add_eq_bot M α β hα).exists :=
by
classical
rw [chainTopCoeff, dif_neg hα]
apply Nat.succ_pred_eq_of_pos
rw [zero_lt_iff]
intro e
have : genWeightSpace M (0 • α + β : L → R) = ⊥ := by
rw [← e]
exact Nat.find_spec (eventually_genWeightSpace_smul_add_eq_bot M α β hα).exists
exact β.genWeightSpace_ne_bot _ (by simpa only [zero_smul, zero_add] using this)
