diff --git a/formal/PVGS_DQ_Bridge/section4_rrc_kernel.lean b/formal/PVGS_DQ_Bridge/section4_rrc_kernel.lean
index 0560524a..08aaa320 100644
--- a/formal/PVGS_DQ_Bridge/section4_rrc_kernel.lean
+++ b/formal/PVGS_DQ_Bridge/section4_rrc_kernel.lean
@@ -47,9 +47,9 @@
 -/
 
 import Mathlib.Data.Nat.Basic
-import Mathlib.Data.Rat.Basic
-import Mathlib.Data.Rat.Order
-import Mathlib.Algebra.Order.AbsoluteValue
+import Mathlib.Data.Rat.Defs
+import Mathlib.Data.Rat.Lemmas
+import Mathlib.Algebra.Order.AbsoluteValue.Basic
 import Mathlib.Tactic
 
 -- ============================================================
diff --git a/lakefile.lean b/lakefile.lean
index b5728ae2..7e65afb7 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -66,13 +66,11 @@ lean_lib «SilverSightRRC» where
     `RRCLib.RRCEmit
   ]
 
--- NOTE: PVGS_DQ_Bridge files depend on Mathlib modules not available
--- in SilverSight's pinned version. Needs Mathlib compatibility work.
--- lean_lib «SilverSightPVGS» where
---   srcDir := "formal"
---   roots := #[
---     `PVGS_DQ_Bridge.section4_rrc_kernel
---   ]
+lean_lib «SilverSightPVGS» where
+  srcDir := "formal"
+  roots := #[
+    `PVGS_DQ_Bridge.section4_rrc_kernel
+  ]
 
 lean_exe «rrc-emit-fixture» where
   root := `RrcEmitFixture
diff --git a/lean-toolchain b/lean-toolchain
index 63f51eaf..6c7e31ff 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.32.0-rc1
\ No newline at end of file
+leanprover/lean4:v4.30.0-rc2