Lemma 4.2 (simplified): determinants with a low-rank p⁻¹-correction #
If v(A_{st}) ≥ w_s + w_t with w ≤ 0, and U, V are p-integral of inner dimension r, then
v_p^G(det(A + p⁻¹ U V)) ≥ 2 ∑ w - r (via the Schur complement).
theorem
Zeta5Irrational.det_lowrank_bound
{p : ℕ}
[hp : Fact (Nat.Prime p)]
{h r : ℕ}
(A : Matrix (Fin h) (Fin h) (Polynomial ℚ))
(U : Matrix (Fin h) (Fin r) ℚ)
(V : Matrix (Fin r) (Fin h) ℚ)
(w : Fin h → ℚ)
(hw : ∀ (s : Fin h), w s ≤ 0)
(hA : ∀ (s t : Fin h), GV p (A s t) (w s + w t))
(hU : ∀ (s : Fin h) (u : Fin r), VG p (U s u) 0)
(hV : ∀ (u : Fin r) (t : Fin h), VG p (V u t) 0)
: