diff --git a/formal/PVGS_DQ_Bridge/section2_hermite_sieve.lean b/formal/PVGS_DQ_Bridge/section2_hermite_sieve.lean
index 36358e00..dfe5ab1a 100644
--- a/formal/PVGS_DQ_Bridge/section2_hermite_sieve.lean
+++ b/formal/PVGS_DQ_Bridge/section2_hermite_sieve.lean
@@ -229,7 +229,7 @@ theorem bms_implies_sieve (x m : ℕ) (hx : x ≥ 2) (hm : m ≥ 3)
   -- For each pair, the diagonal H-KdF polynomial evaluates to zero by
   -- construction from the PVGS generating function.
   -- PROOF: finite enumeration via interval_cases + native_decide.
-  sorry
+  interval_cases x <;> interval_cases m <;> native_decide
 
 -- ---------------------------------------------------------------------------
 -- §2e  SIEVE CONDITION DISCRIMINATES REPNIT COLLISIONS