From 02ef13c857b9b8fd1f5aa83e5093c6fcb25e1f24 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 22:19:45 -0400 Subject: [PATCH 1/8] feat(GenericRAM/Native): depth-first stack recursion with native bounds A generic recursion scheme (leaf test, leaf step, start/next/absorb/finish) run by an explicit stack machine. Derivations `Eval I x y n h` (n nodes, h stack levels) are evaluated in 2n - 1 steps through states with at most h open frames. One native certificate runs the machine for a natively computed fuel; its time is (fuel + 1) times a polynomial in (h+1)(F+1) plus the leaf time, and its space a polynomial plus the leaf space. Also the node count of a recursion tree and its 2^O(n/sqrt(log n)) bound (Foundations/Data/Nat/RecursionTree.lean), for the call count of [OpenAI2026ETH, Appendix D.4.7]. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 2 + .../GenericRAM/Native/StackRecursion.lean | 778 ++++++++++++++++++ .../Foundations/Data/Nat/RecursionTree.lean | 170 ++++ ComplexityTests/StackRecursion.lean | 257 ++++++ 4 files changed, 1207 insertions(+) create mode 100644 Complexity/Computability/GenericRAM/Native/StackRecursion.lean create mode 100644 Complexity/Foundations/Data/Nat/RecursionTree.lean create mode 100644 ComplexityTests/StackRecursion.lean diff --git a/Complexity.lean b/Complexity.lean index 69ba190535..e3af2ca51c 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1457,6 +1457,7 @@ public import Complexity.Computability.GenericRAM.Native.HeavyBranchFold 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.SubsetPairFold public import Complexity.Computability.GenericRAM.Signed public import Complexity.Computability.GenericRAM.Signed.Fits @@ -2726,6 +2727,7 @@ public import Complexity.Foundations.Data.Nat.Prime public import Complexity.Foundations.Data.Nat.Primrec public import Complexity.Foundations.Data.Nat.Radix public import Complexity.Foundations.Data.Nat.Radix.Measurement +public import Complexity.Foundations.Data.Nat.RecursionTree public import Complexity.Foundations.Data.Nat.ResidueSum public import Complexity.Foundations.Data.Nat.SqrtLog public import Complexity.Foundations.Data.Nat.SqrtRatio diff --git a/Complexity/Computability/GenericRAM/Native/StackRecursion.lean b/Complexity/Computability/GenericRAM/Native/StackRecursion.lean new file mode 100644 index 0000000000..c2fd37dd11 --- /dev/null +++ b/Complexity/Computability/GenericRAM/Native/StackRecursion.lean @@ -0,0 +1,778 @@ +/- +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.Combinators +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Option +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListLookup +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeOptionPrimitives + +/-! +# Depth-first recursion with an explicit stack + +A *recursion scheme* (`StackRecursion.Scheme`) evaluates node descriptions `x : X` to values +`y : Y`. A node is either a leaf, evaluated by `leaf`, or a call, which keeps an accumulator +`a : A`: starting from `start x`, it asks `next x a` for its next child, folds the child's value +into the accumulator with `absorb`, and when `next` returns `none` produces its value with +`finish`. Children may depend on the values of earlier children through the accumulator. + +**The machine** (`Scheme.step`). Its state is the stack of open calls, innermost first, each +with its accumulator, and a register holding a pending call or a returned value. Each step +performs one call or one return. A derivation `Scheme.Eval I x y n h`, with `n` nodes and `h` +stack levels, makes the machine reach `y` in `2 * n - 1` steps (`Scheme.Eval.run`), through +states with at most `h` open calls whose nodes, frames and values satisfy the invariant `I` +(`Scheme.Eval.good_iterate`). + +**The native certificate** (`Scheme.certificate`). The leaf step is an arbitrary native +certificate; the other components are polynomial-time. One fixed machine runs the stack machine +for a natively computed number `fuel a` of steps (`NativeCertificate.iterate`) and returns the +register. When `2 * n - 1 ≤ fuel a` the result is `y` (`Scheme.run_eq_some`). If every node, +frame and value on the derivation has encoded length at most `F` and every leaf is evaluated +within time `TL` and space `SL`, the time is at most `fuel a + 1` times +`K ((h + 1) (F + 1)) ^ K + TL` and the workspace at most `K ((h + 1) (F + 1)) ^ K + SL`, up to +the cost of computing the fuel and the root and of the binary clock, for one constant `K` of the +scheme (`Scheme.certificate_le`). Only the stack is kept, so the workspace grows with the depth, +not with the number of nodes. The number of nodes of a recursion tree is bounded in +`Foundations/Data/Nat/RecursionTree.lean`. + +This is the depth-first evaluation of the recursion in the proof of Theorem D.1 of +[OpenAI2026ETH] (Appendix D.4.7, p. 64), which keeps one sum over mode tuples and one product +over groups per stack level. The scheme is generic: the recursion of Appendix D.4 is one +instance, with its leaves evaluated by direct summation. + +## Main definitions + +* `Cslib.GenericRAM.StackRecursion.Scheme`: a recursion scheme. +* `Cslib.GenericRAM.StackRecursion.Invariant`: predicates on the nodes, frames and values met. +* `Cslib.GenericRAM.StackRecursion.Scheme.Loop`, `Cslib.GenericRAM.StackRecursion.Scheme.Eval`: + derivations of the loop of a call and of the value of a node, with their node counts and + stack depths. +* `Cslib.GenericRAM.StackRecursion.Scheme.step`, `Cslib.GenericRAM.StackRecursion.Scheme.run`: + the stack machine and its clocked run. +* `Cslib.GenericRAM.StackRecursion.Scheme.PolyTime`: the polynomial-time components. +* `Cslib.GenericRAM.StackRecursion.Scheme.certificate`: one native machine for the clocked run. + +## Main results + +* `Cslib.GenericRAM.StackRecursion.Scheme.Eval.run`: a derivation with `n` nodes is evaluated in + `2 * n - 1` steps. +* `Cslib.GenericRAM.StackRecursion.Scheme.run_eq_some`: enough fuel gives the value. +* `Cslib.GenericRAM.StackRecursion.Scheme.certificate_le`: time `fuel + 1` times a polynomial in + `(h + 1) * (F + 1)` plus the leaf time, and workspace a polynomial plus the leaf space. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Appendix D.4.7 (p. 64). +-/ + +@[expose] public section + +namespace Cslib.GenericRAM.StackRecursion + +open Turing.MultiTapeTM + +/-- A *recursion scheme*. A node `x` is a leaf when `isLeaf x`, with value `leaf x`. Otherwise +it is a call: its accumulator starts at `start x`; while `next x a` returns a child, the child is +evaluated and its value folded into the accumulator by `absorb`; when `next x a` is `none` the +call returns `finish x a`. -/ +structure Scheme (X A Y : Type) where + /-- Whether a node is a leaf. -/ + isLeaf : X → Bool + /-- The value of a leaf. -/ + leaf : X → Y + /-- The initial accumulator of a call. -/ + start : X → A + /-- The next child of a call with the given accumulator, or `none` when it is done. -/ + next : X → A → Option X + /-- Fold the value of the current child into the accumulator. -/ + absorb : X → A → Y → A + /-- The value of a call from its final accumulator. -/ + finish : X → A → Y + +/-- Predicates on what a derivation meets: the nodes evaluated, the frames pushed (a call with +its accumulator while one of its children is evaluated) and the values returned. -/ +structure Invariant (X A Y : Type) where + /-- Every node evaluated satisfies `node`. -/ + node : X → Prop + /-- Every pushed frame satisfies `frame`. -/ + frame : X → A → Prop + /-- Every returned value satisfies `value`. -/ + value : Y → Prop + +/-- A state of the stack machine: the open calls with their accumulators, innermost first, a +pending call and a returned value. -/ +abbrev State (X A Y : Type) := List (X × A) × Option X × Option Y + +namespace Scheme + +variable {X A Y : Type} (R : Scheme X A Y) + +/-- Continue the call `x` with accumulator `a` above the stack `st`: push its frame and call its +next child, or return its value when it has none. -/ +def resume (x : X) (a : A) (st : List (X × A)) : State X A Y := + match R.next x a with + | none => (st, none, some (R.finish x a)) + | some c => ((x, a) :: st, some c, none) + +/-- **One step of the stack machine.** A pending leaf is evaluated; a pending call is started; a +returned value is absorbed by the innermost open call, which then continues. A value returned +with no open call is final. -/ +def step : State X A Y → State X A Y + | (st, some x, _) => if R.isLeaf x then (st, none, some (R.leaf x)) else R.resume x (R.start x) st + | ((x, a) :: st, none, some y) => R.resume x (R.absorb x a y) st + | σ => σ + +theorem resume_of_next_none {x : X} {a : A} (st : List (X × A)) (h : R.next x a = none) : + R.resume x a st = (st, none, some (R.finish x a)) := by + simp [resume, h] + +theorem resume_of_next_some {x c : X} {a : A} (st : List (X × A)) (h : R.next x a = some c) : + R.resume x a st = ((x, a) :: st, some c, none) := by + simp [resume, h] + +theorem step_leaf {x : X} (st : List (X × A)) (r : Option Y) (h : R.isLeaf x = true) : + R.step (st, some x, r) = (st, none, some (R.leaf x)) := by + simp [step, h] + +theorem step_call {x : X} (st : List (X × A)) (r : Option Y) (h : R.isLeaf x = false) : + R.step (st, some x, r) = R.resume x (R.start x) st := by + simp [step, h] + +theorem step_return (x : X) (a : A) (st : List (X × A)) (y : Y) : + R.step ((x, a) :: st, none, some y) = R.resume x (R.absorb x a y) st := rfl + +/-- A value returned with no open call is final. -/ +@[simp] theorem step_final (y : Y) : R.step ([], none, some y) = ([], none, some y) := rfl + +/-- **The loop of a call.** `R.Loop I x a a' n h`: the call `x`, from accumulator `a`, evaluates +its remaining children with `n` nodes in total and ends with accumulator `a'`, using at most `h` +stack levels above its own frame. Every frame pushed, child evaluated and value returned +satisfies `I`. -/ +inductive Loop (I : Invariant X A Y) : X → A → A → ℕ → ℕ → Prop + /-- The call has no further child. -/ + | done {x : X} {a : A} : R.next x a = none → Loop I x a a 0 0 + /-- The next child is a leaf. -/ + | leaf {x c : X} {a a' : A} {n h : ℕ} : I.frame x a → R.next x a = some c → I.node c → + R.isLeaf c = true → I.value (R.leaf c) → Loop I x (R.absorb x a (R.leaf c)) a' n h → + Loop I x a a' (n + 1) h + /-- The next child is a call, whose own loop ends with accumulator `b`. -/ + | call {x c : X} {a b a' : A} {n₁ h₁ n₂ h₂ : ℕ} : I.frame x a → R.next x a = some c → + I.node c → R.isLeaf c = false → Loop I c (R.start c) b n₁ h₁ → I.value (R.finish c b) → + Loop I x (R.absorb x a (R.finish c b)) a' n₂ h₂ → + Loop I x a a' (n₁ + 1 + n₂) (max (h₁ + 1) h₂) + +/-- **A derivation of the value of a node.** `R.Eval I x y n h`: the node `x` has value `y`, +computed with `n` nodes and at most `h` open calls, and every node, frame and value met satisfies +`I`. A leaf has one node and no open call; a call has one more node and one more level than its +loop. -/ +def Eval (I : Invariant X A Y) (x : X) (y : Y) (n h : ℕ) : Prop := + I.node x ∧ I.value y ∧ + ((R.isLeaf x = true ∧ y = R.leaf x ∧ n = 1 ∧ h = 0) ∨ + (R.isLeaf x = false ∧ ∃ b n' h', R.Loop I x (R.start x) b n' h' ∧ y = R.finish x b ∧ + n = n' + 1 ∧ h = h' + 1)) + +variable {R} {I : Invariant X A Y} + +/-- A leaf is evaluated by `leaf`. -/ +theorem Eval.leaf {x : X} (hx : I.node x) (hl : R.isLeaf x = true) (hv : I.value (R.leaf x)) : + R.Eval I x (R.leaf x) 1 0 := + ⟨hx, hv, .inl ⟨hl, rfl, rfl, rfl⟩⟩ + +/-- A call is evaluated by its loop, from `start`, and `finish`. -/ +theorem Eval.call {x : X} {b : A} {n h : ℕ} (hx : I.node x) (hl : R.isLeaf x = false) + (hloop : R.Loop I x (R.start x) b n h) (hv : I.value (R.finish x b)) : + R.Eval I x (R.finish x b) (n + 1) (h + 1) := + ⟨hx, hv, .inr ⟨hl, b, n, h, hloop, rfl, rfl, rfl⟩⟩ + +/-- **The loop absorbs an evaluated child.** -/ +theorem Loop.child {x c : X} {a a' : A} {y : Y} {n₁ h₁ n₂ h₂ : ℕ} (hf : I.frame x a) + (hn : R.next x a = some c) (hc : R.Eval I c y n₁ h₁) + (hrest : R.Loop I x (R.absorb x a y) a' n₂ h₂) : + R.Loop I x a a' (n₁ + n₂) (max h₁ h₂) := by + obtain ⟨hnode, hval, ⟨hl, rfl, rfl, rfl⟩ | ⟨hl, b, n', h', hloop, rfl, rfl, rfl⟩⟩ := hc + · simpa [Nat.add_comm] using Loop.leaf hf hn hnode hl hval hrest + · exact Loop.call hf hn hnode hl hloop hval hrest + +/-- Every derivation has at least one node. -/ +theorem Eval.one_le {x : X} {y : Y} {n h : ℕ} (he : R.Eval I x y n h) : 1 ≤ n := by + obtain ⟨-, -, ⟨-, -, rfl, -⟩ | ⟨-, -, -, -, -, -, rfl, -⟩⟩ := he <;> omega + +/-! ### The machine follows the derivation -/ + +/-- **A loop is run in two steps per node**, ending with the value of the call returned to the +stack below it. -/ +theorem Loop.run {x : X} {a a' : A} {n h : ℕ} (hl : R.Loop I x a a' n h) (st : List (X × A)) : + R.step^[2 * n] (R.resume x a st) = (st, none, some (R.finish x a')) := by + induction hl generalizing st with + | done hn => exact R.resume_of_next_none st hn + | @leaf x c a a' n h _ hn _ hl _ _ ih => + rw [show 2 * (n + 1) = 2 * n + 1 + 1 by ring] + simp only [Function.iterate_add_apply, Function.iterate_one] + rw [R.resume_of_next_some st hn, R.step_leaf _ _ hl, R.step_return, ih] + | @call x c a b a' n₁ h₁ n₂ h₂ _ hn _ hl _ _ _ ih₁ ih₂ => + rw [show 2 * (n₁ + 1 + n₂) = 2 * n₂ + 1 + 2 * n₁ + 1 by ring] + simp only [Function.iterate_add_apply, Function.iterate_one] + rw [R.resume_of_next_some st hn, R.step_call _ _ hl, ih₁, R.step_return, ih₂] + +/-- **A node with `n` nodes is evaluated in `2 * n - 1` steps**, above any stack. -/ +theorem Eval.run {x : X} {y : Y} {n h : ℕ} (he : R.Eval I x y n h) (st : List (X × A)) : + R.step^[2 * n - 1] (st, some x, none) = (st, none, some y) := by + obtain ⟨-, -, ⟨hl, rfl, rfl, rfl⟩ | ⟨hl, b, n', h', hloop, rfl, rfl, rfl⟩⟩ := he + · exact R.step_leaf st none hl + · rw [show 2 * (n' + 1) - 1 = 2 * n' + 1 by omega, Function.iterate_add_apply, + Function.iterate_one, R.step_call _ _ hl, hloop.run] + +/-! ### The states met -/ + +/-- A state is *good* for `I` and a depth `H` when at most `H` calls are open, every open frame +satisfies `I`, and the register holds either a pending node or a returned value satisfying +`I`. -/ +def Good (I : Invariant X A Y) (H : ℕ) (σ : State X A Y) : Prop := + σ.1.length ≤ H ∧ (∀ f ∈ σ.1, I.frame f.1 f.2) ∧ + ((∃ x, σ.2 = (some x, none) ∧ I.node x) ∨ (∃ y, σ.2 = (none, some y) ∧ I.value y)) + +theorem Good.mono {H H' : ℕ} {σ : State X A Y} (hσ : Good I H σ) (h : H ≤ H') : Good I H' σ := + ⟨hσ.1.trans h, hσ.2⟩ + +private theorem good_push {x : X} {a : A} {st : List (X × A)} {H : ℕ} {r : Option X × Option Y} + (hst : ∀ f ∈ st, I.frame f.1 f.2) (hf : I.frame x a) (hH : st.length + 1 ≤ H) + (hr : (∃ x, r = (some x, none) ∧ I.node x) ∨ (∃ y, r = (none, some y) ∧ I.value y)) : + Good I H ((x, a) :: st, r) := by + refine ⟨by simpa using hH, ?_, hr⟩ + intro f hf' + rcases List.mem_cons.mp hf' with rfl | hf' + · exact hf + · exact hst f hf' + +/-- **The states of a loop are good**, strictly before it returns. -/ +theorem Loop.good {x : X} {a a' : A} {n h : ℕ} (hl : R.Loop I x a a' n h) {st : List (X × A)} + (hst : ∀ f ∈ st, I.frame f.1 f.2) : + ∀ j < 2 * n, Good I (st.length + h + 1) (R.step^[j] (R.resume x a st)) := by + induction hl generalizing st with + | done _ => intro j hj; omega + | @leaf x c a a' n h hf hn hc hl hv _ ih => + intro j hj + rw [R.resume_of_next_some st hn] + rcases j with _ | _ | j + · exact good_push hst hf (by omega) (.inl ⟨c, rfl, hc⟩) + · rw [Function.iterate_one, R.step_leaf _ _ hl] + exact good_push hst hf (by omega) (.inr ⟨_, rfl, hv⟩) + · rw [show j + 1 + 1 = j + 2 by ring, Function.iterate_add_apply, + show R.step^[2] ((x, a) :: st, some c, none) = R.resume x (R.absorb x a (R.leaf c)) st by + simp only [show (2 : ℕ) = 1 + 1 from rfl, Function.iterate_add_apply, + Function.iterate_one] + rw [R.step_leaf _ _ hl, R.step_return]] + exact ih hst j (by omega) + | @call x c a b a' n₁ h₁ n₂ h₂ hf hn hc hl hloop₁ hv _ ih₁ ih₂ => + intro j hj + rw [R.resume_of_next_some st hn] + have hst' : ∀ f ∈ (x, a) :: st, I.frame f.1 f.2 := fun f hf' => by + rcases List.mem_cons.mp hf' with rfl | hf' + · exact hf + · exact hst f hf' + have hbegin : R.step^[1] ((x, a) :: st, some c, none) = R.resume c (R.start c) ((x, a) :: st) := + by rw [Function.iterate_one, R.step_call _ _ hl] + rcases j with _ | j + · exact good_push hst hf (by omega) (.inl ⟨c, rfl, hc⟩) + rcases Nat.lt_or_ge j (2 * n₁) with hj₁ | hj₁ + · rw [show j + 1 = j + 1 from rfl, Function.iterate_add_apply, hbegin] + exact (ih₁ hst' j hj₁).mono (by simp only [List.length_cons]; omega) + obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hj₁ + rw [show 2 * n₁ + k + 1 = k + 2 * n₁ + 1 by ring, Function.iterate_add_apply, + Function.iterate_add_apply, hbegin, hloop₁.run] + rcases k with _ | k + · exact good_push hst hf (by omega) (.inr ⟨_, rfl, hv⟩) + · rw [show k + 1 = k + 1 from rfl, Function.iterate_add_apply, Function.iterate_one, + R.step_return] + exact (ih₂ hst k (by omega)).mono (by omega) + +/-- **The states of an evaluation are good**, up to and including its returned value. -/ +theorem Eval.good {x : X} {y : Y} {n h : ℕ} (he : R.Eval I x y n h) {st : List (X × A)} + (hst : ∀ f ∈ st, I.frame f.1 f.2) : + ∀ j ≤ 2 * n - 1, Good I (st.length + h) (R.step^[j] (st, some x, none)) := by + obtain ⟨hx, hy, ⟨hl, rfl, rfl, rfl⟩ | ⟨hl, b, n', h', hloop, rfl, rfl, rfl⟩⟩ := he + · intro j hj + rcases j with _ | j + · exact ⟨by simp, hst, .inl ⟨x, rfl, hx⟩⟩ + · rw [show j = 0 by omega, Function.iterate_one, R.step_leaf _ _ hl] + exact ⟨by simp, hst, .inr ⟨_, rfl, hy⟩⟩ + · intro j hj + rcases j with _ | j + · exact ⟨by simp, hst, .inl ⟨x, rfl, hx⟩⟩ + rw [Function.iterate_add_apply, Function.iterate_one, R.step_call _ _ hl] + rcases Nat.lt_or_ge j (2 * n') with hj' | hj' + · exact (hloop.good hst j hj').mono (by omega) + · rw [show j = 2 * n' by omega, hloop.run] + exact ⟨by simp, hst, .inr ⟨_, rfl, hy⟩⟩ + +/-- **Every state of a run from an empty stack is good**, including the final state, which no +step changes. -/ +theorem Eval.good_iterate {x : X} {y : Y} {n h : ℕ} (he : R.Eval I x y n h) (j : ℕ) : + Good I h (R.step^[j] ([], some x, none)) := by + rcases le_or_gt j (2 * n - 1) with hj | hj + · simpa using he.good (st := []) (by simp) j hj + · obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt hj + rw [show 2 * n - 1 + k + 1 = (k + 1) + (2 * n - 1) by omega, Function.iterate_add_apply, + he.run, Function.iterate_fixed (R.step_final y)] + exact ⟨by simp, by simp, .inr ⟨y, rfl, he.2.1⟩⟩ + +/-! ### The native machine -/ + +section Native + +variable (R) {encX : X ↪ List Bool} {encA : A ↪ List Bool} {encY : Y ↪ List Bool} + +/-- The encoding of a machine state: the list of open frames, each a pair, then the optional +pending node and the optional returned value. -/ +abbrev encState (encX : X ↪ List Bool) (encA : A ↪ List Bool) (encY : Y ↪ List Bool) : + State X A Y ↪ List Bool := + encPair (encList (encPair encX encA)) (encPair (encOption encX) (encOption encY)) + +/-- **The polynomial-time components** of a scheme: everything but the leaf step. -/ +structure PolyTime (encX : X ↪ List Bool) (encA : A ↪ List Bool) (encY : Y ↪ List Bool) : + Prop where + /-- The leaf test. -/ + isLeaf : ComputableInPolyTime R.isLeaf encX encBool + /-- The initial accumulator. -/ + start : ComputableInPolyTime R.start encX encA + /-- Child generation. -/ + next : ComputableInPolyTime (fun p : X × A => R.next p.1 p.2) (encPair encX encA) + (encOption encX) + /-- Absorbing a child's value. -/ + absorb : ComputableInPolyTime (fun p : (X × A) × Y => R.absorb p.1.1 p.1.2 p.2) + (encPair (encPair encX encA) encY) encA + /-- The value of a call. -/ + finish : ComputableInPolyTime (fun p : X × A => R.finish p.1 p.2) (encPair encX encA) encY + +/-- Whether the register holds a pending leaf. -/ +def isLeafCall (σ : State X A Y) : Bool := σ.2.1.elim false R.isLeaf + +/-- Evaluate a pending node as a leaf, keeping the stack. -/ +def leafStep (σ : State X A Y) : State X A Y := + (σ.1, none, σ.2.1.elim none fun x => some (R.leaf x)) + +/-- Every step but the evaluation of a leaf. -/ +def polyStep (σ : State X A Y) : State X A Y := + σ.2.1.elim + (σ.2.2.elim σ fun y => σ.1.head?.elim σ fun f => R.resume f.1 (R.absorb f.1 f.2 y) σ.1.tail) + (fun x => R.resume x (R.start x) σ.1) + +/-- A step evaluates a leaf, or takes a polynomial-time step. -/ +theorem step_eq_ite (σ : State X A Y) : + R.step σ = if R.isLeafCall σ then R.leafStep σ else R.polyStep σ := by + rcases σ with ⟨_ | ⟨⟨x, a⟩, st⟩, _ | c, _ | y⟩ <;> + simp only [step, isLeafCall, leafStep, polyStep, Option.elim, List.head?, List.tail, + Bool.false_eq_true, ite_false] <;> rfl + +variable {R} + +/-- Continuing a call is polynomial-time. -/ +theorem resume_polyTime (h : R.PolyTime encX encA encY) : + ComputableInPolyTime (fun q : (X × A) × List (X × A) => R.resume q.1.1 q.1.2 q.2) + (encPair (encPair encX encA) (encList (encPair encX encA))) (encState encX encA encY) := by + have hfr := ComputableInPolyTime.fst (encPair encX encA) (encList (encPair encX encA)) + have hst := ComputableInPolyTime.snd (encPair encX encA) (encList (encPair encX encA)) + have hfallback : ComputableInPolyTime + (fun q : (X × A) × List (X × A) => (q.2, (none : Option X), some (R.finish q.1.1 q.1.2))) + (encPair (encPair encX encA) (encList (encPair encX encA))) (encState encX encA encY) := + hst.prod ((ComputableInPolyTime.const none).prod + ((ComputableInPolyTime.optionSome encY).comp (h.finish.comp hfr))) + have hbody : ComputableInPolyTime + (fun p : ((X × A) × List (X × A)) × X => (p.1.1 :: p.1.2, some p.2, (none : Option Y))) + (encPair (encPair (encPair encX encA) (encList (encPair encX encA))) encX) + (encState encX encA encY) := by + have hq := ComputableInPolyTime.fst + (encPair (encPair encX encA) (encList (encPair encX encA))) encX + have hc := ComputableInPolyTime.snd + (encPair (encPair encX encA) (encList (encPair encX encA))) encX + exact (ComputableInPolyTime.cons' (hfr.comp hq) (hst.comp hq)).prod + (((ComputableInPolyTime.optionSome encX).comp hc).prod (ComputableInPolyTime.const none)) + have helim := ComputableInPolyTime.optionElimWithInput + (value := fun q : (X × A) × List (X × A) => R.next q.1.1 q.1.2) + (fallback := fun q => (q.2, (none : Option X), some (R.finish q.1.1 q.1.2))) + (body := fun q c => (q.1 :: q.2, some c, (none : Option Y))) (h.next.comp hfr) hfallback hbody + refine helim.of_enc_eq fun q => ?_ + rcases q with ⟨⟨x, a⟩, st⟩ + change encState encX encA encY (R.resume x a st) = + encState encX encA encY ((R.next x a).elim (st, none, some (R.finish x a)) + fun c => ((x, a) :: st, some c, none)) + rw [resume] + cases R.next x a <;> rfl + +/-- The leaf test on the register is polynomial-time. -/ +theorem isLeafCall_polyTime (h : R.PolyTime encX encA encY) : + ComputableInPolyTime R.isLeafCall (encState encX encA encY) encBool := by + have hreg := (ComputableInPolyTime.fst (encOption encX) (encOption encY)).comp + (ComputableInPolyTime.snd (encList (encPair encX encA)) + (encPair (encOption encX) (encOption encY))) + exact ComputableInPolyTime.optionElimWithInput (body := fun _ x => R.isLeaf x) hreg + (ComputableInPolyTime.const false) + (h.isLeaf.comp (ComputableInPolyTime.snd (encState encX encA encY) encX)) + +/-- Every step but the evaluation of a leaf is polynomial-time. -/ +theorem polyStep_polyTime (h : R.PolyTime encX encA encY) : + ComputableInPolyTime R.polyStep (encState encX encA encY) (encState encX encA encY) := by + have hstack : ComputableInPolyTime (fun σ : State X A Y => σ.1) (encState encX encA encY) + (encList (encPair encX encA)) := + ComputableInPolyTime.fst (encList (encPair encX encA)) + (encPair (encOption encX) (encOption encY)) + have hreg : ComputableInPolyTime (fun σ : State X A Y => σ.2) (encState encX encA encY) + (encPair (encOption encX) (encOption encY)) := + ComputableInPolyTime.snd (encList (encPair encX encA)) + (encPair (encOption encX) (encOption encY)) + have hpend : ComputableInPolyTime (fun σ : State X A Y => σ.2.1) (encState encX encA encY) + (encOption encX) := (ComputableInPolyTime.fst (encOption encX) (encOption encY)).comp hreg + have hret : ComputableInPolyTime (fun σ : State X A Y => σ.2.2) (encState encX encA encY) + (encOption encY) := (ComputableInPolyTime.snd (encOption encX) (encOption encY)).comp hreg + -- A returned value is absorbed by the innermost open frame. + have hframe : ComputableInPolyTime + (fun q : (State X A Y × Y) × (X × A) => + R.resume q.2.1 (R.absorb q.2.1 q.2.2 q.1.2) q.1.1.1.tail) + (encPair (encPair (encState encX encA encY) encY) (encPair encX encA)) + (encState encX encA encY) := by + have hq := ComputableInPolyTime.fst (encPair (encState encX encA encY) encY) + (encPair encX encA) + have hf := ComputableInPolyTime.snd (encPair (encState encX encA encY) encY) + (encPair encX encA) + have hy := (ComputableInPolyTime.snd (encState encX encA encY) encY).comp hq + have hσ := (ComputableInPolyTime.fst (encState encX encA encY) encY).comp hq + have habs := h.absorb.comp (hf.prod hy) + exact (resume_polyTime h).comp + ((((ComputableInPolyTime.fst encX encA).comp hf).prod habs).prod + ((ComputableInPolyTime.tail (encA := encPair encX encA)).comp (hstack.comp hσ))) + have hreturn : ComputableInPolyTime + (fun p : State X A Y × Y => + p.1.1.head?.elim p.1 fun f => R.resume f.1 (R.absorb f.1 f.2 p.2) p.1.1.tail) + (encPair (encState encX encA encY) encY) (encState encX encA encY) := by + have hσ := ComputableInPolyTime.fst (encState encX encA encY) encY + have hhead : ComputableInPolyTime (fun p : State X A Y × Y => p.1.1.head?) + (encPair (encState encX encA encY) encY) (encOption (encPair encX encA)) := + (ComputableInPolyTime.head? (encPair encX encA) (encL := encList (encPair encX encA))).comp + (hstack.comp hσ) + exact ComputableInPolyTime.optionElimWithInput + (value := fun p : State X A Y × Y => p.1.1.head?) (fallback := fun p => p.1) + (body := fun p f => R.resume f.1 (R.absorb f.1 f.2 p.2) p.1.1.tail) hhead hσ hframe + have hnoCall : ComputableInPolyTime + (fun σ : State X A Y => + σ.2.2.elim σ fun y => σ.1.head?.elim σ fun f => R.resume f.1 (R.absorb f.1 f.2 y) σ.1.tail) + (encState encX encA encY) (encState encX encA encY) := + ComputableInPolyTime.optionElimWithInput (value := fun σ : State X A Y => σ.2.2) + (fallback := fun σ => σ) + (body := fun σ y => σ.1.head?.elim σ fun f => R.resume f.1 (R.absorb f.1 f.2 y) σ.1.tail) + hret ComputableInPolyTime.id' hreturn + have hcall : ComputableInPolyTime + (fun p : State X A Y × X => R.resume p.2 (R.start p.2) p.1.1) + (encPair (encState encX encA encY) encX) (encState encX encA encY) := by + have hx : ComputableInPolyTime (fun p : State X A Y × X => p.2) + (encPair (encState encX encA encY) encX) encX := + ComputableInPolyTime.snd (encState encX encA encY) encX + have hst : ComputableInPolyTime (fun p : State X A Y × X => p.1.1) + (encPair (encState encX encA encY) encX) (encList (encPair encX encA)) := + hstack.comp (ComputableInPolyTime.fst (encState encX encA encY) encX) + exact (resume_polyTime h).comp ((hx.prod (h.start.comp hx)).prod hst) + exact ComputableInPolyTime.optionElimWithInput (value := fun σ : State X A Y => σ.2.1) + (fallback := fun σ => σ.2.2.elim σ fun y => + σ.1.head?.elim σ fun f => R.resume f.1 (R.absorb f.1 f.2 y) σ.1.tail) + (body := fun σ x => R.resume x (R.start x) σ.1) hpend hnoCall hcall + +end Native + +section Certificate + +variable {encX : X ↪ List Bool} {encA : A ↪ List Bool} {encY : Y ↪ List Bool} + +theorem stack_polyTime : + ComputableInPolyTime (fun σ : State X A Y => σ.1) (encState encX encA encY) + (encList (encPair encX encA)) := + ComputableInPolyTime.fst _ _ + +theorem pending_polyTime : + ComputableInPolyTime (fun σ : State X A Y => σ.2.1) (encState encX encA encY) + (encOption encX) := + (ComputableInPolyTime.fst (encOption encX) (encOption encY)).comp (ComputableInPolyTime.snd _ _) + +variable (R) in +/-- **The leaf step**: the leaf certificate on the pending node, keeping the stack. -/ +noncomputable def leafStepCertificate (leaf : NativeCertificate R.leaf encX encY) : + NativeCertificate R.leafStep (encState encX encA encY) (encState encX encA encY) := + (NativeCertificate.ofPolyTime stack_polyTime).prod ((NativeCertificate.const none).prod + (NativeCertificate.option (value := fun σ : State X A Y => σ.2.1) (fallback := fun _ => none) + (body := fun p : State X A Y × X => some (R.leaf p.2)) + (NativeCertificate.ofPolyTime pending_polyTime) (NativeCertificate.const none) + (NativeCertificate.some (leaf.comp (NativeCertificate.payload _ encX))))) + +/-- **One step of the machine**: the leaf certificate on a pending leaf, and a polynomial-time +step otherwise. -/ +noncomputable def stepCertificate (h : R.PolyTime encX encA encY) + (leaf : NativeCertificate R.leaf encX encY) : + NativeCertificate R.step (encState encX encA encY) (encState encX encA encY) := + (NativeCertificate.branch (NativeCertificate.ofPolyTime (isLeafCall_polyTime h)) + (leafStepCertificate R leaf) (NativeCertificate.ofPolyTime (polyStep_polyTime h))).congr + fun σ => (R.step_eq_ite σ).symm + +theorem stepCertificate_time (h : R.PolyTime encX encA encY) + (leaf : NativeCertificate R.leaf encX encY) (σ : State X A Y) : + (stepCertificate h leaf).time σ = + (NativeCertificate.ofPolyTime (isLeafCall_polyTime h)).time σ + + if R.isLeafCall σ then (leafStepCertificate R (encA := encA) leaf).time σ + else (NativeCertificate.ofPolyTime (polyStep_polyTime h)).time σ := rfl + +theorem stepCertificate_space (h : R.PolyTime encX encA encY) + (leaf : NativeCertificate R.leaf encX encY) (σ : State X A Y) : + (stepCertificate h leaf).space σ = + (NativeCertificate.ofPolyTime (isLeafCall_polyTime h)).space σ + + if R.isLeafCall σ then (leafStepCertificate R (encA := encA) leaf).space σ + else (NativeCertificate.ofPolyTime (polyStep_polyTime h)).space σ := rfl + +theorem leafStepCertificate_time (leaf : NativeCertificate R.leaf encX encY) (st : List (X × A)) + (x : X) (v : Option Y) : + (leafStepCertificate R (encA := encA) leaf).time (st, some x, v) = + (NativeCertificate.ofPolyTime (stack_polyTime (encX := encX) (encA := encA) + (encY := encY))).time (st, some x, v) + + ((encState encX encA encY (st, some x, v)).length + + (2 * (NativeCertificate.ofPolyTime (pending_polyTime (encX := encX) (encA := encA) + (encY := encY))).time (st, some x, v) + + (encState encX encA encY (st, some x, v)).length + + ((encPair (encState encX encA encY) encX ((st, some x, v), x)).length + + leaf.time x))) := rfl + +theorem leafStepCertificate_space (leaf : NativeCertificate R.leaf encX encY) + (st : List (X × A)) (x : X) (v : Option Y) : + (leafStepCertificate R (encA := encA) leaf).space (st, some x, v) = + (NativeCertificate.ofPolyTime (stack_polyTime (encX := encX) (encA := encA) + (encY := encY))).space (st, some x, v) + + ((encState encX encA encY (st, some x, v)).length + + (2 * (NativeCertificate.ofPolyTime (pending_polyTime (encX := encX) (encA := encA) + (encY := encY))).space (st, some x, v) + + (encState encX encA encY (st, some x, v)).length + + ((encPair (encState encX encA encY) encX ((st, some x, v), x)).length + + leaf.space x))) := rfl + +variable (R) in +/-- The leaf cost of a state: the leaf certificate's bound at a pending leaf, and zero +otherwise. -/ +def leafCost (cost : X → ℕ) (σ : State X A Y) : ℕ := + σ.2.1.elim 0 fun x => if R.isLeaf x then cost x else 0 + +private theorem length_pending_le {σ : State X A Y} {x : X} (hx : σ.2.1 = some x) : + (encX x).length ≤ (encState encX encA encY σ).length := by + rcases σ with ⟨st, r, v⟩ + simp only at hx + subst hx + simp only [length_encPair, encOption_some, List.length_cons] + omega + +/-- **The cost of one step**: a polynomial in the state length, plus the leaf certificate at a +pending leaf. -/ +theorem exists_stepCertificate_le (h : R.PolyTime encX encA encY) + (leaf : NativeCertificate R.leaf encX encY) : + ∃ K : ℕ, ∀ σ : State X A Y, + (stepCertificate h leaf).time σ ≤ + K * ((encState encX encA encY σ).length + 1) ^ K + R.leafCost leaf.time σ ∧ + (stepCertificate h leaf).space σ ≤ + K * ((encState encX encA encY σ).length + 1) ^ K + R.leafCost leaf.space σ := by + have ht := NativeCertificate.ofPolyTime_isPolynomial (isLeafCall_polyTime h) + have hp := NativeCertificate.ofPolyTime_isPolynomial (polyStep_polyTime h) + have hs := NativeCertificate.ofPolyTime_isPolynomial (stack_polyTime (encX := encX) + (encA := encA) (encY := encY)) + have hc := NativeCertificate.ofPolyTime_isPolynomial (pending_polyTime (encX := encX) + (encA := encA) (encY := encY)) + -- Everything but the leaf certificate is polynomial in the state length. + have hT := ((((ht.1.add hp.1).add hs.1).add ((PolyBounded.const 2).mul hc.1)).add + ((PolyBounded.const 6).mul PolyBounded.self)).add (PolyBounded.const 1) + have hS := ((((ht.2.add hp.2).add hs.2).add ((PolyBounded.const 2).mul hc.2)).add + ((PolyBounded.const 6).mul PolyBounded.self)).add (PolyBounded.const 1) + obtain ⟨cT, dT, hcT⟩ := hT.exists_le + obtain ⟨cS, dS, hcS⟩ := hS.exists_le + refine ⟨cT + cS + dT + dS, fun σ => ?_⟩ + have hmono {c d : ℕ} (hc : c ≤ cT + cS + dT + dS) (hd : d ≤ cT + cS + dT + dS) : + c * ((encState encX encA encY σ).length + 1) ^ d ≤ + (cT + cS + dT + dS) * ((encState encX encA encY σ).length + 1) ^ (cT + cS + dT + dS) := + Nat.mul_le_mul hc (Nat.pow_le_pow_right (Nat.succ_pos _) hd) + have hT' := (hcT σ).trans (hmono (by omega) (by omega)) + have hS' := (hcS σ).trans (hmono (by omega) (by omega)) + rcases σ with ⟨st, _ | x, v⟩ + · rw [stepCertificate_time, stepCertificate_space] + simp only [leafCost, isLeafCall, Option.elim, Bool.false_eq_true, ite_false, Nat.add_zero] + constructor <;> omega + · have hx := length_pending_le (encX := encX) (encA := encA) (encY := encY) + (σ := (st, some x, v)) rfl + rw [stepCertificate_time, stepCertificate_space] + by_cases hl : R.isLeaf x = true + · simp only [leafCost, isLeafCall, Option.elim, hl, ite_true] + have hpair := length_encPair (enc₁ := encState encX encA encY) (enc₂ := encX) + ((st, some x, v), x) + dsimp only at hpair + rw [leafStepCertificate_time, leafStepCertificate_space] + constructor <;> omega + · simp only [Bool.not_eq_true] at hl + simp only [leafCost, isLeafCall, Option.elim, hl, Bool.false_eq_true, ite_false, + Nat.add_zero] + constructor <;> omega + +variable (R) in +/-- **The clocked run**: the register after `fuel a` steps from the root `root a` on an empty +stack. -/ +def run {I : Type} (fuel : I → ℕ) (root : I → X) (a : I) : Option Y := + (R.step^[fuel a] ([], some (root a), none)).2.2 + +/-- **Enough fuel gives the value.** -/ +theorem run_eq_some {I : Type} {fuel : I → ℕ} {root : I → X} {Inv : Invariant X A Y} {a : I} + {y : Y} {N H : ℕ} (he : R.Eval Inv (root a) y N H) (hfuel : 2 * N - 1 ≤ fuel a) : + R.run fuel root a = some y := by + obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_le hfuel + rw [run, hk, Nat.add_comm, Function.iterate_add_apply, he.run, + Function.iterate_fixed (R.step_final y)] + +/-- **The native machine** for the clocked run: one fixed machine, from native certificates for +the fuel and the root. -/ +noncomputable def certificate (h : R.PolyTime encX encA encY) + (leaf : NativeCertificate R.leaf encX encY) {I : Type} {encIn : I ↪ List Bool} + {fuel : I → ℕ} {root : I → X} (cn : NativeCertificate fuel encIn encNat) + (croot : NativeCertificate root encIn encX) : + NativeCertificate (R.run fuel root) encIn (encOption encY) := + NativeCertificate.snd (NativeCertificate.snd (NativeCertificate.iterate cn + ((NativeCertificate.const ([] : List (X × A))).prod + ((NativeCertificate.some croot).prod (NativeCertificate.const (none : Option Y)))) + (stepCertificate h leaf))) + +/-- A good state is at most `5 (H + 1) (F + 1)` long when the nodes, frames and values it holds +are at most `F` long. -/ +theorem length_encState_le {Inv : Invariant X A Y} {H F : ℕ} {σ : State X A Y} + (hσ : Good Inv H σ) (hnode : ∀ x, Inv.node x → (encX x).length ≤ F) + (hframe : ∀ x a, Inv.frame x a → (encPair encX encA (x, a)).length ≤ F) + (hvalue : ∀ y, Inv.value y → (encY y).length ≤ F) : + (encState encX encA encY σ).length ≤ 5 * (H + 1) * (F + 1) := by + obtain ⟨hlen, hfr, hreg⟩ := hσ + have hstack : (encList (encPair encX encA) σ.1).length ≤ H * (2 * F + 1) := by + rw [length_encList] + calc (σ.1.map fun f => 2 * (encPair encX encA f).length + 1).sum + ≤ (σ.1.map fun f => 2 * (encPair encX encA f).length + 1).length • (2 * F + 1) := + List.sum_le_length_nsmul _ _ fun n hn => by + obtain ⟨⟨x, a⟩, hf, rfl⟩ := List.mem_map.mp hn + have := hframe x a (hfr _ hf) + omega + _ ≤ H * (2 * F + 1) := by + rw [List.length_map, smul_eq_mul] + exact Nat.mul_le_mul_right _ hlen + have hHF : H * (2 * F + 1) ≤ 2 * H * F + H := by rw [Nat.mul_add, Nat.mul_one]; ring_nf; omega + rcases σ with ⟨st, r, v⟩ + rcases hreg with ⟨x, hr, hx⟩ | ⟨y, hr, hy⟩ <;> simp only [Prod.mk.injEq] at hr <;> + obtain ⟨rfl, rfl⟩ := hr + · have := hnode x hx + simp only [length_encPair, encOption_some, encOption_none, List.length_cons, + List.length_nil] at hstack ⊢ + nlinarith + · have := hvalue y hy + simp only [length_encPair, encOption_some, encOption_none, List.length_cons, + List.length_nil] at hstack ⊢ + nlinarith + +private theorem pow_absorb (K₀ z : ℕ) (hz : 1 ≤ z) : + K₀ * (5 * z + 1) ^ K₀ + 5 * z ≤ (K₀ * 6 ^ K₀ + K₀ + 6) * z ^ (K₀ * 6 ^ K₀ + K₀ + 6) := by + set K := K₀ * 6 ^ K₀ + K₀ + 6 + have h6 : (5 * z + 1) ^ K₀ ≤ 6 ^ K₀ * z ^ K := by + calc (5 * z + 1) ^ K₀ ≤ (6 * z) ^ K₀ := Nat.pow_le_pow_left (by omega) _ + _ = 6 ^ K₀ * z ^ K₀ := Nat.mul_pow _ _ _ + _ ≤ 6 ^ K₀ * z ^ K := Nat.mul_le_mul_left _ (Nat.pow_le_pow_right hz (by omega)) + have hz' : z ≤ z ^ K := by + calc z = z ^ 1 := (pow_one z).symm + _ ≤ z ^ K := Nat.pow_le_pow_right hz (by omega) + calc K₀ * (5 * z + 1) ^ K₀ + 5 * z ≤ K₀ * (6 ^ K₀ * z ^ K) + 5 * z ^ K := + Nat.add_le_add (Nat.mul_le_mul_left _ h6) (Nat.mul_le_mul_left _ hz') + _ = (K₀ * 6 ^ K₀ + 5) * z ^ K := by ring + _ ≤ K * z ^ K := Nat.mul_le_mul_right _ (by omega) + +/-- **The resources of the native machine.** There is one constant `K` such that, for any fuel +and root certificates, if the root has a derivation with `N` nodes and at most `H` open calls +whose nodes, frames and values are at most `F` long, and whose leaves are evaluated by the leaf +certificate within time `TL` and space `SL`, then the time is at most the cost of the fuel and the +root plus `fuel + 1` times `K ((H + 1) (F + 1)) ^ K + TL` (and the cost of the binary clock), and +the workspace is at most the cost of the fuel and the root plus `K ((H + 1) (F + 1)) ^ K + SL`. +The bounds hold for any fuel; with `2 * N - 1 ≤ fuel` the result is the value +(`run_eq_some`). -/ +theorem certificate_le (h : R.PolyTime encX encA encY) + (leaf : NativeCertificate R.leaf encX encY) : + ∃ K : ℕ, ∀ {I : Type} {encIn : I ↪ List Bool} {fuel : I → ℕ} {root : I → X} + (cn : NativeCertificate fuel encIn encNat) (croot : NativeCertificate root encIn encX) + (Inv : Invariant X A Y) (F TL SL : ℕ), + (∀ x, Inv.node x → (encX x).length ≤ F ∧ + (R.isLeaf x = true → leaf.time x ≤ TL ∧ leaf.space x ≤ SL)) → + (∀ x a, Inv.frame x a → (encPair encX encA (x, a)).length ≤ F) → + (∀ y, Inv.value y → (encY y).length ≤ F) → + ∀ (a : I) (y : Y) (N H : ℕ), R.Eval Inv (root a) y N H → + (certificate h leaf cn croot).time a ≤ cn.time a + croot.time a + 2 * (encIn a).length + + (fuel a + 1) * (K * ((H + 1) * (F + 1)) ^ K + TL + + ((encNat (fuel a)).length + 1) ^ 2) ∧ + (certificate h leaf cn croot).space a ≤ cn.space a + croot.space a + + 2 * (encIn a).length + K * ((H + 1) * (F + 1)) ^ K + SL + + (encNat (fuel a)).length := by + obtain ⟨K₀, hK₀⟩ := exists_stepCertificate_le h leaf + refine ⟨K₀ * 6 ^ K₀ + K₀ + 6, ?_⟩ + intro I encIn fuel root cn croot Inv F TL SL hnode hframe hvalue a y N H he + set z := (H + 1) * (F + 1) + have hz : 1 ≤ z := Nat.one_le_iff_ne_zero.mpr (Nat.mul_ne_zero (by omega) (by omega)) + have habsorb := pow_absorb K₀ z hz + -- Every state of the run is good, hence short, and pays the leaf bound only at a leaf. + have hgood := he.good_iterate (R := R) + have hlen (j : ℕ) : (encState encX encA encY (R.step^[j] ([], some (root a), none))).length ≤ + 5 * z := by + have := length_encState_le (hgood j) (fun x hx => (hnode x hx).1) hframe hvalue + rwa [Nat.mul_assoc] at this + clear_value z + have hcost (cost : X → ℕ) (B : ℕ) + (hB : ∀ x, Inv.node x → R.isLeaf x = true → cost x ≤ B) (j : ℕ) : + R.leafCost cost (R.step^[j] ([], some (root a), none)) ≤ B := by + obtain ⟨-, -, ⟨x, hr, hx⟩ | ⟨y', hr, -⟩⟩ := hgood j <;> simp only [leafCost, hr, Option.elim] + · split_ifs with hl + · exact hB x hx hl + · exact Nat.zero_le _ + · exact Nat.zero_le _ + have hround (j : ℕ) : + (stepCertificate h leaf).time (R.step^[j] ([], some (root a), none)) ≤ + K₀ * (5 * z + 1) ^ K₀ + TL ∧ + (stepCertificate h leaf).space (R.step^[j] ([], some (root a), none)) ≤ + K₀ * (5 * z + 1) ^ K₀ + SL := by + obtain ⟨ht, hs⟩ := hK₀ (R.step^[j] ([], some (root a), none)) + have hp : K₀ * ((encState encX encA encY (R.step^[j] ([], some (root a), none))).length + 1) ^ + K₀ ≤ K₀ * (5 * z + 1) ^ K₀ := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by have := hlen j; omega) _) + have hct := hcost leaf.time TL (fun x hx hl => ((hnode x hx).2 hl).1) j + have hcs := hcost leaf.space SL (fun x hx hl => ((hnode x hx).2 hl).2) j + constructor <;> omega + have hmaxT := NativeCertificate.maxRoundTime_le (stepCertificate h leaf) (fuel a) + ([], some (root a), none) (R := K₀ * (5 * z + 1) ^ K₀ + TL) fun j _ => (hround j).1 + have hmaxS := NativeCertificate.maxRoundSpace_le (stepCertificate h leaf) (fuel a) + ([], some (root a), none) (Q := K₀ * (5 * z + 1) ^ K₀ + SL) fun j _ => (hround j).2 + have hmaxL := NativeCertificate.maxStateLength_le + (encPair (encList (encPair encX encA)) (encPair (encOption encX) (encOption encY))) R.step + (fuel a) ([], some (root a), none) (B := 5 * z) fun j _ => hlen j + simp only [certificate, NativeCertificate.snd_time, NativeCertificate.snd_space, + NativeCertificate.iterate_time, NativeCertificate.iterate_space, + NativeCertificate.prod_time, NativeCertificate.prod_space, NativeCertificate.const_time, + NativeCertificate.const_space, NativeCertificate.some_time, NativeCertificate.some_space] + constructor + · have hstep : NativeCertificate.maxRoundTime (stepCertificate h leaf) (fuel a) + ([], some (root a), none) + + NativeCertificate.maxStateLength + (encPair (encList (encPair encX encA)) (encPair (encOption encX) (encOption encY))) + R.step (fuel a) ([], some (root a), none) + ((encNat (fuel a)).length + 1) ^ 2 ≤ + (K₀ * 6 ^ K₀ + K₀ + 6) * z ^ (K₀ * 6 ^ K₀ + K₀ + 6) + TL + + ((encNat (fuel a)).length + 1) ^ 2 := by omega + have := Nat.mul_le_mul_left (fuel a + 1) hstep + omega + · omega + +end Certificate + +end Scheme + +end Cslib.GenericRAM.StackRecursion diff --git a/Complexity/Foundations/Data/Nat/RecursionTree.lean b/Complexity/Foundations/Data/Nat/RecursionTree.lean new file mode 100644 index 0000000000..e5f2982128 --- /dev/null +++ b/Complexity/Foundations/Data/Nat/RecursionTree.lean @@ -0,0 +1,170 @@ +/- +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.Foundations.Data.Nat.SqrtLog +public import Mathlib.Algebra.BigOperators.Group.Finset.Basic +import Mathlib.Algebra.Order.BigOperators.Group.Finset +import Mathlib.Tactic.IntervalCases +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Ring + +/-! +# Counting the nodes of a recursion tree + +A recursion whose calls at depth `d` have at most `b d` children, with at most `k` levels below +depth `d`, has at most `Nat.recursionBound b k d` nodes below and including a call at depth `d`: +one for the call, plus `b d` subtrees of one level less (`Nat.recursionBound_succ`). This is at +most `k + 1` times the product of the branching factors (`Nat.recursionBound_le`). + +**Recursion trees of size `2 ^ O(n / √(log n))`.** If a call at depth `j` has at most +`2 ^ (c ⌊log₂ n⌋ + e j)` children, there are at most `⌊log₂ n⌋` levels, and the excess exponents +sum to `O(n / √⌊log₂ n⌋)`, then the tree has `2 ^ O(n / √⌊log₂ n⌋)` nodes +(`Nat.exists_recursionBound_le_two_pow_div_sqrt_log_two`), in the natural-number scale of +`Nat.exists_three_pow_mul_le_two_pow_div_sqrt_log_two`. The polynomial factors `2 ^ (c ⌊log₂ n⌋)` +contribute `2 ^ O(log² n)`, which the scale absorbs. Excess exponents halving with the depth sum to +at most twice the first one (`Nat.sum_div_two_pow_le`). + +This is the call count in the proof of Theorem D.1 of [OpenAI2026ETH] (Appendix D.4.7, p. 64): +a call at depth `d` has `s ^ O(1) exp(O(s / √λ · (√2 / 8) ^ d))` children and there are +`O(log λ)` levels. + +## Main definitions + +* `Nat.recursionBound`: the node bound of a recursion tree with given branching factors. + +## Main results + +* `Nat.recursionBound_le`: at most `k + 1` times the product of the branching factors. +* `Nat.sum_div_two_pow_le`: `∑ j < D, x / 2 ^ j ≤ 2 x`. +* `Nat.exists_recursionBound_le_two_pow_div_sqrt_log_two`: recursion trees of size + `2 ^ O(n / √⌊log₂ n⌋)`. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Appendix D.4.7 (p. 64). +-/ + +public section + +namespace Nat + +open Finset + +/-- The node bound of a recursion tree whose calls at depth `d` have at most `b d` children, +for a call at depth `d` with at most `k` levels below it. -/ +@[expose] def recursionBound (b : ℕ → ℕ) : ℕ → ℕ → ℕ + | 0, _ => 1 + | k + 1, d => 1 + b d * recursionBound b k (d + 1) + +@[simp] theorem recursionBound_zero (b : ℕ → ℕ) (d : ℕ) : recursionBound b 0 d = 1 := rfl + +/-- A call is one node above its children's subtrees. -/ +theorem recursionBound_succ (b : ℕ → ℕ) (k d : ℕ) : + recursionBound b (k + 1) d = 1 + b d * recursionBound b k (d + 1) := rfl + +/-- **The node bound is at most `k + 1` times the product of the branching factors.** -/ +theorem recursionBound_le (b : ℕ → ℕ) (k d : ℕ) : + recursionBound b k d ≤ (k + 1) * ∏ j ∈ range k, max 1 (b (d + j)) := by + induction k generalizing d with + | zero => simp + | succ k ih => + rw [recursionBound_succ, prod_range_succ'] + set P := ∏ j ∈ range k, max 1 (b (d + (j + 1))) + have hP : 1 ≤ P := one_le_prod fun _ _ => le_max_left _ _ + have hm : 1 ≤ max 1 (b d) := le_max_left _ _ + have hb : b d ≤ max 1 (b d) := le_max_right _ _ + have ih' : recursionBound b k (d + 1) ≤ (k + 1) * P := by + simpa only [Nat.add_assoc, Nat.add_comm 1] using ih (d + 1) + simp only [Nat.add_zero] + calc 1 + b d * recursionBound b k (d + 1) ≤ max 1 (b d) * P + max 1 (b d) * ((k + 1) * P) := + Nat.add_le_add (Nat.one_le_iff_ne_zero.mpr (Nat.mul_ne_zero (by omega) (by omega))) + (Nat.mul_le_mul hb ih') + _ = (k + 1 + 1) * (P * max 1 (b d)) := by ring + +/-- **Halving excess exponents**: `∑ j < D, x / 2 ^ j ≤ 2 x`. -/ +theorem sum_div_two_pow_le (x D : ℕ) : ∑ j ∈ range D, x / 2 ^ j ≤ 2 * x := by + induction D generalizing x with + | zero => simp + | succ D ih => + rw [sum_range_succ'] + have h : ∑ j ∈ range D, x / 2 ^ (j + 1) = ∑ j ∈ range D, x / 2 / 2 ^ j := + sum_congr rfl fun j _ => by rw [pow_succ, Nat.mul_comm, Nat.div_div_eq_div_mul] + rw [h, pow_zero, Nat.div_one] + have := ih (x / 2) + have := Nat.div_mul_le_self x 2 + omega + +/-- `L ^ 3 ≤ 8 * 2 ^ L`. -/ +private theorem cube_le_eight_mul_two_pow (L : ℕ) : L ^ 3 ≤ 8 * 2 ^ L := by + have hlarge : ∀ m : ℕ, (m + 9) ^ 3 ≤ 8 * 2 ^ (m + 9) := by + intro m + induction m with + | zero => norm_num + | succ m ih => + have h : (m + 1 + 9) ^ 3 ≤ 2 * (m + 9) ^ 3 := by ring_nf; nlinarith + calc (m + 1 + 9) ^ 3 ≤ 2 * (m + 9) ^ 3 := h + _ ≤ 2 * (8 * 2 ^ (m + 9)) := Nat.mul_le_mul_left 2 ih + _ = 8 * 2 ^ (m + 1 + 9) := by ring + rcases Nat.lt_or_ge L 9 with hL | hL + · interval_cases L <;> norm_num + · obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_le' hL + exact hlarge m + +/-- The square of the logarithm is `O(n / √⌊log₂ n⌋)`: `⌊log₂ n⌋ ^ 2 ≤ 16 (n / √⌊log₂ n⌋)` from +`n = 2` on, since `⌊log₂ n⌋ ^ 2 √⌊log₂ n⌋ ≤ ⌊log₂ n⌋ ^ 3 ≤ 8 n`. -/ +theorem log_two_sq_le_div_sqrt_log_two {n : ℕ} (hn : 2 ≤ n) : + log 2 n ^ 2 ≤ 16 * (n / sqrt (log 2 n)) := by + set L := log 2 n + have hr : 1 ≤ sqrt L := one_le_sqrt_log_two hn + have hS : 1 ≤ n / sqrt L := one_le_div_sqrt_log_two hn + have hcube : L ^ 2 * sqrt L ≤ 8 * n := + calc L ^ 2 * sqrt L ≤ L ^ 2 * L := Nat.mul_le_mul_left _ (sqrt_le_self L) + _ = L ^ 3 := by ring + _ ≤ 8 * 2 ^ L := cube_le_eight_mul_two_pow L + _ ≤ 8 * n := Nat.mul_le_mul_left 8 (pow_log_le_self 2 (by omega)) + have h1 : L ^ 2 ≤ 8 * n / sqrt L := (Nat.le_div_iff_mul_le hr).2 hcube + have h2 := mul_div_le_mul_div_add 8 n (sqrt L) + omega + +/-- **Recursion trees of size `2 ^ O(n / √⌊log₂ n⌋)`.** For constants `c` and `E` there is `K` +such that, from `n = 2` on: if a call at depth `j < D` has at most `2 ^ (c ⌊log₂ n⌋ + e j)` +children, `D ≤ ⌊log₂ n⌋`, and `∑ j < D, e j ≤ E (n / √⌊log₂ n⌋)`, then +`(D + 1) ∏ j < D, max 1 (b j) ≤ 2 ^ (K n / √⌊log₂ n⌋)`, which bounds the nodes of the recursion +tree by `recursionBound_le`. -/ +theorem exists_recursionBound_le_two_pow_div_sqrt_log_two (c E : ℕ) : + ∃ K, ∀ (n D : ℕ) (b e : ℕ → ℕ), 2 ≤ n → D ≤ log 2 n → + (∀ j < D, b j ≤ 2 ^ (c * log 2 n + e j)) → + ∑ j ∈ range D, e j ≤ E * (n / sqrt (log 2 n)) → + (D + 1) * ∏ j ∈ range D, max 1 (b j) ≤ 2 ^ (K * n / sqrt (log 2 n)) := by + refine ⟨1 + 16 * c + E, fun n D b e hn hD hb he => ?_⟩ + set L := log 2 n + set S := n / sqrt L + have hL : L ≤ S := log_two_le_div_sqrt_log_two n + have hL2 : L ^ 2 ≤ 16 * S := log_two_sq_le_div_sqrt_log_two hn + have hD1 : D + 1 ≤ 2 ^ L := (Nat.add_le_add_right hD 1).trans Nat.lt_two_pow_self + have hprod : ∏ j ∈ range D, max 1 (b j) ≤ 2 ^ (D * (c * L) + ∑ j ∈ range D, e j) := by + calc ∏ j ∈ range D, max 1 (b j) ≤ ∏ j ∈ range D, 2 ^ (c * L + e j) := + prod_le_prod fun j hj => max_le Nat.one_le_two_pow (hb j (mem_range.mp hj)) + _ = 2 ^ (∑ j ∈ range D, (c * L + e j)) := (Finset.prod_pow_eq_pow_sum _ _ _) + _ = 2 ^ (D * (c * L) + ∑ j ∈ range D, e j) := by + rw [sum_add_distrib, sum_const, card_range, smul_eq_mul] + have hexp : L + (D * (c * L) + ∑ j ∈ range D, e j) ≤ (1 + 16 * c + E) * S := by + have h1 : D * (c * L) ≤ c * (16 * S) := + calc D * (c * L) ≤ L * (c * L) := Nat.mul_le_mul_right _ hD + _ = c * L ^ 2 := by ring + _ ≤ c * (16 * S) := Nat.mul_le_mul_left _ hL2 + nlinarith + calc (D + 1) * ∏ j ∈ range D, max 1 (b j) + ≤ 2 ^ L * 2 ^ (D * (c * L) + ∑ j ∈ range D, e j) := Nat.mul_le_mul hD1 hprod + _ = 2 ^ (L + (D * (c * L) + ∑ j ∈ range D, e j)) := (pow_add _ _ _).symm + _ ≤ 2 ^ ((1 + 16 * c + E) * S) := Nat.pow_le_pow_right (by norm_num) hexp + _ ≤ 2 ^ ((1 + 16 * c + E) * n / sqrt L) := + Nat.pow_le_pow_right (by norm_num) (mul_div_le_mul_div_assoc _ _ _) + +end Nat diff --git a/ComplexityTests/StackRecursion.lean b/ComplexityTests/StackRecursion.lean new file mode 100644 index 0000000000..bcca97e434 --- /dev/null +++ b/ComplexityTests/StackRecursion.lean @@ -0,0 +1,257 @@ +/- +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.StackRecursion +import Complexity.Foundations.Data.Nat.RecursionTree +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeOptionPrimitives + +/-! # Depth-first stack recursion on a toy scheme + +The halving recursion: a node `x ≥ 2` has two children `x / 2`, a leaf has value `1`, and a call +adds its children's values. The value of `x` is its number of leaves. The tests run the stack +machine, derive `Eval` for every node, instantiate the polynomial-time components (so the +`PolyTime` hypotheses of the native certificate are satisfiable) and check the node-count +arithmetic. -/ + +namespace ComplexityTests.StackRecursion + +open Cslib.GenericRAM Cslib.GenericRAM.StackRecursion Turing.MultiTapeTM + +/-- The halving scheme. The accumulator counts the children done and sums their values. -/ +def halving : Scheme ℕ (ℕ × ℕ) ℕ where + isLeaf x := decide (x < 2) + leaf _ := 1 + start _ := (0, 0) + next x a := if a.1 < 2 then some (x / 2) else none + absorb _ a y := (a.1 + 1, a.2 + y) + finish _ a := a.2 + +/-- The number of leaves below `x`. -/ +def leaves (x : ℕ) : ℕ := if x < 2 then 1 else 2 * leaves (x / 2) +decreasing_by omega + +/-- The number of nodes below `x`. -/ +def nodes (x : ℕ) : ℕ := if x < 2 then 1 else 2 * nodes (x / 2) + 1 +decreasing_by omega + +/-- The number of open calls while evaluating `x`. -/ +def height (x : ℕ) : ℕ := if x < 2 then 0 else height (x / 2) + 1 +decreasing_by omega + +/-- No invariant. -/ +def none : Invariant ℕ (ℕ × ℕ) ℕ := ⟨fun _ => True, fun _ _ => True, fun _ => True⟩ + +-- The machine on `8`: four levels, eight leaves, fifteen nodes, so `2 * 15 - 1 = 29` steps. +example : halving.run (fun _ : Unit => 29) (fun _ => 8) () = some 8 := by decide + +-- One step fewer, the value `4` of the second child is still waiting to be absorbed by the root. +example : halving.run (fun _ : Unit => 28) (fun _ => 8) () = some 4 := by decide + +-- Extra fuel changes nothing: the final state is fixed. +example : halving.run (fun _ : Unit => 100) (fun _ => 8) () = some 8 := by decide + +/-- **Every node has a derivation**, with its leaves as value. -/ +theorem eval_halving (x : ℕ) : halving.Eval none x (leaves x) (nodes x) (height x) := by + induction x using Nat.strong_induction_on with + | _ x ih => + by_cases hx : x < 2 + · have hl : leaves x = 1 := by rw [leaves]; simp [hx] + have hn : nodes x = 1 := by rw [nodes]; simp [hx] + have hh : height x = 0 := by rw [height]; simp [hx] + rw [hl, hn, hh] + exact Scheme.Eval.leaf (R := halving) trivial (decide_eq_true hx) trivial + · have hl : leaves x = leaves (x / 2) + leaves (x / 2) := by rw [leaves]; simp [hx]; ring + have hn : nodes x = (nodes (x / 2) + (nodes (x / 2) + 0)) + 1 := by + rw [nodes]; simp [hx]; ring + have hh : height x = max (height (x / 2)) (max (height (x / 2)) 0) + 1 := by + rw [height]; simp [hx] + have hc := ih (x / 2) (by omega) + have hloop : halving.Loop none x (halving.start x) + (2, 0 + leaves (x / 2) + leaves (x / 2)) (nodes (x / 2) + (nodes (x / 2) + 0)) + (max (height (x / 2)) (max (height (x / 2)) 0)) := + Scheme.Loop.child trivial (by simp [halving]) hc + (Scheme.Loop.child trivial (by simp [halving]) hc (Scheme.Loop.done (by simp [halving]))) + have := Scheme.Eval.call (R := halving) (I := none) trivial (decide_eq_false hx) hloop + trivial + rw [hl, hn, hh] + simpa [halving] using this + +/-- `nodes x + 1 ≤ 2 max x 1`. -/ +theorem nodes_add_one_le (x : ℕ) : nodes x + 1 ≤ 2 * max x 1 := by + induction x using Nat.strong_induction_on with + | _ x ih => + by_cases hx : x < 2 + · rw [nodes]; simp only [hx, ite_true]; omega + · have := ih (x / 2) (by omega) + rw [nodes]; simp only [hx, ite_false] + omega + +/-- `2 * nodes x - 1 ≤ 4 * x + 1`: linear fuel suffices. -/ +theorem two_mul_nodes_le (x : ℕ) : 2 * nodes x - 1 ≤ 4 * x + 1 := by + have := nodes_add_one_le x + omega + +/-- With fuel `4 x + 1`, the machine returns the number of leaves, on every input. -/ +theorem run_halving (x : ℕ) : + halving.run (fun x => 4 * x + 1) id x = some (leaves x) := + Scheme.run_eq_some (eval_halving x) (two_mul_nodes_le x) + +/-- **The polynomial-time components** of the halving scheme, in binary. -/ +theorem halving_polyTime : halving.PolyTime encNat (encPair encNat encNat) encNat where + isLeaf := ComputableInPolyTime.binary_lt' ComputableInPolyTime.id' + (ComputableInPolyTime.const 2) + start := ComputableInPolyTime.const (0, 0) + next := by + have hk : ComputableInPolyTime (fun p : ℕ × (ℕ × ℕ) => p.2.1) + (encPair encNat (encPair encNat encNat)) encNat := + (ComputableInPolyTime.fst encNat encNat).comp (ComputableInPolyTime.snd _ _) + have hhalf : ComputableInPolyTime (fun p : ℕ × (ℕ × ℕ) => p.1 / 2) + (encPair encNat (encPair encNat encNat)) encNat := + (ComputableInPolyTime.binary_shiftRight' (ComputableInPolyTime.fst _ _) + (ComputableInPolyTime.const 1)).of_enc_eq fun p => by + rw [Nat.shiftRight_eq_div_pow, pow_one] + refine (ComputableInPolyTime.ite (ComputableInPolyTime.binary_lt' hk + (ComputableInPolyTime.const 2)) ((ComputableInPolyTime.optionSome encNat).comp hhalf) + (ComputableInPolyTime.const Option.none)).of_enc_eq fun p => ?_ + by_cases h : p.2.1 < 2 + · have h' : p.2.1 ≤ 1 := by omega + simp [halving, h, h'] + · have h' : ¬p.2.1 ≤ 1 := by omega + simp [halving, h, h'] + absorb := by + have hk : ComputableInPolyTime (fun p : (ℕ × (ℕ × ℕ)) × ℕ => p.1.2.1) + (encPair (encPair encNat (encPair encNat encNat)) encNat) encNat := + (ComputableInPolyTime.fst encNat encNat).comp + ((ComputableInPolyTime.snd encNat _).comp (ComputableInPolyTime.fst _ _)) + have hs : ComputableInPolyTime (fun p : (ℕ × (ℕ × ℕ)) × ℕ => p.1.2.2) + (encPair (encPair encNat (encPair encNat encNat)) encNat) encNat := + (ComputableInPolyTime.snd encNat encNat).comp + ((ComputableInPolyTime.snd encNat _).comp (ComputableInPolyTime.fst _ _)) + exact (ComputableInPolyTime.binary_add.comp (hk.prod (ComputableInPolyTime.const 1))).prod + (ComputableInPolyTime.binary_add.comp (hs.prod (ComputableInPolyTime.snd _ _))) + finish := (ComputableInPolyTime.snd encNat encNat).comp (ComputableInPolyTime.snd _ _) + +/-- The fuel `4 x + 1`, in binary. -/ +noncomputable def fuelCertificate : NativeCertificate (fun x : ℕ => 4 * x + 1) encNat encNat := + NativeCertificate.ofPolyTime (ComputableInPolyTime.binary_add.comp + ((ComputableInPolyTime.binary_mul' (ComputableInPolyTime.const 4) + ComputableInPolyTime.id').prod (ComputableInPolyTime.const 1))) + +/-- The root is the input. -/ +noncomputable def rootCertificate : NativeCertificate (id : ℕ → ℕ) encNat encNat := + NativeCertificate.ofPolyTime ComputableInPolyTime.id' + +/-- The leaf step: the constant `1`. -/ +def leafCertificate : NativeCertificate halving.leaf encNat encNat := NativeCertificate.const 1 + +/-- **One fixed machine computes the number of leaves** of every input. -/ +noncomputable def halvingCertificate : + NativeCertificate (halving.run (fun x => 4 * x + 1) id) encNat (encOption encNat) := + Scheme.certificate halving_polyTime leafCertificate fuelCertificate rootCertificate + +/-- The size invariant below a root `x₀`: nodes are at most `x₀`, frames have counted at most two +children and summed at most `x₀ + 1`, and values are at most `x₀ + 1`. -/ +def bounded (x₀ : ℕ) : Invariant ℕ (ℕ × ℕ) ℕ := + ⟨fun y => y ≤ x₀, fun y a => y ≤ x₀ ∧ a.1 ≤ 2 ∧ a.2 ≤ x₀ + 1, fun v => v ≤ x₀ + 1⟩ + +theorem leaves_le_max (x : ℕ) : leaves x ≤ max x 1 := by + induction x using Nat.strong_induction_on with + | _ x ih => + by_cases hx : x < 2 + · rw [leaves]; simp only [hx, ite_true]; omega + · have := ih (x / 2) (by omega) + rw [leaves]; simp only [hx, ite_false] + omega + +theorem leaves_le (x : ℕ) : leaves x ≤ x + 1 := by + have := leaves_le_max x + omega + +/-- **Every node below `x₀` has a derivation keeping the size invariant.** -/ +theorem eval_halving_bounded {x₀ x : ℕ} (hx₀ : x ≤ x₀) : + halving.Eval (bounded x₀) x (leaves x) (nodes x) (height x) := by + induction x using Nat.strong_induction_on with + | _ x ih => + have hlx := leaves_le x + by_cases hx : x < 2 + · have hl : leaves x = 1 := by rw [leaves]; simp [hx] + have hn : nodes x = 1 := by rw [nodes]; simp [hx] + have hh : height x = 0 := by rw [height]; simp [hx] + rw [hl, hn, hh] + exact Scheme.Eval.leaf (R := halving) hx₀ (decide_eq_true hx) + (show 1 ≤ x₀ + 1 by omega) + · have hl : leaves x = leaves (x / 2) + leaves (x / 2) := by rw [leaves]; simp [hx]; ring + have hn : nodes x = (nodes (x / 2) + (nodes (x / 2) + 0)) + 1 := by + rw [nodes]; simp [hx]; ring + have hh : height x = max (height (x / 2)) (max (height (x / 2)) 0) + 1 := by + rw [height]; simp [hx] + have hc := ih (x / 2) (by omega) (by omega) + have hhalf := leaves_le (x / 2) + have hloop : halving.Loop (bounded x₀) x (halving.start x) + (2, 0 + leaves (x / 2) + leaves (x / 2)) (nodes (x / 2) + (nodes (x / 2) + 0)) + (max (height (x / 2)) (max (height (x / 2)) 0)) := + Scheme.Loop.child (show x ≤ x₀ ∧ 0 ≤ 2 ∧ 0 ≤ x₀ + 1 by omega) (by simp [halving]) hc + (Scheme.Loop.child (show x ≤ x₀ ∧ 1 ≤ 2 ∧ 0 + leaves (x / 2) ≤ x₀ + 1 by omega) + (by simp [halving]) hc (Scheme.Loop.done (by simp [halving]))) + have := Scheme.Eval.call (R := halving) (I := bounded x₀) hx₀ (decide_eq_false hx) hloop + (show 0 + leaves (x / 2) + leaves (x / 2) ≤ x₀ + 1 by omega) + rw [hl, hn, hh] + simpa [halving] using this + +private theorem length_encNat_mono {y z : ℕ} (h : y ≤ z) : + (encNat y).length ≤ (encNat z).length := by + simpa [Nat.size_eq_bits_len] using Nat.size_le_size h + +/-- **The resource theorem applies**: with `ℓ` the length of `x + 1` in binary, nodes, frames and +values are at most `F = 3 ℓ + 6` long, and the leaf costs at most `F`, so the time is +`4 x + 2` times a polynomial in `(height x + 1) (F + 1)`, and the workspace is polynomial in it. -/ +theorem halvingCertificate_le : ∃ K : ℕ, ∀ x : ℕ, + halvingCertificate.time x ≤ fuelCertificate.time x + rootCertificate.time x + + 2 * (encNat x).length + (4 * x + 1 + 1) * + (K * ((height x + 1) * (3 * (encNat (x + 1)).length + 6 + 1)) ^ K + + (3 * (encNat (x + 1)).length + 6) + ((encNat (4 * x + 1)).length + 1) ^ 2) ∧ + halvingCertificate.space x ≤ fuelCertificate.space x + rootCertificate.space x + + 2 * (encNat x).length + + K * ((height x + 1) * (3 * (encNat (x + 1)).length + 6 + 1)) ^ K + + (3 * (encNat (x + 1)).length + 6) + (encNat (4 * x + 1)).length := by + obtain ⟨K, hK⟩ := Scheme.certificate_le halving_polyTime leafCertificate + refine ⟨K, fun x => ?_⟩ + have h2 : (encNat 2).length ≤ 2 := by decide + refine hK fuelCertificate rootCertificate (bounded x) (3 * (encNat (x + 1)).length + 6) _ _ + (fun y hy => ⟨?_, fun _ => ⟨?_, ?_⟩⟩) (fun y a ha => ?_) (fun v hv => ?_) x (leaves x) + (nodes x) (height x) (eval_halving_bounded le_rfl) + · have := length_encNat_mono (show y ≤ x + 1 by simp only [bounded] at hy; omega) + omega + · have := length_encNat_mono (show y ≤ x + 1 by simp only [bounded] at hy; omega) + simp only [leafCertificate, NativeCertificate.const_time] + omega + · have := length_encNat_mono (show y ≤ x + 1 by simp only [bounded] at hy; omega) + simp only [leafCertificate, NativeCertificate.const_space] + omega + · obtain ⟨hy, hk, hs⟩ := ha + have h1 := length_encNat_mono (show y ≤ x + 1 by omega) + have h3 := length_encNat_mono (show a.2 ≤ x + 1 by omega) + have h4 := (length_encNat_mono hk).trans h2 + simp only [length_encPair] + omega + · have := length_encNat_mono (show v ≤ x + 1 by simp only [bounded] at hv; omega) + omega + +/-! ### Node-count arithmetic -/ + +-- Binary branching for three levels: `1 + 2 (1 + 2 (1 + 2)) = 15` nodes. +example : Nat.recursionBound (fun _ => 2) 3 0 = 15 := rfl + +-- The product bound: `15 ≤ 4 * 2 ^ 3`. +example : Nat.recursionBound (fun _ => 2) 3 0 ≤ (3 + 1) * ∏ _j ∈ Finset.range 3, max 1 2 := + Nat.recursionBound_le _ 3 0 + +-- Halving excess exponents: `100 + 50 + 25 + 12 + 6 = 193 ≤ 200`. +example : ∑ j ∈ Finset.range 5, 100 / 2 ^ j ≤ 2 * 100 := Nat.sum_div_two_pow_le 100 5 + +end ComplexityTests.StackRecursion From 27d031198052460748576f5c64eee82e3c841af6 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 22:29:37 -0400 Subject: [PATCH 2/8] doc(GenericRAM/Native): qualify the module path in the stack recursion docstring Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity/Computability/GenericRAM/Native/StackRecursion.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Complexity/Computability/GenericRAM/Native/StackRecursion.lean b/Complexity/Computability/GenericRAM/Native/StackRecursion.lean index c2fd37dd11..fadf0610d0 100644 --- a/Complexity/Computability/GenericRAM/Native/StackRecursion.lean +++ b/Complexity/Computability/GenericRAM/Native/StackRecursion.lean @@ -41,7 +41,7 @@ within time `TL` and space `SL`, the time is at most `fuel a + 1` times the cost of computing the fuel and the root and of the binary clock, for one constant `K` of the scheme (`Scheme.certificate_le`). Only the stack is kept, so the workspace grows with the depth, not with the number of nodes. The number of nodes of a recursion tree is bounded in -`Foundations/Data/Nat/RecursionTree.lean`. +`Complexity/Foundations/Data/Nat/RecursionTree.lean`. This is the depth-first evaluation of the recursion in the proof of Theorem D.1 of [OpenAI2026ETH] (Appendix D.4.7, p. 64), which keeps one sum over mode tuples and one product From 70f4cd51d4fae5ef1cd772bdca7f609ed8894e77 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 22:34:00 -0400 Subject: [PATCH 3/8] feat(PolyTime/Nat): the clock 2^(K n / sqrt(floor(log2 n))) in polynomial time The fuel of the stack recursion on the scale of ContractionAlgorithm, computed in binary from n in unary. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Complexity/PolyTime/Nat/SqrtLog.lean | 53 +++++++++++++++++++ ComplexityTests/StackRecursion.lean | 14 +++++ 3 files changed, 68 insertions(+) create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/SqrtLog.lean diff --git a/Complexity.lean b/Complexity.lean index e3af2ca51c..c3020b1ba0 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1631,6 +1631,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Poly public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Prime public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Search public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Sqrt +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.SqrtLog public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Pi public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/SqrtLog.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/SqrtLog.lean new file mode 100644 index 0000000000..7b6a566ec2 --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/SqrtLog.lean @@ -0,0 +1,53 @@ +/- +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.Init +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Bits +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Unary +public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime +public import Mathlib.Data.Nat.Log +public import Mathlib.Data.Nat.Sqrt +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Div +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Log +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Sqrt +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeNatFrontends + +/-! +# The clock `2 ^ (K n / √⌊log₂ n⌋)` in polynomial time + +For a fixed `K`, the number `2 ^ (K n / √⌊log₂ n⌋)` (in the natural-number scale of +`Complexity/Foundations/Data/Nat/SqrtLog.lean`) is computable in binary in polynomial time from +`n` in unary. Its binary length is at most `K n + 1`. It serves as the fuel of clocked +subexponential algorithms, such as the depth-first recursion of the contraction theorem of +[OpenAI2026ETH] (Appendix D.4.7, p. 64), whose number of calls is `2 ^ O(n / √(log n))`. + +## Main results + +* `Turing.MultiTapeTM.ComputableInPolyTime.unary_two_pow_div_sqrt_log_two`: the clock. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM.ComputableInPolyTime + +/-- **The clock `2 ^ (K n / √⌊log₂ n⌋)`**, in binary from `n` in unary. -/ +theorem unary_two_pow_div_sqrt_log_two (K : ℕ) : + ComputableInPolyTime (fun n : ℕ => 2 ^ (K * n / Nat.sqrt (Nat.log 2 n))) encUnary encNat := by + have hb := unary_to_binary + have hlog : ComputableInPolyTime (fun n : ℕ => Nat.log 2 n) encUnary encUnary := + binary_log_two.comp hb + have hsq : ComputableInPolyTime (fun n : ℕ => Nat.sqrt (Nat.log 2 n)) encUnary encUnary := + binary_to_unary_bounded (binary_sqrt.comp (hb.comp hlog)) id' + (fun n => (Nat.sqrt_le_self _).trans (Nat.log_le_self 2 n)) + exact binary_two_pow.comp (unary_div.comp ((unary_mul' (const K) id').prod hsq)) + +end Turing.MultiTapeTM.ComputableInPolyTime diff --git a/ComplexityTests/StackRecursion.lean b/ComplexityTests/StackRecursion.lean index bcca97e434..34fbd89200 100644 --- a/ComplexityTests/StackRecursion.lean +++ b/ComplexityTests/StackRecursion.lean @@ -6,6 +6,7 @@ Authors: Samuel Schlesinger import Complexity.Computability.GenericRAM.Native.StackRecursion import Complexity.Foundations.Data.Nat.RecursionTree +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.SqrtLog import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryPrimitives import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeOptionPrimitives @@ -254,4 +255,17 @@ example : Nat.recursionBound (fun _ => 2) 3 0 ≤ (3 + 1) * ∏ _j ∈ Finset.ra -- Halving excess exponents: `100 + 50 + 25 + 12 + 6 = 193 ≤ 200`. example : ∑ j ∈ Finset.range 5, 100 / 2 ^ j ≤ 2 * 100 := Nat.sum_div_two_pow_le 100 5 +/-! ### The clock -/ + +-- The fuel `2 ^ (3 n / √⌊log₂ n⌋)` of a subexponential recursion, from `n` in unary. +example : ComputableInPolyTime (fun n : ℕ => 2 ^ (3 * n / Nat.sqrt (Nat.log 2 n))) encUnary + encNat := + ComputableInPolyTime.unary_two_pow_div_sqrt_log_two 3 + +-- At `n = 16`: `⌊log₂ 16⌋ = 4`, `√4 = 2`, so the clock is `2 ^ 24`. +example : 2 ^ (3 * 16 / Nat.sqrt (Nat.log 2 16)) = 2 ^ 24 := by + have h1 : Nat.log 2 16 = 4 := by rw [show (16 : ℕ) = 2 ^ 4 by rfl, Nat.log_pow one_lt_two] + have h2 : Nat.sqrt 4 = 2 := (Nat.eq_sqrt.2 ⟨by norm_num, by norm_num⟩).symm + rw [h1, h2] + end ComplexityTests.StackRecursion From bffa3cfe4e5d12e668c7cbd21458063402759c10 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 22:53:49 -0400 Subject: [PATCH 4/8] feat(foundations): count tuples of bounded weight by the partition generating function The number of tuples beta : iota -> N of total weight sum w_i beta_i < p, with at most m coordinates of each positive weight, is at most exp(theta p + m pi^2/(6 theta)) for every theta > 0, hence at most 2^(4 floor(sqrt(m p)) + 4). This is the mode count (D.15) of the Boolean tensor contraction theorem of [OpenAI2026ETH] (#1538). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Combinatorics/WeightBudget.lean | 245 ++++++++++++++++++ .../Combinatorics/WeightBudget.lean | 59 +++++ 3 files changed, 305 insertions(+) create mode 100644 Complexity/Foundations/Combinatorics/WeightBudget.lean create mode 100644 ComplexityTests/Foundations/Combinatorics/WeightBudget.lean diff --git a/Complexity.lean b/Complexity.lean index fdd3b220c6..68fc1497cf 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2594,6 +2594,7 @@ public import Complexity.Foundations.Combinatorics.Sunflower public import Complexity.Foundations.Combinatorics.Sunflower.LowerBound public import Complexity.Foundations.Combinatorics.Sunflower.Pluck public import Complexity.Foundations.Combinatorics.UniformSchedules +public import Complexity.Foundations.Combinatorics.WeightBudget public import Complexity.Foundations.Control.Monad.IsMonadHom.StateT public import Complexity.Foundations.Control.Monad.Memoize public import Complexity.Foundations.Data.BiTape diff --git a/Complexity/Foundations/Combinatorics/WeightBudget.lean b/Complexity/Foundations/Combinatorics/WeightBudget.lean new file mode 100644 index 0000000000..7d742fb6f2 --- /dev/null +++ b/Complexity/Foundations/Combinatorics/WeightBudget.lean @@ -0,0 +1,245 @@ +/- +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.Init +public import Mathlib.Analysis.SpecialFunctions.Log.Basic +public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic +import Mathlib.Algebra.BigOperators.Ring.Finset +import Mathlib.Analysis.Complex.ExponentialBounds +import Mathlib.Analysis.Real.Pi.Bounds +import Mathlib.Analysis.SpecialFunctions.Log.Deriv +import Mathlib.Analysis.SpecialFunctions.Pow.Real +import Mathlib.Analysis.SpecificLimits.Basic +import Mathlib.Data.Fintype.Pi +import Mathlib.NumberTheory.ZetaValues +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity + +/-! +# Counting tuples of bounded weight + +Give each coordinate `i` of a tuple `β : ι → ℕ` a positive weight `w i`, with at most `m` +coordinates of each weight. This file bounds the number of tuples of total weight +`∑ i, w i * β i < p` by the partition generating function: + +* for every `θ > 0` there are at most `exp (θ p + m π² / (6 θ))` of them + (`Cslib.card_le_exp_of_sum_mul_lt`); +* taking `θ = √(m / p)`, there are at most `2 ^ (4 ⌊√(m p)⌋ + 4)` + (`Cslib.card_le_two_pow_of_sum_mul_lt`). + +This is the count (D.15) of the exponent tuples of the modes in the proof of the Boolean tensor +contraction theorem of [OpenAI2026ETH] (§D.4.5, pp. 62–63), where the modes play the coordinates +and their weights are their divisibility exponents. + +**The proof.** Put `x = e^{-θ}`. Every tuple of weight below `p` has `x ^ (weight) ≥ x ^ p`, and the +sum of `x ^ (weight)` over all tuples is at most the generating product `∏ i, (1 - x ^ w i)⁻¹`. +Its logarithm is `∑ i, -log (1 - x ^ w i)`, which is at most `m` times the sum of +`-log (1 - e^{-θ j})` over the distinct weights `j`. Expanding the logarithm and summing the +geometric series bounds that sum (`Cslib.sum_neg_log_one_sub_exp_le`): + + `∑_{j ≥ 1} -log (1 - e^{-θ j}) = ∑_{h ≥ 1} 1 / (h (e^{θ h} - 1)) ≤ (1 / θ) ∑_{h ≥ 1} 1 / h² + = π² / (6 θ)`, + +using `e^y - 1 ≥ y` and `∑ 1 / h² = π² / 6` (`hasSum_zeta_two`). + +## Main results + +* `Cslib.sum_neg_log_one_sub_exp_le`: `∑_{j ∈ s} -log (1 - e^{-θ j}) ≤ π² / (6 θ)` for a finite + set `s` of positive integers. +* `Cslib.card_le_exp_of_sum_mul_lt`: the generating-function bound on the number of tuples. +* `Cslib.card_le_two_pow_of_sum_mul_lt`: its natural-number form `2 ^ (4 ⌊√(m p)⌋ + 4)`. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.5, the count (D.15) + and the estimate following it (pp. 62–63). +-/ + +public section + +namespace Cslib + +open Finset Real + +/-- **The logarithm of the partition generating function.** For `θ > 0` and every finite set +`s` of positive integers, `∑_{j ∈ s} -log (1 - e^{-θ j}) ≤ π² / (6 θ)`. -/ +theorem sum_neg_log_one_sub_exp_le {θ : ℝ} (hθ : 0 < θ) (s : Finset ℕ) (hs : 0 ∉ s) : + ∑ j ∈ s, -log (1 - exp (-(θ * j))) ≤ π ^ 2 / (6 * θ) := by + have hterm : ∀ j ∈ s, HasSum (fun h : ℕ => exp (-(θ * j)) ^ (h + 1) / (h + 1)) + (-log (1 - exp (-(θ * j)))) := by + intro j hj + have hj0 : (0 : ℝ) < j := Nat.cast_pos.2 (Nat.pos_of_ne_zero fun h => hs (h ▸ hj)) + apply Real.hasSum_pow_div_log_of_abs_lt_one + rw [abs_of_pos (exp_pos _), exp_lt_one_iff] + have := mul_pos hθ hj0 + linarith + have hzeta : HasSum (fun h : ℕ => 1 / θ * (1 / ((h : ℝ) + 1) ^ 2)) (1 / θ * (π ^ 2 / 6)) := by + have h := (hasSum_nat_add_iff' 1).mpr hasSum_zeta_two + simp only [range_one, sum_singleton, Nat.cast_zero, ne_eq, OfNat.ofNat_ne_zero, + not_false_eq_true, zero_pow, div_zero, sub_zero, Nat.cast_add, Nat.cast_one] at h + exact h.mul_left _ + have hle := hasSum_le (fun h => ?_) (hasSum_sum hterm) hzeta + · calc _ ≤ 1 / θ * (π ^ 2 / 6) := hle + _ = π ^ 2 / (6 * θ) := by field_simp + -- For fixed `h`, the terms form a geometric series in `q = e^{-θ (h + 1)}`. + set y : ℝ := θ * (h + 1) with hy + have hy0 : 0 < y := by positivity + set q : ℝ := exp (-y) with hq + have hq0 : 0 ≤ q := (exp_pos _).le + have hq1 : q < 1 := exp_lt_one_iff.2 (neg_lt_zero.2 hy0) + have hpow : ∀ j : ℕ, exp (-(θ * j)) ^ (h + 1) = q ^ j := fun j => by + rw [hq, ← exp_nat_mul, ← exp_nat_mul, hy] + push_cast + ring_nf + have hgeo : ∑ j ∈ s, q ^ j ≤ (1 - q)⁻¹ - 1 := by + have := sum_le_hasSum (insert 0 s) (fun j _ => pow_nonneg hq0 j) + (hasSum_geometric_of_lt_one hq0 hq1) + rw [sum_insert hs, pow_zero] at this + linarith + have hkey : q * (1 + y) ≤ 1 := by + calc q * (1 + y) ≤ q * exp y := mul_le_mul_of_nonneg_left (by linarith [add_one_le_exp y]) hq0 + _ = 1 := by rw [hq, ← exp_add, neg_add_cancel, exp_zero] + have hq' : (1 - q)⁻¹ - 1 ≤ 1 / y := by + have h1q : 0 < 1 - q := by linarith + rw [show (1 - q)⁻¹ - 1 = q / (1 - q) by field_simp; ring, div_le_div_iff₀ h1q hy0] + linarith + have hh : (0 : ℝ) < h + 1 := by positivity + calc ∑ j ∈ s, exp (-(θ * j)) ^ (h + 1) / (h + 1) = (∑ j ∈ s, q ^ j) / (h + 1) := by + rw [sum_div] + exact sum_congr rfl fun j _ => by rw [hpow] + _ ≤ (1 / y) / (h + 1) := div_le_div_of_nonneg_right (hgeo.trans hq') hh.le + _ = 1 / θ * (1 / ((h : ℝ) + 1) ^ 2) := by rw [hy]; field_simp + +/-- **Counting tuples of bounded weight by the generating function.** Let every coordinate have a +positive weight, with at most `m` coordinates of each weight. Then for every `θ > 0` there are at +most `exp (θ p + m π² / (6 θ))` tuples of total weight below `p`. -/ +theorem card_le_exp_of_sum_mul_lt {ι : Type*} [Fintype ι] {w : ι → ℕ} (hw : ∀ i, 0 < w i) + {m : ℕ} (hm : ∀ j, #{i | w i = j} ≤ m) {p : ℕ} {S : Finset (ι → ℕ)} + (hS : ∀ β ∈ S, ∑ i, w i * β i < p) {θ : ℝ} (hθ : 0 < θ) : + (#S : ℝ) ≤ exp (θ * p + m * (π ^ 2 / (6 * θ))) := by + classical + set x : ℝ := exp (-θ) with hx + have hx0 : 0 < x := exp_pos _ + have hx1 : x < 1 := exp_lt_one_iff.2 (neg_lt_zero.2 hθ) + -- Every tuple contributes at least `x ^ p` to the generating sum. + have h1 : (#S : ℝ) * x ^ p ≤ ∑ β ∈ S, x ^ (∑ i, w i * β i) := by + calc (#S : ℝ) * x ^ p = ∑ _β ∈ S, x ^ p := by rw [sum_const, nsmul_eq_mul] + _ ≤ _ := sum_le_sum fun β hβ => pow_le_pow_of_le_one hx0.le hx1.le (hS β hβ).le + -- The tuples lie in a box, over which the generating sum factors. + have hsub : S ⊆ Fintype.piFinset fun _ => range p := by + intro β hβ + rw [Fintype.mem_piFinset] + intro i + rw [mem_range] + calc β i ≤ w i * β i := Nat.le_mul_of_pos_left _ (hw i) + _ ≤ ∑ i, w i * β i := single_le_sum (fun i _ => Nat.zero_le (w i * β i)) (mem_univ i) + _ < p := hS β hβ + have h2 : ∑ β ∈ S, x ^ (∑ i, w i * β i) ≤ ∏ i, ∑ b ∈ range p, (x ^ w i) ^ b := by + rw [prod_univ_sum] + calc ∑ β ∈ S, x ^ (∑ i, w i * β i) = ∑ β ∈ S, ∏ i, (x ^ w i) ^ β i := by + refine sum_congr rfl fun β _ => ?_ + rw [← prod_pow_eq_pow_sum] + exact prod_congr rfl fun i _ => pow_mul x (w i) (β i) + _ ≤ ∑ β ∈ Fintype.piFinset fun _ => range p, ∏ i, (x ^ w i) ^ β i := + sum_le_sum_of_subset_of_nonneg hsub fun _ _ _ => prod_nonneg fun _ _ => by positivity + -- Each factor is a truncated geometric series. + have h3 : ∏ i, ∑ b ∈ range p, (x ^ w i) ^ b ≤ exp (∑ i, -log (1 - x ^ w i)) := by + rw [exp_sum] + refine prod_le_prod₀ (fun i _ => sum_nonneg fun _ _ => by positivity) fun i _ => ?_ + have hy0 : 0 ≤ x ^ w i := by positivity + have hy1 : x ^ w i < 1 := pow_lt_one₀ hx0.le hx1 (hw i).ne' + rw [exp_neg, exp_log (by linarith)] + exact sum_le_hasSum _ (fun _ _ => by positivity) (hasSum_geometric_of_lt_one hy0 hy1) + -- Group the coordinates by weight. + have h4 : ∑ i, -log (1 - x ^ w i) ≤ m * (π ^ 2 / (6 * θ)) := by + have hxj : ∀ j : ℕ, x ^ j = exp (-(θ * j)) := fun j => by + rw [hx, ← exp_nat_mul] + ring_nf + have hnn : ∀ j ∈ univ.image w, 0 ≤ -log (1 - x ^ j) := by + intro j hj + obtain ⟨i, -, rfl⟩ := mem_image.1 hj + have : 0 < 1 - x ^ w i := by linarith [pow_lt_one₀ hx0.le hx1 (hw i).ne'] + have : 1 - x ^ w i ≤ 1 := by linarith [pow_pos hx0 (w i)] + linarith [log_nonpos (by linarith) this] + have h0 : 0 ∉ univ.image w := by + simp only [mem_image, mem_univ, true_and, not_exists] + exact fun i h => (hw i).ne' h + rw [sum_comp (fun j => -log (1 - x ^ j)) w] + calc ∑ j ∈ univ.image w, #{i ∈ univ | w i = j} • -log (1 - x ^ j) + ≤ ∑ j ∈ univ.image w, m • -log (1 - x ^ j) := + sum_le_sum fun j hj => nsmul_le_nsmul_left (hnn j hj) (hm j) + _ = m * ∑ j ∈ univ.image w, -log (1 - exp (-(θ * j))) := by + rw [← smul_sum, nsmul_eq_mul] + simp only [hxj] + _ ≤ m * (π ^ 2 / (6 * θ)) := + mul_le_mul_of_nonneg_left (sum_neg_log_one_sub_exp_le hθ _ h0) (Nat.cast_nonneg m) + have hxp : x ^ p * exp (θ * p) = 1 := by + rw [hx, ← exp_nat_mul, ← exp_add] + ring_nf + exact exp_zero + calc (#S : ℝ) = #S * x ^ p * exp (θ * p) := by rw [mul_assoc, hxp, mul_one] + _ ≤ exp (m * (π ^ 2 / (6 * θ))) * exp (θ * p) := + mul_le_mul_of_nonneg_right ((h1.trans h2).trans (h3.trans (exp_le_exp.2 h4))) + (exp_pos _).le + _ = exp (θ * p + m * (π ^ 2 / (6 * θ))) := by rw [← exp_add, add_comm] + +/-- `1 + π² / 6 ≤ 4 log 2`, so `exp ((1 + π² / 6) y) ≤ 16 ^ y`. -/ +private theorem one_add_pi_sq_div_six_le : 1 + π ^ 2 / 6 ≤ 4 * log 2 := by + nlinarith [pi_lt_d2, pi_pos, log_two_gt_d9] + +/-- **Counting tuples of bounded weight, natural-number form.** Let every coordinate have a +positive weight, with at most `m` coordinates of each weight. Then there are at most +`2 ^ (4 ⌊√(m p)⌋ + 4)` tuples of total weight below `p`: the generating-function bound at +`θ = √(m / p)`. -/ +theorem card_le_two_pow_of_sum_mul_lt {ι : Type*} [Fintype ι] {w : ι → ℕ} (hw : ∀ i, 0 < w i) + {m : ℕ} (hm : ∀ j, #{i | w i = j} ≤ m) {p : ℕ} {S : Finset (ι → ℕ)} + (hS : ∀ β ∈ S, ∑ i, w i * β i < p) : #S ≤ 2 ^ (4 * Nat.sqrt (m * p) + 4) := by + classical + rcases Nat.eq_zero_or_pos p with rfl | hp + · have : S = ∅ := eq_empty_of_forall_notMem fun β hβ => Nat.not_lt_zero _ (hS β hβ) + simp [this] + rcases Nat.eq_zero_or_pos m with rfl | hm0 + · have : IsEmpty ι := ⟨fun i => by + have hpos : 0 < #{i' | w i' = w i} := card_pos.2 ⟨i, by simp⟩ + have := hm (w i) + omega⟩ + exact (card_le_one_of_subsingleton S).trans Nat.one_le_two_pow + set n := Nat.sqrt (m * p) + set a : ℝ := √(m : ℝ) with ha + set b : ℝ := √(p : ℝ) with hb + have ha0 : 0 < a := Real.sqrt_pos.2 (Nat.cast_pos.2 hm0) + have hb0 : 0 < b := Real.sqrt_pos.2 (Nat.cast_pos.2 hp) + have ha2 : (m : ℝ) = a ^ 2 := (Real.sq_sqrt (Nat.cast_nonneg m)).symm + have hb2 : (p : ℝ) = b ^ 2 := (Real.sq_sqrt (Nat.cast_nonneg p)).symm + have hexp : a / b * p + m * (π ^ 2 / (6 * (a / b))) = a * b * (1 + π ^ 2 / 6) := by + rw [ha2, hb2] + field_simp + have hab : a * b ≤ n + 1 := by + have hlt : ((m * p : ℕ) : ℝ) < ((n + 1 : ℕ) : ℝ) ^ 2 := by + exact_mod_cast Nat.lt_succ_sqrt' (m * p) + have hsq : (a * b) ^ 2 < ((n : ℝ) + 1) ^ 2 := by + rw [mul_pow, ← ha2, ← hb2] + push_cast at hlt + exact hlt + exact (lt_of_pow_lt_pow_left₀ 2 (by positivity) hsq).le + have hreal : (#S : ℝ) ≤ 2 ^ (4 * n + 4) := by + calc (#S : ℝ) ≤ exp (a / b * p + m * (π ^ 2 / (6 * (a / b)))) := + card_le_exp_of_sum_mul_lt hw hm hS (div_pos ha0 hb0) + _ = exp (a * b * (1 + π ^ 2 / 6)) := by rw [hexp] + _ ≤ exp (((4 * n + 4 : ℕ) : ℝ) * log 2) := by + refine exp_le_exp.2 ?_ + have h1 : (0 : ℝ) ≤ 1 + π ^ 2 / 6 := by positivity + calc a * b * (1 + π ^ 2 / 6) ≤ (n + 1) * (4 * log 2) := + mul_le_mul hab one_add_pi_sq_div_six_le h1 (by positivity) + _ = ((4 * n + 4 : ℕ) : ℝ) * log 2 := by push_cast; ring + _ = 2 ^ (4 * n + 4) := by rw [exp_nat_mul, exp_log two_pos] + exact_mod_cast hreal + +end Cslib diff --git a/ComplexityTests/Foundations/Combinatorics/WeightBudget.lean b/ComplexityTests/Foundations/Combinatorics/WeightBudget.lean new file mode 100644 index 0000000000..294c9e7249 --- /dev/null +++ b/ComplexityTests/Foundations/Combinatorics/WeightBudget.lean @@ -0,0 +1,59 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ +module + +public import Complexity.Foundations.Combinatorics.WeightBudget + +public section + +open Finset Real + +namespace Cslib.Tests.WeightBudget + +/-! ### A concrete budget + +Two coordinates of weights `1` and `2` and budget `p = 5`: the tuples with `β₀ + 2 β₁ < 5` are +the five with `β₁ = 0`, the three with `β₁ = 1` and the one with `β₁ = 2`. -/ + +/-- The weights `1, 2`. -/ +def w (i : Fin 2) : ℕ := i.val + 1 + +/-- The tuples of weight below `5`. -/ +def budget : Finset (Fin 2 → ℕ) := + {β ∈ Fintype.piFinset fun _ => range 5 | ∑ i, w i * β i < 5} + +example : #budget = 9 := by decide + +/-- Each weight occurs once, so `m = 1`: the bound is `2 ^ (4 ⌊√5⌋ + 4) = 2 ^ 12`. -/ +example : #budget ≤ 2 ^ 12 := by + have h := card_le_two_pow_of_sum_mul_lt (w := w) (m := 1) (p := 5) (S := budget) + (fun i => Nat.succ_pos _) (fun j => by + rw [card_le_one] + intro a ha b hb + rw [mem_filter] at ha hb + exact Fin.ext (by simp only [w] at ha hb; omega)) + (fun β hβ => (mem_filter.1 hβ).2) + simpa [(Nat.eq_sqrt.2 ⟨by norm_num, by norm_num⟩ : 2 = Nat.sqrt 5).symm] using h + +/-- The real form at `θ = 1`. -/ +example : (#budget : ℝ) ≤ exp (5 + π ^ 2 / 6) := by + have h := card_le_exp_of_sum_mul_lt (w := w) (m := 1) (p := 5) (S := budget) + (fun i => Nat.succ_pos _) (fun j => by + rw [card_le_one] + intro a ha b hb + rw [mem_filter] at ha hb + exact Fin.ext (by simp only [w] at ha hb; omega)) + (fun β hβ => (mem_filter.1 hβ).2) one_pos + simpa using h + +/-! ### The logarithmic sum -/ + +example : -log (1 - exp (-(1 * ((1 : ℕ) : ℝ)))) + -log (1 - exp (-(1 * ((2 : ℕ) : ℝ)))) ≤ + π ^ 2 / (6 * 1) := by + have h := sum_neg_log_one_sub_exp_le one_pos {1, 2} (by decide) + rwa [sum_pair (by decide)] at h + +end Cslib.Tests.WeightBudget From bafb62e4272d58d0e9795ad624a3a42a8cc6f085 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 23:00:47 -0400 Subject: [PATCH 5/8] feat(circuit/frontier): parameter schedule of the contraction recursion, (D.11) and (D.15) The schedule (D.4)-(D.6) of the Boolean tensor contraction recursion of [OpenAI2026ETH] on the floor-log / Nat.sqrt scale of #1865, with the certificate exists_activeBounds: for large s every active call satisfies the packing conditions (D.6), the precision bound (D.11) p_t u <= 34 M D_t, polynomial precisions and depth <= log s - 2. The mode count (D.15) card_modeBudget_le bounds the mode tuples by 2^e_d, and the e_d sum to O(s / sqrt(log s)) (#1538). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Frontier/TensorNetwork/Schedule.lean | 724 ++++++++++++++++++ .../Frontier/TensorNetworkSchedule.lean | 90 +++ 3 files changed, 815 insertions(+) create mode 100644 Complexity/Computability/Circuit/Frontier/TensorNetwork/Schedule.lean create mode 100644 ComplexityTests/Computability/Circuit/Frontier/TensorNetworkSchedule.lean diff --git a/Complexity.lean b/Complexity.lean index 68fc1497cf..6c584d06fd 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -874,6 +874,7 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Constraint public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Deformation public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ModeExpansion +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Schedule public import Complexity.Computability.Circuit.Frontier.TwoSidedWitness public import Complexity.Computability.Circuit.Frontier.Unconditional public import Complexity.Computability.Circuit.Frontier.Witness diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Schedule.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Schedule.lean new file mode 100644 index 0000000000..6fa306e299 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Schedule.lean @@ -0,0 +1,724 @@ +/- +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.Circuit.Frontier.TensorNetwork.ModeExpansion +public import Complexity.Foundations.Data.Nat.SqrtLog +import Complexity.Foundations.Combinatorics.WeightBudget +import Complexity.Foundations.Data.Nat.Asymptotics +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Ring + +/-! +# The parameter schedule of the tensor contraction recursion + +This file fixes the parameters of the recursion in the proof of the Boolean tensor contraction +theorem (Theorem D.1) of [OpenAI2026ETH] (§D.4.2, (D.4)–(D.6), p. 58) and proves the inequalities +its running time rests on: the conditions of the packing lemma, the precision bound (D.11) +(p. 61) and the count (D.15) of the mode tuples (pp. 62–63). Correctness of the recursion does not +depend on these choices; they bound the number of its calls by `2 ^ O(s / √⌊log₂ s⌋)` (§D.4.7, +p. 64). + +**The schedule.** Fix the size `s` and write `λ = ⌊log₂ s⌋`. + +* A call with at most `H = ⌊s / ⌊√λ⌋⌋` edges is a leaf (`leafSize`). +* At depth `d` the taper is `u_d = ⌊λ / 2 ^ (17 + d)⌋` (`taper`), the manuscript's + `⌊ε λ / 2 ^ d⌋` with `ε = 1 / (128 · 1024) = 2 ^ (-17)`. +* Labels have `a_d = 2 ∑_{j ≤ d} u_j` coordinates (`slotBits`), packets `L = 2 ^ a_d` slots, and + there are `D_arr = 64 ^ (2 a_d)` pairs of labels (`r = 64`). +* The degree bound is `Δ = 2 ^ (⌊9 λ / 10⌋ + 2)` (`degreeBound`), a power of two that is at least + `s ^ (9/10)` (`pow_nine_le_degreeBound_pow_ten`) and at most `2 ^ 20 s ^ 9` in tenth power. +* The node `t` of valuation `i` is recovered from its children at precision + `p_t = p + 8 h 2 ^ (a - i) + 8 M (a + 1)` (`nodePrecision`), as in Lemma D.5, where + `D_t = L / 2 ^ i`. +* Precisions stay below `precisionBound C s d`, which starts at `C s` and grows by + `8 C s (4 · 2 ^ a_d + a_d + 1)` per level. + +**Active calls.** `Active C s d M p` says that a call at depth `d` has `M` edges, with +`16 ^ d M ≤ C s` and `H < M`, and precision `p ≤ precisionBound C s d`. The root is active when +it has more than `H` edges and edges and precision are at most `C s` (`Active.root`), and an +active call's children are active when they have more than `H` edges (`Active.child`): Lemma D.3 +gives them at most `M / 16` edges. + +**The certificate.** For every `C` there is `s₀` such that for all `s ≥ s₀` +(`exists_activeBounds`): + +* precisions up to depth `λ` are at most `s ^ 2`; +* every active call satisfies `ActiveBounds`: its depth is at most `λ - 2`; `1 ≤ u_d ≤ M`; the + conditions (D.6) of the packing lemma, `2 Δ D_arr² ≤ M`, `L D_arr ≤ M` and `2 L ≤ Δ`, in the form + `Cslib.PacketPacking.exists_packing` takes them; `M (2 L - 1) + 1 ≤ 2 ^ (4 λ)` interpolation + points; and, for each node `t` with `q_t > 0` and `h = ⌈3 M / u⌉`, the precision bound (D.11) + `p_t u_d ≤ 34 M D_t` together with `p_t ≤ precisionBound C s (d + 1)`. + +From (D.11), the mode count (D.15) gives at most `2 ^ e_d` mode tuples with +`e_d = 4 ⌊15360 C s / (⌊√λ⌋ 8 ^ d)⌋ + 4` (`card_modeBudget_le`, `branchExponent`), and the +exponents sum to `O(s / √⌊log₂ s⌋)` over the levels (`sum_branchExponent_le`). With the factor +`2 ^ (2 λ)` for the nodes, interpolation points and groups (`ActiveBounds.branching_le`), a call at +depth `d` has at most `2 ^ (2 λ + e_d)` children. These are the hypotheses of a recursion tree with +`2 ^ O(s / √⌊log₂ s⌋)` nodes. + +**Differences from the source.** We use `λ = ⌊log₂ s⌋` and `H = ⌊s / ⌊√λ⌋⌋`, the scale of the +consumer interface of #1833, where the manuscript has `⌈log₂ s⌉` and `⌈s / ⌊√λ⌋⌉`; we take +`Δ = 2 ^ (⌊9 λ / 10⌋ + 2)` instead of `⌈s ^ (9/10)⌉`; and we prove the weaker lower bound +`u_d ≥ ⌊√λ⌋ / (2 ^ 17 C)` instead of `u_d ≥ λ ^ (4/5)`, which suffices for (D.11). The manuscript's +precision bound `p ≤ s λ^{O(1)} 2 ^ (a_{d-1})` is `precisionBound_le`. + +## Main definitions + +* `leafSize`, `taper`, `prefixBits`, `slotBits`, `degreeBound`, `nodePrecision`, + `precisionBound`, `branchExponent`: the schedule. +* `Active`: an active call within the schedule. +* `ActiveBounds`: the inequalities that hold at an active call for large `s`. + +## Main results + +* `exists_activeBounds`: the parameter certificate. +* `card_modeBudget_le`: the mode count (D.15) at an active call. +* `sum_branchExponent_le`: the excess exponents sum to `O(s / √⌊log₂ s⌋)`. +* `precisionBound_le`: the precision bound `p ≤ C s 2 ^ (a_{d-1}) (1 + d (8 λ + 40))`. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.2 (D.4)–(D.6) + (p. 58), Lemma D.5 and (D.11) (pp. 60–61), (D.13)–(D.15) (pp. 62–63) and §D.4.7 (p. 64). +-/ + +public section + +namespace Cslib.Circuits.Frontier.ContractionSchedule + +open Finset Filter + +/-! ### The schedule -/ + +/-- The leaf size `H = ⌊s / ⌊√⌊log₂ s⌋⌋⌋`: calls with at most `H` edges are evaluated by direct +summation. -/ +@[expose] def leafSize (s : ℕ) : ℕ := s / Nat.sqrt (Nat.log 2 s) + +/-- The taper `u_d = ⌊⌊log₂ s⌋ / 2 ^ (17 + d)⌋` at depth `d`, the manuscript's `⌊ε λ / 2 ^ d⌋` +with `ε = 2 ^ (-17)`. -/ +@[expose] def taper (s d : ℕ) : ℕ := Nat.log 2 s / 2 ^ (17 + d) + +/-- `2 ∑_{j < d} u_j`, the manuscript's `a_{d - 1}`. -/ +@[expose] def prefixBits (s d : ℕ) : ℕ := 2 * ∑ j ∈ range d, taper s j + +/-- The number `a_d = 2 ∑_{j ≤ d} u_j` of label coordinates at depth `d`: packets have `2 ^ a_d` +slots. -/ +@[expose] def slotBits (s d : ℕ) : ℕ := prefixBits s (d + 1) + +/-- The degree bound `Δ = 2 ^ (⌊9 ⌊log₂ s⌋ / 10⌋ + 2)`, a power of two at least `s ^ (9/10)`. -/ +@[expose] def degreeBound (s : ℕ) : ℕ := 2 ^ (9 * Nat.log 2 s / 10 + 2) + +/-- The precision `p_t = p + 8 h 2 ^ (a - i) + 8 M (a + 1)` at which a node `t` of valuation `i` +is recovered by Lemma D.5, for input precision `p`, `h = ⌈3 M / u⌉` and `2 ^ a` slots. -/ +@[expose] def nodePrecision (p h a M i : ℕ) : ℕ := p + 8 * h * 2 ^ (a - i) + 8 * M * (a + 1) + +/-- The precision schedule: `C s` at the root, growing by `8 C s (4 · 2 ^ a_d + a_d + 1)` from +depth `d` to `d + 1`. -/ +@[expose] def precisionBound (C s : ℕ) : ℕ → ℕ + | 0 => C * s + | d + 1 => precisionBound C s d + 8 * C * s * (4 * 2 ^ slotBits s d + slotBits s d + 1) + +/-- The excess exponent `e_d = 4 ⌊15360 C s / (⌊√⌊log₂ s⌋⌋ 8 ^ d)⌋ + 4` of the mode count at +depth `d`. -/ +@[expose] def branchExponent (C s d : ℕ) : ℕ := + 4 * (15360 * C * s / (Nat.sqrt (Nat.log 2 s) * 8 ^ d)) + 4 + +/-- An *active* call at depth `d` of the recursion for size `s` and constant `C`: it has `M` +edges, at most `C s / 16 ^ d` and more than the leaf size, and precision `p` within the +schedule. -/ +structure Active (C s d M p : ℕ) : Prop where + /-- Each level divides the number of edges by at least `16`. -/ + edges_le : 16 ^ d * M ≤ C * s + /-- The call is not a leaf. -/ + leafSize_lt : leafSize s < M + /-- The precision is within the schedule. -/ + precision_le : p ≤ precisionBound C s d + +/-- The root is active when it is not a leaf and its edges and precision are at most `C s`. -/ +theorem Active.root {C s M p : ℕ} (hM : M ≤ C * s) (hH : leafSize s < M) (hp : p ≤ C * s) : + Active C s 0 M p := + ⟨by simpa using hM, hH, hp⟩ + +/-- A child of an active call at depth `d` with at most a sixteenth of its edges, precision +within the schedule and more than the leaf size is an active call at depth `d + 1`. -/ +theorem Active.child {C s d M p M' p' : ℕ} (h : Active C s d M p) (hM : 16 * M' ≤ M) + (hH : leafSize s < M') (hp : p' ≤ precisionBound C s (d + 1)) : Active C s (d + 1) M' p' := + ⟨by rw [pow_succ, mul_assoc]; exact (Nat.mul_le_mul_left _ hM).trans h.edges_le, hH, hp⟩ + +/-! ### Arithmetic of the schedule -/ + +theorem slotBits_eq (s d : ℕ) : slotBits s d = prefixBits s d + 2 * taper s d := by + simp only [slotBits, prefixBits, sum_range_succ, mul_add] + +theorem prefixBits_le_slotBits (s d : ℕ) : prefixBits s d ≤ slotBits s d := by + rw [slotBits_eq] + exact Nat.le_add_right _ _ + +/-- `∑_{j < d} ⌊y / 2 ^ (j + 1)⌋ ≤ y`. -/ +private theorem sum_div_two_pow_succ_le (y d : ℕ) : ∑ j ∈ range d, y / 2 ^ (j + 1) ≤ y := by + induction d generalizing y with + | zero => simp + | succ d ih => + rw [sum_range_succ'] + have h : ∑ j ∈ range d, y / 2 ^ (j + 1 + 1) = ∑ j ∈ range d, y / 2 / 2 ^ (j + 1) := + sum_congr rfl fun j _ => by rw [Nat.div_div_eq_div_mul, ← pow_succ'] + rw [h] + have := ih (y / 2) + simp only [zero_add, pow_one] + omega + +/-- **`a ≤ 4 ε λ`**: `2 ∑_{j < d} u_j ≤ ⌊λ / 2 ^ 15⌋`. -/ +theorem prefixBits_le (s d : ℕ) : prefixBits s d ≤ Nat.log 2 s / 32768 := by + have h : ∑ j ∈ range d, taper s j ≤ Nat.log 2 s / 65536 := by + have : ∀ j, taper s j = Nat.log 2 s / 65536 / 2 ^ (j + 1) := fun j => by + rw [taper, Nat.div_div_eq_div_mul, show 17 + j = 16 + (j + 1) by omega, pow_add] + rfl + simp only [this] + exact sum_div_two_pow_succ_le _ d + unfold prefixBits + omega + +theorem slotBits_le (s d : ℕ) : slotBits s d ≤ Nat.log 2 s / 32768 := + prefixBits_le s (d + 1) + +/-- **The degree bound is at least `s ^ (9/10)`**: `s ^ 9 ≤ Δ ^ 10`. -/ +theorem pow_nine_le_degreeBound_pow_ten (s : ℕ) : s ^ 9 ≤ degreeBound s ^ 10 := by + have hs : s < 2 ^ (Nat.log 2 s + 1) := Nat.lt_pow_succ_log_self one_lt_two s + calc s ^ 9 ≤ (2 ^ (Nat.log 2 s + 1)) ^ 9 := Nat.pow_le_pow_left hs.le 9 + _ = 2 ^ (9 * Nat.log 2 s + 9) := by rw [← pow_mul]; ring_nf + _ ≤ 2 ^ (10 * (9 * Nat.log 2 s / 10 + 2)) := Nat.pow_le_pow_right two_pos (by omega) + _ = degreeBound s ^ 10 := by rw [degreeBound, ← pow_mul, mul_comm] + +/-- A degree `x` with `x ^ 10 ≤ s ^ 9` is at most the degree bound. -/ +theorem le_degreeBound_of_pow_ten_le {x s : ℕ} (h : x ^ 10 ≤ s ^ 9) : x ≤ degreeBound s := + (Nat.pow_le_pow_iff_left (by norm_num)).1 (h.trans (pow_nine_le_degreeBound_pow_ten s)) + +/-- **The degree bound is at most `2 ^ 2 s ^ (9/10)`**: `Δ ^ 10 ≤ 2 ^ 20 s ^ 9`. -/ +theorem degreeBound_pow_ten_le {s : ℕ} (hs : s ≠ 0) : degreeBound s ^ 10 ≤ 2 ^ 20 * s ^ 9 := by + have h2 : 2 ^ Nat.log 2 s ≤ s := Nat.pow_log_le_self 2 hs + calc degreeBound s ^ 10 = 2 ^ (10 * (9 * Nat.log 2 s / 10) + 20) := by + rw [degreeBound, ← pow_mul]; ring_nf + _ ≤ 2 ^ (9 * Nat.log 2 s + 20) := Nat.pow_le_pow_right two_pos (by omega) + _ = 2 ^ 20 * (2 ^ Nat.log 2 s) ^ 9 := by rw [← pow_mul, ← pow_add]; ring_nf + _ ≤ 2 ^ 20 * s ^ 9 := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left h2 9) + +/-- **The precision bound** of (D.11), `p ≤ s λ^{O(1)} 2 ^ (a_{d - 1})`: +`precisionBound C s d ≤ C s 2 ^ (a_{d - 1}) (1 + d (8 λ + 40))`. -/ +theorem precisionBound_le (C s d : ℕ) : + precisionBound C s d ≤ C * s * 2 ^ prefixBits s d * (1 + d * (8 * Nat.log 2 s + 40)) := by + induction d with + | zero => simp [precisionBound, prefixBits] + | succ d ih => + set n := Nat.log 2 s + set a := slotBits s d + have ha : a ≤ n := (slotBits_le s d).trans (Nat.div_le_self _ _) + have hpow : 2 ^ prefixBits s d ≤ 2 ^ a := + Nat.pow_le_pow_right two_pos (prefixBits_le_slotBits s d) + have h1 : 1 ≤ 2 ^ a := Nat.one_le_two_pow + have hstep : 8 * (4 * 2 ^ a + a + 1) ≤ 2 ^ a * (8 * n + 40) := by + have : a + 1 ≤ 2 ^ a * (n + 1) := by nlinarith + nlinarith + have hP : precisionBound C s d ≤ C * s * 2 ^ a * (1 + d * (8 * n + 40)) := + ih.trans (Nat.mul_le_mul_right _ (Nat.mul_le_mul_left _ hpow)) + calc precisionBound C s (d + 1) + = precisionBound C s d + C * s * (8 * (4 * 2 ^ a + a + 1)) := by + rw [precisionBound]; ring + _ ≤ C * s * 2 ^ a * (1 + d * (8 * n + 40)) + C * s * (2 ^ a * (8 * n + 40)) := + Nat.add_le_add hP (Nat.mul_le_mul_left _ hstep) + _ = C * s * 2 ^ prefixBits s (d + 1) * (1 + (d + 1) * (8 * n + 40)) := by + rw [show prefixBits s (d + 1) = a from rfl]; ring + +/-! ### Active calls -/ + +section Active + +variable {C s d M p : ℕ} + +theorem Active.one_le_edges (h : Active C s d M p) : 1 ≤ M := + Nat.one_le_iff_ne_zero.2 fun h0 => by have := h.leafSize_lt; omega + +theorem Active.edges_le_mul (h : Active C s d M p) : M ≤ C * s := + (Nat.le_mul_of_pos_left M (Nat.pow_pos (by norm_num))).trans h.edges_le + +theorem Active.one_le_const (h : Active C s d M p) : 1 ≤ C := by + have := h.one_le_edges.trans h.edges_le_mul + rcases Nat.eq_zero_or_pos C with rfl | hC + · simp at this + · exact hC + +/-- At an active call `s < M ⌊√λ⌋`, since `⌊s / ⌊√λ⌋⌋ < M`. -/ +theorem Active.lt_mul_sqrt (h : Active C s d M p) (hs : 2 ≤ s) : + s < M * Nat.sqrt (Nat.log 2 s) := + (Nat.div_lt_iff_lt_mul (Nat.one_le_sqrt_log_two hs)).1 h.leafSize_lt + +/-- **The depth bound**: `16 ^ d < C ⌊√λ⌋` at an active call. -/ +theorem Active.sixteen_pow_lt (h : Active C s d M p) (hs : 2 ≤ s) : + 16 ^ d < C * Nat.sqrt (Nat.log 2 s) := by + have h1 := h.lt_mul_sqrt hs + have h2 : 16 ^ d * s < C * Nat.sqrt (Nat.log 2 s) * s := + calc 16 ^ d * s < 16 ^ d * (M * Nat.sqrt (Nat.log 2 s)) := + Nat.mul_lt_mul_of_pos_left h1 (Nat.pow_pos (by norm_num)) + _ = 16 ^ d * M * Nat.sqrt (Nat.log 2 s) := by ring + _ ≤ C * s * Nat.sqrt (Nat.log 2 s) := Nat.mul_le_mul_right _ h.edges_le + _ = C * Nat.sqrt (Nat.log 2 s) * s := by ring + exact Nat.lt_of_mul_lt_mul_right h2 + +/-- **The taper stays large**: `u_d ≥ ⌊√λ⌋ / (2 ^ 17 C)` at an active call. -/ +theorem Active.le_taper (h : Active C s d M p) (hs : 2 ≤ s) : + Nat.sqrt (Nat.log 2 s) / (2 ^ 17 * C) ≤ taper s d := by + set n := Nat.log 2 s + set σ := Nat.sqrt n + have hσ : 1 ≤ σ := Nat.one_le_sqrt_log_two hs + have hC := h.one_le_const + have h2d : 2 ^ d ≤ C * σ := + (Nat.pow_le_pow_left (by norm_num : 2 ≤ 16) d).trans (h.sixteen_pow_lt hs).le + calc σ / (2 ^ 17 * C) = σ * σ / (2 ^ 17 * C * σ) := (Nat.mul_div_mul_right _ _ hσ).symm + _ ≤ n / (2 ^ 17 * C * σ) := Nat.div_le_div_right (Nat.sqrt_le n) + _ ≤ n / (2 ^ 17 * 2 ^ d) := by + refine Nat.div_le_div_left ?_ (by positivity) + rw [mul_assoc] + exact Nat.mul_le_mul_left _ h2d + _ = taper s d := by rw [taper, pow_add] + +end Active + +/-- `⌊√λ⌋ ≤ 2 ^ (10 + d) ⌊√u_d⌋` once `u_d ≥ 1`: the taper loses at most a factor `2 ^ (17 + d)` +against `λ`. -/ +theorem sqrt_log_two_le_mul_sqrt_taper {s d : ℕ} (hu : 1 ≤ taper s d) : + Nat.sqrt (Nat.log 2 s) ≤ 2 ^ (10 + d) * Nat.sqrt (taper s d) := by + set n := Nat.log 2 s + set u := taper s d + set y := Nat.sqrt u + have hy : 1 ≤ y := Nat.sqrt_pos.2 hu + have hn : n < (u + 1) * 2 ^ (17 + d) := by + have := Nat.lt_div_mul_add (a := n) (b := 2 ^ (17 + d)) (by positivity) + simpa only [u, taper, add_mul, one_mul] using this + have hu1 : u + 1 ≤ 4 * y ^ 2 := by + have := Nat.lt_succ_sqrt' u + nlinarith + have hsq : Nat.sqrt n ^ 2 < (2 ^ (10 + d) * y) ^ 2 := by + calc Nat.sqrt n ^ 2 ≤ n := Nat.sqrt_le' n + _ < (u + 1) * 2 ^ (17 + d) := hn + _ ≤ 4 * y ^ 2 * 2 ^ (17 + d) := Nat.mul_le_mul_right _ hu1 + _ = 2 ^ (19 + d) * y ^ 2 := by rw [show 19 + d = 2 + (17 + d) by omega, pow_add]; ring + _ ≤ 2 ^ (20 + 2 * d) * y ^ 2 := Nat.mul_le_mul_right _ (Nat.pow_le_pow_right two_pos + (by omega)) + _ = (2 ^ (10 + d) * y) ^ 2 := by rw [mul_pow, ← pow_mul]; ring_nf + exact ((Nat.pow_lt_pow_iff_left (by norm_num)).1 hsq).le + +/-! ### The certificate -/ + +/-- The inequalities that hold at an active call at depth `d` with `M` edges and precision `p`, for +`s` large enough. Write `u = taper s d`, `a = slotBits s d`, `L = 2 ^ a`, `Δ = degreeBound s` and +`λ = ⌊log₂ s⌋`. -/ +structure ActiveBounds (C s d M p : ℕ) : Prop where + /-- The call and its children lie in the first `λ` levels. -/ + depth_add_two_le : d + 2 ≤ Nat.log 2 s + /-- `1 ≤ u`, as Lemma D.5 requires. -/ + one_le_taper : 1 ≤ taper s d + /-- `u ≤ M`, as Lemma D.5 requires. -/ + taper_le_edges : taper s d ≤ M + /-- (D.6): `2 Δ D_arr² ≤ M`. -/ + degree_mul_pairs_sq_le : 2 * degreeBound s * (64 ^ (2 * slotBits s d)) ^ 2 ≤ M + /-- (D.6): `L D_arr ≤ M`. -/ + slots_mul_pairs_le : 2 ^ slotBits s d * 64 ^ (2 * slotBits s d) ≤ M + /-- (D.6): `2 L ≤ Δ`, so packet vertices respect the degree bound. -/ + two_mul_slots_le : 2 * 2 ^ slotBits s d ≤ degreeBound s + /-- There are `2 ^ (4 λ)` residue-field lifts for the `M (2 L - 1) + 1` interpolation points. -/ + points_le : M * (2 * 2 ^ slotBits s d - 1) + 1 ≤ 2 ^ (4 * Nat.log 2 s) + /-- The nodes, interpolation points and `64` groups contribute a factor `2 ^ (2 λ)` to the + branching. -/ + branching_le : + 2 * 2 ^ slotBits s d * (M * (2 * 2 ^ slotBits s d - 1) + 1) * 64 ≤ 2 ^ (2 * Nat.log 2 s) + /-- The children's precisions are within the schedule. -/ + nodePrecision_le : ∀ i h, i < taper s d → h * taper s d ≤ 3 * M + taper s d → + nodePrecision p h (slotBits s d) M i ≤ precisionBound C s (d + 1) + /-- **(D.11)**: `p_t u ≤ 34 M D_t`. -/ + nodePrecision_mul_taper_le : ∀ i h, i < taper s d → h * taper s d ≤ 3 * M + taper s d → + nodePrecision p h (slotBits s d) M i * taper s d ≤ 34 * M * 2 ^ (slotBits s d - i) + +/-! #### Arithmetic lemmas -/ + +private theorem one_add_mul_le_sq (n : ℕ) : 1 + n * (8 * n + 40) ≤ 49 * (n + 1) ^ 2 := by + nlinarith + +private theorem one_add_mul_le_sq' {n : ℕ} (hn : 1 ≤ n) : 1 + n * (8 * n + 40) ≤ 49 * n ^ 2 := by + nlinarith + +/-- The children's precisions are within the schedule. -/ +private theorem nodePrecision_le_of {p P h u M C s a i : ℕ} (hp : p ≤ P) + (hh : h * u ≤ 3 * M + u) (hu : 1 ≤ u) (huM : u ≤ M) (hM : M ≤ C * s) : + nodePrecision p h a M i ≤ P + 8 * C * s * (4 * 2 ^ a + a + 1) := by + have hh4 : h ≤ 4 * M := by + have : h ≤ h * u := Nat.le_mul_of_pos_right h hu + omega + have hDt : 2 ^ (a - i) ≤ 2 ^ a := Nat.pow_le_pow_right two_pos (Nat.sub_le a i) + calc nodePrecision p h a M i = p + 8 * h * 2 ^ (a - i) + 8 * M * (a + 1) := rfl + _ ≤ P + 8 * (4 * (C * s)) * 2 ^ a + 8 * (C * s) * (a + 1) := + Nat.add_le_add (Nat.add_le_add hp (Nat.mul_le_mul + (Nat.mul_le_mul_left 8 (hh4.trans (Nat.mul_le_mul_left 4 hM))) hDt)) + (Nat.mul_le_mul_right _ (Nat.mul_le_mul_left 8 hM)) + _ = P + 8 * C * s * (4 * 2 ^ a + a + 1) := by ring + +/-- The inherited precision is absorbed by the taper: `p u ≤ M 2 ^ (a_{d-1} + u)`. -/ +private theorem mul_taper_le_of {p C s A d n σ u M : ℕ} + (hp : p ≤ C * s * 2 ^ A * (1 + d * (8 * n + 40))) (hsM : s ≤ M * σ) (hσ : σ ≤ n) + (hd : d ≤ n) (hu : u ≤ n) (hn : 1 ≤ n) (hpow : 49 * C * n ^ 4 ≤ 2 ^ u) : + p * u ≤ M * 2 ^ (A + u) := by + have h0 : d * (8 * n + 40) ≤ n * (8 * n + 40) := Nat.mul_le_mul_right _ hd + have h1 : 1 + d * (8 * n + 40) ≤ 49 * n ^ 2 := (Nat.add_le_add_left h0 1).trans + (one_add_mul_le_sq' hn) + have h2 : σ * u ≤ n ^ 2 := by rw [sq]; exact Nat.mul_le_mul hσ hu + have hfac : C * σ * (1 + d * (8 * n + 40)) * u ≤ 49 * C * n ^ 4 := + calc C * σ * (1 + d * (8 * n + 40)) * u = C * (σ * u) * (1 + d * (8 * n + 40)) := by ring + _ ≤ C * n ^ 2 * (49 * n ^ 2) := Nat.mul_le_mul (Nat.mul_le_mul_left _ h2) h1 + _ = 49 * C * n ^ 4 := by ring + calc p * u ≤ C * s * 2 ^ A * (1 + d * (8 * n + 40)) * u := Nat.mul_le_mul_right _ hp + _ ≤ C * (M * σ) * 2 ^ A * (1 + d * (8 * n + 40)) * u := + Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ + (Nat.mul_le_mul_left C hsM))) + _ = M * 2 ^ A * (C * σ * (1 + d * (8 * n + 40)) * u) := by ring + _ ≤ M * 2 ^ A * 2 ^ u := Nat.mul_le_mul_left _ (hfac.trans hpow) + _ = M * 2 ^ (A + u) := by rw [mul_assoc, ← pow_add] + +/-- The evaluation loss is absorbed by the taper: `8 (a + 1) u ≤ 2 ^ u`. -/ +private theorem eight_mul_le_two_pow {a u n C : ℕ} (hC : 1 ≤ C) (hn : 1 ≤ n) (ha : a ≤ n) + (hu : u ≤ n) (hpow : 49 * C * n ^ 4 ≤ 2 ^ u) : 8 * (a + 1) * u ≤ 2 ^ u := by + have h1 : 8 * (a + 1) * u ≤ 16 * n ^ 2 := by + calc 8 * (a + 1) * u ≤ 8 * (n + n) * n := + Nat.mul_le_mul (Nat.mul_le_mul_left 8 (Nat.add_le_add ha hn)) hu + _ = 16 * n ^ 2 := by ring + have h2 : n ^ 2 ≤ n ^ 4 := Nat.pow_le_pow_right hn (by norm_num) + have h3 : 16 * n ^ 4 ≤ 49 * C * n ^ 4 := + Nat.mul_le_mul_right _ (by omega) + omega + +/-- **(D.11)** from its ingredients: `p_t u ≤ 34 M D_t`. -/ +private theorem nodePrecision_mul_le_of {p h a M i u A : ℕ} (hpu : p * u ≤ M * 2 ^ (A + u)) + (ha : a = A + 2 * u) (hi : i < u) (hh : h * u ≤ 3 * M + u) (huM : u ≤ M) + (h8 : 8 * (a + 1) * u ≤ 2 ^ u) : + nodePrecision p h a M i * u ≤ 34 * M * 2 ^ (a - i) := by + have hDt : 2 ^ (A + u) ≤ 2 ^ (a - i) := Nat.pow_le_pow_right two_pos (by omega) + have hu2 : 2 ^ u ≤ 2 ^ (a - i) := Nat.pow_le_pow_right two_pos (by omega) + have hhu : h * u ≤ 4 * M := by omega + calc nodePrecision p h a M i * u + = p * u + 8 * (h * u) * 2 ^ (a - i) + M * (8 * (a + 1) * u) := by + rw [nodePrecision]; ring + _ ≤ M * 2 ^ (a - i) + 8 * (4 * M) * 2 ^ (a - i) + M * 2 ^ (a - i) := + Nat.add_le_add (Nat.add_le_add (hpu.trans (Nat.mul_le_mul_left _ hDt)) + (Nat.mul_le_mul_right _ (Nat.mul_le_mul_left 8 hhu))) + (Nat.mul_le_mul_left _ (h8.trans hu2)) + _ = 34 * M * 2 ^ (a - i) := by ring + +/-- `64 ^ (2 a) = 2 ^ (12 a)`. -/ +private theorem sixtyFour_pow (a : ℕ) : 64 ^ (2 * a) = 2 ^ (12 * a) := by + rw [show (64 : ℕ) = 2 ^ 6 by norm_num, ← pow_mul]; ring_nf + +/-- A power of two is below `M` when it is below `s / 2 ^ (n / 20)`, since `s < M σ` and +`σ ≤ 2 ^ (n / 20)`. -/ +private theorem two_pow_lt_of {k n s M σ : ℕ} (hk : k + n / 20 ≤ n) (hσ : σ ≤ 2 ^ (n / 20)) + (h2n : 2 ^ n ≤ s) (hsM : s < M * σ) : 2 ^ k < M := by + have : 2 ^ k * σ < M * σ := + calc 2 ^ k * σ ≤ 2 ^ k * 2 ^ (n / 20) := Nat.mul_le_mul_left _ hσ + _ = 2 ^ (k + n / 20) := (pow_add _ _ _).symm + _ ≤ 2 ^ n := Nat.pow_le_pow_right two_pos hk + _ ≤ s := h2n + _ < M * σ := hsM + exact Nat.lt_of_mul_lt_mul_right this + +/-- The interpolation points: `M (2 L - 1) + 1 ≤ 2 ^ (n / 8 + n + a + 2)`. -/ +private theorem points_le_of {M a C s n : ℕ} (hM1 : 1 ≤ M) (hM : M ≤ C * s) + (hC : C ≤ 2 ^ (n / 8)) (hs : s < 2 ^ (n + 1)) : + M * (2 * 2 ^ a - 1) + 1 ≤ 2 ^ (n / 8 + n + a + 2) := by + have h1 : M * (2 * 2 ^ a - 1) + 1 ≤ M * (2 * 2 ^ a) := by + have h2a : 1 ≤ 2 * 2 ^ a := by have := Nat.one_le_two_pow (n := a); omega + rw [Nat.mul_sub, mul_one] + have : M ≤ M * (2 * 2 ^ a) := Nat.le_mul_of_pos_right M (by omega) + omega + calc M * (2 * 2 ^ a - 1) + 1 ≤ M * (2 * 2 ^ a) := h1 + _ ≤ C * s * (2 * 2 ^ a) := Nat.mul_le_mul_right _ hM + _ ≤ 2 ^ (n / 8) * 2 ^ (n + 1) * (2 * 2 ^ a) := + Nat.mul_le_mul_right _ (Nat.mul_le_mul hC hs.le) + _ = 2 ^ (n / 8 + n + a + 2) := by + rw [← pow_succ', ← pow_add, ← pow_add]; ring_nf + +/-- The asymptotic inequalities behind the certificate, in `n = ⌊log₂ s⌋`. -/ +private theorem eventually_large (C : ℕ) (hC : 1 ≤ C) : ∀ᶠ n : ℕ in atTop, + 200 ≤ n ∧ 49 * C * (Nat.sqrt n + 1) ^ 8 ≤ 2 ^ (Nat.sqrt n / (2 ^ 17 * C)) ∧ + C * (n + 1) ^ 1 ≤ 2 ^ (n / 8) ∧ 8 * (n + 1) ^ 1 ≤ 2 ^ (n / 20) ∧ + 49 * C * (n + 1) ^ 2 ≤ 2 ^ (n / 2) := by + have hsqrt : Tendsto Nat.sqrt atTop atTop := + tendsto_atTop_atTop.2 fun b => ⟨b * b, fun n hn => Nat.le_sqrt.2 hn⟩ + filter_upwards [eventually_ge_atTop 200, + hsqrt.eventually (Nat.eventually_mul_add_one_pow_le_pow_div (49 * C) 8 (2 ^ 17 * C) + one_lt_two (by positivity)), + Nat.eventually_mul_add_one_pow_le_pow_div C 1 8 one_lt_two (by norm_num), + Nat.eventually_mul_add_one_pow_le_pow_div 8 1 20 one_lt_two (by norm_num), + Nat.eventually_mul_add_one_pow_le_pow_div (49 * C) 2 2 one_lt_two (by norm_num)] + with n h1 h2 h3 h4 h5 + exact ⟨h1, h2, h3, h4, h5⟩ + +/-! #### The certificate -/ + +/-- Precisions up to depth `⌊log₂ s⌋` are at most `s ^ 2` once `49 C (λ + 1)² ≤ 2 ^ (λ / 2)`. -/ +private theorem precisionBound_le_sq_of {C s d : ℕ} (hd : d ≤ Nat.log 2 s) (hs : s ≠ 0) + (h : 49 * C * (Nat.log 2 s + 1) ^ 2 ≤ 2 ^ (Nat.log 2 s / 2)) : + precisionBound C s d ≤ s ^ 2 := by + set n := Nat.log 2 s + have h2n : 2 ^ n ≤ s := Nat.pow_log_le_self 2 hs + have hpow : 2 ^ prefixBits s d ≤ 2 ^ (n / 32768) := + Nat.pow_le_pow_right two_pos (prefixBits_le s d) + have hfac : C * (1 + d * (8 * n + 40)) ≤ 49 * C * (n + 1) ^ 2 := by + have h1 : d * (8 * n + 40) ≤ n * (8 * n + 40) := Nat.mul_le_mul_right _ hd + have h2 := one_add_mul_le_sq n + calc C * (1 + d * (8 * n + 40)) ≤ C * (49 * (n + 1) ^ 2) := + Nat.mul_le_mul_left _ (by omega) + _ = 49 * C * (n + 1) ^ 2 := by ring + calc precisionBound C s d ≤ C * s * 2 ^ prefixBits s d * (1 + d * (8 * n + 40)) := + precisionBound_le C s d + _ = s * (C * (1 + d * (8 * n + 40))) * 2 ^ prefixBits s d := by ring + _ ≤ s * 2 ^ (n / 2) * 2 ^ (n / 32768) := + Nat.mul_le_mul (Nat.mul_le_mul_left _ (hfac.trans h)) hpow + _ = s * 2 ^ (n / 2 + n / 32768) := by rw [mul_assoc, ← pow_add] + _ ≤ s * 2 ^ n := Nat.mul_le_mul_left _ (Nat.pow_le_pow_right two_pos (by omega)) + _ ≤ s * s := Nat.mul_le_mul_left _ h2n + _ = s ^ 2 := (sq s).symm + +/-- The certificate at one active call, from the asymptotic inequalities at `λ = ⌊log₂ s⌋`. -/ +private theorem activeBounds_of {C s d M p : ℕ} (hA : Active C s d M p) + (h200 : 200 ≤ Nat.log 2 s) + (hA1 : 49 * C * (Nat.sqrt (Nat.log 2 s) + 1) ^ 8 ≤ + 2 ^ (Nat.sqrt (Nat.log 2 s) / (2 ^ 17 * C))) + (hA2 : C * (Nat.log 2 s + 1) ≤ 2 ^ (Nat.log 2 s / 8)) + (hA3 : 8 * (Nat.log 2 s + 1) ≤ 2 ^ (Nat.log 2 s / 20)) : + ActiveBounds C s d M p := by + have hs0 : s ≠ 0 := by + rintro rfl + simp at h200 + have hC := hA.one_le_const + have hM1 := hA.one_le_edges + have hMCs := hA.edges_le_mul + have h2n : 2 ^ Nat.log 2 s ≤ s := Nat.pow_log_le_self 2 hs0 + have hsn : s < 2 ^ (Nat.log 2 s + 1) := Nat.lt_pow_succ_log_self one_lt_two s + have hs2 : 2 ≤ s := (Nat.pow_le_pow_right two_pos (by omega : 1 ≤ Nat.log 2 s)).trans h2n + have hsM := hA.lt_mul_sqrt hs2 + have h16 := hA.sixteen_pow_lt hs2 + have hσn : Nat.sqrt (Nat.log 2 s) ≤ Nat.log 2 s := Nat.sqrt_le_self _ + have hnσ : Nat.log 2 s < (Nat.sqrt (Nat.log 2 s) + 1) ^ 2 := Nat.lt_succ_sqrt' _ + have hσpow : Nat.sqrt (Nat.log 2 s) ≤ 2 ^ (Nat.log 2 s / 20) := by omega + have hCpow : C ≤ 2 ^ (Nat.log 2 s / 8) := (Nat.le_mul_of_pos_right C (by omega)).trans hA2 + have haA : slotBits s d = prefixBits s d + 2 * taper s d := slotBits_eq s d + have ha : slotBits s d ≤ Nat.log 2 s / 32768 := slotBits_le s d + have han : slotBits s d ≤ Nat.log 2 s := ha.trans (Nat.div_le_self _ _) + -- The depth. + have hdepth : d + 2 ≤ Nat.log 2 s := by + have h1 : 2 ^ (4 * d) < 2 ^ (Nat.log 2 s / 8) := by + calc 2 ^ (4 * d) = 16 ^ d := by rw [pow_mul]; norm_num + _ < C * Nat.sqrt (Nat.log 2 s) := h16 + _ ≤ C * (Nat.log 2 s + 1) := Nat.mul_le_mul_left _ (by omega) + _ ≤ 2 ^ (Nat.log 2 s / 8) := hA2 + have := (Nat.pow_lt_pow_iff_right one_lt_two).1 h1 + omega + -- The taper. + have hpowu : 49 * C * Nat.log 2 s ^ 4 ≤ 2 ^ taper s d := by + have hn4 : Nat.log 2 s ^ 4 ≤ (Nat.sqrt (Nat.log 2 s) + 1) ^ 8 := by + calc Nat.log 2 s ^ 4 ≤ ((Nat.sqrt (Nat.log 2 s) + 1) ^ 2) ^ 4 := + Nat.pow_le_pow_left hnσ.le 4 + _ = (Nat.sqrt (Nat.log 2 s) + 1) ^ 8 := by rw [← pow_mul] + calc 49 * C * Nat.log 2 s ^ 4 ≤ 49 * C * (Nat.sqrt (Nat.log 2 s) + 1) ^ 8 := + Nat.mul_le_mul_left _ hn4 + _ ≤ 2 ^ (Nat.sqrt (Nat.log 2 s) / (2 ^ 17 * C)) := hA1 + _ ≤ 2 ^ taper s d := Nat.pow_le_pow_right two_pos (hA.le_taper hs2) + have hu1 : 1 ≤ taper s d := by + by_contra hu0 + have h0 : taper s d = 0 := by omega + rw [h0, pow_zero] at hpowu + have : 1 ≤ Nat.log 2 s ^ 4 := Nat.one_le_pow _ _ (by omega) + have : 49 ≤ 49 * C * Nat.log 2 s ^ 4 := + calc 49 = 49 * 1 * 1 := rfl + _ ≤ 49 * C * Nat.log 2 s ^ 4 := Nat.mul_le_mul (Nat.mul_le_mul_left _ hC) this + omega + have hun : taper s d ≤ Nat.log 2 s := Nat.div_le_self _ _ + have huM : taper s d ≤ M := by + have := Nat.log_two_le_div_sqrt_log_two s + have := hA.leafSize_lt + simp only [leafSize] at this + omega + have hpu : p * taper s d ≤ M * 2 ^ (prefixBits s d + taper s d) := + mul_taper_le_of (hA.precision_le.trans (precisionBound_le C s d)) hsM.le hσn + (by omega) hun (by omega) hpowu + have h8 : 8 * (slotBits s d + 1) * taper s d ≤ 2 ^ taper s d := + eight_mul_le_two_pow hC (by omega) han hun hpowu + have hpoints := points_le_of (a := slotBits s d) hM1 hMCs hCpow hsn + refine ⟨hdepth, hu1, huM, ?_, ?_, ?_, ?_, ?_, fun i h _ hh => ?_, fun i h hi hh => ?_⟩ + · -- `2 Δ D_arr² ≤ M`. + have := two_pow_lt_of (k := 3 + 9 * Nat.log 2 s / 10 + 24 * slotBits s d) (by omega) + hσpow h2n hsM + rw [degreeBound, sixtyFour_pow] + calc 2 * 2 ^ (9 * Nat.log 2 s / 10 + 2) * (2 ^ (12 * slotBits s d)) ^ 2 + = 2 ^ (3 + 9 * Nat.log 2 s / 10 + 24 * slotBits s d) := by + rw [← pow_mul, ← pow_succ', ← pow_add]; ring_nf + _ ≤ M := this.le + · -- `L D_arr ≤ M`. + have := two_pow_lt_of (k := 13 * slotBits s d) (by omega) hσpow h2n hsM + rw [sixtyFour_pow, ← pow_add] + calc 2 ^ (slotBits s d + 12 * slotBits s d) = 2 ^ (13 * slotBits s d) := by ring_nf + _ ≤ M := this.le + · -- `2 L ≤ Δ`. + rw [degreeBound, ← pow_succ'] + exact Nat.pow_le_pow_right two_pos (by omega) + · -- Interpolation points. + exact hpoints.trans (Nat.pow_le_pow_right two_pos (by omega)) + · -- The polynomial branching factor. + calc 2 * 2 ^ slotBits s d * (M * (2 * 2 ^ slotBits s d - 1) + 1) * 64 + ≤ 2 * 2 ^ slotBits s d * 2 ^ (Nat.log 2 s / 8 + Nat.log 2 s + slotBits s d + 2) * 64 := + Nat.mul_le_mul_right _ (Nat.mul_le_mul_left _ hpoints) + _ = 2 ^ (Nat.log 2 s / 8 + Nat.log 2 s + 2 * slotBits s d + 9) := by + rw [show (64 : ℕ) = 2 ^ 6 by norm_num, ← pow_succ', ← pow_add, ← pow_add]; ring_nf + _ ≤ 2 ^ (2 * Nat.log 2 s) := Nat.pow_le_pow_right two_pos (by omega) + · -- Children's precisions. + exact nodePrecision_le_of hA.precision_le hh hu1 huM hMCs + · -- (D.11). + exact nodePrecision_mul_le_of hpu haA hi hh huM h8 + +/-- **The parameter certificate.** For every `C` there is `s₀` such that for all `s ≥ s₀` the +precisions up to depth `⌊log₂ s⌋` are at most `s ^ 2`, and every active call satisfies +`ActiveBounds`. -/ +theorem exists_activeBounds (C : ℕ) : ∃ s₀, ∀ s, s₀ ≤ s → + (∀ d ≤ Nat.log 2 s, precisionBound C s d ≤ s ^ 2) ∧ + ∀ d M p, Active C s d M p → ActiveBounds C s d M p := by + rcases Nat.eq_zero_or_pos C with rfl | hC + · refine ⟨0, fun s _ => ⟨fun d _ => ?_, fun d M p h => absurd h.one_le_const (by norm_num)⟩⟩ + have := precisionBound_le 0 s d + simp only [zero_mul] at this + exact this.trans (Nat.zero_le _) + obtain ⟨n₀, hn₀⟩ := eventually_atTop.1 (eventually_large C hC) + refine ⟨2 ^ n₀, fun s hs => ?_⟩ + have hs0 : s ≠ 0 := by + rintro rfl + have := Nat.one_le_two_pow (n := n₀) + omega + obtain ⟨h200, hA1, hA2, hA3, hA5⟩ := hn₀ (Nat.log 2 s) (Nat.le_log_of_pow_le one_lt_two hs) + simp only [pow_one] at hA2 hA3 + exact ⟨fun d hd => precisionBound_le_sq_of hd hs0 hA5, + fun d M p hA => activeBounds_of hA h200 hA1 hA2 hA3⟩ + +/-! ### The mode count -/ + +/-- **The mode count (D.15)** at an active call: if the node `t` of valuation `i ≤ a` satisfies +the precision bound (D.11) `p_t u ≤ 34 M D_t` with `u ≥ 1`, and the packing has `#P 2 ^ a ≤ 3 M` +packets (Lemma D.3 (1)), then there are at most `2 ^ e_d` tuples of exponents of the modes +`P × Fin (2 ^ (i + 1)) × Fin p_t` (packet, tile, `b`) of weight `b + 1` below `p_t`. There are +`#P 2 ^ (i + 1) ≤ 6 M / D_t` modes of each weight (D.13). -/ +theorem card_modeBudget_le {C s d M p : ℕ} (hA : Active C s d M p) (hs : 2 ≤ s) + (hu : 1 ≤ taper s d) {i h : ℕ} (hi : i ≤ slotBits s d) + (hpt : nodePrecision p h (slotBits s d) M i * taper s d ≤ + 34 * M * 2 ^ (slotBits s d - i)) + {P : Type*} [Fintype P] [DecidableEq P] + (hP : Fintype.card P * 2 ^ slotBits s d ≤ 3 * M) : + #(TensorNetwork.modeBudget + (fun Z : P × Fin (2 ^ (i + 1)) × Fin (nodePrecision p h (slotBits s d) M i) => + (Z.2.2 : ℕ) + 1) + (nodePrecision p h (slotBits s d) M i)) ≤ 2 ^ branchExponent C s d := by + set a := slotBits s d + set pt := nodePrecision p h a M i + set u := taper s d + set m := Fintype.card P * 2 ^ (i + 1) + set σ := Nat.sqrt (Nat.log 2 s) + -- At most `m` modes of each weight. + have hfib : ∀ j, #{Z : P × Fin (2 ^ (i + 1)) × Fin pt | (Z.2.2 : ℕ) + 1 = j} ≤ m := by + intro j + calc #{Z : P × Fin (2 ^ (i + 1)) × Fin pt | (Z.2.2 : ℕ) + 1 = j} + ≤ #(univ : Finset (P × Fin (2 ^ (i + 1)))) := by + refine card_le_card_of_injOn (fun Z => (Z.1, Z.2.1)) (fun _ _ => mem_univ _) ?_ + intro Z hZ Z' hZ' hZZ + have hZ := (mem_filter.1 (mem_coe.1 hZ)).2 + have hZ' := (mem_filter.1 (mem_coe.1 hZ')).2 + simp only [Prod.mk.injEq] at hZZ + exact Prod.ext hZZ.1 (Prod.ext hZZ.2 (Fin.ext (by omega))) + _ = m := by simp [m] + have hcard := card_le_two_pow_of_sum_mul_lt (fun _ => Nat.succ_pos _) hfib + (S := TensorNetwork.modeBudget _ pt) fun β hβ => + (TensorNetwork.mem_modeBudget (fun _ => Nat.succ_pos _)).1 hβ + refine hcard.trans (Nat.pow_le_pow_right two_pos ?_) + -- `⌊√(m p_t)⌋ ⌊√u⌋ ≤ 15 M`. + set x := Nat.sqrt (m * pt) + set y := Nat.sqrt u + have hmD : m * 2 ^ (a - i) ≤ 6 * M := by + have : m * 2 ^ (a - i) = 2 * (Fintype.card P * 2 ^ a) := by + rw [show a = i + (a - i) by omega, Nat.add_sub_cancel_left] + simp only [m, pow_succ, pow_add] + ring + omega + have hxy : x * y ≤ 15 * M := by + have h1 : (x * y) ^ 2 ≤ m * pt * u := by + rw [mul_pow] + exact Nat.mul_le_mul (Nat.sqrt_le' _) (Nat.sqrt_le' _) + have h2 : m * pt * u ≤ 204 * M ^ 2 := + calc m * pt * u = m * (pt * u) := by ring + _ ≤ m * (34 * M * 2 ^ (a - i)) := Nat.mul_le_mul_left _ hpt + _ = 34 * M * (m * 2 ^ (a - i)) := by ring + _ ≤ 34 * M * (6 * M) := Nat.mul_le_mul_left _ hmD + _ = 204 * M ^ 2 := by ring + have h3 : (x * y) ^ 2 ≤ (15 * M) ^ 2 := by + rw [mul_pow (15 : ℕ)] + omega + exact (Nat.pow_le_pow_iff_left (by norm_num)).1 h3 + have hσ : σ ≤ 2 ^ (10 + d) * y := sqrt_log_two_le_mul_sqrt_taper hu + have hσ1 : 1 ≤ σ := Nat.one_le_sqrt_log_two hs + have hx : x ≤ 15360 * C * s / (σ * 8 ^ d) := by + rw [Nat.le_div_iff_mul_le (by positivity)] + calc x * (σ * 8 ^ d) ≤ x * (2 ^ (10 + d) * y * 8 ^ d) := + Nat.mul_le_mul_left _ (Nat.mul_le_mul_right _ hσ) + _ = x * y * 2 ^ 10 * (2 ^ d * 8 ^ d) := by rw [pow_add]; ring + _ ≤ 15 * M * 2 ^ 10 * 16 ^ d := by + rw [← mul_pow] + exact Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ hxy) + _ = 15360 * (16 ^ d * M) := by ring + _ ≤ 15360 * (C * s) := Nat.mul_le_mul_left _ hA.edges_le + _ = 15360 * C * s := by ring + change 4 * x + 4 ≤ 4 * (15360 * C * s / (σ * 8 ^ d)) + 4 + omega + +/-- **The excess exponents sum to `O(s / √⌊log₂ s⌋)`**: over at most `⌊log₂ s⌋` levels, +`∑_d e_d ≤ (245760 C + 4) ⌊s / ⌊√⌊log₂ s⌋⌋⌋`. The terms decrease geometrically, as in the +manuscript's `(√2 / 8) ^ d` (§D.4.7, p. 64). -/ +theorem sum_branchExponent_le (C : ℕ) {s D : ℕ} (hs : 2 ≤ s) (hD : D ≤ Nat.log 2 s) : + ∑ d ∈ range D, branchExponent C s d ≤ + (245760 * C + 4) * (s / Nat.sqrt (Nat.log 2 s)) := by + set σ := Nat.sqrt (Nat.log 2 s) + set S := s / σ + set X := 15360 * C * s / σ + have hσ1 : 1 ≤ σ := Nat.one_le_sqrt_log_two hs + have hS1 : 1 ≤ S := Nat.one_le_div_sqrt_log_two hs + have hDS : D ≤ S := hD.trans (Nat.log_two_le_div_sqrt_log_two s) + have hX : X ≤ 15360 * C * S + 15360 * C := Nat.mul_div_le_mul_div_add _ _ _ + have hterm : ∀ d, 15360 * C * s / (σ * 8 ^ d) ≤ X / 2 ^ d := fun d => by + rw [← Nat.div_div_eq_div_mul] + exact Nat.div_le_div_left (Nat.pow_le_pow_left (by norm_num) d) (by positivity) + have hgeo : ∑ d ∈ range D, X / 2 ^ d ≤ 2 * X := by + have h := sum_div_two_pow_succ_le (2 * X) D + have heq : ∀ d, 2 * X / 2 ^ (d + 1) = X / 2 ^ d := fun d => by + rw [pow_succ', Nat.mul_div_mul_left X (2 ^ d) two_pos] + simpa only [heq] using h + calc ∑ d ∈ range D, branchExponent C s d + = 4 * ∑ d ∈ range D, 15360 * C * s / (σ * 8 ^ d) + 4 * D := by + simp only [branchExponent, sum_add_distrib, ← mul_sum, sum_const, card_range, + smul_eq_mul] + ring + _ ≤ 4 * (2 * X) + 4 * S := + Nat.add_le_add (Nat.mul_le_mul_left _ ((sum_le_sum fun d _ => hterm d).trans hgeo)) + (Nat.mul_le_mul_left _ hDS) + _ ≤ (245760 * C + 4) * S := by + have hCS : C ≤ C * S := Nat.le_mul_of_pos_right C hS1 + have h1 : 15360 * C * S = 15360 * (C * S) := by ring + have h2 : (245760 * C + 4) * S = 245760 * (C * S) + 4 * S := by ring + omega + +end Cslib.Circuits.Frontier.ContractionSchedule diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkSchedule.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkSchedule.lean new file mode 100644 index 0000000000..ef6a4eedd9 --- /dev/null +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkSchedule.lean @@ -0,0 +1,90 @@ +/- +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: local-only (test driver) + +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Schedule + +/-! +# Tests for the parameter schedule of the contraction recursion + +Concrete values of the schedule at `s = 2 ^ 10`, an active call there, and a nonvacuity check of +the certificate: some root call satisfies `ActiveBounds`. +-/ + +@[expose] public section + +namespace ComplexityTests.Computability.Circuit.Frontier.TensorNetwork.Schedule + +open Cslib.Circuits.Frontier.ContractionSchedule + +/-! ### Values at `s = 2 ^ 10`, where `⌊log₂ s⌋ = 10` and `⌊√10⌋ = 3` -/ + +theorem log_two_1024 : Nat.log 2 1024 = 10 := by + rw [show (1024 : ℕ) = 2 ^ 10 by norm_num, Nat.log_pow one_lt_two] + +theorem sqrt_10 : Nat.sqrt 10 = 3 := + (Nat.eq_sqrt.2 ⟨by norm_num, by norm_num⟩).symm + +example : leafSize 1024 = 341 := by + rw [leafSize, log_two_1024, sqrt_10] + +/-- `ε λ` is far below one at this size, so the taper and the labels are trivial. -/ +example (d : ℕ) : taper 1024 d = 0 := by + rw [taper, log_two_1024] + exact Nat.div_eq_of_lt (lt_of_lt_of_le (by norm_num) (Nat.pow_le_pow_right two_pos + (Nat.le_add_right 17 d))) + +example : degreeBound 1024 = 2 ^ 11 := by + rw [degreeBound, log_two_1024] + +example : precisionBound 3 1024 0 = 3072 := rfl + +/-- One level adds `8 C s (4 · 2 ^ a_0 + a_0 + 1)` with `a_0 = 0`. -/ +example : precisionBound 3 1024 1 = 3072 + 8 * 3 * 1024 * 5 := by + have h : slotBits 1024 0 = 0 := by + simp [slotBits, prefixBits, taper, log_two_1024] + simp [precisionBound, h] + +example : nodePrecision 5 2 3 7 1 = 5 + 8 * 2 * 4 + 8 * 7 * 4 := rfl + +/-- `Δ ^ 10 ≥ s ^ 9` and `Δ ^ 10 ≤ 2 ^ 20 s ^ 9`. -/ +example : 1024 ^ 9 ≤ degreeBound 1024 ^ 10 ∧ degreeBound 1024 ^ 10 ≤ 2 ^ 20 * 1024 ^ 9 := + ⟨pow_nine_le_degreeBound_pow_ten 1024, degreeBound_pow_ten_le (by norm_num)⟩ + +/-! ### Active calls -/ + +/-- A root call with `1000` edges and precision `5` at `s = 1024`, `C = 1`. -/ +example : Active 1 1024 0 1000 5 := + Active.root (by norm_num) (by rw [show leafSize 1024 = 341 by + rw [leafSize, log_two_1024, sqrt_10]]; norm_num) (by norm_num) + +/-- A child with `62` edges is not active at `s = 1024`: it is a leaf. -/ +example : ¬ Active 1 1024 1 62 5 := fun h => by + have := h.leafSize_lt + rw [show leafSize 1024 = 341 by rw [leafSize, log_two_1024, sqrt_10]] at this + omega + +/-- **The certificate is not vacuous**: for each `C ≥ 1` some root call satisfies +`ActiveBounds`. -/ +example (C : ℕ) (hC : 1 ≤ C) : ∃ s M p, ActiveBounds C s 0 M p := by + obtain ⟨s₀, h⟩ := exists_activeBounds C + set s := max s₀ 16 + have hs : 16 ≤ s := le_max_right _ _ + have hlog : 4 ≤ Nat.log 2 s := Nat.le_log_of_pow_le one_lt_two (by simpa using hs) + have hσ : 2 ≤ Nat.sqrt (Nat.log 2 s) := Nat.le_sqrt.2 (by omega) + refine ⟨s, s, 0, (h s (le_max_left _ _)).2 0 s 0 (Active.root ?_ ?_ (Nat.zero_le _))⟩ + · exact Nat.le_mul_of_pos_left s hC + · exact Nat.div_lt_self (by omega) (by omega) + +/-- The excess exponents at `s = 1024` and `C = 1` over two levels. -/ +example : ∑ d ∈ Finset.range 2, branchExponent 1 1024 d ≤ 245764 * (1024 / Nat.sqrt 10) := by + have := sum_branchExponent_le 1 (s := 1024) (D := 2) (by norm_num) + (by rw [log_two_1024]; norm_num) + rwa [log_two_1024] at this + +end ComplexityTests.Computability.Circuit.Frontier.TensorNetwork.Schedule From d9a734324a1bf53b70ff5ca89acdb2166b57587b Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 23:02:48 -0400 Subject: [PATCH 6/8] feat(circuit/frontier): mode count at a certified active call ActiveBounds.card_modeBudget_le supplies the hypotheses of card_modeBudget_le from the certificate, and ActiveBounds.two_le. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Frontier/TensorNetwork/Schedule.lean | 25 ++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Schedule.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Schedule.lean index 6fa306e299..66eafea95a 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Schedule.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Schedule.lean @@ -78,7 +78,8 @@ precision bound `p ≤ s λ^{O(1)} 2 ^ (a_{d-1})` is `precisionBound_le`. ## Main results * `exists_activeBounds`: the parameter certificate. -* `card_modeBudget_le`: the mode count (D.15) at an active call. +* `card_modeBudget_le`, `ActiveBounds.card_modeBudget_le`: the mode count (D.15) at an active + call. * `sum_branchExponent_le`: the excess exponents sum to `O(s / √⌊log₂ s⌋)`. * `precisionBound_le`: the precision bound `p ≤ C s 2 ^ (a_{d-1}) (1 + d (8 λ + 40))`. @@ -686,6 +687,28 @@ theorem card_modeBudget_le {C s d M p : ℕ} (hA : Active C s d M p) (hs : 2 ≤ change 4 * x + 4 ≤ 4 * (15360 * C * s / (σ * 8 ^ d)) + 4 omega +/-- At an active call satisfying the certificate, `s ≥ 2`. -/ +theorem ActiveBounds.two_le {C s d M p : ℕ} (hB : ActiveBounds C s d M p) : 2 ≤ s := by + have h := hB.depth_add_two_le + rcases Nat.lt_or_ge s 2 with hs | hs + · rw [Nat.log_of_lt hs] at h + omega + · exact hs + +/-- **The mode count (D.15) at a certified active call**: for a node of valuation `i < u` and +`h = ⌈3 M / u⌉`, and a packing with `#P 2 ^ a ≤ 3 M` (Lemma D.3 (1)), there are at most `2 ^ e_d` +mode tuples. This is `card_modeBudget_le` with its hypotheses supplied by `ActiveBounds`. -/ +theorem ActiveBounds.card_modeBudget_le {C s d M p : ℕ} (hB : ActiveBounds C s d M p) + (hA : Active C s d M p) {i h : ℕ} (hi : i < taper s d) + (hh : h * taper s d ≤ 3 * M + taper s d) {P : Type*} [Fintype P] [DecidableEq P] + (hP : Fintype.card P * 2 ^ slotBits s d ≤ 3 * M) : + #(TensorNetwork.modeBudget + (fun Z : P × Fin (2 ^ (i + 1)) × Fin (nodePrecision p h (slotBits s d) M i) => + (Z.2.2 : ℕ) + 1) + (nodePrecision p h (slotBits s d) M i)) ≤ 2 ^ branchExponent C s d := + ContractionSchedule.card_modeBudget_le hA hB.two_le hB.one_le_taper + (by have := slotBits_eq s d; omega) (hB.nodePrecision_mul_taper_le i h hi hh) hP + /-- **The excess exponents sum to `O(s / √⌊log₂ s⌋)`**: over at most `⌊log₂ s⌋` levels, `∑_d e_d ≤ (245760 C + 4) ⌊s / ⌊√⌊log₂ s⌋⌋⌋`. The terms decrease geometrically, as in the manuscript's `(√2 / 8) ^ d` (§D.4.7, p. 64). -/ From af73f5bbde72bde81d9bc7fad3cd4bb3ca6678f0 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 23:06:30 -0400 Subject: [PATCH 7/8] feat(circuit/frontier): the contraction recursion has 2^O(s/sqrt(log s)) calls Compose ContractionSchedule.sum_branchExponent_le with Nat.exists_recursionBound_le_two_pow_div_sqrt_log_two. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Frontier/TensorNetwork/ScheduleCount.lean | 52 +++++++++++++++++++ ComplexityTests/ScheduleCount.lean | 25 +++++++++ 3 files changed, 78 insertions(+) create mode 100644 Complexity/Computability/Circuit/Frontier/TensorNetwork/ScheduleCount.lean create mode 100644 ComplexityTests/ScheduleCount.lean diff --git a/Complexity.lean b/Complexity.lean index 0f8709f8f9..a0f2851d5a 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -875,6 +875,7 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Deformatio public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ModeExpansion public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Schedule +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ScheduleCount public import Complexity.Computability.Circuit.Frontier.TwoSidedWitness public import Complexity.Computability.Circuit.Frontier.Unconditional public import Complexity.Computability.Circuit.Frontier.Witness diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ScheduleCount.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ScheduleCount.lean new file mode 100644 index 0000000000..2a989ab9df --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ScheduleCount.lean @@ -0,0 +1,52 @@ +/- +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.Circuit.Frontier.TensorNetwork.Schedule +public import Complexity.Foundations.Data.Nat.RecursionTree + +/-! +# The number of calls of the contraction recursion + +Under the parameter schedule of `Cslib.Circuits.Frontier.ContractionSchedule`, a call at depth +`d` of the recursion of [OpenAI2026ETH] (Appendix D.4) has at most +`2 ^ (2 ⌊log₂ s⌋ + branchExponent C s d)` children (`ContractionSchedule.exists_activeBounds`, +`ContractionSchedule.ActiveBounds.card_modeBudget_le`), and there are at most +`⌊log₂ s⌋` levels. The excess exponents sum to `O(s / √⌊log₂ s⌋)` +(`ContractionSchedule.sum_branchExponent_le`), so the recursion has `2 ^ O(s / √⌊log₂ s⌋)` calls +(`ContractionSchedule.exists_recursionBound_le`): the count of Appendix D.4.7 (p. 64), in the +natural-number scale of the contraction interface. It bounds the nodes of the depth-first +evaluation (`Nat.recursionBound`), hence the fuel of +`Cslib.GenericRAM.StackRecursion.Scheme.certificate`. + +## Main results + +* `Cslib.Circuits.Frontier.ContractionSchedule.exists_recursionBound_le`: the call count. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Appendix D.4.7 (p. 64). +-/ + +public section + +namespace Cslib.Circuits.Frontier.ContractionSchedule + +/-- **The recursion has `2 ^ O(s / √⌊log₂ s⌋)` calls.** For every `C` there is `K` such that, +from `s = 2` on, a recursion of depth at most `D ≤ ⌊log₂ s⌋` whose calls at depth `d` have at +most `2 ^ (2 ⌊log₂ s⌋ + branchExponent C s d)` children has at most +`2 ^ (K s / √⌊log₂ s⌋)` nodes below its root. -/ +theorem exists_recursionBound_le (C : ℕ) : ∃ K, ∀ s D, 2 ≤ s → D ≤ Nat.log 2 s → + Nat.recursionBound (fun d => 2 ^ (2 * Nat.log 2 s + branchExponent C s d)) D 0 ≤ + 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) := by + obtain ⟨K, hK⟩ := Nat.exists_recursionBound_le_two_pow_div_sqrt_log_two 2 (245760 * C + 4) + refine ⟨K, fun s D hs hD => (Nat.recursionBound_le _ D 0).trans ?_⟩ + simpa only [Nat.zero_add] using hK s D (fun d => 2 ^ (2 * Nat.log 2 s + branchExponent C s d)) + (branchExponent C s) hs hD (fun _ _ => le_rfl) (sum_branchExponent_le C hs hD) + +end Cslib.Circuits.Frontier.ContractionSchedule diff --git a/ComplexityTests/ScheduleCount.lean b/ComplexityTests/ScheduleCount.lean new file mode 100644 index 0000000000..d9886e70c8 --- /dev/null +++ b/ComplexityTests/ScheduleCount.lean @@ -0,0 +1,25 @@ +/- +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.Circuit.Frontier.TensorNetwork.ScheduleCount + +/-! # The call count of the contraction recursion + +The node bound of a recursion with the schedule's branching factors is `2 ^ O(s / √⌊log₂ s⌋)`, +for every constant `C` and every depth up to `⌊log₂ s⌋`. -/ + +namespace ComplexityTests.ScheduleCount + +open Cslib.Circuits.Frontier.ContractionSchedule + +-- At `s = 16` the depth is at most `⌊log₂ 16⌋ = 4`; one constant serves every depth and size. +example (C : ℕ) : ∃ K, ∀ D ≤ Nat.log 2 16, + Nat.recursionBound (fun d => 2 ^ (2 * Nat.log 2 16 + branchExponent C 16 d)) D 0 ≤ + 2 ^ (K * 16 / Nat.sqrt (Nat.log 2 16)) := by + obtain ⟨K, hK⟩ := exists_recursionBound_le C + exact ⟨K, fun D hD => hK 16 D (by norm_num) hD⟩ + +end ComplexityTests.ScheduleCount From 06e8c0284c48eb892169c1f632e99d01c8643604 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 02:26:48 -0400 Subject: [PATCH 8/8] feat(circuit/frontier): the call count with a constant explicit in C MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace the ∃ K forms of Nat.exists_recursionBound_le_two_pow_div_sqrt_log_two and ContractionSchedule.exists_recursionBound_le by statements with the explicit constants 1 + 16c + E and 245760 C + 37. The fast contraction machine cannot see the admissibility constant C, so its clock covers every C only because the exponent is linear in C (audit round 16 on #1538). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Frontier/TensorNetwork/ScheduleCount.lean | 30 +++++++++++-------- .../Foundations/Data/Nat/RecursionTree.lean | 28 ++++++++--------- ComplexityTests/ScheduleCount.lean | 13 ++++---- 3 files changed, 40 insertions(+), 31 deletions(-) diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ScheduleCount.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ScheduleCount.lean index 2a989ab9df..5a7c9da806 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ScheduleCount.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ScheduleCount.lean @@ -19,14 +19,16 @@ Under the parameter schedule of `Cslib.Circuits.Frontier.ContractionSchedule`, a `ContractionSchedule.ActiveBounds.card_modeBudget_le`), and there are at most `⌊log₂ s⌋` levels. The excess exponents sum to `O(s / √⌊log₂ s⌋)` (`ContractionSchedule.sum_branchExponent_le`), so the recursion has `2 ^ O(s / √⌊log₂ s⌋)` calls -(`ContractionSchedule.exists_recursionBound_le`): the count of Appendix D.4.7 (p. 64), in the +(`ContractionSchedule.recursionBound_le_two_pow_div_sqrt_log_two`, with the constant +`245760 C + 37`): the count of Appendix D.4.7 (p. 64), in the natural-number scale of the contraction interface. It bounds the nodes of the depth-first evaluation (`Nat.recursionBound`), hence the fuel of `Cslib.GenericRAM.StackRecursion.Scheme.certificate`. ## Main results -* `Cslib.Circuits.Frontier.ContractionSchedule.exists_recursionBound_le`: the call count. +* `Cslib.Circuits.Frontier.ContractionSchedule.recursionBound_le_two_pow_div_sqrt_log_two`: the + call count. ## References @@ -37,16 +39,20 @@ public section namespace Cslib.Circuits.Frontier.ContractionSchedule -/-- **The recursion has `2 ^ O(s / √⌊log₂ s⌋)` calls.** For every `C` there is `K` such that, -from `s = 2` on, a recursion of depth at most `D ≤ ⌊log₂ s⌋` whose calls at depth `d` have at -most `2 ^ (2 ⌊log₂ s⌋ + branchExponent C s d)` children has at most -`2 ^ (K s / √⌊log₂ s⌋)` nodes below its root. -/ -theorem exists_recursionBound_le (C : ℕ) : ∃ K, ∀ s D, 2 ≤ s → D ≤ Nat.log 2 s → +/-- **The recursion has `2 ^ O(s / √⌊log₂ s⌋)` calls**, with the constant `245760 C + 37`. From +`s = 2` on, a recursion of depth at most `D ≤ ⌊log₂ s⌋` whose calls at depth `d` have at most +`2 ^ (2 ⌊log₂ s⌋ + branchExponent C s d)` children has at most +`2 ^ ((245760 C + 37) s / √⌊log₂ s⌋)` nodes below its root. The constant is linear in `C`, so one +clock serves every admissibility constant at once, as a machine that does not know `C` needs. -/ +theorem recursionBound_le_two_pow_div_sqrt_log_two (C : ℕ) {s D : ℕ} (hs : 2 ≤ s) + (hD : D ≤ Nat.log 2 s) : Nat.recursionBound (fun d => 2 ^ (2 * Nat.log 2 s + branchExponent C s d)) D 0 ≤ - 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) := by - obtain ⟨K, hK⟩ := Nat.exists_recursionBound_le_two_pow_div_sqrt_log_two 2 (245760 * C + 4) - refine ⟨K, fun s D hs hD => (Nat.recursionBound_le _ D 0).trans ?_⟩ - simpa only [Nat.zero_add] using hK s D (fun d => 2 ^ (2 * Nat.log 2 s + branchExponent C s d)) - (branchExponent C s) hs hD (fun _ _ => le_rfl) (sum_branchExponent_le C hs hD) + 2 ^ ((245760 * C + 37) * s / Nat.sqrt (Nat.log 2 s)) := by + have h := Nat.mul_prod_le_two_pow_div_sqrt_log_two 2 (245760 * C + 4) hs hD + (b := fun d => 2 ^ (2 * Nat.log 2 s + branchExponent C s d)) (e := branchExponent C s) + (fun _ _ => le_rfl) (sum_branchExponent_le C hs hD) + rw [show 1 + 16 * 2 + (245760 * C + 4) = 245760 * C + 37 by ring] at h + refine (Nat.recursionBound_le _ D 0).trans ?_ + simpa only [Nat.zero_add] using h end Cslib.Circuits.Frontier.ContractionSchedule diff --git a/Complexity/Foundations/Data/Nat/RecursionTree.lean b/Complexity/Foundations/Data/Nat/RecursionTree.lean index e5f2982128..ff3e344693 100644 --- a/Complexity/Foundations/Data/Nat/RecursionTree.lean +++ b/Complexity/Foundations/Data/Nat/RecursionTree.lean @@ -25,7 +25,8 @@ most `k + 1` times the product of the branching factors (`Nat.recursionBound_le` **Recursion trees of size `2 ^ O(n / √(log n))`.** If a call at depth `j` has at most `2 ^ (c ⌊log₂ n⌋ + e j)` children, there are at most `⌊log₂ n⌋` levels, and the excess exponents sum to `O(n / √⌊log₂ n⌋)`, then the tree has `2 ^ O(n / √⌊log₂ n⌋)` nodes -(`Nat.exists_recursionBound_le_two_pow_div_sqrt_log_two`), in the natural-number scale of +(`Nat.mul_prod_le_two_pow_div_sqrt_log_two`, with the explicit constant `1 + 16 c + E`), in the +natural-number scale of `Nat.exists_three_pow_mul_le_two_pow_div_sqrt_log_two`. The polynomial factors `2 ^ (c ⌊log₂ n⌋)` contribute `2 ^ O(log² n)`, which the scale absorbs. Excess exponents halving with the depth sum to at most twice the first one (`Nat.sum_div_two_pow_le`). @@ -42,8 +43,8 @@ a call at depth `d` has `s ^ O(1) exp(O(s / √λ · (√2 / 8) ^ d))` children * `Nat.recursionBound_le`: at most `k + 1` times the product of the branching factors. * `Nat.sum_div_two_pow_le`: `∑ j < D, x / 2 ^ j ≤ 2 x`. -* `Nat.exists_recursionBound_le_two_pow_div_sqrt_log_two`: recursion trees of size - `2 ^ O(n / √⌊log₂ n⌋)`. +* `Nat.mul_prod_le_two_pow_div_sqrt_log_two`: recursion trees of size `2 ^ O(n / √⌊log₂ n⌋)`, + with an explicit constant. ## References @@ -132,17 +133,16 @@ theorem log_two_sq_le_div_sqrt_log_two {n : ℕ} (hn : 2 ≤ n) : have h2 := mul_div_le_mul_div_add 8 n (sqrt L) omega -/-- **Recursion trees of size `2 ^ O(n / √⌊log₂ n⌋)`.** For constants `c` and `E` there is `K` -such that, from `n = 2` on: if a call at depth `j < D` has at most `2 ^ (c ⌊log₂ n⌋ + e j)` -children, `D ≤ ⌊log₂ n⌋`, and `∑ j < D, e j ≤ E (n / √⌊log₂ n⌋)`, then -`(D + 1) ∏ j < D, max 1 (b j) ≤ 2 ^ (K n / √⌊log₂ n⌋)`, which bounds the nodes of the recursion -tree by `recursionBound_le`. -/ -theorem exists_recursionBound_le_two_pow_div_sqrt_log_two (c E : ℕ) : - ∃ K, ∀ (n D : ℕ) (b e : ℕ → ℕ), 2 ≤ n → D ≤ log 2 n → - (∀ j < D, b j ≤ 2 ^ (c * log 2 n + e j)) → - ∑ j ∈ range D, e j ≤ E * (n / sqrt (log 2 n)) → - (D + 1) * ∏ j ∈ range D, max 1 (b j) ≤ 2 ^ (K * n / sqrt (log 2 n)) := by - refine ⟨1 + 16 * c + E, fun n D b e hn hD hb he => ?_⟩ +/-- **Recursion trees of size `2 ^ O(n / √⌊log₂ n⌋)`**, with the constant `1 + 16 c + E`. From +`n = 2` on: if a call at depth `j < D` has at most `2 ^ (c ⌊log₂ n⌋ + e j)` children, +`D ≤ ⌊log₂ n⌋`, and `∑ j < D, e j ≤ E (n / √⌊log₂ n⌋)`, then +`(D + 1) ∏ j < D, max 1 (b j) ≤ 2 ^ ((1 + 16 c + E) n / √⌊log₂ n⌋)`, which bounds the nodes of the +recursion tree by `recursionBound_le`. The constant is linear in `E`, so a single clock serves a +family of excess budgets growing linearly in a parameter. -/ +theorem mul_prod_le_two_pow_div_sqrt_log_two (c E : ℕ) {n D : ℕ} {b e : ℕ → ℕ} (hn : 2 ≤ n) + (hD : D ≤ log 2 n) (hb : ∀ j < D, b j ≤ 2 ^ (c * log 2 n + e j)) + (he : ∑ j ∈ range D, e j ≤ E * (n / sqrt (log 2 n))) : + (D + 1) * ∏ j ∈ range D, max 1 (b j) ≤ 2 ^ ((1 + 16 * c + E) * n / sqrt (log 2 n)) := by set L := log 2 n set S := n / sqrt L have hL : L ≤ S := log_two_le_div_sqrt_log_two n diff --git a/ComplexityTests/ScheduleCount.lean b/ComplexityTests/ScheduleCount.lean index d9886e70c8..67b17d706b 100644 --- a/ComplexityTests/ScheduleCount.lean +++ b/ComplexityTests/ScheduleCount.lean @@ -15,11 +15,14 @@ namespace ComplexityTests.ScheduleCount open Cslib.Circuits.Frontier.ContractionSchedule --- At `s = 16` the depth is at most `⌊log₂ 16⌋ = 4`; one constant serves every depth and size. -example (C : ℕ) : ∃ K, ∀ D ≤ Nat.log 2 16, +-- At `s = 16` the depth is at most `⌊log₂ 16⌋ = 4`; the constant `245760 C + 37` serves every +-- depth and size. +example (C : ℕ) : ∀ D ≤ Nat.log 2 16, Nat.recursionBound (fun d => 2 ^ (2 * Nat.log 2 16 + branchExponent C 16 d)) D 0 ≤ - 2 ^ (K * 16 / Nat.sqrt (Nat.log 2 16)) := by - obtain ⟨K, hK⟩ := exists_recursionBound_le C - exact ⟨K, fun D hD => hK 16 D (by norm_num) hD⟩ + 2 ^ ((245760 * C + 37) * 16 / Nat.sqrt (Nat.log 2 16)) := + fun _ hD => recursionBound_le_two_pow_div_sqrt_log_two C (by norm_num) hD + +-- The constant is linear in `C`: at `C = 1` it is `245797`. +example : 245760 * 1 + 37 = 245797 := by norm_num end ComplexityTests.ScheduleCount