diff --git a/Cslib.lean b/Cslib.lean
index c0269e0bb..95672df25 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -53,6 +53,7 @@ public import Cslib.Foundations.Control.Monad.Free
 public import Cslib.Foundations.Control.Monad.Free.Effects
 public import Cslib.Foundations.Control.Monad.Free.Fold
 public import Cslib.Foundations.Data.BiTape
+public import Cslib.Foundations.Data.BinaryTree
 public import Cslib.Foundations.Data.DecidableEqZero
 public import Cslib.Foundations.Data.FinFun.Basic
 public import Cslib.Foundations.Data.FinFun.Update
@@ -66,6 +67,9 @@ public import Cslib.Foundations.Data.OmegaSequence.Temporal
 public import Cslib.Foundations.Data.RelatesInSteps
 public import Cslib.Foundations.Data.Relation
 public import Cslib.Foundations.Data.Set.Saturation
+public import Cslib.Foundations.Data.SplayTree.Basic
+public import Cslib.Foundations.Data.SplayTree.Complexity
+public import Cslib.Foundations.Data.SplayTree.Correctness
 public import Cslib.Foundations.Data.StackTape
 public import Cslib.Foundations.Lint.Basic
 public import Cslib.Foundations.Logic.InferenceSystem
diff --git a/Cslib/Foundations/Data/BinaryTree.lean b/Cslib/Foundations/Data/BinaryTree.lean
new file mode 100644
index 000000000..abbd19e20
--- /dev/null
+++ b/Cslib/Foundations/Data/BinaryTree.lean
@@ -0,0 +1,336 @@
+/-
+Copyright (c) 2025 Sorrachai Yingchareonthawornchai. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anton Kovsharov, Antoine du Fresne von Hohenesche,
+  Sorrachai Yingchareonthawornchai
+-/
+
+module
+
+public import Cslib.Init
+public import Mathlib.Combinatorics.SimpleGraph.Basic
+public import Mathlib.Combinatorics.SimpleGraph.Metric
+public import Mathlib.Data.Tree.Basic
+
+/-!
+# Binary Tree
+
+In this file we introduce the `Tree` data structure and its basic operations.
+-/
+
+@[expose] public section
+
+variable {α : Type}
+
+namespace Tree
+
+/-- A tree node. -/
+notation:65 l:66 " △[" v "] " r:66 => Tree.node v l r
+
+/-! ### Core Definitions -/
+section CoreDefs
+
+theorem non_empty_exist (s : Tree α) (h : s ≠ .nil) :
+    ∃ A k B, s = A △[k] B := by
+  induction s <;> grind
+
+/-- The number of nodes in a tree. -/
+def nodeCount : Tree α → ℕ
+  | .nil => 0
+  | .node _ l r => 1 + nodeCount l + nodeCount r
+
+@[simp] lemma nodeCount_empty : nodeCount (nil : Tree α) = 0 := rfl
+
+@[simp] lemma nodeCount_node (l : Tree α) (k : α) (r : Tree α) :
+    (l △[k] r).nodeCount = 1 + l.nodeCount + r.nodeCount := rfl
+
+/-- In-order traversal as a list of keys. -/
+def toKeyList : Tree α → List α
+  | .nil => []
+  | l △[k] r => l.toKeyList ++ [k] ++ r.toKeyList
+
+@[simp] lemma toKeyList_empty : toKeyList (nil : Tree α) = [] := rfl
+
+@[simp] lemma toKeyList_node (l : Tree α) (k : α) (r : Tree α) :
+    (l △[k] r).toKeyList = l.toKeyList ++ [k] ++ r.toKeyList := rfl
+
+/-- Number of nodes on the search path for `q` in `t`. Zero on the empty
+tree; on a node this counts the root plus (if `q ≠ k`) the search path
+length in the appropriate subtree. -/
+def searchPathLen [LinearOrder α] (t : Tree α) (q : α) : ℕ :=
+  match t with
+  | nil => 0
+  | l △[key] r =>
+    if q < key then
+      1 + l.searchPathLen q
+    else if key < q then
+      1 + r.searchPathLen q
+    else
+      1
+
+/--
+Remark:
+This implementation is not really a "contain function",
+because a binary tree could have q >/< key while being in
+the left/right subtree of key respectively.
+If `contains t q` is true, then `q` is in `t`; but
+the converse need not necessarily hold true. The
+converse is true for a binary search tree. Hence the name of it.
+-/
+def bstContains [LinearOrder α] (t : Tree α) (q : α) : Prop :=
+  match t with
+  | nil => False
+  | l △[key] r =>
+    if q < key then
+      l.bstContains q
+    else if key < q then
+      r.bstContains q
+    else
+      True
+
+end CoreDefs
+
+
+/-! ### Membership -/
+section Membership
+
+/-- Inductive membership relation on binary trees, modelled on `List.Mem`. -/
+inductive Mem (a : α) : Tree α → Prop where
+  /-- `a` is the key at the root. -/
+  | here  {l r : Tree α} : Mem a (l △[a] r)
+  /-- `a` lies in the left subtree. -/
+  | left  {k : α} {l r : Tree α} : Mem a l → Mem a (l △[k] r)
+  /-- `a` lies in the right subtree. -/
+  | right {k : α} {l r : Tree α} : Mem a r → Mem a (l △[k] r)
+
+instance instMembership : Membership α (Tree α) := ⟨fun t a => Mem a t⟩
+
+@[simp] lemma not_mem_nil (a : α) : a ∉ (nil : Tree α) := nofun
+
+@[simp] lemma mem_node_iff {a k : α} {l r : Tree α} :
+    a ∈ (l △[k] r) ↔ a = k ∨ a ∈ l ∨ a ∈ r := by
+  refine ⟨fun h => ?_, fun h => ?_⟩
+  · cases h with
+    | here    => exact Or.inl rfl
+    | left h  => exact Or.inr (Or.inl h)
+    | right h => exact Or.inr (Or.inr h)
+  · rcases h with rfl | h | h
+    · exact .here
+    · exact .left h
+    · exact .right h
+
+/-- Membership agrees with membership in the in-order key list. -/
+theorem mem_iff_mem_toKeyList {a : α} {t : Tree α} :
+    a ∈ t ↔ a ∈ t.toKeyList := by
+  induction t with
+  | nil => simp
+  | node k l r ihl ihr =>
+    rw [toKeyList_node, mem_node_iff]
+    simp only [List.mem_append, List.mem_singleton, ihl, ihr]
+    tauto
+
+instance decidableMem [DecidableEq α] (a : α) : ∀ t : Tree α, Decidable (a ∈ t)
+  | .nil       => isFalse nofun
+  | l △[k] r =>
+    haveI : Decidable (a ∈ l) := decidableMem a l
+    haveI : Decidable (a ∈ r) := decidableMem a r
+    decidable_of_iff (a = k ∨ a ∈ l ∨ a ∈ r) mem_node_iff.symm
+
+/-- The search-path `contains` implies membership. The converse needs the BST
+invariant. -/
+theorem contains_imp_mem [LinearOrder α] {t : Tree α} {q : α} :
+    t.bstContains q → q ∈ t := by
+  induction t with
+  | nil => simp [bstContains]
+  | node k l r ihl ihr =>
+    intro h
+    simp only [bstContains] at h
+    split_ifs at h with h1 h2
+    · exact .left (ihl h)
+    · exact .right (ihr h)
+    · have hqk : q = k := le_antisymm (not_lt.mp h2) (not_lt.mp h1)
+      exact hqk ▸ .here
+
+end Membership
+
+
+/-! ### Rotations and Mirroring -/
+section Transformations
+
+/-- Right rotation at the root: pivot the left child up. Leaves the tree
+unchanged if there is no left child. -/
+def rotateRight : Tree α → Tree α
+  | (a △[x] b) △[y] c => a △[x] (b △[y] c)
+  | t => t
+
+/-- Left rotation at the root: pivot the right child up. Leaves the tree
+unchanged if there is no right child. -/
+def rotateLeft : Tree α → Tree α
+  | a △[x] (b △[y] c) => (a △[x] b) △[y] c
+  | t => t
+
+/-- Mirror a binary tree: swap every left and right subtree. -/
+def mirror : Tree α → Tree α
+  | .nil => .nil
+  | l △[k] r => r.mirror △[k] l.mirror
+
+@[simp] lemma mirror_empty : (nil : Tree α).mirror = nil := rfl
+
+@[simp] lemma mirror_node (l : Tree α) (k : α) (r : Tree α) :
+    (l △[k] r).mirror = r.mirror △[k] l.mirror := rfl
+
+@[simp] lemma mirror_mirror (t : Tree α) : t.mirror.mirror = t := by
+  induction t <;> simp_all
+
+@[simp] lemma nodeCount_mirror (t : Tree α) : t.mirror.nodeCount = t.nodeCount := by
+  induction t <;> simp_all [nodeCount]; omega
+
+@[simp] lemma mirror_rotateRight (t : Tree α) :
+    (rotateRight t).mirror = rotateLeft t.mirror := by
+  rcases t with _ | ⟨k, (_ | ⟨lk, ll, lr⟩), r⟩ <;>
+    simp [rotateRight, rotateLeft, mirror]
+
+@[simp] lemma mirror_rotateLeft (t : Tree α) :
+    (rotateLeft t).mirror = rotateRight t.mirror := by
+  rcases t with _ | ⟨k, l, (_ | ⟨rk, rl, rr⟩)⟩ <;>
+    simp [rotateRight, rotateLeft, mirror]
+
+@[simp] theorem nodeCount_rotateRight (t : Tree α) :
+    (rotateRight t).nodeCount = t.nodeCount := by
+  rcases t with _ | ⟨k, (_ | ⟨lk, ll, lr⟩), r⟩ <;>
+    simp [rotateRight]; omega
+
+@[simp] theorem nodeCount_rotateLeft (t : Tree α) :
+    (rotateLeft t).nodeCount = t.nodeCount := by
+  have h := nodeCount_rotateRight t.mirror
+  simp only [← mirror_rotateLeft, nodeCount_mirror] at h; exact h
+
+end Transformations
+
+
+/-! ### Contains Characterizations -/
+section ContainsLemmas
+
+@[simp] lemma not_contains_empty [LinearOrder α] (q : α) :
+    ¬ (nil : Tree α).bstContains q := nofun
+
+@[simp] lemma contains_node_lt [LinearOrder α] {l : Tree α} {k q : α}
+    {r : Tree α} (h : q < k) :
+    (l △[k] r).bstContains q ↔ l.bstContains q := by
+  simp [bstContains, h]
+
+@[simp] lemma contains_node_gt [LinearOrder α] {l : Tree α} {k q : α}
+    {r : Tree α} (h : k < q) :
+    (l △[k] r).bstContains q ↔ r.bstContains q := by
+  simp [bstContains, h, not_lt_of_gt h]
+
+@[simp] lemma contains_node_not_eq_not_lt [LinearOrder α]
+    {l : Tree α} {k q : α} {r : Tree α}
+    (h1 : ¬ q = k) (h2 : ¬ q < k) :
+    (l △[k] r).bstContains q ↔ r.bstContains q := by
+  have hgt : k < q := lt_of_le_of_ne (Std.not_lt.mp h2) (Ne.symm (Ne.intro h1))
+  simp [bstContains, hgt, not_lt_of_gt hgt]
+
+end ContainsLemmas
+
+
+/-! ### Tree Invariants and BST Properties -/
+section Invariants
+
+/-- BST invariant parameterised by optional lower/upper key bounds.
+`IsBSTAux t lb ub` holds iff every key in `t` lies strictly in `(lb, ub)`
+(absent bound = ±∞) and children satisfy the BST property recursively. -/
+inductive IsBSTAux [LinearOrder α] : Tree α → Option α → Option α → Prop where
+  | nil (lb ub : Option α) : IsBSTAux .nil lb ub
+  | node {l r : Tree α} {k : α} {lb ub : Option α}
+      (hlb : lb.elim True (· < k))
+      (hub : ub.elim True (k < ·))
+      (hl  : IsBSTAux l lb (some k))
+      (hr  : IsBSTAux r (some k) ub) :
+      IsBSTAux (l △[k] r) lb ub
+
+/-- A tree is a binary search tree when it satisfies `IsBSTAux` with no
+bounds. -/
+def IsBST [LinearOrder α] (t : Tree α) : Prop := t.IsBSTAux none none
+
+end Invariants
+
+/-! ### Accessor Lemmas for IsBST -/
+section IsBSTAccessors
+
+@[simp] lemma IsBSTAux_nil [LinearOrder α] (lb ub : Option α) :
+    IsBSTAux (.nil : Tree α) lb ub := .nil lb ub
+
+@[simp] lemma IsBSTAux_node [LinearOrder α] (l : Tree α) (k : α) (r : Tree α)
+    (lb ub : Option α) :
+    IsBSTAux (l △[k] r) lb ub ↔
+      lb.elim True (· < k) ∧ ub.elim True (k < ·) ∧
+      IsBSTAux l lb (some k) ∧ IsBSTAux r (some k) ub :=
+  ⟨fun h => by cases h with | node hlb hub hl hr => exact ⟨hlb, hub, hl, hr⟩,
+   fun ⟨h1, h2, h3, h4⟩ => .node h1 h2 h3 h4⟩
+
+@[simp] lemma IsBST_node [LinearOrder α] (l : Tree α) (k : α) (r : Tree α) :
+    IsBST (l △[k] r) ↔ IsBSTAux l none (some k) ∧ IsBSTAux r (some k) none := by
+  simp [IsBST, IsBSTAux_node]
+
+end IsBSTAccessors
+
+
+/-! ### BST Membership -/
+section BSTMembership
+
+/-- In a BST subtree with upper bound `some ub`, every member is `< ub`. -/
+private lemma IsBSTAux.lt_of_mem_ub [LinearOrder α] {t : Tree α} {q ub : α}
+    {lb : Option α} (h : IsBSTAux t lb (some ub)) (hmem : q ∈ t) : q < ub := by
+  induction t generalizing lb ub with
+  | nil => simp at hmem
+  | node k l r ihl ihr =>
+    obtain ⟨_, hub, hl, hr⟩ := (IsBSTAux_node l k r lb (some ub)).mp h
+    rcases mem_node_iff.mp hmem with rfl | hml | hmr
+    · exact hub
+    · exact lt_trans (ihl hl hml) hub
+    · exact ihr hr hmr
+
+/-- In a BST subtree with lower bound `some lb`, every member is `> lb`. -/
+private lemma IsBSTAux.gt_of_mem_lb [LinearOrder α] {t : Tree α} {q lb : α}
+    {ub : Option α} (h : IsBSTAux t (some lb) ub) (hmem : q ∈ t) : lb < q := by
+  induction t generalizing lb ub with
+  | nil => simp at hmem
+  | node k l r ihl ihr =>
+    obtain ⟨hlb, _, hl, hr⟩ := (IsBSTAux_node l k r (some lb) ub).mp h
+    rcases mem_node_iff.mp hmem with rfl | hml | hmr
+    · exact hlb
+    · exact ihl hl hml
+    · exact lt_trans hlb (ihr hr hmr)
+
+/-- Membership implies the BST search path finds the key, for any bound
+configuration. -/
+private theorem IsBSTAux.mem_imp_contains [LinearOrder α] {t : Tree α} {q : α}
+    {lb ub : Option α} (h : IsBSTAux t lb ub) (hmem : q ∈ t) : t.bstContains q := by
+  induction t generalizing lb ub with
+  | nil => simp at hmem
+  | node k l r ihl ihr =>
+    obtain ⟨_, _, hl, hr⟩ := (IsBSTAux_node l k r lb ub).mp h
+    rcases mem_node_iff.mp hmem with rfl | hml | hmr
+    · simp [bstContains]
+    · have hlt : q < k := IsBSTAux.lt_of_mem_ub hl hml
+      simp only [bstContains, if_pos hlt]
+      exact ihl hl hml
+    · have hgt : k < q := IsBSTAux.gt_of_mem_lb hr hmr
+      simp only [bstContains, if_neg (not_lt.mpr hgt.le), if_pos hgt]
+      exact ihr hr hmr
+
+/-- Converse of `contains_imp_mem` for BSTs: membership implies the search-path
+`contains` succeeds. -/
+theorem mem_imp_contains [LinearOrder α] {t : Tree α} (hbst : IsBST t)
+    {q : α} (hmem : q ∈ t) : t.bstContains q :=
+  IsBSTAux.mem_imp_contains hbst hmem
+
+/-- For BSTs, the search-path `contains` coincides with membership. -/
+theorem contains_iff_mem [LinearOrder α] {t : Tree α} (hbst : IsBST t) {q : α} :
+    t.bstContains q ↔ q ∈ t :=
+  ⟨contains_imp_mem, mem_imp_contains hbst⟩
+
+end BSTMembership
+
+end Tree
diff --git a/Cslib/Foundations/Data/SplayTree/Basic.lean b/Cslib/Foundations/Data/SplayTree/Basic.lean
new file mode 100644
index 000000000..09202cc70
--- /dev/null
+++ b/Cslib/Foundations/Data/SplayTree/Basic.lean
@@ -0,0 +1,373 @@
+/-
+Copyright (c) 2026 Sorrachai Yingchareonthawornchai. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anton Kovsharov, Antoine du Fresne von Hohenesche,
+  Sorrachai Yingchareonthawornchai
+-/
+
+module
+
+public import Cslib.Foundations.Data.BinaryTree
+public import Mathlib.Data.List.Sort
+
+/-!
+# Splay Tree Basic Definitions
+
+This module defines the core operations of a bottom-up splay tree, including
+rotation primitives, path frames, and the `splay` and `splayUp` functions.
+It also provides fundamental structural lemmas regarding tree size and descent paths.
+-/
+
+@[expose] public section
+
+variable {α : Type}
+
+namespace SplayTree
+
+open Tree
+
+/-! ### Definitions -/
+section Definitions
+
+/-- The direction taken from a parent while descending toward a target. -/
+inductive Dir
+  /-- The target lies in the left subtree of this parent. -/
+  | L
+  /-- The target lies in the right subtree of this parent. -/
+  | R
+  deriving DecidableEq, Repr
+
+/-- Flip a direction: `L ↔ R`. -/
+def Dir.flip : Dir → Dir
+  | .L => .R
+  | .R => .L
+
+@[simp] lemma Dir.flip_flip (d : Dir) : d.flip.flip = d := by cases d <;> rfl
+@[simp] lemma Dir.flip_ne (d : Dir) : d.flip ≠ d := by cases d <;> simp [flip]
+@[simp] lemma Dir.ne_flip (d : Dir) : d ≠ d.flip := by cases d <;> simp [flip]
+
+/-- Single primitive rotation that brings the `d`-child of the root up one
+level. `L` ↦ `rotateRight`, `R` ↦ `rotateLeft`. -/
+def Dir.bringUp : Dir → Tree α → Tree α
+  | .L => rotateRight
+  | .R => rotateLeft
+
+/-- Apply `op` to the `d`-child of the root, leaving everything else fixed. -/
+def applyChild (d : Dir) (op : Tree α → Tree α) : Tree α → Tree α
+  | l △[k] r =>
+    match d with
+    | .L => (op l) △[k] r
+    | .R => l △[k] (op r)
+  | .nil => .nil
+
+/-- One frame of the search path: the direction we took from this ancestor,
+its key, and the subtree we did *not* descend into. -/
+structure Frame α where
+  /-- Direction taken from this ancestor. -/
+  dir : Dir
+  /-- Key stored at this ancestor. -/
+  key : α
+  /-- The subtree we did not descend into. -/
+  sibling : Tree α
+
+/-- Re-attach a subtree `c` below the ancestor described by `f`. -/
+def Frame.attach (c : Tree α) (f : Frame α) : Tree α :=
+  match f.dir with
+  | .L => c △[f.key] f.sibling
+  | .R => f.sibling △[f.key] c
+
+@[simp] lemma mirror_bringUp (d : Dir) (t : Tree α) :
+    (d.bringUp t).mirror = d.flip.bringUp t.mirror := by
+  cases d <;> simp [Dir.bringUp, Dir.flip]
+
+/-- Flip a frame: reverse the direction and mirror the sibling. -/
+def Frame.flip (f : Frame α) : Frame α :=
+  { dir := f.dir.flip, key := f.key, sibling := f.sibling.mirror }
+
+@[simp] lemma mirror_attach (c : Tree α) (f : Frame α) :
+    (f.attach c).mirror = f.flip.attach c.mirror := by
+  cases f with | mk d k s =>
+    cases d <;> simp [Frame.attach, Frame.flip, Dir.flip]
+
+@[simp] lemma mirror_applyChild_bringUp (d₁ d₂ : Dir)
+    (t : Tree α) :
+    (applyChild d₁ d₂.bringUp t).mirror =
+      applyChild d₁.flip d₂.flip.bringUp t.mirror := by
+  rcases t with _ | ⟨k, l, r⟩
+  · cases d₁ <;> cases d₂ <;> simp [applyChild]
+  · cases d₁ <;> cases d₂ <;>
+      simp only [applyChild, Dir.flip, Dir.bringUp,
+        mirror_node] <;> congr 1 <;>
+      first | exact mirror_rotateRight _ | exact mirror_rotateLeft _
+
+/-- Descend from `t` toward `q`, returning the subtree reached (either the
+matching node or `.nil` if `q` is absent) and the path above it. The head
+of the returned list is the deepest frame (parent of the returned subtree). -/
+def descend [LinearOrder α] (t : Tree α) (q : α) : Tree α × List (Frame α) :=
+  go t []
+where
+  /-- Worker for `descend`: accumulates path frames while walking toward `q`. -/
+  go : Tree α → List (Frame α) → Tree α × List (Frame α)
+  | .nil, acc => (.nil, acc)
+  | l △[k] r, acc =>
+    if q = k then (l △[k] r, acc)
+    else if q < k then go l ({ dir := .L, key := k, sibling := r } :: acc)
+    else go r ({ dir := .R, key := k, sibling := l } :: acc)
+
+/-- Splay the subtree `c` upward along `path`, pairing frames from the bottom
+up. Each double step (parent `f1`, grandparent `f2`) is:
+* **same-direction** (`zig-zig` / `zag-zag`): two outer rotations in direction
+  `f2.dir`;
+* **opposite-direction** (`zig-zag` / `zag-zig`): one inner rotation at the
+  `f2.dir`-child (in direction `f1.dir`), then one outer rotation (in
+  direction `f2.dir`).
+A leftover single frame is a plain zig/zag. -/
+def splayUp : Tree α → List (Frame α) → Tree α
+  | c, [] => c
+  | c, [f] => f.dir.bringUp (f.attach c)
+  | c, f1 :: f2 :: rest =>
+    let s := f2.attach (f1.attach c)
+    let s' :=
+      if f1.dir = f2.dir then
+        f2.dir.bringUp (f2.dir.bringUp s)
+      else
+        f2.dir.bringUp (applyChild f2.dir f1.dir.bringUp s)
+    splayUp s' rest
+
+/-- Bottom-up splay: the "textbook" splay analysed by Tarjan, Sundar, and
+Elmasry. If `q` is absent the last visited ancestor is splayed to the root. -/
+def splay [LinearOrder α] (t : Tree α) (q : α) : Tree α :=
+  match descend t q with
+  | (.nil, []) => .nil
+  | (.nil, f :: rest) => splayUp (f.attach .nil) rest
+  | (x@(.node _ _ _), path) => splayUp x path
+
+/-- Reassemble a subtree `c` with its ancestral path `path` (deepest frame
+first) back into the original tree. -/
+def reassemble (c : Tree α) (path : List (Frame α)) : Tree α :=
+  path.foldl (fun c' f => f.attach c') c
+
+@[simp] lemma reassemble_nil (c : Tree α) : reassemble c [] = c := rfl
+
+@[simp] lemma reassemble_cons (c : Tree α) (f : Frame α) (rest : List (Frame α)) :
+    reassemble c (f :: rest) = reassemble (f.attach c) rest := rfl
+
+/-- Number of nodes a single frame contributes when re-attached: the
+ancestor itself plus its sibling subtree. -/
+def Frame.nodes (f : Frame α) : ℕ := 1 + f.sibling.nodeCount
+
+/-- Total number of nodes contributed by a path above a subtree. -/
+def pathNodes : List (Frame α) → ℕ
+  | [] => 0
+  | f :: rest => f.nodes + pathNodes rest
+
+end Definitions
+
+
+/-! ### Unfolding and Induction Lemmas for `splayUp` -/
+section SplayUpInduction
+
+@[simp] theorem splayUp_nil (c : Tree α) : splayUp c [] = c := rfl
+
+@[simp] theorem splayUp_singleton (c : Tree α) (f : Frame α) :
+    splayUp c [f] = f.dir.bringUp (f.attach c) := rfl
+
+theorem splayUp_cons_cons (c : Tree α) (f1 f2 : Frame α) (rest : List (Frame α)) :
+    splayUp c (f1 :: f2 :: rest) =
+      splayUp
+        (if f1.dir = f2.dir then
+          f2.dir.bringUp (f2.dir.bringUp (f2.attach (f1.attach c)))
+        else
+          f2.dir.bringUp (applyChild f2.dir f1.dir.bringUp
+            (f2.attach (f1.attach c))))
+        rest := rfl
+
+theorem splayUp_cons_cons_same (c : Tree α) (f1 f2 : Frame α)
+    (rest : List (Frame α)) (h : f1.dir = f2.dir) :
+    splayUp c (f1 :: f2 :: rest) =
+      splayUp (f2.dir.bringUp (f2.dir.bringUp (f2.attach (f1.attach c)))) rest := by
+  rw [splayUp_cons_cons]; simp [h]
+
+theorem splayUp_cons_cons_opp (c : Tree α) (f1 f2 : Frame α)
+    (rest : List (Frame α)) (h : f1.dir ≠ f2.dir) :
+    splayUp c (f1 :: f2 :: rest) =
+      splayUp (f2.dir.bringUp
+        (applyChild f2.dir f1.dir.bringUp (f2.attach (f1.attach c)))) rest := by
+  rw [splayUp_cons_cons]; simp [h]
+
+/-- Two-step induction principle specialised to `splayUp`: base (empty path),
+singleton frame, and the general pair-cons step. The tree `c` is
+generalised automatically. -/
+theorem splayUp_induction
+    {motive : Tree α → List (Frame α) → Prop}
+    (nil : ∀ c, motive c [])
+    (single : ∀ c f, motive c [f])
+    (step : ∀ c f1 f2 rest,
+      (∀ c', motive c' rest) → motive c (f1 :: f2 :: rest))
+    (c : Tree α) (path : List (Frame α)) : motive c path := by
+  induction path using List.twoStepInduction generalizing c with
+  | nil => exact nil c
+  | singleton f => exact single c f
+  | cons_cons f1 f2 rest ih _ => exact step c f1 f2 rest (fun c' => ih c')
+
+end SplayUpInduction
+
+
+/-! ### Node-Count Invariants -/
+section NodeCount
+
+@[simp] lemma pathNodes_nil : pathNodes ([] : List (Frame α)) = 0 := rfl
+
+@[simp] lemma pathNodes_cons (f : Frame α) (rest : List (Frame α)) :
+    pathNodes (f :: rest) = f.nodes + pathNodes rest := rfl
+
+@[simp]
+theorem nodeCount_Frame_attach (c : Tree α) (f : Frame α) :
+    (f.attach c).nodeCount = c.nodeCount + f.nodes := by
+  unfold Frame.attach Frame.nodes
+  cases f.dir <;> simp <;> omega
+
+@[simp]
+theorem nodeCount_bringUp (d : Dir) (t : Tree α) :
+    (d.bringUp t).nodeCount = t.nodeCount := by
+  cases d <;> simp [Dir.bringUp]
+
+@[simp]
+theorem nodeCount_applyChild (d : Dir) (op : Tree α → Tree α)
+    (hop : ∀ s, (op s).nodeCount = s.nodeCount) (t : Tree α) :
+    (applyChild d op t).nodeCount = t.nodeCount := by
+  cases t with
+  | nil => rfl
+  | node k l r =>
+    cases d <;> simp [applyChild, hop]
+
+theorem nodeCount_applyChild_bringUp (d₁ d₂ : Dir) (t : Tree α) :
+    (applyChild d₁ d₂.bringUp t).nodeCount = t.nodeCount :=
+  nodeCount_applyChild _ _ (nodeCount_bringUp _) _
+
+@[simp]
+theorem nodeCount_splayUp (c : Tree α) (path : List (Frame α)) :
+    (splayUp c path).nodeCount = c.nodeCount + pathNodes path := by
+  induction path using List.twoStepInduction generalizing c with
+  | nil => simp [splayUp]
+  | singleton f => simp [splayUp, Frame.nodes, pathNodes]
+  | cons_cons f1 f2 rest ih _ =>
+    unfold splayUp
+    split_ifs with h
+    · rw [ih]; simp [Frame.nodes, pathNodes_cons]; omega
+    · rw [ih]; simp [Frame.nodes, pathNodes_cons]; omega
+
+theorem nodeCount_descend_go [LinearOrder α] (t : Tree α) (q : α) (acc : List (Frame α)) :
+    let r := descend.go q t acc
+    r.1.nodeCount + pathNodes r.2 = t.nodeCount + pathNodes acc := by
+  induction t generalizing acc with
+  | nil => simp [descend.go]
+  | node k l r ihl ihr =>
+    unfold descend.go
+    split_ifs with h1 h2
+    · simp
+    · have := ihl (acc := ⟨.L, k, r⟩ :: acc)
+      simp [Frame.nodes] at this ⊢; omega
+    · have := ihr (acc := ⟨.R, k, l⟩ :: acc)
+      simp [Frame.nodes] at this ⊢; omega
+
+theorem nodeCount_descend [LinearOrder α] (t : Tree α) (q : α) :
+    (descend t q).1.nodeCount + pathNodes (descend t q).2 = t.nodeCount := by
+  have := nodeCount_descend_go t q []
+  simpa [descend] using this
+
+@[simp]
+theorem nodeCount_splay [LinearOrder α] (t : Tree α) (q : α) :
+    (splay t q).nodeCount = t.nodeCount := by
+  unfold splay
+  have hd := nodeCount_descend t q
+  match h : descend t q with
+  | (.nil, []) =>
+      rw [h] at hd
+      simp at hd
+      simp [hd]
+  | (.nil, f :: rest) =>
+      rw [h] at hd
+      simp only [nodeCount_splayUp, nodeCount_Frame_attach,
+        nodeCount_empty, pathNodes_cons] at hd ⊢
+      omega
+  | (.node k l r, path) =>
+      rw [h] at hd
+      simp only [nodeCount_splayUp]
+      omega
+
+end NodeCount
+
+
+/-! ### Characterizations of `descend` -/
+section DescendLemmas
+
+@[simp] lemma descend_empty [LinearOrder α] (q : α) : descend .nil q = (.nil, []) := rfl
+
+lemma descend_go_append [LinearOrder α] (q : α) (t : Tree α) (acc : List (Frame α)) :
+    descend.go q t acc =
+      ((descend.go q t []).1, (descend.go q t []).2 ++ acc) := by
+  induction t generalizing acc with
+  | nil => simp [descend.go]
+  | node k l r ihl ihr =>
+    unfold descend.go
+    split_ifs with h1 h2
+    · simp
+    · rw [ihl (acc := ⟨.L, k, r⟩ :: acc),
+        ihl (acc := [⟨.L, k, r⟩])]; simp
+    · rw [ihr (acc := ⟨.R, k, l⟩ :: acc),
+        ihr (acc := [⟨.R, k, l⟩])]; simp
+
+lemma descend_node_eq [LinearOrder α] (l : Tree α) (k : α) (r : Tree α) :
+    descend (l △[k] r) k = (l △[k] r, []) := by
+  simp [descend, descend.go]
+
+lemma descend_eq_descend_go [LinearOrder α] (t : Tree α) (q : α) :
+    descend t q = descend.go q t [] := rfl
+
+lemma descend_node_lt [LinearOrder α] {l : Tree α} {k : α}
+    {r : Tree α} {q : α} (h : q < k) :
+    descend (l △[k] r) q =
+      ((descend l q).1,
+       (descend l q).2 ++ [⟨.L, k, r⟩]) := by
+  have hne : q ≠ k := ne_of_lt h
+  change descend.go q (l △[k] r) [] = _
+  unfold descend.go
+  rw [if_neg hne, if_pos h, descend_go_append q l [⟨.L, k, r⟩]]; rfl
+
+lemma descend_node_gt [LinearOrder α] {l : Tree α} {k : α}
+    {r : Tree α} {q : α} (h : k < q) :
+    descend (l △[k] r) q =
+      ((descend r q).1,
+       (descend r q).2 ++ [⟨.R, k, l⟩]) := by
+  have hne : q ≠ k := ne_of_gt h
+  change descend.go q (l △[k] r) [] = _
+  unfold descend.go
+  rw [if_neg hne, if_neg (not_lt.mpr h.le),
+      descend_go_append q r [⟨.R, k, l⟩]]; rfl
+
+lemma reassemble_append (c : Tree α) (p1 p2 : List (Frame α)) :
+    reassemble c (p1 ++ p2) = reassemble (reassemble c p1) p2 := by
+  simp [reassemble, List.foldl_append]
+
+theorem descend_go_preserves_tree [LinearOrder α] (t : Tree α)
+  (q : α) (acc : List (Frame α)) :
+    reassemble (descend.go q t acc).1 (descend.go q t acc).2 =
+      reassemble t acc := by
+  induction t generalizing acc with
+  | nil => simp [descend.go]
+  | node k l r ihl ihr =>
+    unfold descend.go
+    split_ifs with h1 h2
+    · simp
+    · exact ihl (acc := ⟨.L, k, r⟩ :: acc)
+    · exact ihr (acc := ⟨.R, k, l⟩ :: acc)
+
+theorem descend_preserves_tree [LinearOrder α] (t : Tree α) (q : α) :
+    reassemble (descend t q).1 (descend t q).2 = t := by
+  have := descend_go_preserves_tree t q []
+  simpa [descend] using this
+
+end DescendLemmas
+
+end SplayTree
diff --git a/Cslib/Foundations/Data/SplayTree/Complexity.lean b/Cslib/Foundations/Data/SplayTree/Complexity.lean
new file mode 100644
index 000000000..def1f22fa
--- /dev/null
+++ b/Cslib/Foundations/Data/SplayTree/Complexity.lean
@@ -0,0 +1,650 @@
+/-
+Copyright (c) 2026 Sorrachai Yingchareonthawornchai. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anton Kovsharov, Antoine du Fresne von Hohenesche,
+  Sorrachai Yingchareonthawornchai
+-/
+
+module
+
+public import Cslib.Foundations.Data.SplayTree.Basic
+public import Mathlib.Data.Real.Basic
+public import Mathlib.Analysis.SpecialFunctions.Log.Base
+
+/-!
+# Amortized Complexity of Splay Trees
+
+This module formalizes the amortized time complexity of bottom-up splay trees
+using the potential method introduced by Sleator and Tarjan.
+
+We define the rank of a tree as the base-2 logarithm of its node count, and
+the potential Φ as the sum of ranks over all subtrees. It culminates in
+the classical O(m log n + n log n) total cost bound for a sequence of
+splay operations.
+-/
+
+@[expose] public section
+
+variable {α : Type}
+
+namespace SplayTree
+
+open Tree
+
+/-! ### Cost and Search-Path Length -/
+section CostAndSearchPath
+
+/-- Cost of a bottom-up splay: one unit per rotation.
+Caution: If the search fails, we do not rotate (as currently
+defined in splay) the empty leaf and start to rotate from
+its ancestor, so the cost is path.length - 1. -/
+def splay.cost [LinearOrder α] (t : Tree α) (q : α) : ℕ :=
+  match descend t q with
+  | (.nil, []) => 0
+  | (.nil, _ :: rest) => rest.length
+  | (.node _ _ _, path) => path.length
+
+/-- Subtrees have positive search path length. -/
+lemma searchPathLen_node_pos [LinearOrder α] (l : Tree α) (k : α) (r : Tree α)
+    (q : α) : 1 ≤ (l △[k] r).searchPathLen q := by
+  unfold searchPathLen
+  split_ifs <;> omega
+
+/-- Relation between `searchPathLen` and the length of the path produced by
+`descend`. When `descend` reaches a node, the search path is one link longer;
+when it reaches `.nil`, the two are equal. -/
+theorem searchPathLen_eq_descend_length [LinearOrder α] (t : Tree α) (q : α) :
+    t.searchPathLen q =
+      (descend t q).2.length +
+        (match (descend t q).1 with | .nil => 0 | .node _ _ _ => 1) := by
+  induction t with
+  | nil => simp [searchPathLen, descend, descend.go]
+  | node k l r ihl ihr =>
+    by_cases hqk : q = k
+    · subst hqk
+      simp [searchPathLen, descend_node_eq]
+    · by_cases hlt : q < k
+      · rw [descend_node_lt hlt]
+        unfold searchPathLen
+        simp only [hlt, if_true, List.length_append, List.length_singleton]
+        rw [ihl]; omega
+      · have hgt : k < q := by grind only
+        rw [descend_node_gt hgt]
+        unfold searchPathLen
+        simp only [hlt, hgt, if_false, if_true, List.length_append,
+          List.length_singleton]
+        rw [ihr]; omega
+
+end CostAndSearchPath
+
+
+/-! ### Amortized Complexity (Potential Method)
+We follow Sleator–Tarjan's potential method. The rank of a tree is
+`log_2(nodeCount)`, the potential `φ` is the sum of ranks over all
+subtrees. Each splay step (zig, zig-zig, zig-zag) satisfies a
+per-step potential inequality, and these telescope along the frame
+path to give the O(log n) amortized bound.
+-/
+noncomputable section PotentialMethod
+
+/-- Rank of a tree: `log_2(nodeCount)`, or 0 for the empty tree. -/
+def rank (t : Tree α) : ℝ :=
+  if t.nodeCount = 0 then 0 else Real.logb 2 t.nodeCount
+
+/-- Potential of a tree: sum of ranks over all subtrees (including itself). -/
+def φ : Tree α → ℝ
+  | .nil => 0
+  | s@(l △[_] r) => rank s + φ l + φ r
+
+/-! #### The key logarithmic inequality (AM-GM for logs) -/
+
+theorem log_sum_le {a b c : ℝ} (ha : 0 < a) (hb : 0 < b)
+    (hsum : a + b ≤ c) :
+    Real.logb 2 a + Real.logb 2 b ≤ 2 * Real.logb 2 c - 2 := by
+  have hc : 0 < c := by linarith
+  have hab_le : a * b ≤ c ^ 2 / 4 := by nlinarith [sq_nonneg (a - b)]
+  have hln2 : (0 : ℝ) < Real.log 2 := Real.log_pos (by norm_num)
+  suffices h : Real.log a + Real.log b ≤
+      2 * Real.log c - 2 * Real.log 2 by
+    simp only [Real.logb]
+    rw [show Real.log a / Real.log 2 + Real.log b / Real.log 2 =
+      (Real.log a + Real.log b) / Real.log 2 from by ring]
+    rw [show 2 * (Real.log c / Real.log 2) - 2 =
+      (2 * Real.log c - 2 * Real.log 2) / Real.log 2 from by
+        field_simp]
+    exact div_le_div_of_nonneg_right h hln2.le
+  calc Real.log a + Real.log b
+      = Real.log (a * b) := by
+        rw [Real.log_mul (by positivity) (by positivity)]
+    _ ≤ Real.log (c ^ 2 / 4) :=
+        Real.log_le_log (by positivity) hab_le
+    _ = Real.log (c ^ 2) - Real.log 4 :=
+        Real.log_div (by positivity) (by positivity)
+    _ = 2 * Real.log c - 2 * Real.log 2 := by
+        rw [Real.log_pow, show (4:ℝ) = 2^2 from by norm_num,
+          Real.log_pow]; push_cast; ring
+
+/-! #### Basic rank and potential lemmas -/
+
+@[simp] lemma rank_empty : rank (.nil : Tree α) = 0 := by simp [rank]
+
+lemma rank_nonneg (t : Tree α) : 0 ≤ rank t := by
+  simp only [rank]; split_ifs with h
+  · rfl
+  · exact Real.logb_nonneg (by grind)
+      (by exact_mod_cast Nat.one_le_iff_ne_zero.mpr h)
+
+@[simp] lemma φ_empty : φ (.nil : Tree α) = 0 := rfl
+
+@[simp] lemma φ_node (l : Tree α) (k : α) (r : Tree α) :
+    φ (l △[k] r) = rank (l △[k] r) + φ l + φ r := rfl
+
+lemma φ_nonneg : ∀ t : Tree α, 0 ≤ φ t
+  | .nil => le_refl _
+  | l △[k] r => by
+      simp [φ]; linarith [rank_nonneg (l △[k] r), φ_nonneg l, φ_nonneg r]
+
+lemma rank_le_of_nodeCount_le {s t : Tree α}
+    (h : s.nodeCount ≤ t.nodeCount) : rank s ≤ rank t := by
+  simp only [rank]
+  split_ifs with hs ht ht
+  · exact le_refl _
+  · exact Real.logb_nonneg (by norm_num)
+      (by exact_mod_cast Nat.one_le_iff_ne_zero.mpr ht)
+  · omega
+  · apply Real.logb_le_logb_of_le (by norm_num)
+      (by exact_mod_cast Nat.one_le_iff_ne_zero.mpr hs)
+      (by simp_all only [Nat.cast_le])
+
+lemma rank_eq_of_nodeCount_eq {s t : Tree α}
+    (h : s.nodeCount = t.nodeCount) : rank s = rank t := by
+  exact le_antisymm (rank_le_of_nodeCount_le (le_of_eq h))
+    (rank_le_of_nodeCount_le (le_of_eq h.symm))
+
+@[simp] lemma rank_splay [LinearOrder α] (t : Tree α) (q : α) :
+    rank (splay t q) = rank t :=
+  rank_eq_of_nodeCount_eq (nodeCount_splay t q)
+
+/-! #### Mirror preserves rank and potential -/
+
+lemma rank_mirror (t : Tree α) : rank t.mirror = rank t := by
+  simp [rank]
+
+lemma φ_mirror : ∀ t : Tree α, φ t.mirror = φ t
+  | .nil => rfl
+  | l △[k] r => by
+    change rank (r.mirror △[k] l.mirror) + φ r.mirror + φ l.mirror =
+      rank (l △[k] r) + φ l + φ r
+    rw [φ_mirror l, φ_mirror r]
+    linarith [rank_eq_of_nodeCount_eq
+      (show (r.mirror △[k] l.mirror).nodeCount =
+        (l △[k] r).nodeCount by simp [nodeCount]; omega)]
+
+/-- Transfer a potential-step inequality from mirrored trees to the
+originals. -/
+private lemma φ_transfer_mirror
+    {step s c step' s' : Tree α}
+    (hstep : step.mirror = step')
+    (hs : s.mirror = s')
+    (h : φ step' - φ s' + 2 ≤
+      3 * (rank step' - rank c.mirror)) :
+    φ step - φ s + 2 ≤ 3 * (rank step - rank c) := by
+  rw [← hstep, φ_mirror, rank_mirror] at h
+  rw [← hs, φ_mirror] at h
+  linarith [rank_mirror c]
+
+/-! #### Short‐hands for `logb 2` arithmetic (used in zig‐zig / zig‐zag) -/
+
+/-- Monotonicity of `logb 2`. -/
+private lemma logb_mono {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :
+    Real.logb 2 a ≤ Real.logb 2 b :=
+  Real.logb_le_logb_of_le (by norm_num) ha hab
+
+/-- Non‐negativity of `logb 2 x` when `x ≥ 1`. -/
+private lemma logb_nonneg {x : ℝ} (hx : 1 ≤ x) :
+    0 ≤ Real.logb 2 x :=
+  Real.logb_nonneg (by norm_num) hx
+
+/-- `logb 2 x ≥ 1` when `x ≥ 2`. -/
+private lemma one_le_logb {x : ℝ} (hx : 2 ≤ x) :
+    1 ≤ Real.logb 2 x := by
+  rwa [Real.le_logb_iff_rpow_le (by norm_num : (1 : ℝ) < 2) (by linarith),
+    show (2 : ℝ) ^ (1 : ℝ) = 2 from by norm_num]
+
+/-! #### Potential of subtrees versus the whole tree -/
+
+theorem φ_subtree_le_left (l : Tree α) (k : α) (r : Tree α) :
+    φ l ≤ φ (l △[k] r) := by
+  simp [φ]; linarith [rank_nonneg (l △[k] r), φ_nonneg r]
+
+theorem φ_subtree_le_right (l : Tree α) (k : α) (r : Tree α) :
+    φ r ≤ φ (l △[k] r) := by
+  simp [φ]; linarith [rank_nonneg (l △[k] r), φ_nonneg l]
+
+theorem φ_le_attach (c : Tree α) (f : Frame α) :
+  φ c ≤ φ (f.attach c) := by
+  cases f with | mk d k s =>
+  cases d <;> simp [Frame.attach, φ_node] <;>
+  linarith [rank_nonneg (c △[k] s), rank_nonneg (s △[k] c),
+  φ_nonneg c, φ_nonneg s]
+
+theorem φ_le_reassemble (c : Tree α) (path : List (Frame α)) :
+    φ c ≤ φ (reassemble c path) := by
+  induction path generalizing c with
+  | nil => simp
+  | cons f rest ih => simp only [reassemble_cons]; exact le_trans (φ_le_attach c f) (ih _)
+
+theorem φ_descend_subtree_le [LinearOrder α] (t : Tree α) (q : α) :
+    φ (descend t q).1 ≤ φ t := by
+  have h := descend_preserves_tree t q
+  calc φ (descend t q).1
+      ≤ φ (reassemble (descend t q).1 (descend t q).2) :=
+        φ_le_reassemble _ _
+    _ = φ t := by rw [h]
+
+/-! #### Splay step potential bounds -/
+
+theorem φ_zig (c : Tree α) (f : Frame α) :
+    φ (f.dir.bringUp (f.attach c)) - φ (f.attach c) ≤
+      rank (f.dir.bringUp (f.attach c)) - rank c := by
+  rcases f with ⟨d, key, sib⟩
+  rcases c with _ | ⟨k, l, r⟩ <;> cases d <;>
+    all_goals simp only [Dir.bringUp, rotateLeft, rotateRight,
+    Frame.attach, φ_node, φ_empty, add_zero, sub_self, rank_empty, sub_zero]
+  -- empty: 0 ≤ rank t; node: rank(child) ≤ rank(parent)
+  · exact rank_nonneg _
+  · exact rank_nonneg _
+  · linarith [rank_le_of_nodeCount_le (show
+      (r △[key] sib).nodeCount ≤
+      ((l △[k] r) △[key] sib).nodeCount
+      by simp)]
+  · linarith [rank_le_of_nodeCount_le (show
+      (sib △[key] l).nodeCount ≤
+      (sib △[key] (l △[k] r)).nodeCount
+      by simp; omega)]
+
+/-- Zig-zig, left–left direction only. -/
+private theorem φ_zigzig_left (c : Tree α)
+    (k1 : α) (n1 : Tree α) (k2 : α) (n2 : Tree α) :
+    let s := (Frame.mk .L k2 n2).attach ((Frame.mk .L k1 n1).attach c)
+    let step := rotateRight (rotateRight s)
+    φ step - φ s + 2 ≤ 3 * (rank step - rank c) := by
+  set nn1 := (n1.nodeCount : ℝ); set nn2 := (n2.nodeCount : ℝ)
+  have h1 : (0 : ℝ) ≤ nn1 := by positivity
+  have h2 : (0 : ℝ) ≤ nn2 := by positivity
+  rcases c with _ | ⟨k, l, r⟩ <;>
+    simp +decide only [Frame.attach, rotateRight,
+      φ_node, φ_empty, rank, add_zero, sub_zero,
+      nodeCount_node, nodeCount_empty,
+      Nat.add_eq_zero_iff, false_and, and_self,
+      ↓reduceIte, Nat.cast_add, Nat.cast_one]
+  all_goals ring_nf
+  · nlinarith [
+      logb_mono (show (0 : ℝ) < 1 + nn1 + nn2 by linarith)
+        (show 1 + nn1 + nn2 ≤ 2 + nn1 + nn2 by linarith),
+      logb_nonneg (show (1 : ℝ) ≤ 1 + nn1 by linarith),
+      one_le_logb (show (2 : ℝ) ≤ 2 + nn1 + nn2 by linarith)]
+  · set a := (l.nodeCount : ℝ); set b := (r.nodeCount : ℝ)
+    have ha : (0 : ℝ) ≤ a := by positivity
+    have hb : (0 : ℝ) ≤ b := by positivity
+    have hls := log_sum_le
+        (show (0 : ℝ) < 1 + a + b by linarith)
+        (show (0 : ℝ) < 1 + nn1 + nn2 by linarith)
+        (show 1 + a + b + (1 + nn1 + nn2) ≤
+          3 + a + b + nn1 + nn2 by linarith)
+    nlinarith [
+      logb_mono (show (0 : ℝ) < 2 + b + nn1 + nn2 by linarith)
+        (show 2 + b + nn1 + nn2 ≤
+          3 + a + b + nn1 + nn2 by linarith),
+      logb_mono (show (0 : ℝ) < 1 + a + b by linarith)
+        (show 1 + a + b ≤ 2 + a + b + nn1 by linarith)]
+
+theorem φ_zigzig (c : Tree α) (f1 f2 : Frame α)
+    (heq : f1.dir = f2.dir) :
+    let s := f2.attach (f1.attach c)
+    let step := f2.dir.bringUp (f2.dir.bringUp s)
+    φ step - φ s + 2 ≤ 3 * (rank step - rank c) := by
+  rcases f1 with ⟨d, k1, n1⟩; rcases f2 with ⟨_, k2, n2⟩; subst heq
+  cases d
+  · exact φ_zigzig_left c k1 n1 k2 n2
+  · have h := φ_zigzig_left c.mirror k1 n1.mirror k2 n2.mirror
+    simp only [Frame.attach, Dir.bringUp] at h ⊢
+    exact φ_transfer_mirror (by simp [mirror_rotateLeft]) (by simp) h
+
+/-- Zig-zag, left–right direction only. -/
+private theorem φ_zigzag_left (c : Tree α)
+    (k1 : α) (n1 : Tree α) (k2 : α) (n2 : Tree α) :
+    let f1 : Frame α := ⟨.L, k1, n1⟩
+    let f2 : Frame α := ⟨.R, k2, n2⟩
+    let s := f2.attach (f1.attach c)
+    let step := rotateLeft (applyChild .R rotateRight s)
+    φ step - φ s + 2 ≤ 3 * (rank step - rank c) := by
+  set nn1 := (n1.nodeCount : ℝ); set nn2 := (n2.nodeCount : ℝ)
+  have h1 : (0 : ℝ) ≤ nn1 := by positivity
+  have h2 : (0 : ℝ) ≤ nn2 := by positivity
+  rcases c with _ | ⟨k, l, r⟩ <;>
+    simp +decide only [Frame.attach, applyChild,
+      rotateRight, rotateLeft,
+      φ_node, φ_empty, rank, add_zero, sub_zero,
+      nodeCount_node, nodeCount_empty,
+      Nat.add_eq_zero_iff, false_and, and_self,
+      ↓reduceIte, Nat.cast_add, Nat.cast_one]
+  all_goals ring_nf
+  · have hls := log_sum_le
+        (show (0 : ℝ) < nn1 + 1 by linarith)
+        (show (0 : ℝ) < nn2 + 1 by linarith)
+        (show nn1 + 1 + (nn2 + 1) ≤ nn1 + nn2 + 2 by linarith)
+    simp only [show nn1 + 1 = 1 + nn1 by ring,
+      show nn2 + 1 = 1 + nn2 by ring,
+      show nn1 + nn2 + 2 = 2 + nn2 + nn1 by ring] at hls
+    linarith [
+      logb_nonneg (show (1 : ℝ) ≤ 1 + nn1 by linarith),
+      logb_nonneg (show (1 : ℝ) ≤ 1 + nn2 by linarith)]
+  · set a := (l.nodeCount : ℝ); set b := (r.nodeCount : ℝ)
+    have ha : (0 : ℝ) ≤ a := by positivity
+    have hb : (0 : ℝ) ≤ b := by positivity
+    have hls := log_sum_le
+        (show (0 : ℝ) < 1 + nn2 + a by linarith)
+        (show (0 : ℝ) < 1 + b + nn1 by linarith)
+        (show 1 + nn2 + a + (1 + b + nn1) ≤
+          3 + nn2 + a + b + nn1 by linarith)
+    nlinarith [
+      logb_mono (show (0 : ℝ) < 1 + a + b by linarith)
+        (show 1 + a + b ≤ 2 + a + b + nn1 by linarith),
+      logb_mono (show (0 : ℝ) < 1 + a + b by linarith)
+        (show 1 + a + b ≤ 3 + nn2 + a + b + nn1 by linarith)]
+
+theorem φ_zigzag (c : Tree α) (f1 f2 : Frame α)
+    (hne : f1.dir ≠ f2.dir) :
+    let s := f2.attach (f1.attach c)
+    let step := f2.dir.bringUp (applyChild f2.dir f1.dir.bringUp s)
+    φ step - φ s + 2 ≤ 3 * (rank step - rank c) := by
+  rcases f1 with ⟨d1, k1, n1⟩; rcases f2 with ⟨d2, k2, n2⟩
+  cases d1 <;> cases d2 <;> simp_all +decide only [ne_eq]
+  · exact φ_zigzag_left c k1 n1 k2 n2
+  · have h := φ_zigzag_left c.mirror k1 n1.mirror k2 n2.mirror
+    simp only [Frame.attach, Dir.bringUp, applyChild] at h ⊢
+    exact φ_transfer_mirror
+      (by simp [mirror_rotateRight, mirror_rotateLeft]) (by simp) h
+
+/-! #### Telescoping: potential change along the full splayUp -/
+
+lemma φ_attach_congr {s s' : Tree α} (f : Frame α)
+    (h : s.nodeCount = s'.nodeCount) :
+    φ (f.attach s') - φ (f.attach s) = φ s' - φ s := by
+  cases f with | mk d k sib =>
+  cases d <;> simp only [Frame.attach, φ_node, add_sub_add_right_eq_sub] <;>
+    (unfold rank; simp [h])
+
+lemma φ_reassemble_congr {s s' : Tree α} (path : List (Frame α))
+    (h : s.nodeCount = s'.nodeCount) :
+    φ (reassemble s' path) - φ (reassemble s path) = φ s' - φ s := by
+  induction path generalizing s s' with
+  | nil => simp
+  | cons f rest ih =>
+    simp only [reassemble_cons]
+    rw [ih (by simp [nodeCount_Frame_attach, h])]
+    exact φ_attach_congr f h
+
+/-- The total potential change of splayUp plus the path length is at
+    most 3 × the rank increase + 1. -/
+theorem φ_splayUp (c : Tree α) (path : List (Frame α)) :
+    φ (splayUp c path) - φ (reassemble c path) + path.length ≤
+      3 * (rank (splayUp c path) - rank c) + 1 := by
+  induction c, path using splayUp_induction with
+  | nil c => simp
+  | single c f =>
+    simp only [splayUp_singleton, reassemble_cons,
+      reassemble_nil, List.length_singleton, Nat.cast_one]
+    linarith [φ_zig c f,
+      rank_le_of_nodeCount_le (α := α)
+        (show c.nodeCount ≤
+          (f.dir.bringUp (f.attach c)).nodeCount from by simp)]
+  | step c f1 f2 rest ih =>
+    rw [splayUp_cons_cons]; simp only [List.length_cons]
+    split_ifs with hdir
+    · set s := f2.attach (f1.attach c)
+      set step_tree := f2.dir.bringUp (f2.dir.bringUp s)
+      have hnn : step_tree.nodeCount = s.nodeCount := by
+        simp [step_tree]
+      simp only [reassemble_cons]; push_cast
+      nlinarith [ih step_tree,
+        φ_reassemble_congr rest hnn.symm, φ_zigzig c f1 f2 hdir]
+    · set s := f2.attach (f1.attach c)
+      set step_tree :=
+        f2.dir.bringUp (applyChild f2.dir f1.dir.bringUp s)
+      have hnn : step_tree.nodeCount = s.nodeCount := by
+        simp [step_tree]
+      simp only [reassemble_cons]; push_cast
+      nlinarith [ih step_tree,
+        φ_reassemble_congr rest hnn.symm, φ_zigzag c f1 f2 hdir]
+
+/-! #### The main O(log n) amortized bound -/
+
+private lemma rank_eq_logb {t : Tree α}
+    (h : t.nodeCount ≠ 0) :
+    rank t = Real.logb 2 t.nodeCount := by
+  simp [rank, h]
+
+private lemma nodeCount_pos_of_descend_nonempty_path
+    [LinearOrder α] {t : Tree α} {q : α}
+    {reached : Tree α} {path : List (Frame α)}
+    (hdecomp : descend t q = (reached, path))
+    (hpath : path ≠ []) : t.nodeCount ≠ 0 := by
+  intro h0
+  have hd := nodeCount_descend t q
+  rw [hdecomp] at hd; simp at hd
+  rcases path with _ | ⟨f, rest⟩
+  · exact hpath rfl
+  · simp [pathNodes, Frame.nodes] at hd; omega
+
+theorem splay_amortized_bound [LinearOrder α]
+    (t : Tree α) (q : α) :
+    φ (splay t q) - φ t + splay.cost t q ≤
+      3 * Real.logb 2 t.nodeCount + 1 := by
+  rcases hdecomp : descend t q with ⟨reached, path⟩
+  have hpres := descend_preserves_tree t q
+  rw [hdecomp] at hpres; simp only at hpres
+  have h_splay : splay t q = splayUp reached path ∨
+      (∃ f rest, reached = .nil ∧
+        path = f :: rest ∧
+        splay t q = splayUp (f.attach .nil) rest) := by
+    simp only [splay, hdecomp]
+    rcases reached with _ | ⟨k, l, r⟩
+    · rcases path with _ | ⟨f, rest⟩
+      · left; rfl
+      · right; exact ⟨f, rest, rfl, rfl, rfl⟩
+    · left; rfl
+  rcases reached with _ | ⟨k, l, r⟩
+  · rcases path with _ | ⟨f, rest⟩
+    · simp only [reassemble, List.foldl_nil] at hpres
+      subst hpres
+      simp [splay, splay.cost, hdecomp, φ]
+    · have h_cost : splay.cost t q = rest.length := by simp [splay.cost, hdecomp]
+      rw [h_cost]
+      have h_eq : splay t q = splayUp (f.attach .nil) rest := by simp [splay, hdecomp]
+      rw [h_eq]
+      set base := f.attach (.nil : Tree α)
+      have hpres' : reassemble base rest = t := by rw [← hpres]; simp [reassemble, base]
+      have hφ := φ_splayUp base rest
+      rw [hpres'] at hφ
+      have hrank_eq : rank (splayUp base rest) = rank t := by
+        have h := rank_splay t q; simp only [splay, hdecomp] at h; exact h
+      have hnn : t.nodeCount ≠ 0 :=
+        nodeCount_pos_of_descend_nonempty_path hdecomp (List.cons_ne_nil f rest)
+      calc φ (splayUp base rest) - φ t + ↑rest.length
+          ≤ 3 * (rank (splayUp base rest) - rank base) + 1 := by exact_mod_cast hφ
+        _ ≤ 3 * rank (splayUp base rest) + 1 := by linarith [rank_nonneg base]
+        _ = 3 * Real.logb 2 t.nodeCount + 1 := by rw [hrank_eq, rank_eq_logb hnn]
+  · have h_cost : splay.cost t q = path.length := by simp [splay.cost, hdecomp]
+    rw [h_cost]
+    have h_eq : splay t q = splayUp (l △[k] r) path := by simp [splay, hdecomp]
+    rw [h_eq]
+    have hφ := φ_splayUp (l △[k] r) path
+    rw [hpres] at hφ
+    have hrank_eq : rank (splayUp (l △[k] r) path) = rank t := by
+      have h := rank_splay t q; simp only [splay, hdecomp] at h; exact h
+    have hnn : t.nodeCount ≠ 0 := by
+      have hd := nodeCount_descend t q; rw [hdecomp] at hd; simp at hd; omega
+    calc φ (splayUp (l △[k] r) path) - φ t + ↑path.length
+        ≤ 3 * (rank (splayUp (l △[k] r) path) - rank (l △[k] r)) + 1 := by exact_mod_cast hφ
+      _ ≤ 3 * rank (splayUp (l △[k] r) path) + 1 := by linarith [rank_nonneg (l △[k] r)]
+      _ = 3 * Real.logb 2 t.nodeCount + 1 := by rw [hrank_eq, rank_eq_logb hnn]
+
+end PotentialMethod
+
+
+/-! ### Sequence Cost and The O(m log n) Amortized Bound -/
+section SequenceCost
+
+/-! #### Splay Sequence -/
+
+/-- A clean sequence generator for a series of splays. -/
+def splaySeq [LinearOrder α] {m : ℕ} (init : Tree α)
+(X : Fin m → α) : Fin (m + 1) → Tree α :=
+  fun i => Nat.recOn i.val init (fun j acc =>
+    if h : j < m then splay acc (X ⟨j, h⟩) else acc)
+
+/-- The total cost is defined as the sum of actual rotations
+performed across the generated sequence. -/
+def splay.sequenceCost [LinearOrder α] {m : ℕ} (init : Tree α) (X : Fin m → α) : ℕ :=
+  ∑ i : Fin m, splay.cost (splaySeq init X i.castSucc) (X i)
+
+/-- The tree at step `i+1` is exactly the result of splaying the target key
+on the tree at step `i`. -/
+lemma splaySeq_succ [LinearOrder α] {m : ℕ}
+(init : Tree α) (X : Fin m → α) (i : Fin m) :
+    splaySeq init X i.succ = splay (splaySeq init X i.castSucc) (X i) := by
+  unfold splaySeq
+  simp only [Fin.val_succ, Fin.val_castSucc, Fin.is_lt, ↓reduceDIte]
+
+/-- Splaying preserves the number of nodes across the entire sequence. -/
+lemma splaySeq_nodeCount [LinearOrder α] {m : ℕ}
+(init : Tree α) (X : Fin m → α) (i : Fin (m + 1)) :
+    (splaySeq init X i).nodeCount = init.nodeCount := by
+  unfold splaySeq
+  generalize i.val = j
+  induction j with
+  | zero => rfl
+  | succ k ih =>
+    simp_all only
+    split
+    next h => simp_all only [nodeCount_splay]
+    next h => simp_all only [not_lt]
+
+/-! #### Initial Potential Bound -/
+
+private lemma nat_log_le (a b : ℕ) (hab : a ≤ b) :
+    (a : ℝ) * Real.logb 2 a ≤ (a : ℝ) * Real.logb 2 b := by
+  by_cases ha : a = 0
+  · simp [ha]
+  · have ha_pos : (0 : ℝ) < a := Nat.cast_pos.mpr (Nat.pos_of_ne_zero ha)
+    have hab_real : (a : ℝ) ≤ (b : ℝ) := Nat.cast_le.mpr hab
+    have h_log : Real.logb 2 a ≤ Real.logb 2 b :=
+      Real.logb_le_logb_of_le (by norm_num) ha_pos hab_real
+    have ha_nonneg : (0 : ℝ) ≤ a := Nat.cast_nonneg a
+    exact mul_le_mul_of_nonneg_left h_log ha_nonneg
+
+/-- Bound the maximum possible potential of any initial tree: Φ ≤ n log₂ n. -/
+lemma φ_le_n_log_n [LinearOrder α] (init : Tree α) :
+    φ init ≤ init.nodeCount * Real.logb 2 init.nodeCount := by
+  induction init with
+  | nil => simp [φ]
+  | node k l r ihl ihr =>
+    set t := l △[k] r
+    have hl_le : l.nodeCount ≤ t.nodeCount := by simp [t, nodeCount]; omega
+    have hr_le : r.nodeCount ≤ t.nodeCount := by simp [t, nodeCount]
+    have h_rank : rank t = Real.logb 2 t.nodeCount := by
+      unfold rank
+      have : t.nodeCount ≠ 0 := by simp [t, nodeCount]
+      simp [this]
+    calc φ t = rank t + φ l + φ r := rfl
+      _ ≤ rank t + l.nodeCount * Real.logb 2 l.nodeCount +
+                   r.nodeCount * Real.logb 2 r.nodeCount := by linarith
+      _ ≤ Real.logb 2 t.nodeCount +
+          l.nodeCount * Real.logb 2 t.nodeCount +
+          r.nodeCount * Real.logb 2 t.nodeCount := by
+        rw [h_rank]
+        have h1 := nat_log_le _ _ hl_le
+        have h2 := nat_log_le _ _ hr_le
+        linarith
+      _ = (1 + l.nodeCount + r.nodeCount : ℝ) * Real.logb 2 t.nodeCount := by ring
+      _ = t.nodeCount * Real.logb 2 t.nodeCount := by simp [t, nodeCount]
+
+/-! #### General Sequence Cost Theorem -/
+
+theorem amortized_cost_bound {S : Type*} (m : ℕ)
+    (s : Fin (m + 1) → S) (cost : Fin m → ℝ)
+    (Φ : S → ℝ) (B : ℝ)
+    (hamort : ∀ i : Fin m,
+      Φ (s i.succ) - Φ (s i.castSucc) + cost i ≤ B) :
+    ∑ i : Fin m, cost i ≤
+      m * B + Φ (s 0) - Φ (s (Fin.last m)) := by
+  have := Finset.sum_le_sum fun i (_ : i ∈ Finset.univ) =>
+    hamort i
+  simp_all +decide only [Finset.sum_add_distrib, Finset.sum_sub_distrib,
+  Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul,
+  ge_iff_le]
+  linarith! [Fin.sum_univ_castSucc fun i => Φ (s i),
+    Fin.sum_univ_succ fun i => Φ (s i)]
+
+theorem amortized_cost_bound' {S : Type*} (m : ℕ)
+    (s : Fin (m + 1) → S) (cost : Fin m → ℝ)
+    (Φ : S → ℝ) (B : ℝ)
+    (hamort : ∀ i : Fin m,
+      Φ (s i.succ) - Φ (s i.castSucc) + cost i ≤ B)
+    (hΦ_nonneg : ∀ x, 0 ≤ Φ x) :
+    ∑ i : Fin m, cost i ≤ m * B + Φ (s 0) := by
+  linarith [amortized_cost_bound m s cost Φ B hamort,
+    hΦ_nonneg (s (Fin.last m))]
+
+theorem splay_total_cost [LinearOrder α] (m : ℕ)
+    (t : Fin (m + 1) → Tree α)
+    (q : Fin m → α) (n : ℕ)
+    (hseq : ∀ i : Fin m,
+      t i.succ = splay (t i.castSucc) (q i))
+    (hsize : ∀ i : Fin (m + 1),
+      (t i).nodeCount ≤ n) :
+    ∑ i : Fin m,
+      (splay.cost (t i.castSucc) (q i) : ℝ) ≤
+      m * (3 * Real.logb 2 n + 1) + φ (t 0) := by
+  apply amortized_cost_bound' m t
+    (fun i => (splay.cost (t i.castSucc) (q i) : ℝ))
+    φ (3 * Real.logb 2 n + 1)
+  · intro i
+    rw [hseq i]
+    have hb := splay_amortized_bound
+      (t i.castSucc) (q i)
+    by_cases h : (t (Fin.castSucc i)).nodeCount = 0
+    · simp_all +decide [Real.logb]
+      have : (0 : ℝ) ≤ Real.log n / Real.log 2 :=
+        by positivity
+      linarith
+    · calc φ (splay (t i.castSucc) (q i)) -
+              φ (t i.castSucc) +
+              splay.cost (t i.castSucc) (q i)
+          ≤ 3 * Real.logb 2
+              (t i.castSucc).nodeCount + 1 := hb
+        _ ≤ 3 * Real.logb 2 n + 1 := by
+            gcongr <;> [norm_num; exact hsize _]
+  · exact fun x => φ_nonneg x
+
+/-! #### The Main Total Cost Bound Theorem -/
+
+theorem nlogn_cost [LinearOrder α] (n m : ℕ) (X : Fin m → α)
+    (init : Tree α) (h_size : init.nodeCount = n) :
+    splay.sequenceCost init X ≤ m * (3 * Real.logb 2 n + 1) + n * Real.logb 2 n := by
+  have h_amortized := splay_total_cost m (splaySeq init X) X n
+    (splaySeq_succ init X)
+    (fun i => by rw [splaySeq_nodeCount, h_size])
+  have h_phi_bound : φ (splaySeq init X 0) ≤ n * Real.logb 2 n := by
+    have : splaySeq init X 0 = init := rfl
+    rw [this, ← h_size]
+    exact φ_le_n_log_n init
+  unfold splay.sequenceCost
+  push_cast
+  linarith
+
+end SequenceCost
+
+end SplayTree
diff --git a/Cslib/Foundations/Data/SplayTree/Correctness.lean b/Cslib/Foundations/Data/SplayTree/Correctness.lean
new file mode 100644
index 000000000..839e5a467
--- /dev/null
+++ b/Cslib/Foundations/Data/SplayTree/Correctness.lean
@@ -0,0 +1,246 @@
+/-
+Copyright (c) 2026 Sorrachai Yingchareonthawornchai. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anton Kovsharov, Antoine du Fresne von Hohenesche,
+  Sorrachai Yingchareonthawornchai
+-/
+
+module
+
+public import Cslib.Foundations.Data.SplayTree.Basic
+
+/-!
+# Splay Tree Correctness
+
+This module proves the functional correctness of the splay operation.
+It establishes that splaying preserves the binary search tree (BST) invariant
+and guarantees that querying an existing key successfully rotates it to the root.
+-/
+
+@[expose] public section
+
+variable {α : Type}
+
+namespace SplayTree
+
+open Tree
+
+/-! ### `toKeyList` Preservation -/
+section ToKeyListPreservation
+
+@[simp] theorem toKeyList_rotateRight (t : Tree α) :
+    (rotateRight t).toKeyList = t.toKeyList := by
+  cases t; · rfl
+  rename_i k l r
+  cases l <;> simp [rotateRight, toKeyList]
+
+@[simp] theorem toKeyList_rotateLeft (t : Tree α) :
+    (rotateLeft t).toKeyList = t.toKeyList := by
+  cases t; · rfl
+  rename_i k l r
+  cases r <;> simp [rotateLeft, toKeyList]
+
+@[simp] theorem toKeyList_bringUp (d : Dir) (t : Tree α) :
+    (d.bringUp t).toKeyList = t.toKeyList := by
+  cases d <;> simp [Dir.bringUp]
+
+@[simp] theorem toKeyList_applyChild (d : Dir) (op : Tree α → Tree α)
+    (hop : ∀ s, (op s).toKeyList = s.toKeyList) (t : Tree α) :
+    (applyChild d op t).toKeyList = t.toKeyList := by
+  cases t with
+  | nil => rfl
+  | node k l r => cases d <;> simp [applyChild, toKeyList, hop]
+
+theorem toKeyList_applyChild_bringUp (d₁ d₂ : Dir) (t : Tree α) :
+    (applyChild d₁ d₂.bringUp t).toKeyList = t.toKeyList :=
+  toKeyList_applyChild _ _ (toKeyList_bringUp _) _
+
+@[simp] theorem toKeyList_Frame_attach (c : Tree α) (f : Frame α) :
+    (f.attach c).toKeyList =
+      (match f.dir with
+        | .L => c.toKeyList ++ [f.key] ++ f.sibling.toKeyList
+        | .R => f.sibling.toKeyList ++ [f.key] ++ c.toKeyList) := by
+  unfold Frame.attach
+  cases f.dir <;> simp [toKeyList]
+
+lemma reassemble_toKeyList_congr {c1 c2 : Tree α} (path : List (Frame α))
+    (h : c1.toKeyList = c2.toKeyList) :
+    (reassemble c1 path).toKeyList = (reassemble c2 path).toKeyList := by
+  induction path generalizing c1 c2 with
+  | nil => simp [h]
+  | cons f rest ih =>
+    apply ih
+    simp [h]
+
+@[simp]
+theorem toKeyList_splayUp (c : Tree α) (path : List (Frame α)) :
+    (splayUp c path).toKeyList = (reassemble c path).toKeyList := by
+  induction c, path using splayUp_induction with
+  | nil c => simp
+  | single c f =>
+    simp [splayUp, reassemble]
+  | step c f1 f2 rest ih =>
+    unfold splayUp; split_ifs <;>
+      (rw [ih]; apply reassemble_toKeyList_congr; simp)
+
+@[simp]
+theorem toKeyList_splay [LinearOrder α] (t : Tree α) (q : α) :
+    (splay t q).toKeyList = t.toKeyList := by
+  unfold splay
+  have hpres := descend_preserves_tree t q
+  match h : descend t q with
+  | (.nil, []) =>
+      rw [h] at hpres
+      simp at hpres
+      simp [← hpres]
+  | (.nil, f :: rest) =>
+      rw [h] at hpres
+      rw [toKeyList_splayUp, ← hpres]
+      simp [reassemble]
+  | (.node k l r, path) =>
+      rw [h] at hpres
+      rw [toKeyList_splayUp, ← hpres]
+
+theorem splay_empty_iff [LinearOrder α] (t : Tree α) (q : α) :
+    splay t q = .nil ↔ t = .nil := by
+  constructor
+  · intro h
+    have hn := nodeCount_splay t q
+    rw [h] at hn
+    cases t with
+    | nil => rfl
+    | node k l r => simp at hn; omega
+  · rintro rfl
+    simp [splay, descend, descend.go]
+
+end ToKeyListPreservation
+
+
+/-! ### BST Preservation -/
+section BSTPreservation
+
+/-- Helper: `IsBSTAux t lb ub` is equivalent to the key list being bounded
+and sorted. Proved by induction on `t`. -/
+private lemma IsBSTAux_iff_bounded_sorted (t : Tree α) [LinearOrder α] :
+    ∀ lb ub : Option α,
+    IsBSTAux t lb ub ↔
+      (∀ x ∈ t.toKeyList, lb.elim True (· < x)) ∧
+      (∀ x ∈ t.toKeyList, ub.elim True (x < ·)) ∧
+      t.toKeyList.Pairwise (· < ·) := by
+  induction t with
+  | nil => intro lb ub; simp
+  | node k l r ihl ihr =>
+    intro lb ub
+    rw [IsBSTAux_node, ihl lb (some k), ihr (some k) ub]
+    simp only [Option.elim, toKeyList_node, List.mem_append, List.mem_singleton]
+    grind
+
+/-- A tree is a BST iff its in-order traversal is strictly sorted (pairwise
+`<`). Reduces every BST-preservation question to "does the operation
+preserve `toKeyList`?". -/
+theorem IsBST_iff_toKeyList_sorted [LinearOrder α] (t : Tree α) :
+    IsBST t ↔ t.toKeyList.Pairwise (· < ·) := by
+  simp only [IsBST, IsBSTAux_iff_bounded_sorted t none none, Option.elim]
+  exact ⟨fun ⟨_, _, h⟩ => h, fun h => ⟨fun _ _ => trivial, fun _ _ => trivial, h⟩⟩
+
+/-- Transfer BST-ness between trees with the same in-order traversal. -/
+lemma IsBST_of_toKeyList_eq [LinearOrder α] {t t' : Tree α}
+    (h : t'.toKeyList = t.toKeyList) (hbst : IsBST t) : IsBST t' := by
+  rw [IsBST_iff_toKeyList_sorted] at hbst ⊢; rwa [h]
+
+/-- Bottom-up splay preserves the BST invariant. -/
+theorem IsBST_splay [LinearOrder α] (t : Tree α) (q : α) (h : IsBST t) :
+    IsBST (splay t q) :=
+  IsBST_of_toKeyList_eq (toKeyList_splay t q) h
+
+/-- Each primitive rotation preserves the BST invariant. -/
+theorem IsBST_bringUp [LinearOrder α] (d : Dir) (t : Tree α) (h : IsBST t) :
+    IsBST (d.bringUp t) :=
+  IsBST_of_toKeyList_eq (toKeyList_bringUp d t) h
+
+theorem IsBST_applyChild [LinearOrder α] (d : Dir) (op : Tree α → Tree α)
+    (hop_keys : ∀ s, (op s).toKeyList = s.toKeyList)
+    (t : Tree α) (h : IsBST t) :
+    IsBST (applyChild d op t) :=
+  IsBST_of_toKeyList_eq (toKeyList_applyChild d op hop_keys t) h
+
+/-- Any frame-wise splay-up preserves BST-ness of the reassembled tree. -/
+theorem IsBST_splayUp [LinearOrder α] (c : Tree α) (path : List (Frame α))
+    (h : IsBST (reassemble c path)) : IsBST (splayUp c path) :=
+  IsBST_of_toKeyList_eq (toKeyList_splayUp c path) h
+
+end BSTPreservation
+
+
+/-! ### Root of `splay` on a Contained Key -/
+section RootOfContainedKey
+
+/-- If `t.contains q`, the subtree reached by `descend` is a node whose key
+equals `q`. Mirrors how `descend` and `Tree.contains` follow the same
+comparison path. -/
+theorem descend_contains [LinearOrder α] (t : Tree α) (q : α) (h : t.bstContains q) :
+    ∃ l r, (descend t q).1 = l △[q] r := by
+  induction t with
+  | nil => simp [bstContains] at h
+  | node k lt rt ihl ihr =>
+    simp only [bstContains] at h
+    by_cases hlt : q < k
+    · simp only [hlt, ite_true] at h
+      obtain ⟨l', r', hd⟩ := ihl h
+      exact ⟨l', r', by rw [descend_node_lt hlt]; exact hd⟩
+    · simp only [hlt, ite_false] at h
+      by_cases hgt : k < q
+      · simp only [hgt, ite_true] at h
+        obtain ⟨l', r', hd⟩ := ihr h
+        exact ⟨l', r', by rw [descend_node_gt hgt]; exact hd⟩
+      · have hqk : q = k := le_antisymm (not_lt.mp hgt) (not_lt.mp hlt)
+        subst hqk; exact ⟨lt, rt, by rw [descend_node_eq]⟩
+
+/-- Membership-style variant of `descend_contains`: in a BST, if `q ∈ t` then
+`descend` reaches the node with key `q`. -/
+theorem descend_contains' [LinearOrder α] (t : Tree α) (q : α) (hbst : IsBST t)
+    (h : q ∈ t) : ∃ l r, (descend t q).1 = l △[q] r :=
+  descend_contains t q (mem_imp_contains hbst h)
+
+/-- Splaying a node `c = l △[k] r` upward along any path yields a tree
+whose root key is still `k`. Each rotation step brings `c` one level higher
+without changing its root key. -/
+theorem splayUp_root_key_of_node :
+    ∀ (path : List (Frame α)) (l : Tree α) (k : α) (r : Tree α),
+      ∃ l' r', splayUp (l △[k] r) path = l' △[k] r' := by
+  intro path
+  induction path using List.twoStepInduction with
+  | nil => intro l k r; exact ⟨l, r, rfl⟩
+  | singleton f =>
+    intro l k r; obtain ⟨d, kf, s⟩ := f
+    cases d <;> simp [splayUp, Dir.bringUp, Frame.attach,
+      rotateRight, rotateLeft]
+  | cons_cons f1 f2 rest ih _ =>
+    intro l k r; simp only [splayUp]
+    obtain ⟨d1, k1, s1⟩ := f1; obtain ⟨d2, k2, s2⟩ := f2
+    suffices ∃ l' r', (if d1 = d2 then _ else _) =
+        l' △[k] r' by
+      obtain ⟨l', r', heq⟩ := this; rw [heq]; exact ih l' k r'
+    cases d1 <;> cases d2 <;>
+      simp [Frame.attach, Dir.bringUp, applyChild,
+        rotateRight, rotateLeft]
+
+/-- If `t.contains q`, the bottom-up splay of `t` at `q` has `q` at the root. -/
+theorem splay_root_of_contains [LinearOrder α] (t : Tree α) (q : α)
+    (hc : t.bstContains q) : ∃ l r, splay t q = l △[q] r := by
+  obtain ⟨lr, rr, hd⟩ := descend_contains t q hc
+  unfold splay
+  rcases hdecomp : descend t q with ⟨reached, path⟩
+  rw [hdecomp] at hd
+  subst hd
+  exact splayUp_root_key_of_node path lr q rr
+
+/-- Membership-style variant of `splay_root_of_contains`: in a BST, if `q ∈ t`
+then splaying brings `q` to the root. -/
+theorem splay_root_of_contains' [LinearOrder α] (t : Tree α) (q : α)
+    (hbst : IsBST t) (h : q ∈ t) : ∃ l r, splay t q = l △[q] r :=
+  splay_root_of_contains t q (mem_imp_contains hbst h)
+
+end RootOfContainedKey
+
+end SplayTree