diff --git a/.gitignore b/.gitignore
index 0de8f801a1..4b61c652e8 100644
--- a/.gitignore
+++ b/.gitignore
@@ -90,3 +90,4 @@ docker/Xilinx_Unified_*.bin
 # Regenerated by `tri prove` from the spec, so the proof can never drift from
 # the specification it claims to be about. Do not commit.
 fpga/formal/mvp_classifier_dut.v
+lean4_bridge/.lake/
diff --git a/docs/NOW.md b/docs/NOW.md
index 5bbe121356..91b57fb1e6 100644
--- a/docs/NOW.md
+++ b/docs/NOW.md
@@ -1,3 +1,21 @@
+# NOW -- nine dangling gitlinks, one broken checkout for everyone (2026-08-19)
+
+Last updated: 2026-08-19
+
+## ci: lean4_bridge/.lake gitlinks removed; .lake ignored (Refs #1959)
+
+- Since #1304, nine `lean4_bridge/.lake/packages/*` paths were committed as
+  SUBMODULE gitlinks with no `.gitmodules` entries -- Lake's build cache, not
+  sources. Every workflow that checks out with `submodules: recursive`
+  (coverage) has died at `fatal: No url found for submodule path ...` ever
+  since; it failed on the ladder PR and on every other PR the same way
+- The gitlinks are removed from the index and `lean4_bridge/.lake/` is
+  ignored; the three real submodules (chips/phi, chips/euler, chips/gamma)
+  are untouched
+- Found while landing #2217: a required-check triage that separated "your PR
+  broke it" from "it was always broken" -- the second class hides in green
+  repos precisely because nobody reads a check that always failed
+
 # NOW -- the grammar ladder lands, and the merge that argued back (2026-08-19)
 
 Last updated: 2026-08-19
diff --git a/lean4_bridge/.lake/packages/Cli b/lean4_bridge/.lake/packages/Cli
deleted file mode 160000
index 92564e5770..0000000000
--- a/lean4_bridge/.lake/packages/Cli
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit 92564e5770e4d09f2d86dfbf8ada1e9c715b384c
diff --git a/lean4_bridge/.lake/packages/LeanSearchClient b/lean4_bridge/.lake/packages/LeanSearchClient
deleted file mode 160000
index c5d5b8fe6e..0000000000
--- a/lean4_bridge/.lake/packages/LeanSearchClient
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit c5d5b8fe6e5158def25cd28eb94e4141ad97c843
diff --git a/lean4_bridge/.lake/packages/Qq b/lean4_bridge/.lake/packages/Qq
deleted file mode 160000
index f46324995f..0000000000
--- a/lean4_bridge/.lake/packages/Qq
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit f46324995fca5f0483b742e4eb4daec7f4ee50d2
diff --git a/lean4_bridge/.lake/packages/aesop b/lean4_bridge/.lake/packages/aesop
deleted file mode 160000
index e3cb2f7414..0000000000
--- a/lean4_bridge/.lake/packages/aesop
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit e3cb2f741431ce31bf73549fb52316a57368b06f
diff --git a/lean4_bridge/.lake/packages/batteries b/lean4_bridge/.lake/packages/batteries
deleted file mode 160000
index fc38104235..0000000000
--- a/lean4_bridge/.lake/packages/batteries
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit fc38104235ab6cf8a448a74405aa258804ef4e36
diff --git a/lean4_bridge/.lake/packages/importGraph b/lean4_bridge/.lake/packages/importGraph
deleted file mode 160000
index 5c7542ed01..0000000000
--- a/lean4_bridge/.lake/packages/importGraph
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit 5c7542ed018c78194f1e2b903eaf6a792b74c03d
diff --git a/lean4_bridge/.lake/packages/mathlib b/lean4_bridge/.lake/packages/mathlib
deleted file mode 160000
index 2d792c9bea..0000000000
--- a/lean4_bridge/.lake/packages/mathlib
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit 2d792c9bea7859d32dd125ee02ad72fa54a7a237
diff --git a/lean4_bridge/.lake/packages/plausible b/lean4_bridge/.lake/packages/plausible
deleted file mode 160000
index 63045536fe..0000000000
--- a/lean4_bridge/.lake/packages/plausible
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit 63045536fe95024e6c18fc7b48e03f506701c5bc
diff --git a/lean4_bridge/.lake/packages/proofwidgets b/lean4_bridge/.lake/packages/proofwidgets
deleted file mode 160000
index 24b0d9dc08..0000000000
--- a/lean4_bridge/.lake/packages/proofwidgets
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit 24b0d9dc081c5423f8eec7e866c441e5184f29d9