the proof notes, §3 Lemma 4 (greedy lower bound), proved by class-wise partial fractions (Zeta32/Arith/Local/) instead of the Tate-algebra functional of the proof notes, §§1–2.

With the greedy allocation galloc n p (3n) and the monic basis f_i = ∏_{b<p} (t+b)^{galloc n p i b}, every entry U_r(f_i f_k R_n) has v_p ≥ (π_i + π_k)/2 coefficientwise in X (entry_GV), so v_p(Q_n) ≥ ∑ π_i = allocCost (Q_GV). The only hypotheses used are p prime, p ∤ den r and 5n < p²; condition (D), p ≥ 5 and p > K of the proof notes, Lemma 4 are not needed by this route. 5n < p² follows from n^{2/3} < p for n ≥ 125.

the proof notes, §1, Lemma 1 and Corollary 2.

Route change: the Tate-algebra distribution formula is not formalized. The local bounds it served (the proof notes, Lemma 3, Lemma 4) are proved directly by class-wise partial fractions: Zeta32.Arith.Local.VG_polynomialMoment (Local/Binom.lean, the polynomial part of U_r), Zeta32.Arith.Local.VG_res, VG_polyPart_eval (Local/PoleFun.lean) and Zeta32.Arith.Local.Lfun_GV (Local/Entry.lean).

theorem Zeta32.Arith.Local.VG_of_not_dvd_den {p : ℕ} {r : ℚ} (h : ¬p ∣ r.den) : VG p r 0

theorem Zeta32.Arith.Local.natDegree_D_le (m : ℕ) : (D m).natDegree ≤ m

theorem Zeta32.Arith.Local.card_plc_Pl5 {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) (c : ZMod p) : (plc p (Pl5 n) c).card = {j ∈ Finset.Icc 1 (5 * n) | j % p = (-c).val}.card

theorem Zeta32.Arith.Local.entry_GV {r : ℚ} {n p : ℕ} [hp : Fact (Nat.Prime p)] (hr : VG p r 0) (hn : 5 * n < p ^ 2) (i k : Fin (3 * n)) : GV p (Lfun r n (gbasis n p ↑i * gbasis n p ↑k * D n ^ 4)) (↑(gval n p ↑i) / 2 + ↑(gval n p ↑k) / 2)

The entry bound v_p(U_r(f_i f_k R_n)) ≥ (π_i + π_k)/2.

theorem Zeta32.Arith.Local.Q_GV {r : ℚ} {n p : ℕ} [hp : Fact (Nat.Prime p)] (hr : ¬p ∣ r.den) (hn : 5 * n < p ^ 2) : GV p (Q r n) ↑(allocCost n p (galloc n p (3 * n)))

the proof notes, Lemma 4: v_p(Q_n) ≥ allocCost for the greedy allocation.

theorem Zeta32.Arith.Local.greedyBound_of_sq {r : ℚ} {n p : ℕ} [hp : Fact (Nat.Prime p)] (hr : ¬p ∣ r.den) (hn : 5 * n < p ^ 2) : GreedyBound r n p

theorem Zeta32.Arith.Local.five_mul_lt_sq {n p : ℕ} (hn : 125 ≤ n) (h : ↑n ^ (2 / 3) < ↑p) : 5 * n < p ^ 2

n^{2/3} < p gives 5n < p² once n ≥ 125.

theorem Zeta32.Arith.greedy_valuation_bound (r : ℚ) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (p : ℕ), Nat.Prime p → ↑n ^ (2 / 3) < ↑p → p ≤ 5 * n → ¬p ∣ r.den → GreedyBound r n p

the proof notes, Lemma 4 in allocation form, for n^{2/3} < p ≤ 5n.