diff --git a/.github/workflows/c299-critical-ridge.yml b/.github/workflows/c299-critical-ridge.yml
index 32a5e01ce..8d878bcc8 100644
--- a/.github/workflows/c299-critical-ridge.yml
+++ b/.github/workflows/c299-critical-ridge.yml
@@ -31,7 +31,7 @@ jobs:
     env:
       LEAN_NUM_THREADS: '2'
       # Exact frozen five-module and two-control source manifest.
-      C299_MANIFEST_SHA256: '13deb8d5c9a2c50ee419c15bcefaabb4855be16cedf060400fbbf5775a616519'
+      C299_MANIFEST_SHA256: 'f0a2d85dc30f8561fcdd6af3b6eccc00f6d3bb89e7022f64080ffef36c5830ab'
     steps:
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
         with:
diff --git a/frontiers/critical_ridge_20261020/HOSTED_SOURCE_MANIFEST.json b/frontiers/critical_ridge_20261020/HOSTED_SOURCE_MANIFEST.json
index 18d257064..034ee96e7 100644
--- a/frontiers/critical_ridge_20261020/HOSTED_SOURCE_MANIFEST.json
+++ b/frontiers/critical_ridge_20261020/HOSTED_SOURCE_MANIFEST.json
@@ -9,8 +9,8 @@
       "sha256": "ad204aee211aa3074621f56eeaf8e1a3f3a522b7c7cbe2bbdd67f3759833feb9"
     },
     "project/CriticalRidge.lean": {
-      "bytes": 9053,
-      "sha256": "9ff65416927182f6dad06646f04821b3af6bdd131740d93bf229354a81e19c38"
+      "bytes": 9047,
+      "sha256": "4a4d219ac7d38e76dd18ce1f8e42fb877553498e0da1aa80d0c069fb1c59c3a3"
     },
     "project/CriticalRidgeAxiomAudit.lean": {
       "bytes": 2728,
diff --git a/frontiers/critical_ridge_20261020/project/CriticalRidge.lean b/frontiers/critical_ridge_20261020/project/CriticalRidge.lean
index 458917f51..73b6f6450 100644
--- a/frontiers/critical_ridge_20261020/project/CriticalRidge.lean
+++ b/frontiers/critical_ridge_20261020/project/CriticalRidge.lean
@@ -126,10 +126,10 @@ theorem negativePartialGradient_hasFDerivAt (f : E d → ℝ) (p : E d)
   have hcomp := hDp'.comp (0 : E d × V) hadd
   change HasFDerivAt (fun q : E d × V =>
     (fderiv ℝ f (p + ridgeAddition V q)).comp V.subtypeL) _ _
-  convert! hcomp.clm_comp (hasFDerivAt_const V.subtypeL (0 : E d × V)) using 1 <;>
+  convert! hcomp.clm_comp (hasFDerivAt_const V.subtypeL (0 : E d × V)) using 1 ;
     first
     | rfl
-    | (simp only [ContinuousLinearMap.comp_zero, zero_add] <;>
+    | (simp only [ContinuousLinearMap.comp_zero, zero_add] ;
         (apply ContinuousLinearMap.ext
          intro q
          apply ContinuousLinearMap.ext
@@ -199,7 +199,7 @@ theorem exists_negative_partial_gradient_ridge
         (f' := (ContinuousLinearMap.id ℝ (E d)).prod (fderiv ℝ r 0))
         (0 : E d)
         (by
-          convert! hDG using 1 <;>
+          convert! hDG using 1 ;
             first
             | rfl
             | exact Prod.ext rfl hr0)