From c055d95e96c15c7e79e55c034492091427efa362 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Thu, 29 Oct 2026 19:52:17 -0400 Subject: [PATCH 1/2] chore(deps): advance CSLib and Mathlib on Lean rc2 --- docbuild/lake-manifest.json | 8 ++++---- guide/lake-manifest.json | 8 ++++---- lake-manifest.json | 8 ++++---- lakefile.toml | 2 +- 4 files changed, 13 insertions(+), 13 deletions(-) diff --git a/docbuild/lake-manifest.json b/docbuild/lake-manifest.json index a1f5e4692..5f688cd48 100644 --- a/docbuild/lake-manifest.json +++ b/docbuild/lake-manifest.json @@ -73,20 +73,20 @@ "type": "git", "subDir": null, "scope": "", - "rev": "8a8ad7489cdccb007ad7279bfb9d03bbda2229ad", + "rev": "254e30e6d4299c51323aaeaf5f51a4763b375d4a", "name": "cslib", "manifestFile": "lake-manifest.json", - "inputRev": "8a8ad7489cdccb007ad7279bfb9d03bbda2229ad", + "inputRev": "254e30e6d4299c51323aaeaf5f51a4763b375d4a", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9d581dfff2e41de989072ea63abf3daf69311520", + "rev": "69552756cd8a2d2d48763cf7279fd814d6a1224d", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.36.0-rc2", + "inputRev": "69552756cd8a2d2d48763cf7279fd814d6a1224d", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", diff --git a/guide/lake-manifest.json b/guide/lake-manifest.json index 3f19786a0..2c0ddd966 100644 --- a/guide/lake-manifest.json +++ b/guide/lake-manifest.json @@ -73,20 +73,20 @@ "type": "git", "subDir": null, "scope": "", - "rev": "8a8ad7489cdccb007ad7279bfb9d03bbda2229ad", + "rev": "254e30e6d4299c51323aaeaf5f51a4763b375d4a", "name": "cslib", "manifestFile": "lake-manifest.json", - "inputRev": "8a8ad7489cdccb007ad7279bfb9d03bbda2229ad", + "inputRev": "254e30e6d4299c51323aaeaf5f51a4763b375d4a", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9d581dfff2e41de989072ea63abf3daf69311520", + "rev": "69552756cd8a2d2d48763cf7279fd814d6a1224d", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.36.0-rc2", + "inputRev": "69552756cd8a2d2d48763cf7279fd814d6a1224d", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", diff --git a/lake-manifest.json b/lake-manifest.json index a2c1eaffd..f513ec635 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,20 +5,20 @@ "type": "git", "subDir": null, "scope": "", - "rev": "8a8ad7489cdccb007ad7279bfb9d03bbda2229ad", + "rev": "254e30e6d4299c51323aaeaf5f51a4763b375d4a", "name": "cslib", "manifestFile": "lake-manifest.json", - "inputRev": "8a8ad7489cdccb007ad7279bfb9d03bbda2229ad", + "inputRev": "254e30e6d4299c51323aaeaf5f51a4763b375d4a", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9d581dfff2e41de989072ea63abf3daf69311520", + "rev": "69552756cd8a2d2d48763cf7279fd814d6a1224d", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.36.0-rc2", + "inputRev": "69552756cd8a2d2d48763cf7279fd814d6a1224d", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", diff --git a/lakefile.toml b/lakefile.toml index 00f09a874..bfad97b80 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -33,7 +33,7 @@ autoImplicit = false [[require]] name = "cslib" git = "https://github.com/leanprover/cslib" -rev = "8a8ad7489cdccb007ad7279bfb9d03bbda2229ad" +rev = "254e30e6d4299c51323aaeaf5f51a4763b375d4a" [[lean_lib]] name = "Complexity" From ec19e875b8fe86d9309da5c1ca3b2af85834b9d1 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Thu, 29 Oct 2026 19:52:17 -0400 Subject: [PATCH 2/2] fix(proofs): follow renamed Nat induction case labels --- .../Reachability/InductiveCounting/Completeness.lean | 4 ++-- .../Circuit/Boolean/WeightedThreshold/Potential.lean | 4 ++-- .../Computability/Circuit/Frontier/BranchingProgram.lean | 2 +- .../Computability/Circuit/Rational/LaurentReduction.lean | 2 +- Complexity/Computability/Circuit/Rational/Wronskian.lean | 2 +- .../LogSpace/NondeterministicQueryMachine/Bounds.lean | 2 +- .../LogSpace/NondeterministicQueryMachine/Compiler.lean | 2 +- .../LogSpace/NondeterministicQueryMachine/Termination.lean | 2 +- Complexity/Computability/WordRAM/GhostLoop.lean | 2 +- .../Combinatorics/FunctionalGraph/ForestSegments.lean | 2 +- Complexity/Foundations/NumberTheory/Harmonic.lean | 2 +- Complexity/Foundations/NumberTheory/PrimeCounting.lean | 2 +- 12 files changed, 14 insertions(+), 14 deletions(-) diff --git a/Complexity/Algorithms/Reachability/InductiveCounting/Completeness.lean b/Complexity/Algorithms/Reachability/InductiveCounting/Completeness.lean index 302046cf6..8639015a6 100644 --- a/Complexity/Algorithms/Reachability/InductiveCounting/Completeness.lean +++ b/Complexity/Algorithms/Reachability/InductiveCounting/Completeness.lean @@ -357,7 +357,7 @@ theorem accepts_complete (hsource : source < N) (hwidth : N ≤ 2 ^ width) exact h _ _ rfl (invariant_initial hsource) bounded_initial (honest_initial hsource) intro n induction n using Nat.strong_induction_on with - | h n ih => + | ind n ih => intro s hr hi hb hh by_cases hs : halted s = true · refine ⟨[], ?_⟩ @@ -400,7 +400,7 @@ theorem exists_replay_done_final (hsource : source < N) (hwidth : N ≤ 2 ^ widt (by simp [initial, hsource]) intro n induction n using Nat.strong_induction_on with - | h n ih => + | ind n ih => intro s hr hi hb hh hna by_cases hdone : s.phase = .done ∧ s.finalScan = true · refine ⟨[], hdone.1, hdone.2, ?_⟩ diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Potential.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Potential.lean index d7b2c6355..b3f3b0a73 100644 --- a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Potential.lean +++ b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Potential.lean @@ -519,7 +519,7 @@ private theorem one_le_priority (i : Fin g) : 1 ≤ P.priority i := by suffices ∀ k : ℕ, ∀ i : Fin g, g - 1 - i.val = k → 1 ≤ P.priority i from this _ i rfl intro k induction k using Nat.strong_induction_on with - | h k ih => + | ind k ih => intro i hik rw [P.priority_eq] suffices 0 ≤ ∑ j : Fin g, if i < j then P.priority j * |P.gateWeight j i| else 0 by linarith @@ -566,7 +566,7 @@ theorem priority_le_pow {W : ℝ} (hW0 : 0 ≤ W) suffices ∀ m : ℕ, ∀ i : Fin g, g - 1 - i.val = m → P.priority i ≤ (W + 1) ^ m from this _ i rfl intro m induction m using Nat.strong_induction_on with - | h m ih => + | ind m ih => intro i him rw [P.priority_eq, ← one_add_mul_sum_geom W m] have hsum : (∑ j : Fin g, if i < j then P.priority j * |P.gateWeight j i| else 0) ≤ diff --git a/Complexity/Computability/Circuit/Frontier/BranchingProgram.lean b/Complexity/Computability/Circuit/Frontier/BranchingProgram.lean index b30615577..5cbed26fb 100644 --- a/Complexity/Computability/Circuit/Frontier/BranchingProgram.lean +++ b/Complexity/Computability/Circuit/Frontier/BranchingProgram.lean @@ -378,7 +378,7 @@ theorem abs_signedCount_accepted_le [Finite ι] [Finite U] [Finite M] (hP : P.Un (hS : RectangleBias S K b) : |signedCount S P.accepted| ≤ 2 * b * P.accepted.ncard + ((K - 1) ^ 2 * P.size : ℕ) := by induction hn : P.accepted.ncard using Nat.strong_induction_on generalizing P with - | h n ih => + | ind n ih => subst hn by_cases hthick : ∃ t ≤ P.length, ∃ x ∈ P.accepted, K ≤ (P.sweep.pastSide t x).ncard ∧ K ≤ (P.sweep.futureSide t x).ncard diff --git a/Complexity/Computability/Circuit/Rational/LaurentReduction.lean b/Complexity/Computability/Circuit/Rational/LaurentReduction.lean index 4c759cc76..9087b74c6 100644 --- a/Complexity/Computability/Circuit/Rational/LaurentReduction.lean +++ b/Complexity/Computability/Circuit/Rational/LaurentReduction.lean @@ -262,7 +262,7 @@ theorem exists_integralFrame {ι : Type*} [Finite ι] this _ U rfl intro k induction k using Nat.strong_induction_on with - | h k ih => + | ind k ih => intro U hdim by_cases hU : U = ⊥ · subst U diff --git a/Complexity/Computability/Circuit/Rational/Wronskian.lean b/Complexity/Computability/Circuit/Rational/Wronskian.lean index 138a37718..58d38adf0 100644 --- a/Complexity/Computability/Circuit/Rational/Wronskian.lean +++ b/Complexity/Computability/Circuit/Rational/Wronskian.lean @@ -513,7 +513,7 @@ lemma low_coefficients_force_zero {K : Type*} [Field K] {h : ℕ} have hi : ∀ m, ∀ j, (f j).natTrailingDegree = m → m < r → c j = 0 := by intro m induction m using Nat.strong_induction_on with - | h m ih => + | ind m ih => intro j hj hmr have hs : (∑ k, c k • f k).coeff m = c j * (f j).coeff m := by simp only [finsetSum_coeff, coeff_smul, smul_eq_mul] diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Bounds.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Bounds.lean index 151c6653d..9f9db3c2d 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Bounds.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Bounds.lean @@ -88,7 +88,7 @@ theorem choose_inWindow {input : List Bool} (Inv : (Fin k → List Bool) → Pro ∀ ws out, Inv ws → p.head = wordsCfg input (some .choose) ws out → p.InWindow s := by intro n induction n using Nat.strong_induction_on with - | h n ih => + | ind n ih => intro p hlen ws out hInv hhead by_cases hzero : p.length = 0 · rintro _ ⟨j, rfl⟩ i diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Compiler.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Compiler.lean index 6671eeb2c..9e2d0b66c 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Compiler.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Compiler.lean @@ -153,7 +153,7 @@ theorem choose_output (a : α) (p : R.machine.RunPath (enc a)) (s : σ) p.last.output = out ++ [M.accept s'] := by intro n induction n using Nat.strong_induction_on with - | h n ih => + | ind n ih => intro p hn s hs flag out hhead hhalt have hpos : 0 < p.length := by by_contra hz diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Termination.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Termination.lean index 052bf6dd7..af1d2bb23 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Termination.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Termination.lean @@ -75,7 +75,7 @@ theorem choose_haltsFrom {input : List Bool} (Inv : (Fin k → List Bool) → Pr ∃ t, HaltsFrom I P F C (wordsCfg input (some .choose) ws out) t := by intro n induction n using Nat.strong_induction_on with - | h n ih => + | ind n ih => intro ws hr hInv out have branches : ∀ b, ∃ t, HaltsFrom I P F C (wordsCfg input (some (.pass b (P b).q₀)) ws out) t := by diff --git a/Complexity/Computability/WordRAM/GhostLoop.lean b/Complexity/Computability/WordRAM/GhostLoop.lean index 8f3b8e7d3..6e2c03c9f 100644 --- a/Complexity/Computability/WordRAM/GhostLoop.lean +++ b/Complexity/Computability/WordRAM/GhostLoop.lean @@ -44,7 +44,7 @@ theorem ExecWithin.loop_invariant_state {B : Basis} {r w T : ℕ} {σ : Type*} I s' y ∧ ¬cond.Holds y := by intro n induction n using Nat.strong_induction_on with - | h n ih => + | ind n ih => intro s x hμ hI by_cases hc : cond.Holds x · obtain ⟨s₁, y, hy, hIy, hdec⟩ := hbody s x hI hc diff --git a/Complexity/Foundations/Combinatorics/FunctionalGraph/ForestSegments.lean b/Complexity/Foundations/Combinatorics/FunctionalGraph/ForestSegments.lean index c194d2abb..f06913384 100644 --- a/Complexity/Foundations/Combinatorics/FunctionalGraph/ForestSegments.lean +++ b/Complexity/Foundations/Combinatorics/FunctionalGraph/ForestSegments.lean @@ -174,7 +174,7 @@ theorem forest_hull_partition {L : ℕ} (hL : 0 < L) f^[t] a ∈ forestMarks f H ∨ ∃ b d i, IsForestEdge f H b d ∧ d ≤ 2 * L ∧ i < d ∧ f^[i] b = f^[t] a := by induction t using Nat.strong_induction_on with - | h t ih => + | ind t ih => intro a ha ht by_cases hz : t = 0 · subst t diff --git a/Complexity/Foundations/NumberTheory/Harmonic.lean b/Complexity/Foundations/NumberTheory/Harmonic.lean index 6460f4cb9..bb9b8ffa8 100644 --- a/Complexity/Foundations/NumberTheory/Harmonic.lean +++ b/Complexity/Foundations/NumberTheory/Harmonic.lean @@ -78,7 +78,7 @@ theorem two_mul_sum_add_one_mul_harmonic (m : ℕ) : theorem harmonic_le_log_add_one (n : ℕ) : harmonic n ≤ (Nat.log 2 n : ℚ) + 1 := by induction n using Nat.strong_induction_on with - | h n ih => + | ind n ih => rcases lt_or_ge n 2 with hn2 | hn2 · interval_cases n <;> norm_num [harmonic] · set half := n / 2 diff --git a/Complexity/Foundations/NumberTheory/PrimeCounting.lean b/Complexity/Foundations/NumberTheory/PrimeCounting.lean index 6081bc9f0..63f3b2a67 100644 --- a/Complexity/Foundations/NumberTheory/PrimeCounting.lean +++ b/Complexity/Foundations/NumberTheory/PrimeCounting.lean @@ -143,7 +143,7 @@ theorem lcmUpto_add_le {m n : ℕ} (h : n ≤ m) : theorem two_mul_lcmUpto_le_four_pow (n : ℕ) (hn : 1 ≤ n) : 2 * Nat.lcmUpto n ≤ 4 ^ n := by induction n using Nat.strong_induction_on with - | h n ihn => + | ind n ihn => rcases le_or_gt n 2 with hn2 | hn2 · interval_cases n <;> decide · rcases n.even_or_odd with ⟨m, rfl⟩ | ⟨m, rfl⟩