From 226c9e191e0ab966f094a6394f0958cdc28254e0 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <jonathan.jewell@gmail.com>
Date: Tue, 27 Oct 2026 13:56:11 +0000
Subject: [PATCH 1/3] build(lean): move the toolchain from v4.13.0 to v4.35.0
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

lean-toolchain moves to leanprover/lean4:v4.35.0, the estate floor that
hyperpolymath/marches builds on, so marches can depend on this package
(its ROADMAP rung 3d) instead of paraphrasing TropicalAdapterPath.lean.

No statement changes. Seven proof edits, all to core-API drift between
4.13 and 4.35:

- List.not_mem_nil, List.mem_cons_self and List.mem_map_of_mem now take
  their element and function arguments implicitly (TropicalAdapterPath
  x2, Resource/Closure x4).
- tcJoin_concorde_left: Nat.max_def now unfolds to an `if` omega cannot
  see through; `cases c <;> rfl` closes the four concrete goals.
- left/right_distrib_trop and MinPlus left/right_distrib: core now has
  Nat.add_max_add_* / add_min_add_* simp lemmas oriented against the
  local helpers, so `simp [.., helper]` looped; `simp only` keeps the
  helper and drops the conflicting defaults.

Version mentions that state the current pin move to 4.35.0; the dated
records (CHANGELOG, AFFIRMATION environment, the 2026-06-11 audit) stay.

Gates on v4.35.0: lake build → Build completed successfully (20 jobs);
lean.yml's axiom audit, run verbatim, passes (propext/Quot.sound only).
Against the 2026-06-11 index only hub_ceiling changed (propext →
propext, Quot.sound), from core simp, not from these edits; recorded in
docs/LEAN-FORMALIZATION.adoc.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX
---
 .github/workflows/lean.yml           |  2 +-
 EXPLAINME-new.adoc                   |  2 +-
 FOUNDATION_CONTRACT.adoc             |  2 +-
 PROOF-STATUS.adoc                    |  4 ++--
 README.adoc                          |  2 +-
 Resource.lean                        |  2 +-
 Resource/Algebra/Dioid.lean          |  2 +-
 Resource/Algebra/Interface.lean      |  2 +-
 Resource/Algebra/Ordered.lean        |  2 +-
 Resource/Algebra/ParametricLaws.lean |  2 +-
 Resource/Bridge.lean                 |  2 +-
 Resource/Closure.lean                | 10 +++++-----
 Resource/Conformance.lean            |  2 +-
 Resource/EchoBridge.lean             |  2 +-
 Resource/Instances/Affine.lean       |  2 +-
 Resource/Instances/Linear.lean       |  2 +-
 Resource/Instances/MaxPlus.lean      |  2 +-
 Resource/Instances/MinMax.lean       |  2 +-
 Resource/Instances/MinPlus.lean      |  6 +++---
 Resource/Stress.lean                 |  2 +-
 TropicalAdapterPath.lean             |  7 +++----
 TropicalSessionTypes.lean            |  6 +++---
 docs/LEAN-FORMALIZATION.adoc         | 10 ++++++++--
 docs/RESOURCE-ALGEBRA.adoc           |  2 +-
 lakefile.lean                        |  2 +-
 lean-toolchain                       |  2 +-
 26 files changed, 44 insertions(+), 39 deletions(-)

diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml
index 525dab9..6549508 100644
--- a/.github/workflows/lean.yml
+++ b/.github/workflows/lean.yml
@@ -6,7 +6,7 @@
 # Load-bearing build workflow (kept standalone in-repo, not in the shared
 # governance bundle): `lake build` over both order-reversing twins, then a
 # `#print axioms` audit asserting no `sorry`/`Classical.choice` crept in.
-# Toolchain is pinned by ./lean-toolchain (leanprover/lean4:v4.13.0); no Mathlib.
+# Toolchain is pinned by ./lean-toolchain (leanprover/lean4:v4.35.0); no Mathlib.
 
 name: Lean
 
diff --git a/EXPLAINME-new.adoc b/EXPLAINME-new.adoc
index 8e5c545..09a8afc 100644
--- a/EXPLAINME-new.adoc
+++ b/EXPLAINME-new.adoc
@@ -108,7 +108,7 @@ Every headline theorem depends only on propext (+ Quot.sound) — no sorry, no C
 ____
 
 How this is implemented::
-`lake build` is green. `lean-toolchain` pins Lean 4.13.0. Imports are only `Init`. Grep for `sorry` and `Classical.choice` returns no hits in proof terms. Full provenance in `link:docs/LEAN-FORMALIZATION.adoc[]`.
+`lake build` is green. `lean-toolchain` pins Lean 4.35.0. Imports are only `Init`. Grep for `sorry` and `Classical.choice` returns no hits in proof terms. Full provenance in `link:docs/LEAN-FORMALIZATION.adoc[]`.
 
 Caveat::
 The dependence on `propext` and `Quot.sound` is the standard foundational commitment for Lean 4 mathematics using quotients. This is not constructively neutral; a user working in a strict cubical setting would need to re-derive these results.
diff --git a/FOUNDATION_CONTRACT.adoc b/FOUNDATION_CONTRACT.adoc
index ee09ca8..e838296 100644
--- a/FOUNDATION_CONTRACT.adoc
+++ b/FOUNDATION_CONTRACT.adoc
@@ -6,7 +6,7 @@ serving as serious infinite-carrier stress tests.
 
 This file is the stable contract. The machine-checked source of truth is
 the `+Resource.*+` Lean 4 library (aggregator: `+Resource.lean+`), built
-dependency-free on the pinned `+leanprover/lean4:v4.13.0+` (no Mathlib).
+dependency-free on the pinned `+leanprover/lean4:v4.35.0+` (no Mathlib).
 
 === Vocabulary
 
diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc
index f7ba88e..b6bc24c 100644
--- a/PROOF-STATUS.adoc
+++ b/PROOF-STATUS.adoc
@@ -9,7 +9,7 @@ type-checked in this environment from what is CI-gated but not re-checked here.
 
 == Lean 4 — VERIFIED (this environment)
 
-* Toolchain: **Lean 4 v4.13.0** (pinned in `lean-toolchain`), *no Mathlib*
+* Toolchain: **Lean 4 v4.35.0** (pinned in `lean-toolchain`), *no Mathlib*
   dependency (pure core Lean 4).
 * Command: `lake build` after `rm -rf .lake/build` (clean rebuild).
 * Result: **Build completed successfully — 20/20 targets**, i.e. every Lean
@@ -27,7 +27,7 @@ Modules (libs `Tropical` + `Resource`):
 Reproduce:
 [source,sh]
 ----
-# Lean 4 v4.13.0 (e.g. via elan, or the toolchain tarball from GitHub releases)
+# Lean 4 v4.35.0 (e.g. via elan, or the toolchain tarball from GitHub releases)
 lake build
 ----
 
diff --git a/README.adoc b/README.adoc
index 8e4ff65..544c06c 100644
--- a/README.adoc
+++ b/README.adoc
@@ -105,7 +105,7 @@ Vocabulary and contract are in `FOUNDATION_CONTRACT.md`; full detail in `docs/RE
 |===
 | Property | Status
 
-| Lean 4.13.0, `lake build` green
+| Lean 4.35.0, `lake build` green
 | Yes
 
 | Depends only on `Init`
diff --git a/Resource.lean b/Resource.lean
index a1276e5..11d5337 100644
--- a/Resource.lean
+++ b/Resource.lean
@@ -19,7 +19,7 @@ import Resource.Closure
   # `Resource` — the resource-grade axis (aggregator)
 
   Author: Jonathan D.A. Jewell (hyperpolymath)
-  Verified: Lean 4.13.0 (pinned via `lean-toolchain`), no Mathlib.
+  Verified: Lean 4.35.0 (pinned via `lean-toolchain`), no Mathlib.
 
   This is the single import a downstream language (e.g. `my-lang`) needs to pick
   up the entire **resource-grade axis** that `tropical-resource-typing` exports.
diff --git a/Resource/Algebra/Dioid.lean b/Resource/Algebra/Dioid.lean
index d14257d..d0dafc3 100644
--- a/Resource/Algebra/Dioid.lean
+++ b/Resource/Algebra/Dioid.lean
@@ -6,7 +6,7 @@ import Resource.Algebra.Ordered
   # Resource Algebra — the canonical dioid order builder
 
   Author: Jonathan D.A. Jewell (hyperpolymath)
-  Verified: Lean 4.13.0 (pinned via `lean-toolchain`), no Mathlib.
+  Verified: Lean 4.35.0 (pinned via `lean-toolchain`), no Mathlib.
 
   A **dioid** is a semiring whose addition is idempotent (`a ⊞ a = a`).  Every
   dioid carries a *canonical* order
diff --git a/Resource/Algebra/Interface.lean b/Resource/Algebra/Interface.lean
index 233a37e..f11365b 100644
--- a/Resource/Algebra/Interface.lean
+++ b/Resource/Algebra/Interface.lean
@@ -6,7 +6,7 @@ import Init
   # Resource Algebra — the consumer-facing interface (algebra layer)
 
   Author: Jonathan D.A. Jewell (hyperpolymath)
-  Verified: Lean 4.13.0 (pinned via `lean-toolchain`), `import Init` (no Mathlib).
+  Verified: Lean 4.35.0 (pinned via `lean-toolchain`), `import Init` (no Mathlib).
 
   ## What this module is
 
diff --git a/Resource/Algebra/Ordered.lean b/Resource/Algebra/Ordered.lean
index 2363b74..47037e2 100644
--- a/Resource/Algebra/Ordered.lean
+++ b/Resource/Algebra/Ordered.lean
@@ -6,7 +6,7 @@ import Resource.Algebra.Interface
   # Resource Algebra — the ordered layer
 
   Author: Jonathan D.A. Jewell (hyperpolymath)
-  Verified: Lean 4.13.0 (pinned via `lean-toolchain`), no Mathlib.
+  Verified: Lean 4.35.0 (pinned via `lean-toolchain`), no Mathlib.
 
   `ResourceAlgebra R` is the full consumer-facing interface: a
   `ResourceSemiring` (algebra core) together with an order `le` (`⊑`) and the
diff --git a/Resource/Algebra/ParametricLaws.lean b/Resource/Algebra/ParametricLaws.lean
index 7142338..134c7a1 100644
--- a/Resource/Algebra/ParametricLaws.lean
+++ b/Resource/Algebra/ParametricLaws.lean
@@ -6,7 +6,7 @@ import Resource.Algebra.Ordered
   # Resource Algebra — parametric laws and the consumer transport theorem
 
   Author: Jonathan D.A. Jewell (hyperpolymath)
-  Verified: Lean 4.13.0 (pinned via `lean-toolchain`), no Mathlib.
+  Verified: Lean 4.35.0 (pinned via `lean-toolchain`), no Mathlib.
 
   This module exports the **law bundle that downstream soundness proofs depend
   on**, derived once and for all from the `ResourceAlgebra` interface.
diff --git a/Resource/Bridge.lean b/Resource/Bridge.lean
index 9dc572d..c754991 100644
--- a/Resource/Bridge.lean
+++ b/Resource/Bridge.lean
@@ -9,7 +9,7 @@ import TropicalAdapterPath
   # Bridges — the two original twins stand on the resource-grade axis
 
   Author: Jonathan D.A. Jewell (hyperpolymath)
-  Verified: Lean 4.13.0 (pinned via `lean-toolchain`), no Mathlib.
+  Verified: Lean 4.35.0 (pinned via `lean-toolchain`), no Mathlib.
 
   `TropicalSessionTypes.lean` (max-plus session grading) and
   `TropicalAdapterPath.lean` (min-max bottleneck paths) predate the `Resource.*`
diff --git a/Resource/Closure.lean b/Resource/Closure.lean
index 39b50af..8f48e38 100644
--- a/Resource/Closure.lean
+++ b/Resource/Closure.lean
@@ -8,7 +8,7 @@ import Resource.Instances.MinMax
   # Resource Algebra — the Kleene / Floyd–Warshall all-pairs closure layer
 
   Author: Jonathan D.A. Jewell (hyperpolymath)
-  Verified: Lean 4.13.0 (pinned via `lean-toolchain`), `import Init` only (no
+  Verified: Lean 4.35.0 (pinned via `lean-toolchain`), `import Init` only (no
   Mathlib; we import the Mathlib-free `Resource.*` axis).
 
   ## What this module is
@@ -89,11 +89,11 @@ theorem mem_allFins : ∀ (n : Nat) (i : Fin n), i ∈ allFins n := by
   | succ m ih =>
     intro i
     match i with
-    | ⟨0, _⟩ => exact List.mem_cons_self _ _
+    | ⟨0, _⟩ => exact List.mem_cons_self
     | ⟨k+1, h⟩ =>
       apply List.mem_cons_of_mem
       have hmem : (⟨k, by omega⟩ : Fin m) ∈ allFins m := ih _
-      have := List.mem_map_of_mem Fin.succ hmem
+      have := List.mem_map_of_mem (f := Fin.succ) hmem
       simpa [Fin.succ] using this
 
 -- ============================================================================
@@ -122,7 +122,7 @@ theorem lsum_mono {β : Type v} (l : List β) (f g : β → R)
   | nil => exact Resource.ResourceAlgebra.le_refl _
   | cons x xs ih =>
     simp only [List.map_cons, lsum_cons]
-    have hx : (f x) ⊑ (g x) := h x (List.mem_cons_self _ _)
+    have hx : (f x) ⊑ (g x) := h x (List.mem_cons_self)
     have hrest : (lsum (xs.map f)) ⊑ (lsum (xs.map g)) :=
       ih (fun b hb => h b (List.mem_cons_of_mem _ hb))
     exact Resource.add_le_add hx hrest
@@ -260,7 +260,7 @@ theorem le_lsum_of_mem (hab : Absorb R) {a : R} :
     ∀ {l : List R}, a ∈ l → a ⊑ lsum l := by
   intro l
   induction l with
-  | nil => intro h; exact absurd h (List.not_mem_nil a)
+  | nil => intro h; exact absurd h List.not_mem_nil
   | cons x xs ih =>
     intro h
     rcases List.mem_cons.mp h with hx | hxs
diff --git a/Resource/Conformance.lean b/Resource/Conformance.lean
index 17f7490..0f6a462 100644
--- a/Resource/Conformance.lean
+++ b/Resource/Conformance.lean
@@ -12,7 +12,7 @@ import Resource.Instances.MinMax
   #              consumer proof instantiates at all of them
 
   Author: Jonathan D.A. Jewell (hyperpolymath)
-  Verified: Lean 4.13.0 (pinned via `lean-toolchain`), no Mathlib.
+  Verified: Lean 4.35.0 (pinned via `lean-toolchain`), no Mathlib.
 
   This module is the machine-checked statement of the acceptance criteria:
 
diff --git a/Resource/EchoBridge.lean b/Resource/EchoBridge.lean
index 1ec8293..71df228 100644
--- a/Resource/EchoBridge.lean
+++ b/Resource/EchoBridge.lean
@@ -7,7 +7,7 @@ import Resource.Instances.MaxPlus
   # Bridge — a resource algebra may measure Echo residues
 
   Author: Jonathan D.A. Jewell (hyperpolymath)
-  Verified: Lean 4.13.0 (pinned via `lean-toolchain`), no Mathlib.
+  Verified: Lean 4.35.0 (pinned via `lean-toolchain`), no Mathlib.
 
   ## Boundary invariant (the whole point of this file)
 
diff --git a/Resource/Instances/Affine.lean b/Resource/Instances/Affine.lean
index 1850902..864fa92 100644
--- a/Resource/Instances/Affine.lean
+++ b/Resource/Instances/Affine.lean
@@ -6,7 +6,7 @@ import Resource.Algebra.ParametricLaws
   # Resource instance — the affine usage quantity `{0, 1, ω}`
 
   Author: Jonathan D.A. Jewell (hyperpolymath)
-  Verified: Lean 4.13.0 (pinned via `lean-toolchain`), no Mathlib.
+  Verified: Lean 4.35.0 (pinned via `lean-toolchain`), no Mathlib.
 
   The **affine** usage semiring.  Same carrier and same `add`/`mul` as
   `Resource.Instances.Linear`; the *only* difference is the order.
diff --git a/Resource/Instances/Linear.lean b/Resource/Instances/Linear.lean
index f2d2779..484d1ea 100644
--- a/Resource/Instances/Linear.lean
+++ b/Resource/Instances/Linear.lean
@@ -6,7 +6,7 @@ import Resource.Algebra.ParametricLaws
   # Resource instance — the linear usage quantity `{0, 1, ω}`
 
   Author: Jonathan D.A. Jewell (hyperpolymath)
-  Verified: Lean 4.13.0 (pinned via `lean-toolchain`), no Mathlib.
+  Verified: Lean 4.35.0 (pinned via `lean-toolchain`), no Mathlib.
 
   The canonical **linear** (quantitative type theory, à la Atkey 2018) usage
   semiring: a binder is used exactly `0`, exactly `1`, or `ω`-many (unbounded)
diff --git a/Resource/Instances/MaxPlus.lean b/Resource/Instances/MaxPlus.lean
index 6e85af1..d786afa 100644
--- a/Resource/Instances/MaxPlus.lean
+++ b/Resource/Instances/MaxPlus.lean
@@ -7,7 +7,7 @@ import TropicalSessionTypes
   # Resource instance — the max-plus tropical cost algebra
 
   Author: Jonathan D.A. Jewell (hyperpolymath)
-  Verified: Lean 4.13.0 (pinned via `lean-toolchain`), no Mathlib.
+  Verified: Lean 4.35.0 (pinned via `lean-toolchain`), no Mathlib.
 
   This instance **re-exports**, rather than duplicates, the max-plus semiring
   already proved in `TropicalSessionTypes.lean` (`Hyperpolymath.Tropical`,
diff --git a/Resource/Instances/MinMax.lean b/Resource/Instances/MinMax.lean
index 1074388..2dff86c 100644
--- a/Resource/Instances/MinMax.lean
+++ b/Resource/Instances/MinMax.lean
@@ -6,7 +6,7 @@ import Resource.Algebra.Dioid
   # Resource instance — the min-max / bottleneck tropical algebra
 
   Author: Jonathan D.A. Jewell (hyperpolymath)
-  Verified: Lean 4.13.0 (pinned via `lean-toolchain`), no Mathlib.
+  Verified: Lean 4.35.0 (pinned via `lean-toolchain`), no Mathlib.
 
   The **min-max** (a.k.a. *bottleneck*) tropical semiring on `ℕ ∪ {+∞}`:
   choose the better route (`min`), and compose by the worst step (`max`).  This
diff --git a/Resource/Instances/MinPlus.lean b/Resource/Instances/MinPlus.lean
index 8734a13..2ea6e52 100644
--- a/Resource/Instances/MinPlus.lean
+++ b/Resource/Instances/MinPlus.lean
@@ -6,7 +6,7 @@ import Resource.Algebra.Dioid
   # Resource instance — the min-plus tropical cost algebra
 
   Author: Jonathan D.A. Jewell (hyperpolymath)
-  Verified: Lean 4.13.0 (pinned via `lean-toolchain`), no Mathlib.
+  Verified: Lean 4.35.0 (pinned via `lean-toolchain`), no Mathlib.
 
   The classical **min-plus** (shortest-path / Mohri) tropical semiring on
   `ℕ ∪ {+∞}`.  A clean infinite-carrier instance: unlike the bounded `1000000`-
@@ -93,8 +93,8 @@ def semiring : Resource.ResourceSemiring MinPlus where
   mul_one       := by intro a;     cases a <;> simp [mul]
   zero_mul      := by intro a;     cases a <;> rfl
   mul_zero      := by intro a;     cases a <;> rfl
-  left_distrib  := by intro a b c; cases a <;> cases b <;> cases c <;> simp [mul, add, nat_add_min_left]
-  right_distrib := by intro a b c; cases a <;> cases b <;> cases c <;> simp [mul, add, nat_add_min_right]
+  left_distrib  := by intro a b c; cases a <;> cases b <;> cases c <;> simp only [mul, add, nat_add_min_left]
+  right_distrib := by intro a b c; cases a <;> cases b <;> cases c <;> simp only [mul, add, nat_add_min_right]
 
 instance instResourceAlgebra : Resource.ResourceAlgebra MinPlus :=
   Resource.ResourceAlgebra.ofIdempotentAdd (inst := semiring) add_idem
diff --git a/Resource/Stress.lean b/Resource/Stress.lean
index 3751753..8d9928a 100644
--- a/Resource/Stress.lean
+++ b/Resource/Stress.lean
@@ -9,7 +9,7 @@ import Resource.Instances.MinMax
   # Tropical as an infinite-carrier stress test
 
   Author: Jonathan D.A. Jewell (hyperpolymath)
-  Verified: Lean 4.13.0 (pinned via `lean-toolchain`), no Mathlib.
+  Verified: Lean 4.35.0 (pinned via `lean-toolchain`), no Mathlib.
 
   The finite usage instances (`Linear`, `Affine`) have three-element carriers, so
   one *could* discharge their laws by brute enumeration.  The tropical instances
diff --git a/TropicalAdapterPath.lean b/TropicalAdapterPath.lean
index df1dc89..081a94e 100644
--- a/TropicalAdapterPath.lean
+++ b/TropicalAdapterPath.lean
@@ -128,8 +128,7 @@ theorem tcJoin_idem (c : TransportClass) : tcJoin c c = c := by
 theorem tcJoin_concorde_left (c : TransportClass) : tcJoin .Concorde c = c := by
   apply grade_injective
   rw [tcJoin_grade]
-  simp only [grade, Nat.max_def]
-  split <;> omega
+  cases c <;> rfl
 
 theorem tcJoin_concorde_right (c : TransportClass) : tcJoin c .Concorde = c := by
   rw [tcJoin_comm]; exact tcJoin_concorde_left c
@@ -295,7 +294,7 @@ private theorem foldl_tcAdd_le_init :
 private theorem foldl_tcAdd_le_mem :
     ∀ (acc : Nat) (xs : List AdapterPath) (Q : AdapterPath),
     Q ∈ xs → xs.foldl (fun a R => tcAdd a (pathCost R)) acc ≤ pathCost Q
-  | _,   [],          _, hQ  => absurd hQ (List.not_mem_nil _)
+  | _,   [],          _, hQ  => absurd hQ List.not_mem_nil
   | acc, R :: rest,   Q, hQ  =>
       match List.mem_cons.mp hQ with
       | Or.inl h =>
@@ -416,7 +415,7 @@ theorem pathCost_le_sequential (path : AdapterPath) :
 theorem hub_ceiling (e : TransportClass) (path : List TransportClass)
     (h : e ∈ path) : grade e ≤ pathCost path := by
   induction path with
-  | nil => exact absurd h (List.not_mem_nil e)
+  | nil => exact absurd h List.not_mem_nil
   | cons c cs ih =>
     rcases List.mem_cons.mp h with rfl | h'
     · cases cs with
diff --git a/TropicalSessionTypes.lean b/TropicalSessionTypes.lean
index 0fcac24..7811904 100644
--- a/TropicalSessionTypes.lean
+++ b/TropicalSessionTypes.lean
@@ -6,7 +6,7 @@ import Init
 
   Author: Jonathan D.A. Jewell (hyperpolymath)
   Date:   2026-04-11
-  Verified: Lean 4.13.0 (pinned via `lean-toolchain`), `import Init` (no Mathlib dependency)
+  Verified: Lean 4.35.0 (pinned via `lean-toolchain`), `import Init` (no Mathlib dependency)
 
   ## The unsolved problem
 
@@ -167,13 +167,13 @@ private theorem nat_mul_add_max_right (k m n : Nat) :
 theorem left_distrib_trop (a b c : Tropical) :
     tMul a (tAdd b c) = tAdd (tMul a b) (tMul a c) := by
   cases a <;> cases b <;> cases c <;>
-    simp [tMul, tAdd, nat_mul_add_max_left]
+    simp only [tMul, tAdd, nat_mul_add_max_left]
 
 /-- Right distributivity: `(a ⊕ b) ⊗ c = (a ⊗ c) ⊕ (b ⊗ c)`. -/
 theorem right_distrib_trop (a b c : Tropical) :
     tMul (tAdd a b) c = tAdd (tMul a c) (tMul b c) := by
   cases a <;> cases b <;> cases c <;>
-    simp [tMul, tAdd, nat_mul_add_max_right]
+    simp only [tMul, tAdd, nat_mul_add_max_right]
 
 -- ============================================================================
 -- 4. CommSemiring Typeclass (local definition, Mathlib-compatible interface)
diff --git a/docs/LEAN-FORMALIZATION.adoc b/docs/LEAN-FORMALIZATION.adoc
index d673f6f..bfc8601 100644
--- a/docs/LEAN-FORMALIZATION.adoc
+++ b/docs/LEAN-FORMALIZATION.adoc
@@ -33,7 +33,7 @@ compiling definitions are the ones described **here**.
 
 == TL;DR
 
-* Two files, one Lake library, pinned to **Lean 4.13.0** (`lean-toolchain`),
+* Two files, one Lake library, pinned to **Lean 4.35.0** (`lean-toolchain`),
   **no Mathlib** (`import Init` only).
 * `TropicalSessionTypes.lean` — the **max-plus** semiring (⊕ = max, ⊗ = +),
   grading speculative session types.
@@ -49,7 +49,7 @@ compiling definitions are the ones described **here**.
 
 [source,bash]
 ----
-# The toolchain is pinned in ./lean-toolchain (leanprover/lean4:v4.13.0);
+# The toolchain is pinned in ./lean-toolchain (leanprover/lean4:v4.35.0);
 # elan reads it automatically. No network deps — Init only.
 lake build
 
@@ -212,6 +212,12 @@ inventory is recorded verbatim in the migration commit and in `CHANGELOG.md`.
 | `dual_tcMul_is_min` | AdapterPath | propext, Quot.sound
 |===
 
+Re-audited 2026-10-27 on Lean 4.35.0, after the toolchain moved from 4.13.0:
+every row above is unchanged except `hub_ceiling`, now `propext, Quot.sound`.
+Its proof text did not change; v4.35's core `simp` closes the `pathCost` goals
+by a different route. Still within the `lean.yml` policy (no `sorry`, no
+`Classical.choice`).
+
 == Open items (carried from the file headers)
 
 * Generalise `minimax_path_optimal` to full graph-algorithmic Dijkstra
diff --git a/docs/RESOURCE-ALGEBRA.adoc b/docs/RESOURCE-ALGEBRA.adoc
index 022874f..7c55ef1 100644
--- a/docs/RESOURCE-ALGEBRA.adoc
+++ b/docs/RESOURCE-ALGEBRA.adoc
@@ -9,7 +9,7 @@ Jonathan D.A. Jewell
 
 Authoritative reference for the `Resource.*` Lean 4 library — the
 consumer-facing *resource-grade axis* that `tropical-resource-typing` exports for
-downstream languages such as `my-lang`. Pinned to *Lean 4.13.0*
+downstream languages such as `my-lang`. Pinned to *Lean 4.35.0*
 (`lean-toolchain`), `import Init` only, *no Mathlib*.
 
 The two pre-existing root files (`TropicalSessionTypes.lean`,
diff --git a/lakefile.lean b/lakefile.lean
index 76f2271..4a4fa5b 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -5,7 +5,7 @@ import Lake
 open Lake DSL
 
 /-- Pure core Lean 4 proofs (no Mathlib dependency).
-    Toolchain is pinned to `leanprover/lean4:v4.13.0` in `lean-toolchain`. -/
+    Toolchain is pinned to `leanprover/lean4:v4.35.0` in `lean-toolchain`. -/
 package «tropical-resource-typing» where
 
 @[default_target]
diff --git a/lean-toolchain b/lean-toolchain
index 4f86f95..a6aff06 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.13.0
+leanprover/lean4:v4.35.0

From 4a568b13f9bc473e1d80e8b5523ad2db7d2a4f86 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <jonathan.jewell@gmail.com>
Date: Tue, 27 Oct 2026 14:02:46 +0000
Subject: [PATCH 2/3] =?UTF-8?q?fix(ci):=20CI=20context=20contract=20follow?=
 =?UTF-8?q?s=20the=20secret-scan=20=E2=86=92=20scan=20rename?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

#62 (D243) renamed the secret-scanner caller job from `secret-scan` to
`scan`, so it publishes `scan / gitleaks`, `scan / rust-secrets` and
`scan / shell-secrets`. .machine_readable/CI-CONTEXTS.a2ml still named
the old caller, and `Required contexts are producible` has been red on
main since (CONTRACT BROKEN: 'no longer defines caller job secret-scan').
The contract and the docs table now name the caller as it is.

Reproduced: tools/check-ci-contexts.sh . --no-network → CONTRACT BROKEN,
rc=1. After: contract intact, rc=0.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX
---
 .machine_readable/CI-CONTEXTS.a2ml | 4 ++--
 docs/CI-CONTEXTS.adoc              | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/.machine_readable/CI-CONTEXTS.a2ml b/.machine_readable/CI-CONTEXTS.a2ml
index cdfda8d..f87e9d3 100644
--- a/.machine_readable/CI-CONTEXTS.a2ml
+++ b/.machine_readable/CI-CONTEXTS.a2ml
@@ -33,9 +33,9 @@ published-contexts = ["hypatia / Hypatia Neurosymbolic Analysis"]
 [[wrapper]]
 gate = "Secret Scanner"
 workflow = ".github/workflows/secret-scanner.yml"
-caller-job-id = "secret-scan"
+caller-job-id = "scan"
 reusable = "hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml"
-published-contexts = ["secret-scan / gitleaks", "secret-scan / rust-secrets", "secret-scan / shell-secrets"]
+published-contexts = ["scan / gitleaks", "scan / rust-secrets", "scan / shell-secrets"]
 
 [[wrapper]]
 gate = "Governance"
diff --git a/docs/CI-CONTEXTS.adoc b/docs/CI-CONTEXTS.adoc
index cb7a850..fe41102 100644
--- a/docs/CI-CONTEXTS.adoc
+++ b/docs/CI-CONTEXTS.adoc
@@ -61,7 +61,7 @@ prints the same list, and CI runs it:
 | `.github/workflows/hypatia-scan.yml` → standards `hypatia-scan-reusable.yml`
 
 | Secret scan
-| `secret-scan / gitleaks`, `secret-scan / rust-secrets`, `secret-scan / shell-secrets`
+| `scan / gitleaks`, `scan / rust-secrets`, `scan / shell-secrets`
 | `.github/workflows/secret-scanner.yml`
 
 | Governance

From 6a2a6576520391a8c1b202ce80c714adf31a698d Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <jonathan.jewell@gmail.com>
Date: Tue, 27 Oct 2026 14:03:10 +0000
Subject: [PATCH 3/3] docs(lean): hub_ceiling's axiom line matches the 4.35.0
 re-audit

The narrative description still said hub_ceiling depends only on
propext; on Lean 4.35.0 it is propext and Quot.sound. The dated
2026-06-11 theorem index stays as the historical record.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX
---
 docs/LEAN-FORMALIZATION.adoc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/LEAN-FORMALIZATION.adoc b/docs/LEAN-FORMALIZATION.adoc
index bfc8601..b9a5f92 100644
--- a/docs/LEAN-FORMALIZATION.adoc
+++ b/docs/LEAN-FORMALIZATION.adoc
@@ -142,7 +142,7 @@ caps the fidelity of every format that must pass through it, so "universal" and
 "high fidelity" are contradictory the moment any format embeds at grade > 0;
 universal *low* fidelity is the achievable point (that is what JSON already is).
 This corollary closes Protocol Squisher's universal-interoperability claim using
-the project's own algebra. Machine-checked, depends only on `propext`.
+the project's own algebra. Machine-checked; on Lean 4.35.0 it depends on `propext` and `Quot.sound` (`propext` alone on 4.13.0, see the re-audit note under the theorem index).
 
 == The duality: `g ↦ maxGrade − g`