A thick support contains a basis

Positive central thickness rules out containment in a proper linear subspace. A basis selected from the positive support can therefore be used in the initial growth phase.

theorem EGZ.Expansion.IsCentrallyThick.span_positive_eq_top {p d K : ℕ} [NeZero p] [Fact (Nat.Prime p)] {w : FpCoord p d → ℝ} {δ : ℝ} (ht : IsCentrallyThick w K δ) (hw : ∀ (v : FpCoord p d), 0 ≤ w v) (hW : 0 < ∑ v : FpCoord p d, w v) (hδ : 0 < δ) : Submodule.span (ZMod p) {v : FpCoord p d | 0 < w v} = ⊤

theorem EGZ.Expansion.IsCentrallyThick.exists_basis {p d K : ℕ} [NeZero p] [Fact (Nat.Prime p)] {w : FpCoord p d → ℝ} {δ : ℝ} (ht : IsCentrallyThick w K δ) (hw : ∀ (v : FpCoord p d), 0 ≤ w v) (hW : 0 < ∑ v : FpCoord p d, w v) (hδ : 0 < δ) : ∃ (E : Module.Basis (Fin d) (ZMod p) (FpCoord p d)), ∀ (i : Fin d), 0 < w (E i)

Choose a basis indexed by the ambient dimension from positive-weight translations.