docs: add Clebsch diagonal cubic claim + update GraphRank proof status

- Added silversight_claim_clebsch_diagonal_cubic to manifest (Phase 2 geometry witness: 42 nodes→scar-absence, 27 lines→strand topology)
- Updated cleanMerge_preservesGap theorem with crossInputGap hypothesis and documented TODO(lean-port) boundary for Q16_16↔Bool bridge
- Compiler surface unchanged (3314 jobs, 0 errors), full workspace verified (8604 jobs)

Build: 8604 jobs, 0 errors (lake build)

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)
 

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",

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