diff --git a/formal/PVGS_DQ_Bridge/PVGS_DQ_Bridge_fixed.lean b/formal/PVGS_DQ_Bridge/PVGS_DQ_Bridge_fixed.lean
index 321b512b..14457d5e 100644
--- a/formal/PVGS_DQ_Bridge/PVGS_DQ_Bridge_fixed.lean
+++ b/formal/PVGS_DQ_Bridge/PVGS_DQ_Bridge_fixed.lean
@@ -502,14 +502,7 @@ theorem bms_implies_sieve (x m : ℕ) (hx : x ≥ 2) (hm : m ≥ 3)
     (h_bms : x ≤ 90 ∧ m ≤ 13) : sieveCondition x m := by
   rcases h_bms with ⟨hx90, hm13⟩
   unfold sieveCondition Hkdf hermitePoly
-  -- NOTE: The H-KdF diagonal evaluation at (x,-1,x,-1,1/2) involves
-  -- a sum of squared Hermite polynomial terms plus positive factorial weights.
-  -- Within BMS bounds (x∈[2,90], m∈[3,13]), this evaluates to 0 by the
-  -- construction from the PVGS generating function (Giani et al. 2025, §4).
-  -- The computational proof (interval_cases + native_decide) is omitted
-  -- here due to the complexity of rational Hermite polynomial evaluation.
-  -- STATUS: Axiom — the sieve condition holds within BMS bounds by design.
-  sorry
+  interval_cases x <;> interval_cases m <;> native_decide
 
 -- ---------------------------------------------------------------------------
 -- 2e. Sieve Discriminates Repunit Collisions