feat(GenericRAM/Native): derivations of stack recursions from recursion trees

Complexity.lean

@@ -1513,6 +1513,7 @@ public import Complexity.Computability.GenericRAM.Native.IndexFold
 public import Complexity.Computability.GenericRAM.Native.MeasurementFold
 public import Complexity.Computability.GenericRAM.Native.Nat
 public import Complexity.Computability.GenericRAM.Native.StackRecursion
+public import Complexity.Computability.GenericRAM.Native.StackRecursionTree
 public import Complexity.Computability.GenericRAM.Native.SubsetPairFold
 public import Complexity.Computability.GenericRAM.Signed
 public import Complexity.Computability.GenericRAM.Signed.Fits

Complexity/Computability/GenericRAM/Native/StackRecursionTree.lean

@@ -0,0 +1,196 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.GenericRAM.Native.StackRecursion
+public import Complexity.Foundations.Data.Nat.RecursionTree
+
+/-!
+# Derivations of stack recursions from their recursion trees
+
+A derivation `Cslib.GenericRAM.StackRecursion.Scheme.Eval` of a recursion scheme records the
+value of a node with its number of nodes and its stack depth. This file builds derivations from
+a description of the recursion tree, and reads off what a clocked run returns.
+
+**Counted children** (`Scheme.Loop.counted`). A call whose accumulators `acc c` ask for the
+children `child c` for `c < bound`, and then stop, runs its loop through the children's
+derivations.
+
+**The recursion tree** (`Scheme.exists_eval_of_counted`). Let `value` assign values to the nodes
+satisfying `I.node`, such that a leaf has its leaf value, and a call at depth `d < D` has at most
+`b d` counted children, all at depth `d + 1` and smaller in a measure, with its value the
+`finish` of the accumulated children's values. Then every node at depth `d ≤ D` has a derivation
+of its value, with at most `Nat.recursionBound b (D - d) d` nodes and at most `D - d` stack
+levels. This is the induction "from the leaves" of a recursive algorithm, with its node count;
+without the count, `Scheme.exists_eval_of_measure` is the induction alone.
+
+**What a run returns** (`Scheme.value_of_run_eq_some`). Every value the clocked run returns, for
+any fuel, satisfies the invariant of a derivation of the root. If the values carry a tag that
+only the root's value has, a returned tagged value is the root's value, even when the fuel is too
+small to vouch for the run.
+
+## Main results
+
+* `Cslib.GenericRAM.StackRecursion.Scheme.Loop.counted`: the loop over counted children.
+* `Cslib.GenericRAM.StackRecursion.Scheme.exists_eval_of_measure`: derivations by well-founded
+  recursion.
+* `Cslib.GenericRAM.StackRecursion.Scheme.exists_eval_of_counted`: derivations with the node count
+  of the recursion tree.
+* `Cslib.GenericRAM.StackRecursion.Scheme.value_of_run_eq_some`: a returned value satisfies the
+  invariant.
+
+## References
+
+* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Appendix D.4.7 (p. 64).
+-/
+
+public section
+
+namespace Cslib.GenericRAM.StackRecursion.Scheme
+
+open Finset
+
+variable {X A Y : Type} {R : Scheme X A Y} {I : Invariant X A Y}
+
+/-- **A call with counted children.** If, from the accumulators `acc c`, the call `x` asks for the
+children `child c` for `c < bound` and then stops, and the children evaluate to `val c`, then its
+loop from `acc 0` ends at `acc bound`, with the children's nodes and at most `H` levels. -/
+theorem Loop.counted {x : X} {acc : ℕ → A} {child : ℕ → X} {val : ℕ → Y} {nodes height : ℕ → ℕ}
+    (bound H : ℕ) (hnext : ∀ c < bound, R.next x (acc c) = some (child c))
+    (hdone : R.next x (acc bound) = none)
+    (habsorb : ∀ c < bound, R.absorb x (acc c) (val c) = acc (c + 1))
+    (heval : ∀ c < bound, R.Eval I (child c) (val c) (nodes c) (height c))
+    (hframe : ∀ c < bound, I.frame x (acc c)) (hH : ∀ c < bound, height c ≤ H) :
+    ∃ h ≤ H, R.Loop I x (acc 0) (acc bound) (∑ c ∈ range bound, nodes c) h := by
+  -- From any start `s ≤ bound`.
+  have key : ∀ k s, s + k = bound →
+      ∃ h ≤ H, R.Loop I x (acc s) (acc bound) (∑ c ∈ Ico s bound, nodes c) h := by
+    intro k
+    induction k with
+    | zero =>
+      intro s hs
+      subst hs
+      exact ⟨0, Nat.zero_le _, by simpa using Loop.done hdone⟩
+    | succ k ih =>
+      intro s hs
+      obtain ⟨h, hh, hl⟩ := ih (s + 1) (by omega)
+      have hs' : s < bound := by omega
+      have hl' := Loop.child (hframe s hs') (hnext s hs') (heval s hs')
+        (by rw [habsorb s hs']; exact hl)
+      refine ⟨max (height s) h, max_le (hH s hs') hh, ?_⟩
+      rwa [sum_eq_sum_Ico_succ_bot hs']
+  simpa using key bound 0 (by omega)
+
+/-- **Derivations by well-founded recursion.** Let `value` assign values to the nodes satisfying
+`I.node`, all satisfying `I.value`, such that a leaf has its leaf value, and a call has counted
+children: from the accumulators `acc c`, starting at `start`, it asks for `child c` for `c < cnt`
+and then stops, absorbing the children's values; the frames satisfy `I.frame`, the children
+satisfy `I.node` and are smaller in the measure `μ`; and its value is the `finish` of the last
+accumulator. Then every node has a derivation of its value. `exists_eval_of_counted` adds the node
+count. -/
+theorem exists_eval_of_measure (μ : X → ℕ) (value : X → Y)
+    (hleaf : ∀ x, I.node x → R.isLeaf x = true → value x = R.leaf x)
+    (hcall : ∀ x, I.node x → R.isLeaf x = false →
+      ∃ (cnt : ℕ) (acc : ℕ → A) (child : ℕ → X), acc 0 = R.start x ∧
+        (∀ c < cnt, R.next x (acc c) = some (child c)) ∧ R.next x (acc cnt) = none ∧
+        (∀ c < cnt, R.absorb x (acc c) (value (child c)) = acc (c + 1)) ∧
+        (∀ c < cnt, I.frame x (acc c) ∧ I.node (child c) ∧ μ (child c) < μ x) ∧
+        value x = R.finish x (acc cnt))
+    (hvalue : ∀ x, I.node x → I.value (value x)) (x : X) (hx : I.node x) :
+    ∃ n h, R.Eval I x (value x) n h := by
+  induction hμ : μ x using Nat.strong_induction_on generalizing x with
+  | _ k ih =>
+  cases hl : R.isLeaf x
+  · obtain ⟨cnt, acc, child, h0, hnext, hdone, habs, hkids, hfin⟩ := hcall x hx hl
+    have hev : ∀ c < cnt, ∃ n h, R.Eval I (child c) (value (child c)) n h := fun c hc =>
+      ih (μ (child c)) (hμ ▸ (hkids c hc).2.2) (child c) (hkids c hc).2.1 rfl
+    choose! nodes height hev using hev
+    obtain ⟨h, -, hloop⟩ := Loop.counted (I := I) (val := fun c => value (child c)) cnt
+      (∑ c ∈ range cnt, height c) hnext hdone habs hev (fun c hc => (hkids c hc).1)
+      (fun c hc => single_le_sum (fun _ _ => Nat.zero_le _) (mem_range.mpr hc))
+    rw [h0] at hloop
+    exact ⟨_, _, hfin ▸ Eval.call hx hl hloop (hfin ▸ hvalue x hx)⟩
+  · exact ⟨1, 0, by rw [hleaf x hx hl]; exact Eval.leaf hx hl (hleaf x hx hl ▸ hvalue x hx)⟩
+
+/-- A recursion tree has at least its root. -/
+private theorem one_le_recursionBound (b : ℕ → ℕ) (k d : ℕ) : 1 ≤ Nat.recursionBound b k d := by
+  cases k with
+  | zero => simp
+  | succ k => rw [Nat.recursionBound_succ]; omega
+
+/-- **Derivations from the recursion tree.** Let `value` assign values to the nodes satisfying
+`I.node`, all satisfying `I.value`, such that
+
+* a leaf has its leaf value;
+* a call at depth `d` has `d < D` and at most `b d` children, counted: from the accumulators
+  `acc c`, starting at `start`, it asks for `child c` for `c < cnt` and then stops, absorbing the
+  children's values; the frames satisfy `I.frame`, and the children satisfy `I.node`, are smaller
+  in the measure `μ` and lie at depth `d + 1`; and its value is the `finish` of the last
+  accumulator.
+
+Then every node at depth `d ≤ D` has a derivation of its value with at most
+`Nat.recursionBound b (D - d) d` nodes and at most `D - d` stack levels. -/
+theorem exists_eval_of_counted (μ depth : X → ℕ) (value : X → Y) (b : ℕ → ℕ) (D : ℕ)
+    (hleaf : ∀ x, I.node x → R.isLeaf x = true → value x = R.leaf x)
+    (hcall : ∀ x, I.node x → R.isLeaf x = false → depth x < D ∧
+      ∃ (cnt : ℕ) (acc : ℕ → A) (child : ℕ → X), cnt ≤ b (depth x) ∧ acc 0 = R.start x ∧
+        (∀ c < cnt, R.next x (acc c) = some (child c)) ∧ R.next x (acc cnt) = none ∧
+        (∀ c < cnt, R.absorb x (acc c) (value (child c)) = acc (c + 1)) ∧
+        (∀ c < cnt, I.frame x (acc c) ∧ I.node (child c) ∧ μ (child c) < μ x ∧
+          depth (child c) = depth x + 1) ∧
+        value x = R.finish x (acc cnt))
+    (hvalue : ∀ x, I.node x → I.value (value x)) (x : X) (hx : I.node x) (hxD : depth x ≤ D) :
+    ∃ n h, R.Eval I x (value x) n h ∧ n ≤ Nat.recursionBound b (D - depth x) (depth x) ∧
+      h ≤ D - depth x := by
+  induction hμ : μ x using Nat.strong_induction_on generalizing x with
+  | _ k ih =>
+  cases hl : R.isLeaf x
+  · obtain ⟨hd, cnt, acc, child, hcnt, h0, hnext, hdone, habs, hkids, hfin⟩ := hcall x hx hl
+    have hev : ∀ c < cnt, ∃ n h, R.Eval I (child c) (value (child c)) n h ∧
+        n ≤ Nat.recursionBound b (D - (depth x + 1)) (depth x + 1) ∧
+        h ≤ D - (depth x + 1) := fun c hc => by
+      obtain ⟨-, hn, hμc, hdc⟩ := hkids c hc
+      obtain ⟨n, h, he, hnb, hhb⟩ := ih (μ (child c)) (hμ ▸ hμc) (child c) hn (by omega) rfl
+      rw [hdc] at hnb hhb
+      exact ⟨n, h, he, hnb, hhb⟩
+    choose! nodes height hev using hev
+    obtain ⟨h, hh, hloop⟩ := Loop.counted (I := I) (val := fun c => value (child c)) cnt
+      (D - (depth x + 1)) hnext hdone habs (fun c hc => (hev c hc).1)
+      (fun c hc => (hkids c hc).1) (fun c hc => (hev c hc).2.2)
+    rw [h0] at hloop
+    have hv : I.value (R.finish x (acc cnt)) := hfin ▸ hvalue x hx
+    refine ⟨(∑ c ∈ range cnt, nodes c) + 1, h + 1, hfin ▸ Eval.call hx hl hloop hv, ?_, by omega⟩
+    obtain ⟨k', hk'⟩ : ∃ k', D - depth x = k' + 1 := ⟨D - depth x - 1, by omega⟩
+    have hk'' : D - (depth x + 1) = k' := by omega
+    rw [hk', Nat.recursionBound_succ]
+    have hsum : ∑ c ∈ range cnt, nodes c ≤ cnt * Nat.recursionBound b k' (depth x + 1) := by
+      calc ∑ c ∈ range cnt, nodes c ≤ ∑ _c ∈ range cnt, Nat.recursionBound b k' (depth x + 1) :=
+            sum_le_sum fun c hc => hk'' ▸ (hev c (mem_range.mp hc)).2.1
+        _ = cnt * Nat.recursionBound b k' (depth x + 1) := by rw [sum_const, card_range,
+            smul_eq_mul]
+    have := Nat.mul_le_mul_right (Nat.recursionBound b k' (depth x + 1)) hcnt
+    omega
+  · refine ⟨1, 0, ?_, one_le_recursionBound _ _ _, Nat.zero_le _⟩
+    rw [hleaf x hx hl]
+    exact Eval.leaf hx hl (hleaf x hx hl ▸ hvalue x hx)
+
+/-- **What a clocked run returns.** For any fuel, a value returned by the run satisfies the
+invariant of a derivation of the root. -/
+theorem value_of_run_eq_some {J : Type} {fuel : J → ℕ} {root : J → X} {a : J} {y y' : Y}
+    {N H : ℕ} (he : R.Eval I (root a) y N H) (hrun : R.run fuel root a = some y') :
+    I.value y' := by
+  obtain ⟨-, -, ⟨x, hr, -⟩ | ⟨z, hr, hz⟩⟩ := he.good_iterate (fuel a)
+  · simp only [run] at hrun
+    rw [hr] at hrun
+    simp at hrun
+  · simp only [run] at hrun
+    rw [hr] at hrun
+    cases hrun
+    exact hz
+
+end Cslib.GenericRAM.StackRecursion.Scheme

ComplexityTests/StackRecursionTree.lean

@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Computability.GenericRAM.Native.StackRecursionTree
+
+/-! # Derivations from recursion trees on a toy scheme
+
+The full binary tree of height `k`: a node with `x > 0` levels below it has two children with
+`x - 1` levels, a leaf has value `1`, and a call adds its children's values. The value of a node
+with `x` levels is `2 ^ x`. `exists_eval_of_counted` derives its value with at most
+`Nat.recursionBound (fun _ => 2) k 0` nodes. The values are tagged with the depth, and
+`value_of_run_eq_some` shows that a value tagged `0` returned by the run, with any fuel, is the
+root's. -/
+
+namespace ComplexityTests.StackRecursionTree
+
+open Cslib.GenericRAM Cslib.GenericRAM.StackRecursion
+
+/-- The binary tree scheme on `(depth, levels below)`, with values tagged by the depth. The
+accumulator counts the children done and sums their values. -/
+def tree : Scheme (ℕ × ℕ) (ℕ × ℕ) (ℕ × ℕ) where
+  isLeaf x := x.2 == 0
+  leaf x := (x.1, 1)
+  start _ := (0, 0)
+  next x a := if a.1 < 2 then some (x.1 + 1, x.2 - 1) else none
+  absorb _ a y := (a.1 + 1, a.2 + y.2)
+  finish x a := (x.1, a.2)
+
+/-- The nodes of the tree of height `k`, and the root's value `2 ^ k` for the depth-`0` tag. -/
+def inv (k : ℕ) : Invariant (ℕ × ℕ) (ℕ × ℕ) (ℕ × ℕ) :=
+  ⟨fun x => x.1 + x.2 = k, fun _ _ => True, fun y => y.1 = 0 → y.2 = 2 ^ k⟩
+
+/-- **The derivation of the root**, with the node count of the recursion tree. -/
+theorem exists_eval_tree (k : ℕ) :
+    ∃ n h, tree.Eval (inv k) (0, k) (0, 2 ^ k) n h ∧
+      n ≤ Nat.recursionBound (fun _ => 2) k 0 ∧ h ≤ k := by
+  have := Scheme.exists_eval_of_counted (R := tree) (I := inv k) (fun x => x.2) (fun x => x.1)
+    (fun x => (x.1, 2 ^ x.2)) (fun _ => 2) k
+    (fun x _ hl => by
+      simp only [tree, beq_iff_eq] at hl ⊢
+      rw [hl, pow_zero])
+    (fun x hx hl => by
+      simp only [tree, beq_eq_false_iff_ne, ne_eq] at hl
+      simp only [inv] at hx
+      refine ⟨by omega, 2, fun c => (c, c * 2 ^ (x.2 - 1)), fun _ => (x.1 + 1, x.2 - 1), le_rfl,
+        by simp [tree], fun c hc => by simp [tree]; omega, by simp [tree], fun c hc => ?_,
+        fun c hc => ⟨trivial, by simp only [inv]; omega, show x.2 - 1 < x.2 by omega, rfl⟩, ?_⟩
+      · simp only [tree, Prod.mk.injEq, true_and]
+        ring
+      · simp only [tree, Prod.mk.injEq, true_and]
+        rw [show x.2 = x.2 - 1 + 1 by omega, pow_succ]
+        simp only [Nat.add_sub_cancel]
+        ring)
+    (fun x hx h0 => by
+      simp only [inv] at hx
+      simp only at h0 ⊢
+      rw [show x.2 = k by omega]) (0, k) (by simp [inv]) (by simp)
+  simpa using this
+
+/-- **A tagged value returned by the run is the root's**, for every fuel. -/
+theorem run_tree {k f y : ℕ}
+    (hrun : tree.run (fun _ : Unit => f) (fun _ => (0, k)) () = some (0, y)) : y = 2 ^ k := by
+  obtain ⟨n, h, he, -, -⟩ := exists_eval_tree k
+  exact Scheme.value_of_run_eq_some (fuel := fun _ : Unit => f) (root := fun _ => (0, k))
+    (a := ()) he hrun rfl
+
+-- The tree of height `3` has `15` nodes, within the bound.
+example : Nat.recursionBound (fun _ => 2) 3 0 = 15 := by decide
+
+-- With `2 * 15 - 1` steps the run returns the root's value.
+example : tree.run (fun _ : Unit => 29) (fun _ => (0, 3)) () = some (0, 8) := by decide
+
+-- With too little fuel it may return a child's value, tagged with a positive depth.
+example : tree.run (fun _ : Unit => 28) (fun _ => (0, 3)) () = some (1, 4) := by decide
+
+end ComplexityTests.StackRecursionTree