diff --git a/README.adoc b/README.adoc
index c1d692e..e08fd43 100644
--- a/README.adoc
+++ b/README.adoc
@@ -14,7 +14,7 @@ object*: region-crossing well-formedness is a typing judgment on traces
 (`Marches.Trace`), and ill-typed crossings are *unconstructible* — they
 have no derivation — rather than detected and filtered.
 
-Machine-checked, in this repository, by `lake build` (Lean 4, v4.34.1,
+Machine-checked, in this repository, by `lake build` (Lean 4, v4.35.0,
 no dependencies):
 
 * Every well-typed non-empty cross-region trace strictly worsens
@@ -171,7 +171,7 @@ artifact for PROVEN rows. No fabricated identifiers.
 
 [source,shell]
 ----
-elan default leanprover/lean4:v4.34.1   # or let lake read lean-toolchain
+elan default leanprover/lean4:v4.35.0   # or let lake read lean-toolchain
 lake build
 ----
 
diff --git a/STATE.adoc b/STATE.adoc
index 13acd5f..e81a42c 100644
--- a/STATE.adoc
+++ b/STATE.adoc
@@ -1,5 +1,17 @@
 = STATE — cross-session log
 
+== 2026-10-19 — toolchain v4.34.1 → v4.35.0 (weekly track-lean bot)
+
+* Gates on v4.35.0, verbatim:
++
+----
+$ lake build
+Build completed successfully (15 jobs).
+$ grep -rnw sorry Marches/ Marches.lean  # empty
+$ lake env lean Marches/BadGadget.lean
+[(false, false), (true, true), (false, false), (true, true)]
+----
+
 == 2026-10-14 — CI: estate audit pinned to cicd-suite main (not a rung)
 
 * hyperpolymath/cicd-suite#50 merged as `376898b`. Its tree is identical to
@@ -256,7 +268,8 @@ Rung 3 (see ROADMAP.adoc), the remaining items. 3d: import the estate's
 fully proved `TropicalAdapterPath.lean` (hyperpolymath/tropical-types,
 lake package `tropical-resource-typing`, pinned `e172f8a`, Lean v4.13.0)
 behind the `Marches/Tropical.lean` seam — vendor or depend on it, do NOT
-paraphrase, and expect toolchain friction against v4.34.1. 3e: path
-provenance as graded accumulation (echo-types bridge). 3f: file the
-postern cross-issue once that repository exists. Obtain the real files;
-never reconstruct from memory. One rung only.
+paraphrase, and expect toolchain friction against the Lean marches pins
+(`lean-toolchain`; named there, not here, so a weekly bump cannot make
+this line stale). 3e: path provenance as graded accumulation (echo-types
+bridge). 3f: file the postern cross-issue once that repository exists.
+Obtain the real files; never reconstruct from memory. One rung only.
diff --git a/lean-toolchain b/lean-toolchain
index ba8ebf2..a6aff06 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.34.1
+leanprover/lean4:v4.35.0