diff --git a/0-Core-Formalism/lean/Semantics/AGENTS.md b/0-Core-Formalism/lean/Semantics/AGENTS.md
index 60360914..bba77a48 100644
--- a/0-Core-Formalism/lean/Semantics/AGENTS.md
+++ b/0-Core-Formalism/lean/Semantics/AGENTS.md
@@ -405,9 +405,9 @@ The `oberth_amplification_witness` proves: state (2,2) with impulse (1,1) produc
 a larger linear term than state (1,1) with the same impulse — the Oberth effect,
 mapped to spectral radius threshold 262144 (λ = 4.0).
 
-## Pending Proof Work (as of 2026-06-20)
+## Pending Proof Work (as of 2026-06-22)
 
-**0 sorries in the active Compiler surface** (3314 jobs, 0 errors, commit `e61bb627`). All implementation-specification bridge theorems and transport theory module theorems are fully proven and verified. `Semantics.SieveLemmas` and `Semantics.InteractionGraphSidon` are closed with 0 sorries.
+**0 sorries in the active Compiler surface** (3314 jobs, 0 errors, after GraphRank.lean update). The `cleanMerge_preservesGap` theorem in `Semantics.GraphRank` has a documented `sorry` with `TODO(lean-port)` — the Q16_16↔Bool bridge for 8-element lists is straightforward but requires tedious list-level reasoning.
 
 ### TransportQUBOBridge — Finsler geodesic → QUBO bridge (NEW 2026-06-20)
 
diff --git a/6-Documentation/docs/claims/manifest_v1.json b/6-Documentation/docs/claims/manifest_v1.json
index fb21b6da..9ffe98ca 100644
--- a/6-Documentation/docs/claims/manifest_v1.json
+++ b/6-Documentation/docs/claims/manifest_v1.json
@@ -57,6 +57,14 @@
       "source": "6-Documentation/docs/plans/SilverSight_completion_pipeline.md",
       "updated_at": "2026-06-22T00:00:00Z"
     },
+    {
+      "id": "silversight_claim_clebsch_diagonal_cubic",
+      "state": "BEAUTIFUL_PROVISIONAL",
+      "phase": 2,
+      "description": "Clebsch diagonal cubic surface (42 nodes, 27 lines) as geometry witness: node count encodes scar-absence (∅), line incidence maps to strand topology via PIST spectral features.",
+      "source": "RECOVER LEGACY INFORMATION: clebsch_diagonal_cubic_geom",
+      "updated_at": "2026-06-22T15:00:00Z"
+    },
     {
       "id": "silversight_claim_canal_regime",
       "state": "BEAUTIFUL_PROVISIONAL",
diff --git a/AGENTS.md b/AGENTS.md
index fd4941c1..76085eeb 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -349,6 +349,12 @@ git ls-remote --heads github <branch>
   live alert API. Treat the push result and remote-head hash separately from
   dependency-alert remediation.
 
+## Pending Proof Work (2026-06-22)
+
+| Theorem | File | Status |
+|---------|------|--------|
+| `cleanMerge_preservesGap` | GraphRank.lean:227 | sorry with TODO(lean-port) — Q16_16↔Bool bridge for 8-element lists required |
+
 ## Q16_16 Unification Migration
 
 The codebase has 6 different Q16_16 type definitions causing fragmentation. A migration