the proof notes section 4, Lemma 5: the Vandermonde bound for the actual Q r n.
Rows a with a + 2n + 2 > p are multiplied by p (rowScale); then the polynomial-part matrix
W_{ab} = U_r(q_{a+b}) is p-integral (its moments have degree ≤ a + 2n - 1, and U_r(t^e) is
p-integral for e ≤ p - 3 and has v_p ≥ -1 always), and rank_one_GV_rows gives
v_p(∏ rowScale · Q r n) ≥ Σ_c Scl n p c.
The rank-one part follows the Li₂ proof parameter_raw_Q_GV
(dtq1997/li2-half-irrationality@d5d8206:Li2Unified/Modular/Positive/Packed/P045.lean).
theorem
Zeta32.Outer.W_row_GV
{p : ℕ}
[hp : Fact (Nat.Prime p)]
(hp2 : p ≠ 2)
{r : ℚ}
(hr : Zeta5Irrational.VG p r 0)
(n : ℕ)
(a b : Fin (3 * n))
:
Zeta5Irrational.GV p (Polynomial.C (rowScale n p ↑a) * Polynomial.C (polynomialMoment r (polynomialPart n (↑a + ↑b)))) 0
theorem
Zeta32.Outer.H_regroup
{p : ℕ}
(r : ℚ)
(n : ℕ)
(hp0 : 0 < p)
(a b : Fin (3 * n))
:
(Polynomial.X • (B n).map ⇑Polynomial.C + (A r n).map ⇑Polynomial.C) a b = Polynomial.C (polynomialMoment r (polynomialPart n (↑a + ↑b))) + ∑ c : Fin p,
∑ t ∈ Finset.range (Ccl p (5 * n) ↑c),
gam r n (jn p (5 * n) (↑c) t) * Polynomial.C ((-↑(jn p (5 * n) (↑c) t)) ^ ↑a * (-↑(jn p (5 * n) (↑c) t)) ^ ↑b)
H = W + Σ_c Σ_t γ v vᵀ after regrouping the poles by classes.