diff --git a/AGENTS.md b/AGENTS.md
index c0792895..ff7d079e 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -24,6 +24,11 @@ successor. All new formal work MUST go to the **SilverSight repository**.
 **Enforcement:** Any agent that adds new files to the Research Stack
 instead of the SilverSight repository is violating this contract.
 
+**Write Protection:** The Research Stack Lean source directories are
+write-protected (`chmod -R a-w`). Only `.git`, `extraction/`, `.lake/`,
+`4-Infrastructure/`, and `6-Documentation/` remain writable. To temporarily
+enable writes: `chmod -R a+w 0-Core-Formalism/`
+
 ## Local Hermes Deployment (2026-06-20)
 
 Hermes Agent v0.14.0 is the primary chat/dashboard gateway, serving the
@@ -375,7 +380,7 @@ git ls-remote --heads github <branch>
 
 | Theorem | File | Status |
 |---------|------|--------|
-| `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 |
+| `cleanMerge_preservesGap` | GraphRank.lean:213 | sorry with TODO(lean-port) — computational kernel (`mergePattern_check`) verified all 256×256 canonical patterns; normalization extensionality pending |
 
 ## Q16_16 Unification Migration