From 79df529dd3cbd4d3b450c71d395bc3352a65136a Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Tue, 23 Jun 2026 07:53:36 -0500
Subject: [PATCH] =?UTF-8?q?fix:=20PVGS=20Mathlib=20compatibility=20?=
 =?UTF-8?q?=E2=80=94=20update=20imports=20+=20toolchain?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Fixed Mathlib imports for v4.30.0-rc2:
- Mathlib.Data.Rat.Basic → Mathlib.Data.Rat.Defs + Lemmas
- Mathlib.Data.Rat.Order → (covered by Lemmas)
- Mathlib.Algebra.Order.AbsoluteValue → .Basic

Updated lean-toolchain to v4.30.0-rc2 (matches Mathlib).
Added SilverSightPVGS lean_lib to lakefile.

section4_rrc_kernel.lean compiles with 0 errors.
Build: SilverSight 3307 jobs, 0 errors.
---
 formal/PVGS_DQ_Bridge/section4_rrc_kernel.lean |  6 +++---
 lakefile.lean                                  | 12 +++++-------
 lean-toolchain                                 |  2 +-
 3 files changed, 9 insertions(+), 11 deletions(-)

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