diff --git a/Benchmarks/Compile/lake-manifest.json b/Benchmarks/Compile/lake-manifest.json
index bb381a33a..045433cca 100644
--- a/Benchmarks/Compile/lake-manifest.json
+++ b/Benchmarks/Compile/lake-manifest.json
@@ -108,14 +108,14 @@
    "inputRev": null,
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/argumentcomputer/lean4lean",
+  {"url": "https://github.com/argumentcomputer/lean4ix",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "4844eda4fe376a7ab7e23a4b9755189d3c2ffe5b",
+   "rev": "a4188d7c2979378d85c6bb41fdd96c3a48a71371",
    "name": "lean4lean",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "4844eda4fe376a7ab7e23a4b9755189d3c2ffe5b",
+   "inputRev": "a4188d7c2979378d85c6bb41fdd96c3a48a71371",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
diff --git a/lake-manifest.json b/lake-manifest.json
index bb37bc7a4..9a93b385c 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,14 +1,14 @@
 {"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/argumentcomputer/lean4lean",
+ [{"url": "https://github.com/argumentcomputer/lean4ix",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0d9a73e93a29aec110000944ae886daca36c6255",
+   "rev": "a4188d7c2979378d85c6bb41fdd96c3a48a71371",
    "name": "lean4lean",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "0d9a73e93a29aec110000944ae886daca36c6255",
+   "inputRev": "a4188d7c2979378d85c6bb41fdd96c3a48a71371",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
diff --git a/lakefile.lean b/lakefile.lean
index e741fbab8..db17a539c 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -24,13 +24,16 @@ require batteries from git
 /- Reference Lean4-in-Lean4 theory and checker. `IxTcVerify` imports its
 Theory/Verify specification surface, while `bench-lean4lean` and the ignored
 `lean4lean` test runner exercise the implementation. The default `ix` target
-still does not build this dependency. Pin the audited Argument fork exactly:
-this revision carries the upstream v4.32/v4.33 kernel hardening — including
-the `checkNoMVarNoFVar` check on an opaque's value (leanprover/lean4#14498),
-which the replay path in `Benchmarks/Lean4Lean.lean` reaches — on top of the
-fork's certified inductive-environment and projection development. -/
+still does not build this dependency. Pin `argumentcomputer/lean4ix` exactly --
+the Argument development line, a standalone repository rather than a GitHub
+fork of digama0/lean4lean: this revision carries the upstream v4.32/v4.33
+kernel hardening — including the `checkNoMVarNoFVar` check on an opaque's
+value (leanprover/lean4#14498), which the replay path in
+`Benchmarks/Lean4Lean.lean` reaches — on top of that line's certified
+inductive-environment and projection development, and tracks Lean v4.33.1 as
+this package does. -/
 require lean4lean from git
-  "https://github.com/argumentcomputer/lean4lean" @ "0d9a73e93a29aec110000944ae886daca36c6255"
+  "https://github.com/argumentcomputer/lean4ix" @ "a4188d7c2979378d85c6bb41fdd96c3a48a71371"
 
 /-! ## FFI