Determinant perturbation bound and primitive constant reduction. Adapted from Li2Unified/Modular/Base/DetCongruence.lean and PrimitiveReduction.lean (li2-light-certs-2026-09-29/repo-simplify), restated for Zeta32.Arith.Local.VG/GV.

theorem Zeta32.Arith.Local.GV.prod_sub_prod {p : ℕ} [hp : Fact (Nat.Prime p)] {ι : Type u_1} (s : Finset ι) {F G : ι → Polynomial ℚ} {r : ι → ℚ} {δ : ℚ} (hF : ∀ i ∈ s, GV p (F i) (r i)) (hG : ∀ i ∈ s, GV p (G i) (r i)) (hFG : ∀ i ∈ s, GV p (F i - G i) (r i + δ)) : GV p (∏ i ∈ s, F i - ∏ i ∈ s, G i) (∑ i ∈ s, r i + δ)

theorem Zeta32.Arith.Local.det_sub_GV {p : ℕ} [hp : Fact (Nat.Prime p)] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M N : Matrix ι ι (Polynomial ℚ)) (ρ κ : ι → ℚ) (δ : ℚ) (hM : ∀ (i j : ι), GV p (M i j) (ρ i + κ j)) (hN : ∀ (i j : ι), GV p (N i j) (ρ i + κ j)) (hMN : ∀ (i j : ι), GV p (M i j - N i j) (ρ i + κ j + δ)) : GV p (M.det - N.det) (∑ i : ι, ρ i + ∑ j : ι, κ j + δ)

theorem Zeta32.Arith.Local.VG.round_half {p : ℕ} {q : ℚ} (r : ℤ) (h : VG p q (↑r + 1 / 2)) : VG p q (↑r + 1)

theorem Zeta32.Arith.Local.primitive_exists_coeff_not_dvd {p : ℕ} [hp : Fact (Nat.Prime p)] (P : Polynomial ℤ) (hP : P.IsPrimitive) : ∃ (k : ℕ), ¬↑p ∣ P.coeff k

theorem Zeta32.Arith.Local.primitive_constant_reduction_of_dvd {p : ℕ} [hp : Fact (Nat.Prime p)] (P : Polynomial ℤ) (hP : P.IsPrimitive) (hdiv : ∀ (k : ℕ), k ≠ 0 → ↑p ∣ P.coeff k) : ∃ (c : ZMod p), c ≠ 0 ∧ Polynomial.map (Int.castRingHom (ZMod p)) P = Polynomial.C c

theorem Zeta32.Arith.Local.primitive_constant_reduction_of_strict_min {p : ℕ} [hp : Fact (Nat.Prime p)] (P : Polynomial ℤ) (hP : P.IsPrimitive) (hmin : ∀ (k : ℕ), k ≠ 0 → P.coeff k ≠ 0 → padicValInt p (P.coeff 0) < padicValInt p (P.coeff k)) : ∃ (c : ZMod p), c ≠ 0 ∧ Polynomial.map (Int.castRingHom (ZMod p)) P = Polynomial.C c

theorem Zeta32.Arith.Local.unit_of_VG_sub {p : ℕ} [hp : Fact (Nat.Prime p)] {q c : ℚ} (hc : c ≠ 0) (hcval : padicValRat p c = 0) (h : VG p (q - c) 1) : q ≠ 0 ∧ padicValRat p q = 0

theorem Zeta32.Arith.Local.primitive_constant_reduction_of_scaled_congruence {p : ℕ} [hp : Fact (Nat.Prime p)] (P : Polynomial ℤ) (hP : P.IsPrimitive) (F : Polynomial ℚ) (d s c : ℚ) (hd : d ≠ 0) (hs : s ≠ 0) (hprop : Polynomial.map (Int.castRingHom ℚ) P = Polynomial.C d * F) (hc : c ≠ 0) (hcval : padicValRat p c = 0) (hcong : GV p (Polynomial.C s * F - Polynomial.C c) 1) : ∃ (cbar : ZMod p), cbar ≠ 0 ∧ Polynomial.map (Int.castRingHom (ZMod p)) P = Polynomial.C cbar