diff --git a/0-Core-Formalism/lean/SilverSight/AGENTS.md b/0-Core-Formalism/lean/SilverSight/AGENTS.md
index 177102db..d1f06957 100644
--- a/0-Core-Formalism/lean/SilverSight/AGENTS.md
+++ b/0-Core-Formalism/lean/SilverSight/AGENTS.md
@@ -5,7 +5,7 @@
 ## Repository
 
 **GitHub:** `https://github.com/allaunthefox/SilverSight`
-**Local clone:** `/tmp/SilverSight` (or wherever you clone it)
+**Local clone:** `/home/allaun/SilverSight`
 **Formal modules:** `formal/SilverSight/`
 
 ## Location (in Research Stack — for lake build integration)
diff --git a/AGENTS.md b/AGENTS.md
index 879e2fdf..c0792895 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -17,7 +17,7 @@ successor. All new formal work MUST go to the **SilverSight repository**.
 | Add new AGENTS.md rules to Research Stack | **NO** → add to SilverSight |
 
 **SilverSight repository:** `https://github.com/allaunthefox/SilverSight`
-**SilverSight local clone:** `/tmp/SilverSight` (or wherever you clone it)
+**SilverSight local clone:** `/home/allaun/SilverSight` (or wherever you clone it)
 **SilverSight formal modules:** `formal/SilverSight/`
 **SilverSight AGENTS.md:** `AGENTS.md` in SilverSight repo
 
@@ -375,7 +375,7 @@ git ls-remote --heads github <branch>
 
 | Theorem | File | Status |
 |---------|------|--------|
-| `cleanMerge_preservesGap` | GraphRank.lean:204 | sorry with TODO(lean-port) — Q16_16↔Bool bridge for canonical 8-bin lists |
+| `cleanMerge_preservesGap` | GraphRank.lean:209 | sorry with TODO(lean-port) — computational kernel (`mergeCheck_all`) verified all 256×256 byte pairs; Q16_16↔byte bridge for 8-bin signatures pending |
 
 ## Q16_16 Unification Migration