hyperpolymath · Oct 27, 2026 · Oct 27, 2026 · Oct 27, 2026 · Oct 27, 2026 · Oct 27, 2026
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
 
@@ -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`
 
@@ -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
@@ -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
@@ -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
@@ -1 +1 @@
-leanprover/lean4:v4.13.0
+leanprover/lean4:v4.35.0