From 719a66720a552359acf37aca2eb83681a7ff42f8 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 8 May 2026 00:16:03 -0400
Subject: [PATCH 01/12] wip: basic functional queue in lean

---
 .../Lean/FunctionalQueue/FunctionalQueue.lean | 123 ++++++++++++++++++
 1 file changed, 123 insertions(+)
 create mode 100644 Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean

diff --git a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
new file mode 100644
index 000000000..c21c037ad
--- /dev/null
+++ b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
@@ -0,0 +1,123 @@
+
+
+module
+
+/- public import Cslib.Algorithms.Lean.TimeM -/
+
+/-!
+  The simplest functional queue. -/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.Lean
+
+universe u
+
+@[ext] structure RawFunctionalQueue (α : Type u) where
+  front : List α
+  back : List α
+
+@[simp] def invariant {α : Type u} (q : RawFunctionalQueue α) : Prop :=
+  q.front = [] → q.back = []
+
+@[simp] def ghostList {α : Type u} (q : RawFunctionalQueue α) : List α :=
+  List.append q.front q.back.reverse
+
+@[simp] def empty {α : Type u} : RawFunctionalQueue α := ⟨ [], [] ⟩
+
+@[simp] def rebalance {α : Type u} (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
+  match q.front with
+  | [] => ⟨ (q.back).reverse, [] ⟩
+  | _ => q
+
+theorem rebalanceInvert {α : Type u} (q : RawFunctionalQueue α) : (rebalance q).front = [] → q = empty := by
+  intro h_reb
+  generalize gen_reb : (rebalance q).front = q_reb_hd
+  obtain ⟨ q_hd, q_tl ⟩ := q
+  simp; simp at h_reb
+  induction q_reb_hd with
+  | nil =>
+    induction q_hd with
+    | nil =>
+      simp at h_reb
+      grind only
+    | cons q_hd_hd q_hd_tl q_hd_hyp =>
+      grind only
+  | cons q_reb_hd_hd q_reb_hd_tl q_reb_hd_hyp =>
+    induction q_hd with
+    | nil =>
+      simp at h_reb
+      grind only
+    | cons _ _ _ =>
+      simp at h_reb
+
+theorem rebalanceInvariant {α : Type u} {q : RawFunctionalQueue α} : invariant (rebalance q) := by
+  generalize h_front : q.front = l
+  induction l with
+  | nil => simp; rw [h_front]; simp
+  | cons x tl h_cons =>
+    simp; rw [h_front]; simp; rw [h_front]; grind only
+
+@[simp] theorem rebalanceIdempotent {α : Type u} (q : RawFunctionalQueue α) : rebalance (rebalance q) = rebalance q := by
+  generalize h : (rebalance q).front = hd
+  induction hd with
+  | nil =>
+    have h_q_empty : q = empty := rebalanceInvert q h
+    rw [h_q_empty]
+    simp
+  | cons hd_hd hd_tl hd_hyp =>
+    generalize def_q2 : rebalance q = q2
+    rw [def_q2] at h
+    simp
+    rw [h]
+
+@[simp] theorem rebalancePreserveGhost {α : Type u} (q : RawFunctionalQueue α) : ghostList (rebalance q) = ghostList q := by
+  generalize def_hd : q.front = hd
+  induction hd with
+  | nil => simp; rw [def_hd]; simp
+  | cons hd_hd hd_tl h_ind =>
+    simp; rw [def_hd]; simp; grind only [=_ List.cons_append]
+
+@[simp] def push {α : Type u} (x : α) (q : RawFunctionalQueue α) : (RawFunctionalQueue α) :=
+  let q : RawFunctionalQueue α := ⟨ q.front, x :: q.back ⟩
+  rebalance q
+
+theorem appendInvariant {α : Type u} (x : α) (q : RawFunctionalQueue α)
+  : invariant q → invariant (push x q) := by
+  intro h
+  rw [push]
+  apply rebalanceInvariant
+
+theorem appendGhost {α : Type u} (x : α) (q : RawFunctionalQueue α) : ghostList (push x q) = ghostList q ++ [x] := by
+  generalize h_front : q.front = l
+  cases l with
+  | nil =>
+    simp; rw [h_front]; simp
+  | cons l_hd l_tl =>
+    rw [push]
+    rw [rebalancePreserveGhost]
+    rw [ghostList]
+    simp
+
+def pop {α : Type} (q : RawFunctionalQueue α) : Option (α × RawFunctionalQueue α) :=
+  match q.front with
+  | [] => none
+  | x :: tl =>
+    some (x, rebalance ⟨ tl, q.back ⟩)
+
+theorem pop_invariant {α : Type} (x : α) (q q2 : RawFunctionalQueue α) :
+    invariant q → pop q = some (x, q2) → invariant q2 := by
+  intro hq hpop_is_some
+  simp at hq
+  rw [pop] at hpop_is_some
+  generalize h_front : q.front = l
+  cases l with
+  | nil =>
+    rw [h_front] at hpop_is_some; simp at hpop_is_some
+  | cons _ _ =>
+    rw [h_front] at hpop_is_some
+    simp only at hpop_is_some
+    obtain ⟨ rfl, rfl ⟩ := hpop_is_some
+    apply rebalanceInvariant
+
+end Cslib.Algorithms.Lean

From 88bd163102a0c4d0df838a33672d5deee1706a17 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 8 May 2026 21:58:50 -0400
Subject: [PATCH 02/12] remove @[simp] from some defs

---
 .../Lean/FunctionalQueue/FunctionalQueue.lean | 33 +++++++++----------
 1 file changed, 16 insertions(+), 17 deletions(-)

diff --git a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
index c21c037ad..cceb8d8dc 100644
--- a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
+++ b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
@@ -23,24 +23,24 @@ universe u
 @[simp] def ghostList {α : Type u} (q : RawFunctionalQueue α) : List α :=
   List.append q.front q.back.reverse
 
-@[simp] def empty {α : Type u} : RawFunctionalQueue α := ⟨ [], [] ⟩
+def empty {α : Type u} : RawFunctionalQueue α := ⟨ [], [] ⟩
 
-@[simp] def rebalance {α : Type u} (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
+def rebalance {α : Type u} (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
   match q.front with
   | [] => ⟨ (q.back).reverse, [] ⟩
   | _ => q
 
 theorem rebalanceInvert {α : Type u} (q : RawFunctionalQueue α) : (rebalance q).front = [] → q = empty := by
   intro h_reb
+  rw [empty]
   generalize gen_reb : (rebalance q).front = q_reb_hd
   obtain ⟨ q_hd, q_tl ⟩ := q
-  simp; simp at h_reb
+  simp [rebalance] at h_reb
   induction q_reb_hd with
   | nil =>
     induction q_hd with
     | nil =>
-      simp at h_reb
-      grind only
+      simp at h_reb; simp [rebalance] at gen_reb; rw [h_reb]
     | cons q_hd_hd q_hd_tl q_hd_hyp =>
       grind only
   | cons q_reb_hd_hd q_reb_hd_tl q_reb_hd_hyp =>
@@ -51,34 +51,33 @@ theorem rebalanceInvert {α : Type u} (q : RawFunctionalQueue α) : (rebalance q
     | cons _ _ _ =>
       simp at h_reb
 
-theorem rebalanceInvariant {α : Type u} {q : RawFunctionalQueue α} : invariant (rebalance q) := by
+@[simp] theorem rebalanceInvariant {α : Type u} {q : RawFunctionalQueue α} : invariant (rebalance q) := by
   generalize h_front : q.front = l
   induction l with
-  | nil => simp; rw [h_front]; simp
+  | nil => simp [rebalance]; rw [h_front]; simp
   | cons x tl h_cons =>
-    simp; rw [h_front]; simp; rw [h_front]; grind only
+    simp [rebalance]; rw [h_front]; simp; rw [h_front]; grind only
 
 @[simp] theorem rebalanceIdempotent {α : Type u} (q : RawFunctionalQueue α) : rebalance (rebalance q) = rebalance q := by
   generalize h : (rebalance q).front = hd
   induction hd with
   | nil =>
     have h_q_empty : q = empty := rebalanceInvert q h
-    rw [h_q_empty]
-    simp
+    simp [rebalance]; rw [h_q_empty]; simp [empty]
   | cons hd_hd hd_tl hd_hyp =>
     generalize def_q2 : rebalance q = q2
     rw [def_q2] at h
-    simp
+    simp [rebalance]
     rw [h]
 
 @[simp] theorem rebalancePreserveGhost {α : Type u} (q : RawFunctionalQueue α) : ghostList (rebalance q) = ghostList q := by
   generalize def_hd : q.front = hd
   induction hd with
-  | nil => simp; rw [def_hd]; simp
+  | nil => simp [rebalance]; rw [def_hd]; simp
   | cons hd_hd hd_tl h_ind =>
-    simp; rw [def_hd]; simp; grind only [=_ List.cons_append]
+    simp [rebalance]; rw [def_hd]; simp; grind only [=_ List.cons_append]
 
-@[simp] def push {α : Type u} (x : α) (q : RawFunctionalQueue α) : (RawFunctionalQueue α) :=
+def push {α : Type u} (x : α) (q : RawFunctionalQueue α) : (RawFunctionalQueue α) :=
   let q : RawFunctionalQueue α := ⟨ q.front, x :: q.back ⟩
   rebalance q
 
@@ -92,20 +91,20 @@ theorem appendGhost {α : Type u} (x : α) (q : RawFunctionalQueue α) : ghostLi
   generalize h_front : q.front = l
   cases l with
   | nil =>
-    simp; rw [h_front]; simp
+    simp [push, rebalance]; rw [h_front]; simp
   | cons l_hd l_tl =>
     rw [push]
     rw [rebalancePreserveGhost]
     rw [ghostList]
     simp
 
-def pop {α : Type} (q : RawFunctionalQueue α) : Option (α × RawFunctionalQueue α) :=
+def pop {α : Type u} (q : RawFunctionalQueue α) : Option (α × RawFunctionalQueue α) :=
   match q.front with
   | [] => none
   | x :: tl =>
     some (x, rebalance ⟨ tl, q.back ⟩)
 
-theorem pop_invariant {α : Type} (x : α) (q q2 : RawFunctionalQueue α) :
+theorem pop_invariant {α : Type u} (x : α) (q q2 : RawFunctionalQueue α) :
     invariant q → pop q = some (x, q2) → invariant q2 := by
   intro hq hpop_is_some
   simp at hq

From ebe0603575e4ab00612f41b8472f3b49845d5ef1 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 8 May 2026 22:37:58 -0400
Subject: [PATCH 03/12] simplify proofs and cleanup

---
 Cslib.lean                                    |   1 +
 .../Lean/FunctionalQueue/FunctionalQueue.lean | 164 +++++++++---------
 2 files changed, 85 insertions(+), 80 deletions(-)

diff --git a/Cslib.lean b/Cslib.lean
index 92a251cdf..9cf0abfc0 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -1,5 +1,6 @@
 module  -- shake: keep-all
 
+public import Cslib.Algorithms.Lean.FunctionalQueue.FunctionalQueue
 public import Cslib.Algorithms.Lean.MergeSort.MergeSort
 public import Cslib.Algorithms.Lean.TimeM
 public import Cslib.Computability.Automata.Acceptors.Acceptor
diff --git a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
index cceb8d8dc..c51a63deb 100644
--- a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
+++ b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
@@ -1,14 +1,23 @@
-
+/-
+Copyright (c) 2026 Simon Cruanes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Simon Cruanes
+-/
 
 module
 
-/- public import Cslib.Algorithms.Lean.TimeM -/
+import Cslib.Init
 
 /-!
-  The simplest functional queue. -/
+# Functional Queue
+
+A classic two-list queue with amortized O(1) `push` and `pop`.
+-/
 
 @[expose] public section
 
+set_option autoImplicit false
+
 namespace Cslib.Algorithms.Lean
 
 universe u
@@ -17,87 +26,64 @@ universe u
   front : List α
   back : List α
 
-@[simp] def invariant {α : Type u} (q : RawFunctionalQueue α) : Prop :=
+/-- Well-formedness: if front is empty, back must be empty too. -/
+def invariant {α : Type u} (q : RawFunctionalQueue α) : Prop :=
   q.front = [] → q.back = []
 
-@[simp] def ghostList {α : Type u} (q : RawFunctionalQueue α) : List α :=
+/-- The logical contents of the queue: `front ++ back.reverse`. -/
+def ghostList {α : Type u} (q : RawFunctionalQueue α) : List α :=
   List.append q.front q.back.reverse
 
+/-- The empty queue. -/
 def empty {α : Type u} : RawFunctionalQueue α := ⟨ [], [] ⟩
 
+/-- Internal: rebalance by moving `back.reverse` to `front` when `front` is empty. -/
 def rebalance {α : Type u} (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
   match q.front with
   | [] => ⟨ (q.back).reverse, [] ⟩
   | _ => q
 
-theorem rebalanceInvert {α : Type u} (q : RawFunctionalQueue α) : (rebalance q).front = [] → q = empty := by
-  intro h_reb
-  rw [empty]
-  generalize gen_reb : (rebalance q).front = q_reb_hd
-  obtain ⟨ q_hd, q_tl ⟩ := q
-  simp [rebalance] at h_reb
-  induction q_reb_hd with
-  | nil =>
-    induction q_hd with
-    | nil =>
-      simp at h_reb; simp [rebalance] at gen_reb; rw [h_reb]
-    | cons q_hd_hd q_hd_tl q_hd_hyp =>
-      grind only
-  | cons q_reb_hd_hd q_reb_hd_tl q_reb_hd_hyp =>
-    induction q_hd with
-    | nil =>
-      simp at h_reb
-      grind only
-    | cons _ _ _ =>
-      simp at h_reb
-
-@[simp] theorem rebalanceInvariant {α : Type u} {q : RawFunctionalQueue α} : invariant (rebalance q) := by
-  generalize h_front : q.front = l
-  induction l with
-  | nil => simp [rebalance]; rw [h_front]; simp
-  | cons x tl h_cons =>
-    simp [rebalance]; rw [h_front]; simp; rw [h_front]; grind only
-
-@[simp] theorem rebalanceIdempotent {α : Type u} (q : RawFunctionalQueue α) : rebalance (rebalance q) = rebalance q := by
-  generalize h : (rebalance q).front = hd
-  induction hd with
-  | nil =>
-    have h_q_empty : q = empty := rebalanceInvert q h
-    simp [rebalance]; rw [h_q_empty]; simp [empty]
-  | cons hd_hd hd_tl hd_hyp =>
-    generalize def_q2 : rebalance q = q2
-    rw [def_q2] at h
-    simp [rebalance]
-    rw [h]
-
-@[simp] theorem rebalancePreserveGhost {α : Type u} (q : RawFunctionalQueue α) : ghostList (rebalance q) = ghostList q := by
-  generalize def_hd : q.front = hd
-  induction hd with
-  | nil => simp [rebalance]; rw [def_hd]; simp
-  | cons hd_hd hd_tl h_ind =>
-    simp [rebalance]; rw [def_hd]; simp; grind only [=_ List.cons_append]
-
-def push {α : Type u} (x : α) (q : RawFunctionalQueue α) : (RawFunctionalQueue α) :=
-  let q : RawFunctionalQueue α := ⟨ q.front, x :: q.back ⟩
-  rebalance q
-
-theorem appendInvariant {α : Type u} (x : α) (q : RawFunctionalQueue α)
-  : invariant q → invariant (push x q) := by
+theorem rebalanceInvert {α : Type u} (q : RawFunctionalQueue α) :
+    (rebalance q).front = [] → q = empty := by
+  intro h
+  obtain ⟨f, b⟩ := q
+  simp only [rebalance, empty] at h ⊢
+  split at h <;> simp_all
+
+theorem rebalanceInvariant {α : Type u} {q : RawFunctionalQueue α} :
+    invariant (rebalance q) := by
+  obtain ⟨f, b⟩ := q
+  simp [rebalance, invariant]
+  split <;> grind
+
+@[simp] theorem rebalanceIdempotent {α : Type u} (q : RawFunctionalQueue α) :
+    rebalance (rebalance q) = rebalance q := by
+  obtain ⟨f, b⟩ := q
+  simp [rebalance]
+  split <;> grind
+
+@[simp] theorem rebalancePreserveGhost {α : Type u} (q : RawFunctionalQueue α) :
+    ghostList (rebalance q) = ghostList q := by
+  obtain ⟨f, b⟩ := q
+  simp [rebalance, ghostList]
+  split <;> grind [List.reverse_append]
+
+/-- Enqueue an element. -/
+def push {α : Type u} (x : α) (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
+  rebalance ⟨ q.front, x :: q.back ⟩
+
+theorem pushInvariant {α : Type u} (x : α) (q : RawFunctionalQueue α) :
+    invariant q → invariant (push x q) := by
   intro h
   rw [push]
   apply rebalanceInvariant
 
-theorem appendGhost {α : Type u} (x : α) (q : RawFunctionalQueue α) : ghostList (push x q) = ghostList q ++ [x] := by
-  generalize h_front : q.front = l
-  cases l with
-  | nil =>
-    simp [push, rebalance]; rw [h_front]; simp
-  | cons l_hd l_tl =>
-    rw [push]
-    rw [rebalancePreserveGhost]
-    rw [ghostList]
-    simp
+theorem pushGhost {α : Type u} (x : α) (q : RawFunctionalQueue α) :
+    ghostList (push x q) = ghostList q ++ [x] := by
+  rw [push, rebalancePreserveGhost, ghostList]
+  simp [ghostList, List.append_assoc]
 
+/-- Dequeue: returns `some (head, remaining)` or `none` if empty. -/
 def pop {α : Type u} (q : RawFunctionalQueue α) : Option (α × RawFunctionalQueue α) :=
   match q.front with
   | [] => none
@@ -106,17 +92,35 @@ def pop {α : Type u} (q : RawFunctionalQueue α) : Option (α × RawFunctionalQ
 
 theorem pop_invariant {α : Type u} (x : α) (q q2 : RawFunctionalQueue α) :
     invariant q → pop q = some (x, q2) → invariant q2 := by
-  intro hq hpop_is_some
-  simp at hq
-  rw [pop] at hpop_is_some
-  generalize h_front : q.front = l
-  cases l with
-  | nil =>
-    rw [h_front] at hpop_is_some; simp at hpop_is_some
-  | cons _ _ =>
-    rw [h_front] at hpop_is_some
-    simp only at hpop_is_some
-    obtain ⟨ rfl, rfl ⟩ := hpop_is_some
-    apply rebalanceInvariant
+  intro hq hpop
+  obtain ⟨f, b⟩ := q
+  simp [invariant] at hq
+  unfold pop at hpop
+  cases f with
+  | nil => simp at hpop
+  | cons y tl =>
+    simp only at hpop
+    obtain ⟨rfl, rfl⟩ := hpop
+    exact rebalanceInvariant
+
+@[simp] theorem emptyInvariant {α : Type u} : invariant (@empty α) := by
+  simp [invariant, empty]
+
+@[simp] theorem emptyGhost {α : Type u} : ghostList (@empty α) = [] := by
+  simp [ghostList, empty]
+
+theorem pop_ghost {α : Type u} {x : α} {q q2 : RawFunctionalQueue α} :
+    invariant q → pop q = some (x, q2) → ghostList q = x :: ghostList q2 := by
+  intro hq hpop
+  obtain ⟨f, b⟩ := q
+  simp [invariant] at hq
+  unfold pop at hpop
+  cases f with
+  | nil => simp at hpop
+  | cons y tl =>
+    simp only at hpop
+    obtain ⟨rfl, rfl⟩ := hpop
+    simp only [rebalancePreserveGhost]
+    simp [ghostList]
 
 end Cslib.Algorithms.Lean

From 0f1a4d6c628b807fa67ba5d01fbb1f049ee6dccc Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 8 May 2026 23:18:25 -0400
Subject: [PATCH 04/12] define queue with invariant

---
 .../Lean/FunctionalQueue/FunctionalQueue.lean | 74 ++++++++++++++-----
 1 file changed, 55 insertions(+), 19 deletions(-)

diff --git a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
index c51a63deb..b0eb395e8 100644
--- a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
+++ b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
@@ -26,6 +26,8 @@ universe u
   front : List α
   back : List α
 
+namespace Raw
+
 /-- Well-formedness: if front is empty, back must be empty too. -/
 def invariant {α : Type u} (q : RawFunctionalQueue α) : Prop :=
   q.front = [] → q.back = []
@@ -35,7 +37,7 @@ def ghostList {α : Type u} (q : RawFunctionalQueue α) : List α :=
   List.append q.front q.back.reverse
 
 /-- The empty queue. -/
-def empty {α : Type u} : RawFunctionalQueue α := ⟨ [], [] ⟩
+def emptyRaw {α : Type u} : RawFunctionalQueue α := ⟨ [], [] ⟩
 
 /-- Internal: rebalance by moving `back.reverse` to `front` when `front` is empty. -/
 def rebalance {α : Type u} (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
@@ -44,10 +46,10 @@ def rebalance {α : Type u} (q : RawFunctionalQueue α) : RawFunctionalQueue α
   | _ => q
 
 theorem rebalanceInvert {α : Type u} (q : RawFunctionalQueue α) :
-    (rebalance q).front = [] → q = empty := by
+    (rebalance q).front = [] → q = emptyRaw := by
   intro h
   obtain ⟨f, b⟩ := q
-  simp only [rebalance, empty] at h ⊢
+  simp only [rebalance, emptyRaw] at h ⊢
   split at h <;> simp_all
 
 theorem rebalanceInvariant {α : Type u} {q : RawFunctionalQueue α} :
@@ -69,33 +71,33 @@ theorem rebalanceInvariant {α : Type u} {q : RawFunctionalQueue α} :
   split <;> grind [List.reverse_append]
 
 /-- Enqueue an element. -/
-def push {α : Type u} (x : α) (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
+def pushRaw {α : Type u} (x : α) (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
   rebalance ⟨ q.front, x :: q.back ⟩
 
 theorem pushInvariant {α : Type u} (x : α) (q : RawFunctionalQueue α) :
-    invariant q → invariant (push x q) := by
+    invariant q → invariant (pushRaw x q) := by
   intro h
-  rw [push]
+  rw [pushRaw]
   apply rebalanceInvariant
 
 theorem pushGhost {α : Type u} (x : α) (q : RawFunctionalQueue α) :
-    ghostList (push x q) = ghostList q ++ [x] := by
-  rw [push, rebalancePreserveGhost, ghostList]
+    ghostList (pushRaw x q) = ghostList q ++ [x] := by
+  rw [pushRaw, rebalancePreserveGhost, ghostList]
   simp [ghostList, List.append_assoc]
 
 /-- Dequeue: returns `some (head, remaining)` or `none` if empty. -/
-def pop {α : Type u} (q : RawFunctionalQueue α) : Option (α × RawFunctionalQueue α) :=
+def popRaw {α : Type u} (q : RawFunctionalQueue α) : Option (α × RawFunctionalQueue α) :=
   match q.front with
   | [] => none
   | x :: tl =>
     some (x, rebalance ⟨ tl, q.back ⟩)
 
-theorem pop_invariant {α : Type u} (x : α) (q q2 : RawFunctionalQueue α) :
-    invariant q → pop q = some (x, q2) → invariant q2 := by
+theorem popInvariant {α : Type u} (x : α) (q q2 : RawFunctionalQueue α) :
+    invariant q → popRaw q = some (x, q2) → invariant q2 := by
   intro hq hpop
   obtain ⟨f, b⟩ := q
   simp [invariant] at hq
-  unfold pop at hpop
+  unfold popRaw at hpop
   cases f with
   | nil => simp at hpop
   | cons y tl =>
@@ -103,18 +105,18 @@ theorem pop_invariant {α : Type u} (x : α) (q q2 : RawFunctionalQueue α) :
     obtain ⟨rfl, rfl⟩ := hpop
     exact rebalanceInvariant
 
-@[simp] theorem emptyInvariant {α : Type u} : invariant (@empty α) := by
-  simp [invariant, empty]
+@[simp] theorem emptyInvariant {α : Type u} : invariant (@emptyRaw α) := by
+  simp [invariant, emptyRaw]
 
-@[simp] theorem emptyGhost {α : Type u} : ghostList (@empty α) = [] := by
-  simp [ghostList, empty]
+@[simp] theorem emptyGhost {α : Type u} : ghostList (@emptyRaw α) = [] := by
+  simp [ghostList, emptyRaw]
 
-theorem pop_ghost {α : Type u} {x : α} {q q2 : RawFunctionalQueue α} :
-    invariant q → pop q = some (x, q2) → ghostList q = x :: ghostList q2 := by
+theorem popGhost {α : Type u} {x : α} {q q2 : RawFunctionalQueue α} :
+    invariant q → popRaw q = some (x, q2) → ghostList q = x :: ghostList q2 := by
   intro hq hpop
   obtain ⟨f, b⟩ := q
   simp [invariant] at hq
-  unfold pop at hpop
+  unfold popRaw at hpop
   cases f with
   | nil => simp at hpop
   | cons y tl =>
@@ -123,4 +125,38 @@ theorem pop_ghost {α : Type u} {x : α} {q q2 : RawFunctionalQueue α} :
     simp only [rebalancePreserveGhost]
     simp [ghostList]
 
+end Raw
+
+/-- A functional queue with invariant. -/
+structure FunctionalQueue (α : Type u) where
+  q : RawFunctionalQueue α
+  inv : Raw.invariant q
+
+def empty {α : Type u} : FunctionalQueue α := ⟨ @Raw.emptyRaw α, Raw.emptyInvariant ⟩
+
+def push {α : Type u} (x : α) (q : FunctionalQueue α) : FunctionalQueue α :=
+  ⟨ Raw.pushRaw x q.q, Raw.pushInvariant x q.q q.inv ⟩
+
+def pop {α : Type u} (q : FunctionalQueue α) : Option (α × FunctionalQueue α) :=
+  match h : Raw.popRaw q.q with
+  | none => none
+  | some (x, q2) =>
+    some (x, ⟨ q2, Raw.popInvariant x q.q q2 q.inv h ⟩)
+
+@[simp] def ghostList {α : Type u} (q : FunctionalQueue α) : List α := Raw.ghostList q.q
+
+theorem pushGhost {α : Type u} (x : α) (q : FunctionalQueue α) :
+    ghostList (push x q) = ghostList q ++ [x] :=
+  Raw.pushGhost x q.q
+
+theorem popGhost {α : Type u} {x : α} {q q2 : FunctionalQueue α} :
+    pop q = some (x, q2) → ghostList q = x :: ghostList q2 := by
+  intro h
+  simp only [pop, ghostList] at h ⊢
+  split at h
+  · simp only [reduceCtorEq] at h
+  · rename_i x2 q2' heq
+    obtain ⟨ h1, h2 ⟩ := h
+    apply @Raw.popGhost α x q.q q2' q.inv; grind
+
 end Cslib.Algorithms.Lean

From 47549d1980e05c844fd562ee1bf96c4c3a269e06 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 8 May 2026 23:36:13 -0400
Subject: [PATCH 05/12] add Raw namespace

---
 .../Lean/FunctionalQueue/FunctionalQueue.lean | 58 ++++++++++---------
 1 file changed, 30 insertions(+), 28 deletions(-)

diff --git a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
index b0eb395e8..db2f31f78 100644
--- a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
+++ b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
@@ -22,7 +22,7 @@ namespace Cslib.Algorithms.Lean
 
 universe u
 
-@[ext] structure RawFunctionalQueue (α : Type u) where
+structure RawFunctionalQueue (α : Type u) where
   front : List α
   back : List α
 
@@ -37,7 +37,7 @@ def ghostList {α : Type u} (q : RawFunctionalQueue α) : List α :=
   List.append q.front q.back.reverse
 
 /-- The empty queue. -/
-def emptyRaw {α : Type u} : RawFunctionalQueue α := ⟨ [], [] ⟩
+def empty {α : Type u} : RawFunctionalQueue α := ⟨ [], [] ⟩
 
 /-- Internal: rebalance by moving `back.reverse` to `front` when `front` is empty. -/
 def rebalance {α : Type u} (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
@@ -46,10 +46,10 @@ def rebalance {α : Type u} (q : RawFunctionalQueue α) : RawFunctionalQueue α
   | _ => q
 
 theorem rebalanceInvert {α : Type u} (q : RawFunctionalQueue α) :
-    (rebalance q).front = [] → q = emptyRaw := by
+    (rebalance q).front = [] → q = Raw.empty := by
   intro h
   obtain ⟨f, b⟩ := q
-  simp only [rebalance, emptyRaw] at h ⊢
+  simp only [rebalance, Raw.empty] at h ⊢
   split at h <;> simp_all
 
 theorem rebalanceInvariant {α : Type u} {q : RawFunctionalQueue α} :
@@ -71,33 +71,33 @@ theorem rebalanceInvariant {α : Type u} {q : RawFunctionalQueue α} :
   split <;> grind [List.reverse_append]
 
 /-- Enqueue an element. -/
-def pushRaw {α : Type u} (x : α) (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
+def push {α : Type u} (x : α) (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
   rebalance ⟨ q.front, x :: q.back ⟩
 
 theorem pushInvariant {α : Type u} (x : α) (q : RawFunctionalQueue α) :
-    invariant q → invariant (pushRaw x q) := by
+    invariant q → invariant (push x q) := by
   intro h
-  rw [pushRaw]
+  rw [push]
   apply rebalanceInvariant
 
 theorem pushGhost {α : Type u} (x : α) (q : RawFunctionalQueue α) :
-    ghostList (pushRaw x q) = ghostList q ++ [x] := by
-  rw [pushRaw, rebalancePreserveGhost, ghostList]
+    ghostList (push x q) = ghostList q ++ [x] := by
+  rw [push, rebalancePreserveGhost, ghostList]
   simp [ghostList, List.append_assoc]
 
 /-- Dequeue: returns `some (head, remaining)` or `none` if empty. -/
-def popRaw {α : Type u} (q : RawFunctionalQueue α) : Option (α × RawFunctionalQueue α) :=
+def pop {α : Type u} (q : RawFunctionalQueue α) : Option (α × RawFunctionalQueue α) :=
   match q.front with
   | [] => none
   | x :: tl =>
     some (x, rebalance ⟨ tl, q.back ⟩)
 
 theorem popInvariant {α : Type u} (x : α) (q q2 : RawFunctionalQueue α) :
-    invariant q → popRaw q = some (x, q2) → invariant q2 := by
+    invariant q → pop q = some (x, q2) → invariant q2 := by
   intro hq hpop
   obtain ⟨f, b⟩ := q
   simp [invariant] at hq
-  unfold popRaw at hpop
+  unfold pop at hpop
   cases f with
   | nil => simp at hpop
   | cons y tl =>
@@ -105,18 +105,18 @@ theorem popInvariant {α : Type u} (x : α) (q q2 : RawFunctionalQueue α) :
     obtain ⟨rfl, rfl⟩ := hpop
     exact rebalanceInvariant
 
-@[simp] theorem emptyInvariant {α : Type u} : invariant (@emptyRaw α) := by
-  simp [invariant, emptyRaw]
+@[simp] theorem emptyInvariant {α : Type u} : invariant (@Raw.empty α) := by
+  simp [invariant, Raw.empty]
 
-@[simp] theorem emptyGhost {α : Type u} : ghostList (@emptyRaw α) = [] := by
-  simp [ghostList, emptyRaw]
+@[simp] theorem emptyGhost {α : Type u} : ghostList (@Raw.empty α) = [] := by
+  simp [ghostList, Raw.empty]
 
 theorem popGhost {α : Type u} {x : α} {q q2 : RawFunctionalQueue α} :
-    invariant q → popRaw q = some (x, q2) → ghostList q = x :: ghostList q2 := by
+    invariant q → pop q = some (x, q2) → ghostList q = x :: ghostList q2 := by
   intro hq hpop
   obtain ⟨f, b⟩ := q
   simp [invariant] at hq
-  unfold popRaw at hpop
+  unfold pop at hpop
   cases f with
   | nil => simp at hpop
   | cons y tl =>
@@ -128,26 +128,28 @@ theorem popGhost {α : Type u} {x : α} {q q2 : RawFunctionalQueue α} :
 end Raw
 
 /-- A functional queue with invariant. -/
+@[ext]
 structure FunctionalQueue (α : Type u) where
-  q : RawFunctionalQueue α
-  inv : Raw.invariant q
+  raw : RawFunctionalQueue α
+  inv : Raw.invariant raw
 
-def empty {α : Type u} : FunctionalQueue α := ⟨ @Raw.emptyRaw α, Raw.emptyInvariant ⟩
+def empty {α : Type u} : FunctionalQueue α := ⟨ @Raw.empty α, Raw.emptyInvariant ⟩
 
 def push {α : Type u} (x : α) (q : FunctionalQueue α) : FunctionalQueue α :=
-  ⟨ Raw.pushRaw x q.q, Raw.pushInvariant x q.q q.inv ⟩
+  ⟨ Raw.push x q.raw, Raw.pushInvariant x q.raw q.inv ⟩
 
 def pop {α : Type u} (q : FunctionalQueue α) : Option (α × FunctionalQueue α) :=
-  match h : Raw.popRaw q.q with
+  match h : Raw.pop q.raw with
   | none => none
   | some (x, q2) =>
-    some (x, ⟨ q2, Raw.popInvariant x q.q q2 q.inv h ⟩)
+    some (x, ⟨ q2, Raw.popInvariant x q.raw q2 q.inv h ⟩)
 
-@[simp] def ghostList {α : Type u} (q : FunctionalQueue α) : List α := Raw.ghostList q.q
+/-- project to a list view, an ordered sequence of elements -/
+def ghostList {α : Type u} (q : FunctionalQueue α) : List α := Raw.ghostList q.raw
 
 theorem pushGhost {α : Type u} (x : α) (q : FunctionalQueue α) :
     ghostList (push x q) = ghostList q ++ [x] :=
-  Raw.pushGhost x q.q
+  Raw.pushGhost x q.raw
 
 theorem popGhost {α : Type u} {x : α} {q q2 : FunctionalQueue α} :
     pop q = some (x, q2) → ghostList q = x :: ghostList q2 := by
@@ -156,7 +158,7 @@ theorem popGhost {α : Type u} {x : α} {q q2 : FunctionalQueue α} :
   split at h
   · simp only [reduceCtorEq] at h
   · rename_i x2 q2' heq
-    obtain ⟨ h1, h2 ⟩ := h
-    apply @Raw.popGhost α x q.q q2' q.inv; grind
+    obtain ⟨h1, h2⟩ := h
+    exact @Raw.popGhost α x q.raw q2' q.inv heq
 
 end Cslib.Algorithms.Lean

From a9def5302e82329118414205a0fec46bb3107d6d Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 9 May 2026 22:14:15 -0400
Subject: [PATCH 06/12] wip: amortized analysis

---
 Cslib.lean                                    |  1 +
 Cslib/Algorithms/Lean/Amortized.lean          | 31 ++++++++++++
 .../Lean/FunctionalQueue/FunctionalQueue.lean | 48 ++++++++++++++++++-
 3 files changed, 78 insertions(+), 2 deletions(-)
 create mode 100644 Cslib/Algorithms/Lean/Amortized.lean

diff --git a/Cslib.lean b/Cslib.lean
index 9cf0abfc0..8b1715b2d 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -3,6 +3,7 @@ module  -- shake: keep-all
 public import Cslib.Algorithms.Lean.FunctionalQueue.FunctionalQueue
 public import Cslib.Algorithms.Lean.MergeSort.MergeSort
 public import Cslib.Algorithms.Lean.TimeM
+public import Cslib.Algorithms.Lean.Amortized
 public import Cslib.Computability.Automata.Acceptors.Acceptor
 public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
 public import Cslib.Computability.Automata.DA.Basic
diff --git a/Cslib/Algorithms/Lean/Amortized.lean b/Cslib/Algorithms/Lean/Amortized.lean
new file mode 100644
index 000000000..7d111cdcc
--- /dev/null
+++ b/Cslib/Algorithms/Lean/Amortized.lean
@@ -0,0 +1,31 @@
+
+/-
+Copyright (c) 2026 Simon Cruanes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Simon Cruanes
+-/
+
+module
+
+import Cslib.Init
+
+/-!
+# Amortized cost analysis
+
+This complements `TimeM` in the cases where amortized costs are necessary.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.Lean.Amortized
+
+/-- Physicist method: a potential (lower bound on savings) defined on a
+    data structure -/
+class Potential α where
+  /-- non-negative potential. Initial potential should be 0.
+      [Okasaki, *Purely Functional Data Structures*, 1996][okasaki1996] -/
+  potential : α → Nat
+
+end Cslib.Algorithms.Lean.Amortized
+
+end
diff --git a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
index db2f31f78..fc3284420 100644
--- a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
+++ b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
@@ -7,19 +7,28 @@ Authors: Simon Cruanes
 module
 
 import Cslib.Init
+public import Cslib.Algorithms.Lean.Amortized
 
 /-!
 # Functional Queue
 
 A classic two-list queue with amortized O(1) `push` and `pop`.
--/
 
-@[expose] public section
+The representation uses two lists: a front list (for dequeue) and a back list
+(for enqueue). When the front list becomes empty, the back list is reversed
+and becomes the new front. This yields amortized O(1) operations.
+
+## References
+
+* [Okasaki, *Purely Functional Data Structures*, 1996][okasaki1996]
+-/
 
 set_option autoImplicit false
 
 namespace Cslib.Algorithms.Lean
 
+@[expose] public section
+
 universe u
 
 structure RawFunctionalQueue (α : Type u) where
@@ -127,6 +136,39 @@ theorem popGhost {α : Type u} {x : α} {q q2 : RawFunctionalQueue α} :
 
 end Raw
 
+namespace Complexity
+
+def potential {α : Type u} (q : RawFunctionalQueue α) : Nat :=
+  q.back.length
+
+instance functionalQueuePotential {α : Type u}
+    : Amortized.Potential (RawFunctionalQueue α) :=
+  ⟨ potential ⟩
+
+inductive queueOp (α : Type u) where
+  | push : α → queueOp α
+  | pop
+
+def applyOp {α : Type u} (op : queueOp α) (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
+  match op with
+  | .push x => Raw.push x q
+  | .pop =>
+    match Raw.pop q with
+    | none => q
+    | some (_, q2) => q2
+
+def applyOps {α : Type u} (ops : List (queueOp α)) (q : RawFunctionalQueue α)
+    : RawFunctionalQueue α :=
+  ops.foldl (fun q op => applyOp op q) q
+
+theorem constantTimeAmortized {α : Type u} :
+    ∀ (q : RawFunctionalQueue α) (ops:List (queueOp α)),
+    false
+ := by
+   sorry
+
+end Complexity
+
 /-- A functional queue with invariant. -/
 @[ext]
 structure FunctionalQueue (α : Type u) where
@@ -161,4 +203,6 @@ theorem popGhost {α : Type u} {x : α} {q q2 : FunctionalQueue α} :
     obtain ⟨h1, h2⟩ := h
     exact @Raw.popGhost α x q.raw q2' q.inv heq
 
+end
+
 end Cslib.Algorithms.Lean

From b93816b64f7e2e5bc753b213f87fcc9b780870f7 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sun, 10 May 2026 00:14:34 -0400
Subject: [PATCH 07/12] wip: define physicist method in Amortized.lean, start
 using it for the queue

---
 Cslib/Algorithms/Lean/Amortized.lean          |  14 +-
 .../Lean/FunctionalQueue/FunctionalQueue.lean | 169 ++++++++++++------
 Cslib/Algorithms/Lean/TimeM.lean              |   2 +-
 3 files changed, 126 insertions(+), 59 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Amortized.lean b/Cslib/Algorithms/Lean/Amortized.lean
index 7d111cdcc..5c3895e34 100644
--- a/Cslib/Algorithms/Lean/Amortized.lean
+++ b/Cslib/Algorithms/Lean/Amortized.lean
@@ -1,4 +1,3 @@
-
 /-
 Copyright (c) 2026 Simon Cruanes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -8,6 +7,7 @@ Authors: Simon Cruanes
 module
 
 import Cslib.Init
+public import Cslib.Algorithms.Lean.TimeM
 
 /-!
 # Amortized cost analysis
@@ -26,6 +26,18 @@ class Potential α where
       [Okasaki, *Purely Functional Data Structures*, 1996][okasaki1996] -/
   potential : α → Nat
 
+class Op α o where
+  applyOp : α → o → TimeM ℕ α
+
+@[simp] def applyOps {α o : Type u} [Op α o] (ops : List o) (x : α)
+    : TimeM ℕ α :=
+  List.foldlM (fun x op => Op.applyOp x op) x ops
+
+/-- Amortized cost with the physicist's method,
+    following Okasaki, chapter 5 -/
+def amortizedCost {α o : Type*} [Op α o] [Potential α] (x : α) (op : o) : ℕ :=
+  (Op.applyOp x op).time + Potential.potential (Op.applyOp x op).ret - Potential.potential x
+
 end Cslib.Algorithms.Lean.Amortized
 
 end
diff --git a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
index fc3284420..859a3b45f 100644
--- a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
+++ b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
@@ -8,6 +8,7 @@ module
 
 import Cslib.Init
 public import Cslib.Algorithms.Lean.Amortized
+public import Cslib.Algorithms.Lean.TimeM
 
 /-!
 # Functional Queue
@@ -31,78 +32,89 @@ namespace Cslib.Algorithms.Lean
 
 universe u
 
-structure RawFunctionalQueue (α : Type u) where
+namespace Raw
+
+structure FunctionalQueue (α : Type u) where
   front : List α
   back : List α
 
-namespace Raw
-
 /-- Well-formedness: if front is empty, back must be empty too. -/
-def invariant {α : Type u} (q : RawFunctionalQueue α) : Prop :=
+def invariant {α : Type u} (q : Raw.FunctionalQueue α) : Prop :=
   q.front = [] → q.back = []
 
 /-- The logical contents of the queue: `front ++ back.reverse`. -/
-def ghostList {α : Type u} (q : RawFunctionalQueue α) : List α :=
+def ghostList {α : Type u} (q : FunctionalQueue α) : List α :=
   List.append q.front q.back.reverse
 
 /-- The empty queue. -/
-def empty {α : Type u} : RawFunctionalQueue α := ⟨ [], [] ⟩
+def empty {α : Type u} : FunctionalQueue α := ⟨ [], [] ⟩
 
 /-- Internal: rebalance by moving `back.reverse` to `front` when `front` is empty. -/
-def rebalance {α : Type u} (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
+def rebalance {α : Type u} (q : FunctionalQueue α)
+    : TimeM ℕ (FunctionalQueue α) :=
   match q.front with
-  | [] => ⟨ (q.back).reverse, [] ⟩
-  | _ => q
+  | [] => do
+    TimeM.tick q.back.length
+    pure ⟨ (q.back).reverse, [] ⟩
+  | _ => pure q
 
-theorem rebalanceInvert {α : Type u} (q : RawFunctionalQueue α) :
-    (rebalance q).front = [] → q = Raw.empty := by
+theorem rebalanceInvert {α : Type u} (q : FunctionalQueue α) :
+    (rebalance q).ret.front = [] → q = empty := by
   intro h
   obtain ⟨f, b⟩ := q
   simp only [rebalance, Raw.empty] at h ⊢
   split at h <;> simp_all
 
-theorem rebalanceInvariant {α : Type u} {q : RawFunctionalQueue α} :
-    invariant (rebalance q) := by
+theorem rebalanceInvariant {α : Type u} {q : FunctionalQueue α} :
+    invariant (rebalance q).ret := by
   obtain ⟨f, b⟩ := q
   simp [rebalance, invariant]
   split <;> grind
 
-@[simp] theorem rebalanceIdempotent {α : Type u} (q : RawFunctionalQueue α) :
-    rebalance (rebalance q) = rebalance q := by
+@[simp] theorem rebalanceIdempotent {α : Type u} (q : FunctionalQueue α) :
+    (rebalance (rebalance q).ret).ret = (rebalance q).ret := by
   obtain ⟨f, b⟩ := q
   simp [rebalance]
   split <;> grind
 
-@[simp] theorem rebalancePreserveGhost {α : Type u} (q : RawFunctionalQueue α) :
-    ghostList (rebalance q) = ghostList q := by
+@[simp] theorem rebalancePreserveGhost {α : Type u} (q : FunctionalQueue α) :
+    ghostList (rebalance q).ret = ghostList q := by
   obtain ⟨f, b⟩ := q
   simp [rebalance, ghostList]
   split <;> grind [List.reverse_append]
 
 /-- Enqueue an element. -/
-def push {α : Type u} (x : α) (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
+def push {α : Type u} (x : α) (q : FunctionalQueue α)
+    : TimeM ℕ (FunctionalQueue α) := do
+  TimeM.tick 1
   rebalance ⟨ q.front, x :: q.back ⟩
 
-theorem pushInvariant {α : Type u} (x : α) (q : RawFunctionalQueue α) :
-    invariant q → invariant (push x q) := by
+theorem pushInvariant {α : Type u} (x : α) (q : FunctionalQueue α)
+    : invariant q → invariant (push x q).ret := by
   intro h
   rw [push]
   apply rebalanceInvariant
 
-theorem pushGhost {α : Type u} (x : α) (q : RawFunctionalQueue α) :
-    ghostList (push x q) = ghostList q ++ [x] := by
-  rw [push, rebalancePreserveGhost, ghostList]
+theorem pushGhost {α : Type u} (x : α) (q : Raw.FunctionalQueue α)
+    : ghostList (push x q).ret = ghostList q ++ [x] := by
+  rw [push]
+  simp only [TimeM.ret_bind, rebalancePreserveGhost]
+  rw [ghostList]
   simp [ghostList, List.append_assoc]
 
 /-- Dequeue: returns `some (head, remaining)` or `none` if empty. -/
-def pop {α : Type u} (q : RawFunctionalQueue α) : Option (α × RawFunctionalQueue α) :=
+def pop {α : Type u} (q : Raw.FunctionalQueue α)
+    : TimeM ℕ (Option (α × Raw.FunctionalQueue α)) :=
   match q.front with
-  | [] => none
-  | x :: tl =>
-    some (x, rebalance ⟨ tl, q.back ⟩)
-
-theorem popInvariant {α : Type u} (x : α) (q q2 : RawFunctionalQueue α) :
-    invariant q → pop q = some (x, q2) → invariant q2 := by
+  | [] => pure none
+  | x :: tl => do
+    let q2 ← rebalance ⟨ tl, q.back ⟩
+    pure (some (x, q2))
+
+theorem popInvariant {α : Type u} (x : α) (q q2 : FunctionalQueue α)
+    : invariant q →
+      (pop q).ret = some (x, q2) →
+      invariant q2 := by
   intro hq hpop
   obtain ⟨f, b⟩ := q
   simp [invariant] at hq
@@ -120,8 +132,10 @@ theorem popInvariant {α : Type u} (x : α) (q q2 : RawFunctionalQueue α) :
 @[simp] theorem emptyGhost {α : Type u} : ghostList (@Raw.empty α) = [] := by
   simp [ghostList, Raw.empty]
 
-theorem popGhost {α : Type u} {x : α} {q q2 : RawFunctionalQueue α} :
-    invariant q → pop q = some (x, q2) → ghostList q = x :: ghostList q2 := by
+theorem popGhost {α : Type u} {x : α} {q q2 : Raw.FunctionalQueue α}
+    : invariant q →
+      (pop q).ret = some (x, q2) →
+      ghostList q = x :: ghostList q2 := by
   intro hq hpop
   obtain ⟨f, b⟩ := q
   simp [invariant] at hq
@@ -138,65 +152,106 @@ end Raw
 
 namespace Complexity
 
-def potential {α : Type u} (q : RawFunctionalQueue α) : Nat :=
+def potential {α : Type u} (q : Raw.FunctionalQueue α) : Nat :=
   q.back.length
 
 instance functionalQueuePotential {α : Type u}
-    : Amortized.Potential (RawFunctionalQueue α) :=
+    : Amortized.Potential (Raw.FunctionalQueue α) :=
   ⟨ potential ⟩
 
 inductive queueOp (α : Type u) where
   | push : α → queueOp α
   | pop
 
-def applyOp {α : Type u} (op : queueOp α) (q : RawFunctionalQueue α) : RawFunctionalQueue α :=
+def applyOp {α : Type u} (q : Raw.FunctionalQueue α) (op : queueOp α)
+    : TimeM ℕ (Raw.FunctionalQueue α) :=
   match op with
   | .push x => Raw.push x q
-  | .pop =>
-    match Raw.pop q with
-    | none => q
-    | some (_, q2) => q2
+  | .pop => do
+    match (← Raw.pop q) with
+    | none => pure q
+    | some (_, q2) => pure q2
+
+instance functionalQueueApplyOp {α : Type u}
+    : Amortized.Op (Raw.FunctionalQueue α) (queueOp α) :=
+  ⟨ applyOp ⟩
 
-def applyOps {α : Type u} (ops : List (queueOp α)) (q : RawFunctionalQueue α)
-    : RawFunctionalQueue α :=
-  ops.foldl (fun q op => applyOp op q) q
+theorem costRebalanceEmpty {α : Type u} (q : Raw.FunctionalQueue α)
+    : q.front = [] → (Raw.rebalance q).time = potential q := by
+  intro h
+  simp only [Raw.rebalance]; rw [h]; simp [potential]
+
+grind_pattern costRebalanceEmpty => (Raw.rebalance q).time
+
+theorem costRebalanceNonEmpty {α : Type u} (q : Raw.FunctionalQueue α)
+    : q.front ≠ [] → (Raw.rebalance q).time = 0 := by
+  intro h
+  simp [Raw.rebalance]
+
+grind_pattern costRebalanceNonEmpty => (Raw.rebalance q).time
+
+theorem costPush {α : Type u} (x : α) (q : Raw.FunctionalQueue α)
+    : (Raw.push x q).time ≤ potential q := by
+  simp [Raw.push]
+  sorry
+  /- cases q.front <;> grind -/
+  /-     grind [Raw.push] -/
+
+theorem costApplyOp {α : Type u} (op : queueOp α) (q : Raw.FunctionalQueue α)
+    : (applyOp q op).time ≤ 1 + potential q := by
+  sorry
+  /- cases op with -/
+  /- | .pu -/
+  /- simp [applyOp] -/
+  /- grind -/
 
 theorem constantTimeAmortized {α : Type u} :
-    ∀ (q : RawFunctionalQueue α) (ops:List (queueOp α)),
-    false
- := by
-   sorry
+    ∀ (q : Raw.FunctionalQueue α) (ops : List (queueOp α)),
+    (Amortized.applyOps ops q).time ≤ 2 * potential (Amortized.applyOps ops q).ret
+    := by
+  intro q ops
+  induction ops generalizing q with
+  | nil => simp
+  | cons op otherOps hOps =>
+    simp
+    sorry
 
 end Complexity
 
 /-- A functional queue with invariant. -/
 @[ext]
 structure FunctionalQueue (α : Type u) where
-  raw : RawFunctionalQueue α
+  raw : Raw.FunctionalQueue α
   inv : Raw.invariant raw
 
 def empty {α : Type u} : FunctionalQueue α := ⟨ @Raw.empty α, Raw.emptyInvariant ⟩
 
-def push {α : Type u} (x : α) (q : FunctionalQueue α) : FunctionalQueue α :=
-  ⟨ Raw.push x q.raw, Raw.pushInvariant x q.raw q.inv ⟩
+def push {α : Type u} (x : α) (q : FunctionalQueue α)
+    : TimeM ℕ (FunctionalQueue α) :=
+  let r := Raw.push x q.raw
+  ⟨ ⟨ r.ret, Raw.pushInvariant x q.raw q.inv ⟩, r.time ⟩
 
-def pop {α : Type u} (q : FunctionalQueue α) : Option (α × FunctionalQueue α) :=
-  match h : Raw.pop q.raw with
-  | none => none
+def pop {α : Type u} (q : FunctionalQueue α)
+    : TimeM ℕ (Option (α × FunctionalQueue α)) :=
+  let r := Raw.pop q.raw
+  match h : r.ret with
+  | none => ⟨ none, r.time ⟩
   | some (x, q2) =>
-    some (x, ⟨ q2, Raw.popInvariant x q.raw q2 q.inv h ⟩)
+    ⟨ some (x, ⟨ q2, Raw.popInvariant x q.raw q2 q.inv h ⟩), r.time ⟩
 
 /-- project to a list view, an ordered sequence of elements -/
 def ghostList {α : Type u} (q : FunctionalQueue α) : List α := Raw.ghostList q.raw
 
 theorem pushGhost {α : Type u} (x : α) (q : FunctionalQueue α) :
-    ghostList (push x q) = ghostList q ++ [x] :=
+    ghostList (push x q).ret = ghostList q ++ [x] :=
   Raw.pushGhost x q.raw
 
-theorem popGhost {α : Type u} {x : α} {q q2 : FunctionalQueue α} :
-    pop q = some (x, q2) → ghostList q = x :: ghostList q2 := by
-  intro h
+theorem popGhost {α : Type u} {x : α} {q2 : FunctionalQueue α} :
+    ∀ {q : FunctionalQueue α},
+    (pop q).ret = some (x, q2) → ghostList q = x :: ghostList q2 := by
+  intro q h
   simp only [pop, ghostList] at h ⊢
+  simp only [TimeM.ret] at h
   split at h
   · simp only [reduceCtorEq] at h
   · rename_i x2 q2' heq
diff --git a/Cslib/Algorithms/Lean/TimeM.lean b/Cslib/Algorithms/Lean/TimeM.lean
index 389d6945b..164a653cd 100644
--- a/Cslib/Algorithms/Lean/TimeM.lean
+++ b/Cslib/Algorithms/Lean/TimeM.lean
@@ -85,7 +85,7 @@ instance [Add T] : SeqLeft (TimeM T) where
 instance [Add T] : SeqRight (TimeM T) where
   seqRight x y := ⟨(y ()).ret, x.time + (y ()).time⟩
 
-instance [AddZero T] : Monad (TimeM T) where
+instance [Add T] [Zero T] : Monad (TimeM T) where
   pure := Pure.pure
   bind := Bind.bind
   map := Functor.map

From a3c04241e20e2d00774206b31430a1a92672fb97 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sun, 10 May 2026 21:42:18 -0400
Subject: [PATCH 08/12] directly use amortized cost for proofs

---
 .../Lean/FunctionalQueue/FunctionalQueue.lean | 54 +++++--------------
 1 file changed, 14 insertions(+), 40 deletions(-)

diff --git a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
index 859a3b45f..4e5b9db13 100644
--- a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
+++ b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
@@ -176,45 +176,20 @@ instance functionalQueueApplyOp {α : Type u}
     : Amortized.Op (Raw.FunctionalQueue α) (queueOp α) :=
   ⟨ applyOp ⟩
 
-theorem costRebalanceEmpty {α : Type u} (q : Raw.FunctionalQueue α)
-    : q.front = [] → (Raw.rebalance q).time = potential q := by
-  intro h
-  simp only [Raw.rebalance]; rw [h]; simp [potential]
-
-grind_pattern costRebalanceEmpty => (Raw.rebalance q).time
-
-theorem costRebalanceNonEmpty {α : Type u} (q : Raw.FunctionalQueue α)
-    : q.front ≠ [] → (Raw.rebalance q).time = 0 := by
-  intro h
-  simp [Raw.rebalance]
-
-grind_pattern costRebalanceNonEmpty => (Raw.rebalance q).time
-
-theorem costPush {α : Type u} (x : α) (q : Raw.FunctionalQueue α)
-    : (Raw.push x q).time ≤ potential q := by
-  simp [Raw.push]
-  sorry
-  /- cases q.front <;> grind -/
-  /-     grind [Raw.push] -/
-
-theorem costApplyOp {α : Type u} (op : queueOp α) (q : Raw.FunctionalQueue α)
-    : (applyOp q op).time ≤ 1 + potential q := by
-  sorry
-  /- cases op with -/
-  /- | .pu -/
-  /- simp [applyOp] -/
-  /- grind -/
-
-theorem constantTimeAmortized {α : Type u} :
-    ∀ (q : Raw.FunctionalQueue α) (ops : List (queueOp α)),
-    (Amortized.applyOps ops q).time ≤ 2 * potential (Amortized.applyOps ops q).ret
-    := by
-  intro q ops
-  induction ops generalizing q with
-  | nil => simp
-  | cons op otherOps hOps =>
-    simp
-    sorry
+theorem potentialEmptyIsZero {α : Type u}
+    : potential (@Raw.empty α) = 0 := by
+  simp [potential, Raw.empty]
+
+theorem amortizedCostQueueOp {α : Type u} (q : Raw.FunctionalQueue α) (op : queueOp α)
+    : Amortized.amortizedCost q op ≤ 2 := by
+  simp only [Amortized.amortizedCost, Amortized.Potential.potential, Nat.sub_le_iff_le_add]
+  cases op with
+  | push x =>
+    simp only [Amortized.Op.applyOp, applyOp, potential]
+    cases h_front : q.front <;> (rw [Raw.push, Raw.rebalance, h_front] at ⊢; grind)
+  | pop =>
+    simp only [Amortized.Op.applyOp, applyOp, potential]
+    cases h_front : q.front <;> (rw [Raw.pop, h_front] at ⊢; grind [Raw.rebalance])
 
 end Complexity
 
@@ -251,7 +226,6 @@ theorem popGhost {α : Type u} {x : α} {q2 : FunctionalQueue α} :
     (pop q).ret = some (x, q2) → ghostList q = x :: ghostList q2 := by
   intro q h
   simp only [pop, ghostList] at h ⊢
-  simp only [TimeM.ret] at h
   split at h
   · simp only [reduceCtorEq] at h
   · rename_i x2 q2' heq

From 5fb8647144bb65b840c1f1402e41a6b322883226 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 18 May 2026 23:06:30 -0400
Subject: [PATCH 09/12] complexity result for list of operations

---
 Cslib/Algorithms/Lean/Amortized.lean          | 46 +++++++++++++++++--
 .../Lean/FunctionalQueue/FunctionalQueue.lean | 16 +++++++
 2 files changed, 58 insertions(+), 4 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Amortized.lean b/Cslib/Algorithms/Lean/Amortized.lean
index 5c3895e34..104b0c426 100644
--- a/Cslib/Algorithms/Lean/Amortized.lean
+++ b/Cslib/Algorithms/Lean/Amortized.lean
@@ -7,6 +7,7 @@ Authors: Simon Cruanes
 module
 
 import Cslib.Init
+import Mathlib
 public import Cslib.Algorithms.Lean.TimeM
 
 /-!
@@ -22,21 +23,58 @@ namespace Cslib.Algorithms.Lean.Amortized
 /-- Physicist method: a potential (lower bound on savings) defined on a
     data structure -/
 class Potential α where
-  /-- non-negative potential. Initial potential should be 0.
+  /-- Initial potential should be 0.
       [Okasaki, *Purely Functional Data Structures*, 1996][okasaki1996] -/
   potential : α → Nat
 
 class Op α o where
   applyOp : α → o → TimeM ℕ α
 
-@[simp] def applyOps {α o : Type u} [Op α o] (ops : List o) (x : α)
+@[simp] def applyOps {α o : Type*} [Op α o] (x : α) (ops : List o)
     : TimeM ℕ α :=
   List.foldlM (fun x op => Op.applyOp x op) x ops
 
+def triples {α o : Type*} [Op α o] (x : α) (ops : List o) : List (α × o) × α :=
+  match ops with
+  | [] => ([], x)
+  | o :: ops2 =>
+    let ⟨ x2, _cost ⟩ := Op.applyOp x o
+    let ⟨ pairs, final ⟩ := triples x2 ops2
+    ((x2, o) :: pairs, final)
+
 /-- Amortized cost with the physicist's method,
     following Okasaki, chapter 5 -/
-def amortizedCost {α o : Type*} [Op α o] [Potential α] (x : α) (op : o) : ℕ :=
-  (Op.applyOp x op).time + Potential.potential (Op.applyOp x op).ret - Potential.potential x
+def amortizedCost {α o : Type*} [Op α o] [Potential α]
+    (x : α) (op : o) : ℕ :=
+  (Op.applyOp x op).time
+    + Potential.potential (Op.applyOp x op).ret
+    - Potential.potential x
+
+def amortizedCostL {α o : Type*} [Op α o] [Potential α]
+    (x : α) (ops : List o) : ℕ :=
+  (applyOps x ops).time
+    + Potential.potential (applyOps x ops).ret
+    - Potential.potential x
+
+/-- If each operation's cost is bounded by `k`, then the amortized
+  cost over a series of operations is bounded by `k * ops.length`. -/
+theorem constantAmortizedCostL {α o : Type*}
+    [h_op : Op α o] [h_pot : Potential α]
+    (k : ℕ) (h_bounded : ∀ (x : α) (op : o), amortizedCost x op ≤ k)
+    (x : α) (ops : List o)
+    : amortizedCostL x ops ≤ k * ops.length
+    := by
+  simp only [amortizedCostL, applyOps, tsub_le_iff_right]
+  revert x
+  induction ops with
+  | nil => simp [List.foldlM]
+  | cons op ops2 h_ind =>
+    intro x
+    simp only [amortizedCost, tsub_le_iff_right] at h_bounded
+    simp [List.foldlM, List.length_cons]
+    have bound1 := h_bounded x op
+    have bound2 := h_ind (Op.applyOp x op).ret
+    linarith
 
 end Cslib.Algorithms.Lean.Amortized
 
diff --git a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
index 4e5b9db13..e1bfe5c5a 100644
--- a/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
+++ b/Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean
@@ -19,6 +19,8 @@ The representation uses two lists: a front list (for dequeue) and a back list
 (for enqueue). When the front list becomes empty, the back list is reversed
 and becomes the new front. This yields amortized O(1) operations.
 
+Cost model: each list cons is worth one `TimeM` tick.
+
 ## References
 
 * [Okasaki, *Purely Functional Data Structures*, 1996][okasaki1996]
@@ -191,6 +193,20 @@ theorem amortizedCostQueueOp {α : Type u} (q : Raw.FunctionalQueue α) (op : qu
     simp only [Amortized.Op.applyOp, applyOp, potential]
     cases h_front : q.front <;> (rw [Raw.pop, h_front] at ⊢; grind [Raw.rebalance])
 
+/-- cost of applying operations to a queue -/
+theorem costQueueOps {α : Type u}
+    (q : Raw.FunctionalQueue α) (ops : List (queueOp α))
+    : (Amortized.applyOps q ops).time
+        + potential (Amortized.applyOps q ops).ret
+        - potential q
+      ≤ 2 * ops.length
+    := by
+  have useful
+    := Amortized.constantAmortizedCostL 2 amortizedCostQueueOp q ops
+  simp only [Amortized.amortizedCostL, Amortized.Potential.potential]
+    at useful
+  grind only
+
 end Complexity
 
 /-- A functional queue with invariant. -/

From deda5586f945b3bd644f2b8a91c55799663330a0 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 19 May 2026 22:01:49 -0400
Subject: [PATCH 10/12] remove dead code

---
 Cslib/Algorithms/Lean/Amortized.lean | 11 +----------
 1 file changed, 1 insertion(+), 10 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Amortized.lean b/Cslib/Algorithms/Lean/Amortized.lean
index 104b0c426..9ddacc045 100644
--- a/Cslib/Algorithms/Lean/Amortized.lean
+++ b/Cslib/Algorithms/Lean/Amortized.lean
@@ -23,8 +23,7 @@ namespace Cslib.Algorithms.Lean.Amortized
 /-- Physicist method: a potential (lower bound on savings) defined on a
     data structure -/
 class Potential α where
-  /-- Initial potential should be 0.
-      [Okasaki, *Purely Functional Data Structures*, 1996][okasaki1996] -/
+  /-- [Okasaki, *Purely Functional Data Structures*, 1996][okasaki1996] -/
   potential : α → Nat
 
 class Op α o where
@@ -34,14 +33,6 @@ class Op α o where
     : TimeM ℕ α :=
   List.foldlM (fun x op => Op.applyOp x op) x ops
 
-def triples {α o : Type*} [Op α o] (x : α) (ops : List o) : List (α × o) × α :=
-  match ops with
-  | [] => ([], x)
-  | o :: ops2 =>
-    let ⟨ x2, _cost ⟩ := Op.applyOp x o
-    let ⟨ pairs, final ⟩ := triples x2 ops2
-    ((x2, o) :: pairs, final)
-
 /-- Amortized cost with the physicist's method,
     following Okasaki, chapter 5 -/
 def amortizedCost {α o : Type*} [Op α o] [Potential α]

From a3e6fc7d60674ba41cf9698e1ddef88cfe8b662d Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 23 May 2026 00:24:15 -0400
Subject: [PATCH 11/12] wtf man

---
 Cslib/Algorithms/Lean/Amortized.lean | 55 ++++++++++++++++++----------
 1 file changed, 36 insertions(+), 19 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Amortized.lean b/Cslib/Algorithms/Lean/Amortized.lean
index 9ddacc045..87f7d58fb 100644
--- a/Cslib/Algorithms/Lean/Amortized.lean
+++ b/Cslib/Algorithms/Lean/Amortized.lean
@@ -9,6 +9,9 @@ module
 import Cslib.Init
 import Mathlib
 public import Cslib.Algorithms.Lean.TimeM
+public import Mathlib.Algebra.Ring.Defs
+public import Mathlib.Order.Defs.PartialOrder
+public import Mathlib.Algebra.Order.Ring.Defs
 
 /-!
 # Amortized cost analysis
@@ -22,9 +25,11 @@ namespace Cslib.Algorithms.Lean.Amortized
 
 /-- Physicist method: a potential (lower bound on savings) defined on a
     data structure -/
-class Potential α where
+class Potential φ α extends CommRing φ, PartialOrder φ, IsStrictOrderedRing φ where
   /-- [Okasaki, *Purely Functional Data Structures*, 1996][okasaki1996] -/
-  potential : α → Nat
+  potential : α → φ
+
+  potentialNonNegative : forall (x : α), (potential x : φ) ≥ 0
 
 class Op α o where
   applyOp : α → o → TimeM ℕ α
@@ -35,36 +40,48 @@ class Op α o where
 
 /-- Amortized cost with the physicist's method,
     following Okasaki, chapter 5 -/
-def amortizedCost {α o : Type*} [Op α o] [Potential α]
-    (x : α) (op : o) : ℕ :=
-  (Op.applyOp x op).time
+def amortizedCost {α o φ : Type*}
+    [Op α o] [Add φ] [Sub φ] [NatCast φ] [Potential φ α]
+    (x : α) (op : o) : φ :=
+  Nat.cast (Op.applyOp x op).time
     + Potential.potential (Op.applyOp x op).ret
     - Potential.potential x
 
-def amortizedCostL {α o : Type*} [Op α o] [Potential α]
-    (x : α) (ops : List o) : ℕ :=
-  (applyOps x ops).time
-    + Potential.potential (applyOps x ops).ret
-    - Potential.potential x
-
 /-- If each operation's cost is bounded by `k`, then the amortized
   cost over a series of operations is bounded by `k * ops.length`. -/
-theorem constantAmortizedCostL {α o : Type*}
-    [h_op : Op α o] [h_pot : Potential α]
-    (k : ℕ) (h_bounded : ∀ (x : α) (op : o), amortizedCost x op ≤ k)
+theorem constantAmortizedCostL {α o φ : Type*}
+    [h_op : Op α o] [h_pot : Potential φ α]
+    (k : φ) (h_k_pos : k > 0) (h_bounded : ∀ (x : α) (op : o), amortizedCost x op ≤ k)
     (x : α) (ops : List o)
-    : amortizedCostL x ops ≤ k * ops.length
+    : (applyOps x ops).time
+        + Potential.potential (applyOps x ops).ret - Potential.potential x
+      ≤ k * Nat.cast ops.length
     := by
-  simp only [amortizedCostL, applyOps, tsub_le_iff_right]
+  simp only [applyOps]
   revert x
   induction ops with
-  | nil => simp [List.foldlM]
+  | nil =>
+    intro x
+    simp only [List.foldlM, TimeM.time_pure, CharP.cast_eq_zero,
+      TimeM.ret_pure, zero_add, sub_self,
+      List.length_nil, mul_zero, Std.le_refl]
   | cons op ops2 h_ind =>
     intro x
-    simp only [amortizedCost, tsub_le_iff_right] at h_bounded
-    simp [List.foldlM, List.length_cons]
+    simp only [amortizedCost] at h_bounded
+    simp only [List.foldlM, TimeM.time_bind, Nat.cast_add, TimeM.ret_bind, List.length_cons,
+      Nat.cast_one]
     have bound1 := h_bounded x op
     have bound2 := h_ind (Op.applyOp x op).ret
+    set applyOpX := (Op.applyOp x op : TimeM ℕ α)
+    set applyOps2 := (List.foldlM (fun x op => Op.applyOp x op) (Op.applyOp x op).ret ops2)
+    set potX := (Potential.potential x : φ)
+    set potOpX := (Potential.potential applyOpX.ret : φ)
+    set potOps2 := (Potential.potential applyOps2.ret : φ)
+    have potOpXPos := (Potential.potentialNonNegative (φ := φ) applyOpX.ret)
+    ring_nf
+    have jfdoit := add_le_add bound1 bound2
+    ring_nf at jfdoit
+    exact jfdoit
     linarith
 
 end Cslib.Algorithms.Lean.Amortized

From 201ac9f9e04bd4826c38df53c2f8f0f743ff3d42 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 23 May 2026 00:33:13 -0400
Subject: [PATCH 12/12] yay linearize yo partial order now

---
 Cslib/Algorithms/Lean/Amortized.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Amortized.lean b/Cslib/Algorithms/Lean/Amortized.lean
index 87f7d58fb..ff2511cc4 100644
--- a/Cslib/Algorithms/Lean/Amortized.lean
+++ b/Cslib/Algorithms/Lean/Amortized.lean
@@ -25,7 +25,7 @@ namespace Cslib.Algorithms.Lean.Amortized
 
 /-- Physicist method: a potential (lower bound on savings) defined on a
     data structure -/
-class Potential φ α extends CommRing φ, PartialOrder φ, IsStrictOrderedRing φ where
+class Potential φ α extends CommRing φ, LinearOrder φ, IsStrictOrderedRing φ where
   /-- [Okasaki, *Purely Functional Data Structures*, 1996][okasaki1996] -/
   potential : α → φ
 
@@ -51,7 +51,7 @@ def amortizedCost {α o φ : Type*}
   cost over a series of operations is bounded by `k * ops.length`. -/
 theorem constantAmortizedCostL {α o φ : Type*}
     [h_op : Op α o] [h_pot : Potential φ α]
-    (k : φ) (h_k_pos : k > 0) (h_bounded : ∀ (x : α) (op : o), amortizedCost x op ≤ k)
+    (k : φ) (h_bounded : ∀ (x : α) (op : o), amortizedCost x op ≤ k)
     (x : α) (ops : List o)
     : (applyOps x ops).time
         + Potential.potential (applyOps x ops).ret - Potential.potential x
@@ -81,7 +81,6 @@ theorem constantAmortizedCostL {α o φ : Type*}
     ring_nf
     have jfdoit := add_le_add bound1 bound2
     ring_nf at jfdoit
-    exact jfdoit
     linarith
 
 end Cslib.Algorithms.Lean.Amortized