From 0e14efa7c39345a613a28c5f84a6104b1172de41 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
 <41898583+github-actions[bot]@users.noreply.github.com>
Date: Mon, 19 Oct 2026 07:39:13 +0000
Subject: [PATCH 1/2] chore(toolchain): track Lean v4.35.0

Weekly track-lean run: https://github.com/hyperpolymath/marches/actions/runs/39217325020. All three gates pass on v4.35.0.
---
 README.adoc    |  4 ++--
 STATE.adoc     | 12 ++++++++++++
 lean-toolchain |  2 +-
 3 files changed, 15 insertions(+), 3 deletions(-)

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..3f60c82 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
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

From 465d1a3750f4e0e4b9ad404b770626e77658a975 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 19 Oct 2026 12:10:34 +0000
Subject: [PATCH 2/2] docs(state): name no Lean version in "Next action"

CodeRabbit (marches#47, Minor): "toolchain friction against v4.34.1"
goes stale once this bump lands. track-lean.yml rewrites version
mentions in README.adoc only, so a version written here would go stale
on every weekly bump. Point at lean-toolchain instead.

Gates on this head: lake build -> Build completed successfully (15
jobs); grep -rnw sorry Marches/ Marches.lean -> empty; BadGadget #eval
orbit -> [(false, false), (true, true), (false, false), (true, true)].

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX
---
 STATE.adoc | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/STATE.adoc b/STATE.adoc
index 3f60c82..e81a42c 100644
--- a/STATE.adoc
+++ b/STATE.adoc
@@ -268,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.