diff --git a/AGENTS.md b/AGENTS.md
index cd4f8c68..177102db 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -2,7 +2,13 @@
 
 **SilverSight is the clean-slate rebase of the Research Stack.**
 
-## Location
+## Repository
+
+**GitHub:** `https://github.com/allaunthefox/SilverSight`
+**Local clone:** `/tmp/SilverSight` (or wherever you clone it)
+**Formal modules:** `formal/SilverSight/`
+
+## Location (in Research Stack — for lake build integration)
 
 ```
 0-Core-Formalism/lean/SilverSight/
@@ -18,7 +24,7 @@
 
 ## Rules
 
-1. **SilverSight is the ONLY target for new formal work.** Do NOT add new modules to `0-Core-Formalism/lean/Semantics/Semantics/`. All new Lean code goes here.
+1. **SilverSight is the ONLY target for new formal work.** Do NOT add new modules to `0-Core-Formalism/lean/Semantics/Semantics/`. All new Lean code goes to the SilverSight repository.
 
 2. **Imports from Semantics are allowed** (cross-project): `import Semantics.FixedPoint`, `import Semantics.Spectrum`, etc.