diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md
new file mode 120000
index 0000000..be77ac8
--- /dev/null
+++ b/.claude/CLAUDE.md
@@ -0,0 +1 @@
+../AGENTS.md
\ No newline at end of file
diff --git a/AGENTS.md b/AGENTS.md
new file mode 100644
index 0000000..f8167c9
--- /dev/null
+++ b/AGENTS.md
@@ -0,0 +1,20 @@
+# Hex repo family
+
+`hex-dev` is the development monorepo where new Hex sublibraries are
+incubated before they are split out for release. `hex` is the released
+aggregate repo; it depends on released split libraries at exact Lake
+revisions.
+
+The currently pinned upstream split repos for `hex` are:
+
+- `hex-matrix`
+- `hex-matrix-mathlib`
+- `hex-gram-schmidt`
+- `hex-gram-schmidt-mathlib`
+- `hex-lll`
+- `hex-lll-mathlib`
+
+Treat this as the current pinned set, not a permanent exhaustive list:
+more sublibraries may be released from `hex-dev` later. Computational
+libraries are Mathlib-free; `*-mathlib` repos are the Mathlib bridge
+layers and should contain correspondence proofs and Mathlib-facing APIs.
diff --git a/lake-manifest.json b/lake-manifest.json
index dc6443b..da716ae 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,60 +5,60 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c73b5db35df9775eee9601ff629133e75085eb37",
+   "rev": "4fb7328b3456d262b80001e68805627161eae61a",
    "name": "HexLLLMathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "e4554e109e1cd93547572819499c33db769300af",
+   "inputRev": "4fb7328b3456d262b80001e68805627161eae61a",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/kim-em/hex-lll.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "4c5774effb54cb1107a456287ccca3053438e756",
+   "rev": "79eb689115559c45edf7eb35ae809379243290a5",
    "name": "HexLLL",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "ff9729a08b65fda89f391eca5ce5b4497711f815",
+   "inputRev": "79eb689115559c45edf7eb35ae809379243290a5",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/kim-em/hex-gram-schmidt-mathlib.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "ddf7de1193033da3480b1ae595c8a8adc4ec1e9b",
+   "rev": "9e04dc003acbb73973b0aa728a437174534f0066",
    "name": "HexGramSchmidtMathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "29404cfe535ec3dc53a6a174235e69fbf0c3c7e8",
+   "inputRev": "9e04dc003acbb73973b0aa728a437174534f0066",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/kim-em/hex-gram-schmidt.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9e91dd73311bc2739ca0740ba815a58453008666",
+   "rev": "3ce6d453934ca1bb5eb84ebd5e09b43e3d8ae4ce",
    "name": "HexGramSchmidt",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "d9ffab41cd4b400bc05eb69eb1724484d43017e3",
+   "inputRev": "3ce6d453934ca1bb5eb84ebd5e09b43e3d8ae4ce",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/kim-em/hex-matrix-mathlib.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "bbdbd6f2b4b3ed8dcd95abb170d9186ceb88e3a1",
+   "rev": "9cc6d8689d12c2775f8e1016b946a3debe6a8c9f",
    "name": "HexMatrixMathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "7e2eed8ae6d962d11e65d5763ce93439ce3fcb72",
+   "inputRev": "9cc6d8689d12c2775f8e1016b946a3debe6a8c9f",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/kim-em/hex-matrix.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "863836597fb000c6263042ce023a9375db33cb1f",
+   "rev": "85c2bb9b2f93677fe1435d898c81a56b9e7b33e8",
    "name": "HexMatrix",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "20e4c73f958cf7996199972a45e538d06121f91f",
+   "inputRev": "85c2bb9b2f93677fe1435d898c81a56b9e7b33e8",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
diff --git a/lakefile.toml b/lakefile.toml
index f894007..b4675c2 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -8,32 +8,32 @@ defaultTargets = ["HexAll"]
 [[require]]
 name = "HexMatrix"
 git = "https://github.com/kim-em/hex-matrix.git"
-rev = "863836597fb000c6263042ce023a9375db33cb1f"
+rev = "85c2bb9b2f93677fe1435d898c81a56b9e7b33e8"
 
 [[require]]
 name = "HexMatrixMathlib"
 git = "https://github.com/kim-em/hex-matrix-mathlib.git"
-rev = "bbdbd6f2b4b3ed8dcd95abb170d9186ceb88e3a1"
+rev = "9cc6d8689d12c2775f8e1016b946a3debe6a8c9f"
 
 [[require]]
 name = "HexGramSchmidt"
 git = "https://github.com/kim-em/hex-gram-schmidt.git"
-rev = "9e91dd73311bc2739ca0740ba815a58453008666"
+rev = "3ce6d453934ca1bb5eb84ebd5e09b43e3d8ae4ce"
 
 [[require]]
 name = "HexGramSchmidtMathlib"
 git = "https://github.com/kim-em/hex-gram-schmidt-mathlib.git"
-rev = "ddf7de1193033da3480b1ae595c8a8adc4ec1e9b"
+rev = "9e04dc003acbb73973b0aa728a437174534f0066"
 
 [[require]]
 name = "HexLLL"
 git = "https://github.com/kim-em/hex-lll.git"
-rev = "4c5774effb54cb1107a456287ccca3053438e756"
+rev = "79eb689115559c45edf7eb35ae809379243290a5"
 
 [[require]]
 name = "HexLLLMathlib"
 git = "https://github.com/kim-em/hex-lll-mathlib.git"
-rev = "c73b5db35df9775eee9601ff629133e75085eb37"
+rev = "4fb7328b3456d262b80001e68805627161eae61a"
 
 [[lean_lib]]
 name = "HexAll"