From 730fd5f28055fe70c6b0f00bfc1e631f83c2791c Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Mon, 22 Jun 2026 21:53:50 -0500
Subject: [PATCH] docs: update AGENTS.md with GitHub repo reference

SilverSight is the primary target for all new formal work.
Research Stack is read-only.
---
 AGENTS.md | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

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.