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/4] 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 69ba19053..e3af2ca51 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 000000000..c2fd37dd1 --- /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 000000000..e5f298212 --- /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 000000000..bcca97e43 --- /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/4] 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 c2fd37dd1..fadf0610d 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/4] 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 e3af2ca51..c3020b1ba 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 000000000..7b6a566ec --- /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 bcca97e43..34fbd8920 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 792613291bce8b9d183ff5b14b4ccb2664042655 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 23:21:15 -0400 Subject: [PATCH 4/4] feat(circuit/frontier): direct summation over networks with described tensors Networks whose tensors are given by descriptors and an evaluator, and their direct summation as a stack recursion: one native machine for the contraction modulo 2^P from any native certificate of the evaluator, with time (2^m (k+1) + 1) (poly + 2E) and space poly + ES. This is the leaf step of [OpenAI2026ETH, Appendix D.4.7] with implicit packet tensors. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../TensorNetwork/DescribedContraction.lean | 896 ++++++++++++++++++ ComplexityTests/DescribedContraction.lean | 79 ++ 3 files changed, 976 insertions(+) create mode 100644 Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedContraction.lean create mode 100644 ComplexityTests/DescribedContraction.lean diff --git a/Complexity.lean b/Complexity.lean index f7c0c0ab9..8217887b3 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -872,6 +872,7 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Binarize public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Constraint public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Deformation +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DescribedContraction public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DirectContraction public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IntegralCoordinates diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedContraction.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedContraction.lean new file mode 100644 index 000000000..fb1320cf9 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedContraction.lean @@ -0,0 +1,896 @@ +/- +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.Explicit +public import Complexity.Computability.GenericRAM.Native.StackRecursion +public import Complexity.Foundations.Data.BitString.List.Binary +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Words +public import Complexity.Computability.GenericRAM.Native.BooleanFold +public import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListLookup +public import Complexity.Computability.Machines.Turing.MultiTape.Internal.DegreeOptionPrimitives +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Degree.Bounds +import Complexity.Foundations.Data.BitString.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +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.Internal.EqualityPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryDivision +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListBinaryLookup +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListMap +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListToBits +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeNatFrontends +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeOptionPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length +import Mathlib.Algebra.BigOperators.Fin +import Mathlib.Algebra.BigOperators.Intervals +import Mathlib.Data.List.GetD + +/-! +# Contracting a network with described tensors by direct summation + +The leaves of the recursion in the proof of Theorem D.1 of [OpenAI2026ETH] are summed directly +over all Boolean edge assignments (Appendix D.4.7, p. 64), but their tensors are not tables: a +packet vertex has up to `2 L` ports, so its table would be superpolynomial, and its entries are +computed from a description instead (Appendix D.4.6, p. 63). A *described network* +(`DescribedNetwork T`) has, for each vertex, its ports and a descriptor `t : T` of its tensor, +whose entry at the bits `bs` on the ports is `eval t bs` for an evaluator `eval`. Explicit +networks are the case of tables (`DescribedNetwork.ofExplicit`). + +**Direct summation as a stack recursion** (`DescribedNetwork.sumScheme`). The sum over the +`2 ^ m` assignments is a call whose children are the assignments, in binary order; an assignment +is a call whose children are the entries of the vertices at its bits, multiplied modulo `2 ^ P`; +an entry is a leaf, evaluated by the evaluator. The derivation has `2 ^ m (k + 1) + 1` nodes for +`k` vertices and two open calls (`DescribedNetwork.eval_sumRoot`). So a native certificate of the +evaluator, with any bounds, gives one native machine for the contraction modulo `2 ^ P` on every +input (`DescribedNetwork.contractionCertificate`), through +`Cslib.GenericRAM.StackRecursion.Scheme.certificate`. If the evaluator takes time `E`, space `ES` +and outputs at most `Ev` bits on every vertex, the machine takes time `2 ^ m (k + 1) + 1` times +`K (n + Ev + 1) ^ K + 2 E` and space `K (n + Ev + 1) ^ K + ES` on inputs of length `n` +(`DescribedNetwork.contractionCertificate_le`). This is the leaf step of the contraction +algorithm, with implicit packet tensors as descriptors. + +## Main definitions + +* `Cslib.Circuits.Frontier.DescribedNetwork`: a network with described tensors. +* `Cslib.Circuits.Frontier.DescribedNetwork.contraction`: its contraction. +* `Cslib.Circuits.Frontier.DescribedNetwork.sumScheme`: direct summation as a recursion scheme. +* `Cslib.Circuits.Frontier.DescribedNetwork.encDescribed`: the encoding of a described network. +* `Cslib.Circuits.Frontier.DescribedNetwork.contractionCertificate`: one native machine for the + contraction modulo `2 ^ P`. + +## Main results + +* `Cslib.GenericRAM.StackRecursion.Scheme.Loop.counted`: a call whose children are indexed by + a counter. +* `Cslib.Circuits.Frontier.DescribedNetwork.eval_sumRoot`: direct summation evaluates to the + contraction modulo `2 ^ P`, with `2 ^ m (k + 1) + 1` nodes and two open calls. +* `Cslib.Circuits.Frontier.DescribedNetwork.contraction_ofExplicit`: explicit networks. +* `Cslib.Circuits.Frontier.DescribedNetwork.run_sumScheme`: the machine computes the contraction + modulo `2 ^ P`. +* `Cslib.Circuits.Frontier.DescribedNetwork.contractionCertificate_le`: its time and space. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Appendix D.4.6–D.4.7 + (pp. 63–64). +-/ + +@[expose] public section + +namespace Cslib.GenericRAM.StackRecursion.Scheme + +open Finset + +variable {X A Y : Type} {R : Scheme X A Y} {I : Invariant X A Y} + +/-- **A call with counted children.** If, from the accumulators `acc c`, the call `x` asks for the +children `child c` for `c < bound` and then stops, and the children evaluate to `val c`, then its +loop from `acc 0` ends at `acc bound`, with the children's nodes and at most `H` levels. -/ +theorem Loop.counted {x : X} {acc : ℕ → A} {child : ℕ → X} {val : ℕ → Y} {nodes height : ℕ → ℕ} + (bound H : ℕ) (hnext : ∀ c < bound, R.next x (acc c) = some (child c)) + (hdone : R.next x (acc bound) = none) + (habsorb : ∀ c < bound, R.absorb x (acc c) (val c) = acc (c + 1)) + (heval : ∀ c < bound, R.Eval I (child c) (val c) (nodes c) (height c)) + (hframe : ∀ c < bound, I.frame x (acc c)) (hH : ∀ c < bound, height c ≤ H) : + ∃ h ≤ H, R.Loop I x (acc 0) (acc bound) (∑ c ∈ range bound, nodes c) h := by + -- From any start `s ≤ bound`. + have key : ∀ k s, s + k = bound → + ∃ h ≤ H, R.Loop I x (acc s) (acc bound) (∑ c ∈ Ico s bound, nodes c) h := by + intro k + induction k with + | zero => + intro s hs + subst hs + exact ⟨0, Nat.zero_le _, by simpa using Loop.done hdone⟩ + | succ k ih => + intro s hs + obtain ⟨h, hh, hl⟩ := ih (s + 1) (by omega) + have hs' : s < bound := by omega + have hl' := Loop.child (hframe s hs') (hnext s hs') (heval s hs') + (by rw [habsorb s hs']; exact hl) + refine ⟨max (height s) h, max_le (hH s hs') hh, ?_⟩ + rwa [sum_eq_sum_Ico_succ_bot hs'] + simpa using key bound 0 (by omega) + +end Cslib.GenericRAM.StackRecursion.Scheme + +namespace Cslib.Circuits.Frontier + +open Finset Cslib.BitString Cslib.GenericRAM Cslib.GenericRAM.StackRecursion + +/-- A Boolean tensor network with *described* tensors: the number of edges, numbered from zero, +and for each vertex its ordered list of ports and a descriptor of its tensor. -/ +structure DescribedNetwork (T : Type) where + /-- The number of edges; the edges are numbered `0, …, numEdges - 1`. -/ + numEdges : ℕ + /-- The vertices, each given by its ports and the descriptor of its tensor. -/ + vertices : List (List ℕ × T) + +namespace DescribedNetwork + +variable {T : Type} (eval : T → List Bool → ℕ) + +/-- The bits that a word, read as an assignment of bits to the edges, puts on a list of ports; +a port past the end of the word reads `false`. -/ +def wordBits (word : List Bool) (ports : List ℕ) : List Bool := + ports.map fun i => word.getD i false + +/-- The *contraction*: the sum over all assignments of bits to the edges of the product of the +entries of the vertices at the bits on their ports. -/ +def contraction (d : DescribedNetwork T) : ℕ := + ∑ x : Fin d.numEdges → Bool, + (d.vertices.map fun v => eval v.2 (wordBits (List.ofFn x) v.1)).prod + +/-- An explicit network, with its tables as descriptors. -/ +def ofExplicit (d : ExplicitTensorNetwork ℕ) : DescribedNetwork (List ℕ) := + ⟨d.numEdges, d.vertices⟩ + +private theorem getD_ofFn {n : ℕ} (x : Fin n → Bool) (i : ℕ) : + (List.ofFn x).getD i false = if h : i < n then x ⟨i, h⟩ else false := by + by_cases h : i < n + · rw [dite_eq_left h, List.getD_eq_getElem _ _ (by simpa using h), List.getElem_ofFn] + · rw [dite_eq_right h, List.getD_eq_default _ _ (by simp only [List.length_ofFn]; omega)] + +/-- **Explicit networks**: with table lookup as the evaluator, the contraction is that of the +explicit network. -/ +theorem contraction_ofExplicit (d : ExplicitTensorNetwork ℕ) : + (ofExplicit d).contraction ExplicitTensorNetwork.entry = d.contraction := by + refine sum_congr rfl fun x _ => ?_ + simp only [wordBits, ExplicitTensorNetwork.portBits] + congr 1 + refine List.map_congr_left fun v _ => ?_ + congr 2 + funext i + exact getD_ofFn x i + +/-! ### Direct summation as a recursion scheme -/ + +/-- A node of direct summation: its kind (`0` the sum, `1` an assignment, `2` an entry), the +precision and the network, and the current word and vertex index. -/ +abbrev Node (T : Type) := ℕ × ((ℕ × DescribedNetwork T) × (List Bool × ℕ)) + +/-- The entry of a node: the evaluator at the descriptor of its vertex and the bits of its word +on the vertex's ports, or zero for an index past the vertices. -/ +def entryOf (x : Node T) : ℕ := + (x.2.1.2.vertices[x.2.2.2]?).elim 0 fun v => eval v.2 (wordBits x.2.2.1 v.1) + +/-- **Direct summation as a recursion scheme.** The sum (kind `0`) has the `2 ^ m` assignments as +children, adding their values modulo `2 ^ P`; an assignment (kind `1`) has the entries of the +vertices as children, multiplying them modulo `2 ^ P`; an entry (kind `2`) is a leaf. The +accumulator is a counter and a residue. -/ +def sumScheme : Scheme (Node T) (ℕ × ℕ) ℕ where + isLeaf x := x.1 == 2 + leaf := entryOf eval + start x := (0, (if x.1 = 0 then 0 else 1) % 2 ^ x.2.1.1) + next x a := + if x.1 = 0 then + (if a.1 < 2 ^ x.2.1.2.numEdges then some (1, (x.2.1, (lowBits x.2.1.2.numEdges a.1, 0))) + else none) + else if x.1 = 1 then + (if a.1 < x.2.1.2.vertices.length then + some (2, (x.2.1, (x.2.2.1, min x.2.1.2.vertices.length a.1))) else none) + else none + absorb x a y := (a.1 + 1, if x.1 = 0 then (a.2 + y) % 2 ^ x.2.1.1 else a.2 * y % 2 ^ x.2.1.1) + finish _ a := a.2 + +/-- The root of direct summation on `(P, d)`. -/ +def sumRoot (q : ℕ × DescribedNetwork T) : Node T := (0, (q, ([], 0))) + +/-- The weight of a word modulo `2 ^ P`: the product of the entries at its bits, reduced after +each factor. -/ +def weightMod (P : ℕ) (d : DescribedNetwork T) (word : List Bool) : ℕ := + d.vertices.foldl (fun acc v => acc * eval v.2 (wordBits word v.1) % 2 ^ P) (1 % 2 ^ P) + +/-- The shape of a node of direct summation on `q`: it keeps `q`, its kind is at most `2`, its +word has at most `m` bits and its index is at most the number of vertices. -/ +def NodeShape (q : ℕ × DescribedNetwork T) (x : Node T) : Prop := + x.2.1 = q ∧ x.1 ≤ 2 ∧ x.2.2.1.length ≤ q.2.numEdges ∧ x.2.2.2 ≤ q.2.vertices.length + +/-- The invariant of direct summation on `q = (P, d)`: nodes have the shape of `NodeShape`, frames +also have a counter at most `2 ^ m + k` and a residue below `2 ^ P`, and every value is a residue +below `2 ^ P` or an entry of a vertex at the bits of an `m`-bit word. -/ +def sumInvariant (q : ℕ × DescribedNetwork T) : Invariant (Node T) (ℕ × ℕ) ℕ := + ⟨NodeShape q, fun x a => NodeShape q x ∧ a.1 ≤ 2 ^ q.2.numEdges + q.2.vertices.length ∧ + a.2 < 2 ^ q.1, + fun y => y < 2 ^ q.1 ∨ ∃ v ∈ q.2.vertices, ∃ w : List Bool, w.length = q.2.numEdges ∧ + y = eval v.2 (wordBits w v.1)⟩ + +variable {eval} + +/-- An entry is a leaf. -/ +theorem eval_entry (q : ℕ × DescribedNetwork T) {word : List Bool} {v : ℕ} + (hw : word.length = q.2.numEdges) (hv : v < q.2.vertices.length) : + (sumScheme eval).Eval (sumInvariant eval q) (2, (q, (word, v))) + (entryOf eval (2, (q, (word, v)))) 1 0 := by + refine Scheme.Eval.leaf (R := sumScheme eval) ⟨rfl, by omega, hw.le, hv.le⟩ rfl + (.inr ⟨q.2.vertices[v], List.getElem_mem hv, word, hw, ?_⟩) + change (q.2.vertices[v]?).elim 0 _ = _ + rw [List.getElem?_eq_getElem hv] + rfl + +private theorem foldl_take_succ (d : DescribedNetwork T) (P : ℕ) (word : List Bool) (c : ℕ) + (hc : c < d.vertices.length) : + (d.vertices.take (c + 1)).foldl (fun acc v => acc * eval v.2 (wordBits word v.1) % 2 ^ P) + (1 % 2 ^ P) = + (d.vertices.take c).foldl (fun acc v => acc * eval v.2 (wordBits word v.1) % 2 ^ P) + (1 % 2 ^ P) * entryOf eval (2, ((P, d), (word, c))) % 2 ^ P := by + rw [List.take_add_one, List.getElem?_eq_getElem hc, Option.toList_some, List.foldl_append] + simp [entryOf, List.getElem?_eq_getElem hc] + +private theorem foldl_mod_lt {α : Type} (f : α → ℕ) (P : ℕ) (l : List α) : + l.foldl (fun acc v => acc * f v % 2 ^ P) (1 % 2 ^ P) < 2 ^ P := by + have h (a : ℕ) (ha : a < 2 ^ P) : l.foldl (fun acc v => acc * f v % 2 ^ P) a < 2 ^ P := by + induction l generalizing a with + | nil => exact ha + | cons v l ih => exact ih _ (Nat.mod_lt _ (Nat.two_pow_pos P)) + exact h _ (Nat.mod_lt _ (Nat.two_pow_pos P)) + +/-- **An assignment evaluates to the weight of its word**, with one node per vertex plus one +and one open call. -/ +theorem eval_assign (P : ℕ) (d : DescribedNetwork T) {word : List Bool} + (hw : word.length = d.numEdges) : + ∃ h ≤ 1, (sumScheme eval).Eval (sumInvariant eval (P, d)) (1, ((P, d), (word, 0))) + (weightMod eval P d word) (d.vertices.length + 1) h := by + set acc : ℕ → ℕ × ℕ := fun c => (c, (d.vertices.take c).foldl + (fun acc v => acc * eval v.2 (wordBits word v.1) % 2 ^ P) (1 % 2 ^ P)) + have hshape : NodeShape (P, d) ((1, ((P, d), (word, 0))) : Node T) := + ⟨rfl, by omega, hw.le, Nat.zero_le _⟩ + obtain ⟨h, hh, hloop⟩ := Scheme.Loop.counted (R := sumScheme eval) + (I := sumInvariant eval (P, d)) + (x := (1, ((P, d), (word, 0)))) (acc := acc) + (child := fun c => (2, ((P, d), (word, c)))) + (val := fun c => entryOf eval (2, ((P, d), (word, c)))) + (nodes := fun _ => 1) (height := fun _ => 0) d.vertices.length 0 + (fun c hc => by simp [sumScheme, acc, hc, min_eq_right hc.le]) + (by simp [sumScheme, acc]) + (fun c hc => by + simp only [sumScheme, acc, one_ne_zero, ite_false] + rw [foldl_take_succ d P word c hc]) + (fun c hc => eval_entry (P, d) hw hc) + (fun c hc => ⟨hshape, (Nat.le_of_lt hc).trans (Nat.le_add_left _ _), foldl_mod_lt _ _ _⟩) + (fun _ _ => le_rfl) + have hstart : (sumScheme eval).start (1, ((P, d), (word, 0))) = acc 0 := by + simp [sumScheme, acc] + rw [← hstart] at hloop + refine ⟨h + 1, by omega, ?_⟩ + have := Scheme.Eval.call (R := sumScheme eval) (I := sumInvariant eval (P, d)) + (x := (1, ((P, d), (word, 0)))) hshape rfl hloop (.inl (foldl_mod_lt _ _ _)) + simpa [sumScheme, acc, weightMod, List.take_length, Finset.sum_const, Finset.card_range] using + this + +private theorem sum_lowBits (n : ℕ) (g : List Bool → ℕ) : + ∑ j ∈ range (2 ^ n), g (lowBits n j) = ∑ x : Fin n → Bool, g (List.ofFn x) := by + rw [← Fin.sum_univ_eq_sum_range] + exact Fintype.sum_equiv (equivFin n).symm _ _ fun k => by + rw [lowBits_eq_ofFn_equivFin_symm] + +private theorem foldl_mul_mod {α : Type} (f : α → ℕ) (m : ℕ) (l : List α) (a : ℕ) : + l.foldl (fun acc v => acc * f v % m) (a % m) = a * (l.map f).prod % m := by + induction l generalizing a with + | nil => simp + | cons v l ih => + rw [List.foldl_cons, Nat.mod_mul_mod, ih, List.map_cons, List.prod_cons, Nat.mul_assoc] + +private theorem weightMod_eq (P : ℕ) (d : DescribedNetwork T) (word : List Bool) : + weightMod eval P d word = + (d.vertices.map fun v => eval v.2 (wordBits word v.1)).prod % 2 ^ P := by + rw [weightMod, foldl_mul_mod, Nat.one_mul] + +/-- **Direct summation computes the contraction modulo `2 ^ P`**, with `2 ^ m (k + 1) + 1` +nodes for `m` edges and `k` vertices, and at most two open calls. -/ +theorem eval_sumRoot (P : ℕ) (d : DescribedNetwork T) : + ∃ h ≤ 2, (sumScheme eval).Eval (sumInvariant eval (P, d)) (sumRoot (P, d)) + (d.contraction eval % 2 ^ P) (2 ^ d.numEdges * (d.vertices.length + 1) + 1) h := by + set acc : ℕ → ℕ × ℕ := fun c => (c, (∑ j ∈ range c, weightMod eval P d (lowBits d.numEdges j)) % + 2 ^ P) + have hassign (c : ℕ) := eval_assign (eval := eval) P d (length_lowBits d.numEdges c) + choose hgt hhgt heval using hassign + have hshape : NodeShape (P, d) (sumRoot (P, d)) := ⟨rfl, by simp [sumRoot], by simp [sumRoot], + by simp [sumRoot]⟩ + obtain ⟨h, hh, hloop⟩ := Scheme.Loop.counted (R := sumScheme eval) + (I := sumInvariant eval (P, d)) + (x := sumRoot (P, d)) (acc := acc) + (child := fun c => (1, ((P, d), (lowBits d.numEdges c, 0)))) + (val := fun c => weightMod eval P d (lowBits d.numEdges c)) + (nodes := fun _ => d.vertices.length + 1) (height := hgt) (2 ^ d.numEdges) 1 + (fun c hc => by simp [sumScheme, sumRoot, acc, hc]) + (by simp [sumScheme, sumRoot, acc]) + (fun c hc => by simp [sumScheme, sumRoot, acc, sum_range_succ, Nat.add_mod]) + (fun c _ => heval c) + (fun c hc => ⟨hshape, by simp only [acc]; omega, Nat.mod_lt _ (Nat.two_pow_pos P)⟩) + (fun c _ => hhgt c) + have hstart : (sumScheme eval).start (sumRoot (P, d)) = acc 0 := by + simp [sumScheme, sumRoot, acc] + rw [← hstart] at hloop + refine ⟨h + 1, by omega, ?_⟩ + have := Scheme.Eval.call (R := sumScheme eval) (I := sumInvariant eval (P, d)) + (x := sumRoot (P, d)) hshape rfl hloop (.inl (Nat.mod_lt _ (Nat.two_pow_pos P))) + have hval : (sumScheme eval).finish (sumRoot (P, d)) (acc (2 ^ d.numEdges)) = + d.contraction eval % 2 ^ P := by + simp only [sumScheme, acc, contraction] + rw [sum_lowBits d.numEdges (weightMod eval P d)] + simp only [weightMod_eq] + exact (Finset.sum_nat_mod _ _ _).symm + rw [hval, sum_const, card_range, smul_eq_mul] at this + exact this + +/-! ### The native machine -/ + +section Native + +open Turing.MultiTapeTM + +variable (encT : T ↪ List Bool) + +/-- A described network is its number of edges and its list of vertices. -/ +def equivProd : DescribedNetwork T ≃ ℕ × List (List ℕ × T) where + toFun d := (d.numEdges, d.vertices) + invFun p := ⟨p.1, p.2⟩ + left_inv _ := rfl + right_inv _ := rfl + +/-- **The encoding of a described network**: its number of edges in unary, then its vertices, +each the pair of its list of ports in binary and its descriptor. -/ +def encDescribed : DescribedNetwork T ↪ List Bool := + encOfEquiv equivProd (encPair encUnary (encList (encPair (encList encNat) encT))) + +/-- The encoding of an input `(P, d)`: the precision in unary and the network. -/ +abbrev encInput : ℕ × DescribedNetwork T ↪ List Bool := encPair encUnary (encDescribed encT) + +/-- The encoding of a node: its kind in unary, its input, its word and its vertex index in +unary. -/ +abbrev encNode : Node T ↪ List Bool := + encPair encUnary (encPair (encInput encT) (encPair encBits encUnary)) + +/-- The encoding of an accumulator: the counter and the residue, in binary. -/ +abbrev encAcc : ℕ × ℕ ↪ List Bool := encPair encNat encNat + +variable {encT} + +/-- The number of edges of a described network, in unary. -/ +theorem numEdges_polyTime : + ComputableInPolyTime (fun d : DescribedNetwork T => d.numEdges) (encDescribed encT) + encUnary := + (ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.of_eq (f := equivProd) fun _ => rfl) + +/-- The vertices of a described network. -/ +theorem vertices_polyTime : + ComputableInPolyTime (fun d : DescribedNetwork T => d.vertices) (encDescribed encT) + (encList (encPair (encList encNat) encT)) := + (ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.of_eq (f := equivProd) fun _ => rfl) + +/-- The kind of a node. -/ +theorem kind_polyTime : ComputableInPolyTime (fun x : Node T => x.1) (encNode encT) + encUnary := ComputableInPolyTime.fst _ _ + +/-- The input `(P, d)` of a node. -/ +theorem input_polyTime : ComputableInPolyTime (fun x : Node T => x.2.1) (encNode encT) + (encInput encT) := (ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _) + +/-- The precision of a node. -/ +theorem precision_polyTime : ComputableInPolyTime (fun x : Node T => x.2.1.1) + (encNode encT) encUnary := (ComputableInPolyTime.fst _ _).comp input_polyTime + +/-- The network of a node. -/ +theorem network_polyTime : ComputableInPolyTime (fun x : Node T => x.2.1.2) + (encNode encT) (encDescribed encT) := (ComputableInPolyTime.snd _ _).comp input_polyTime + +/-- The word of a node. -/ +theorem word_polyTime : ComputableInPolyTime (fun x : Node T => x.2.2.1) + (encNode encT) encBits := + (ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _).snd' + +/-- The vertex index of a node. -/ +theorem index_polyTime : ComputableInPolyTime (fun x : Node T => x.2.2.2) + (encNode encT) encUnary := + (ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.snd _ _).snd' + +/-- `2 ^ P`, from `P` in unary. -/ +private theorem twoPow {α : Type} {encIn : α ↪ List Bool} {P : α → ℕ} + (hP : ComputableInPolyTime P encIn encUnary) : + ComputableInPolyTime (fun a => 2 ^ P a) encIn encNat := + ComputableInPolyTime.binary_two_pow.comp hP + +/-- `x % 2 ^ P`, from `P` in unary. -/ +private theorem modTwoPow {α : Type} {encIn : α ↪ List Bool} {x P : α → ℕ} + (hx : ComputableInPolyTime x encIn encNat) (hP : ComputableInPolyTime P encIn encUnary) : + ComputableInPolyTime (fun a => x a % 2 ^ P a) encIn encNat := + ComputableInPolyTime.binary_mod.comp (hx.prod (twoPow hP)) + +/-- **The polynomial-time components of direct summation.** -/ +theorem sumScheme_polyTime : (sumScheme eval).PolyTime (encNode encT) encAcc encNat where + isLeaf := ComputableInPolyTime.beq kind_polyTime (ComputableInPolyTime.const 2) + start := by + refine (ComputableInPolyTime.const 0).prod (modTwoPow ?_ precision_polyTime) + refine (ComputableInPolyTime.ite (encMid := encNat) (ComputableInPolyTime.beq kind_polyTime + (ComputableInPolyTime.const 0)) (ComputableInPolyTime.const 0) + (ComputableInPolyTime.const 1)).of_enc_eq fun x => ?_ + by_cases h : x.1 = 0 <;> simp [h] + next := by + have hx := ComputableInPolyTime.fst (encNode encT) encAcc + have ha := ComputableInPolyTime.snd (encNode encT) encAcc + have hk := kind_polyTime.comp hx + have hc := (ComputableInPolyTime.fst encNat encNat).comp ha + have hq := input_polyTime.comp hx + have hd := network_polyTime.comp hx + have hm := numEdges_polyTime.comp hd + have hlen := (ComputableInPolyTime.length_list _).comp (vertices_polyTime.comp hd) + have hassign : ComputableInPolyTime (fun p : Node T × (ℕ × ℕ) => + (if p.2.1 < 2 ^ p.1.2.1.2.numEdges then + some ((1, (p.1.2.1, (lowBits p.1.2.1.2.numEdges p.2.1, 0))) : Node T) else none)) + (encPair (encNode encT) encAcc) (encOption (encNode encT)) := + (ComputableInPolyTime.ite (ComputableInPolyTime.binary_lt' hc (twoPow hm)) + ((ComputableInPolyTime.optionSome (encNode encT)).comp + ((ComputableInPolyTime.const (encOut := encUnary) 1).prod + (hq.prod ((BooleanFold.decoder_polyTime.comp (hm.prod hc)).prod + (ComputableInPolyTime.const (encOut := encUnary) 0))))) + (ComputableInPolyTime.const none)).of_enc_eq fun p => by + by_cases h : p.2.1 < 2 ^ p.1.2.1.2.numEdges <;> simp [h] + have hentry : ComputableInPolyTime (fun p : Node T × (ℕ × ℕ) => + (if p.2.1 < p.1.2.1.2.vertices.length then + some ((2, (p.1.2.1, (p.1.2.2.1, min p.1.2.1.2.vertices.length p.2.1))) : Node T) + else none)) + (encPair (encNode encT) encAcc) (encOption (encNode encT)) := + (ComputableInPolyTime.ite (ComputableInPolyTime.binary_lt' hc + (ComputableInPolyTime.unary_to_binary.comp hlen)) + ((ComputableInPolyTime.optionSome (encNode encT)).comp + ((ComputableInPolyTime.const (encOut := encUnary) 2).prod + (hq.prod ((word_polyTime.comp hx).prod + (ComputableInPolyTime.binary_min_unary' hlen hc))))) + (ComputableInPolyTime.const none)).of_enc_eq fun p => by + by_cases h : p.2.1 < p.1.2.1.2.vertices.length <;> simp [h] + refine (ComputableInPolyTime.ite (ComputableInPolyTime.beq hk (ComputableInPolyTime.const 0)) + hassign (ComputableInPolyTime.ite (ComputableInPolyTime.beq hk + (ComputableInPolyTime.const 1)) hentry (ComputableInPolyTime.const none))).of_enc_eq + fun p => ?_ + by_cases h0 : p.1.1 = 0 + · simp [sumScheme, h0] + · by_cases h1 : p.1.1 = 1 <;> simp [sumScheme, h0, h1] + absorb := by + have hx := (ComputableInPolyTime.fst (encNode encT) encAcc).comp + (ComputableInPolyTime.fst (encPair (encNode encT) encAcc) encNat) + have ha := (ComputableInPolyTime.snd (encNode encT) encAcc).comp + (ComputableInPolyTime.fst (encPair (encNode encT) encAcc) encNat) + have hy := ComputableInPolyTime.snd (encPair (encNode encT) encAcc) encNat + have hc := (ComputableInPolyTime.fst encNat encNat).comp ha + have hr := (ComputableInPolyTime.snd encNat encNat).comp ha + have hP := precision_polyTime.comp hx + refine (ComputableInPolyTime.binary_add.comp (hc.prod (ComputableInPolyTime.const 1))).prod + ((ComputableInPolyTime.ite (ComputableInPolyTime.beq (kind_polyTime.comp hx) + (ComputableInPolyTime.const 0)) + (modTwoPow (ComputableInPolyTime.binary_add.comp (hr.prod hy)) hP) + (modTwoPow (ComputableInPolyTime.binary_mul' hr hy) hP)).of_enc_eq fun q => ?_) + by_cases h : q.1.1.1 = 0 <;> simp [h] + finish := (ComputableInPolyTime.snd encNat encNat).comp (ComputableInPolyTime.snd _ _) + +/-- The descriptor of a vertex and the bits of the node's word on its ports. -/ +theorem query_polyTime : + ComputableInPolyTime (fun p : Node T × (List ℕ × T) => (p.2.2, wordBits p.1.2.2.1 p.2.1)) + (encPair (encNode encT) (encPair (encList encNat) encT)) (encPair encT encBits) := by + have hv := ComputableInPolyTime.snd (encNode encT) (encPair (encList encNat) encT) + have hports := (ComputableInPolyTime.fst (encList encNat) encT).comp hv + have hword := word_polyTime.comp (ComputableInPolyTime.fst (encNode encT) + (encPair (encList encNat) encT)) + let E := encPair (encNode encT) (encPair (encList encNat) encT) + have hbit : ComputableInPolyTime (fun z : (Node T × (List ℕ × T)) × ℕ => + z.1.1.2.2.1.getD z.2 false) (encPair E encNat) encBool := + ComputableInPolyTime.listGetD_binary (encA := encBool) (encL := encBits) false + (hword.comp (ComputableInPolyTime.fst E encNat)) (ComputableInPolyTime.snd E encNat) + have hbits := ComputableInPolyTime.listToBits.comp + (ComputableInPolyTime.mapWithInput (f := fun p i => p.1.2.2.1.getD i false) hports hbit) + exact ((ComputableInPolyTime.snd (encList encNat) encT).comp hv).prod hbits + +/-- The vertex of a node, if its index is in range. -/ +noncomputable def vertexCertificate : + NativeCertificate (fun x : Node T => x.2.1.2.vertices[x.2.2.2]?) (encNode encT) + (encOption (encPair (encList encNat) encT)) := + NativeCertificate.ofPolyTime (ComputableInPolyTime.getElem? + (vertices_polyTime.comp network_polyTime) index_polyTime) + +/-- The query to the evaluator: the descriptor and the bits on the ports. -/ +noncomputable def queryCertificate : + NativeCertificate (fun p : Node T × (List ℕ × T) => (p.2.2, wordBits p.1.2.2.1 p.2.1)) + (encPair (encNode encT) (encPair (encList encNat) encT)) (encPair encT encBits) := + NativeCertificate.ofPolyTime query_polyTime + +variable (eval) in +/-- **The leaf step**: the evaluator at the descriptor of the node's vertex and its bits, from a +native certificate of the evaluator with any bounds. -/ +noncomputable def leafCertificate + (ev : NativeCertificate (fun q : T × List Bool => eval q.1 q.2) (encPair encT encBits) + encNat) : + NativeCertificate (sumScheme eval).leaf (encNode encT) encNat := + NativeCertificate.option (value := fun x : Node T => x.2.1.2.vertices[x.2.2.2]?) + (fallback := fun _ => 0) (body := fun p => eval p.2.2 (wordBits p.1.2.2.1 p.2.1)) + vertexCertificate (NativeCertificate.const 0) (ev.comp queryCertificate) + +/-- The time of the leaf step: the vertex lookup, and the query and the evaluator at a vertex. -/ +theorem leafCertificate_time + (ev : NativeCertificate (fun q : T × List Bool => eval q.1 q.2) (encPair encT encBits) + encNat) (x : Node T) : + (leafCertificate eval ev).time x = 2 * (vertexCertificate (encT := encT)).time x + + (encNode encT x).length + + (x.2.1.2.vertices[x.2.2.2]?).elim (encNode encT x).length + fun v => (queryCertificate (encT := encT)).time (x, v) + + ev.time (v.2, wordBits x.2.2.1 v.1) := rfl + +/-- The space of the leaf step. -/ +theorem leafCertificate_space + (ev : NativeCertificate (fun q : T × List Bool => eval q.1 q.2) (encPair encT encBits) + encNat) (x : Node T) : + (leafCertificate eval ev).space x = 2 * (vertexCertificate (encT := encT)).space x + + (encNode encT x).length + + (x.2.1.2.vertices[x.2.2.2]?).elim (encNode encT x).length + fun v => (queryCertificate (encT := encT)).space (x, v) + + ev.space (v.2, wordBits x.2.2.1 v.1) := rfl + +/-- The number of steps of direct summation: `2 (2 ^ m (k + 1) + 1) - 1`. -/ +def fuel (q : ℕ × DescribedNetwork T) : ℕ := + 2 * (2 ^ q.2.numEdges * (q.2.vertices.length + 1)) + 1 + +/-- The fuel in polynomial time. -/ +theorem fuel_polyTime : ComputableInPolyTime (fuel (T := T)) (encInput encT) encNat := by + have hd := ComputableInPolyTime.snd encUnary (encDescribed encT) + have hm := numEdges_polyTime.comp hd + have hlen := (ComputableInPolyTime.length_list _).comp (vertices_polyTime.comp hd) + exact ComputableInPolyTime.binary_add.comp ((ComputableInPolyTime.binary_mul' + (ComputableInPolyTime.const 2) (ComputableInPolyTime.binary_mul' (twoPow hm) + (ComputableInPolyTime.unary_to_binary.comp (ComputableInPolyTime.unary_add' hlen + (ComputableInPolyTime.const 1))))).prod (ComputableInPolyTime.const 1)) + +/-- The root in polynomial time. -/ +theorem sumRoot_polyTime : ComputableInPolyTime (sumRoot (T := T)) (encInput encT) + (encNode encT) := + (ComputableInPolyTime.const 0).prod (ComputableInPolyTime.id'.prod + (ComputableInPolyTime.const ([], 0))) + +variable (eval) in +/-- **One native machine for direct summation over described networks**, from a native +certificate of the evaluator. It returns `some (d.contraction eval % 2 ^ P)` +(`run_sumScheme`). -/ +noncomputable def sumCertificate + (ev : NativeCertificate (fun q : T × List Bool => eval q.1 q.2) (encPair encT encBits) + encNat) : + NativeCertificate ((sumScheme eval).run fuel sumRoot) (encInput encT) (encOption encNat) := + Scheme.certificate sumScheme_polyTime (leafCertificate eval ev) + (NativeCertificate.ofPolyTime fuel_polyTime) (NativeCertificate.ofPolyTime sumRoot_polyTime) + +/-- **The machine computes the contraction modulo `2 ^ P`.** -/ +theorem run_sumScheme (q : ℕ × DescribedNetwork T) : + (sumScheme eval).run fuel sumRoot q = some (q.2.contraction eval % 2 ^ q.1) := by + obtain ⟨h, -, he⟩ := eval_sumRoot (eval := eval) q.1 q.2 + exact Scheme.run_eq_some he (by simp [fuel]; omega) + +variable (eval) in +/-- **Direct summation over described networks, as a native certificate** for the contraction +modulo `2 ^ P` on every input `(P, d)`, from a native certificate of the evaluator. -/ +noncomputable def contractionCertificate + (ev : NativeCertificate (fun q : T × List Bool => eval q.1 q.2) (encPair encT encBits) + encNat) : + NativeCertificate (fun q : ℕ × DescribedNetwork T => q.2.contraction eval % 2 ^ q.1) + (encInput encT) encNat := + (NativeCertificate.post (sumCertificate eval ev) + (ComputableInDegree.getD (enc₁ := encNat) (enc := encOption encNat) 0).inO_one).congr + fun q => by simp [run_sumScheme] + +/-- The time is that of the stack machine. -/ +@[simp] theorem contractionCertificate_time + (ev : NativeCertificate (fun q : T × List Bool => eval q.1 q.2) (encPair encT encBits) + encNat) : + (contractionCertificate eval ev).time = (sumCertificate eval ev).time := rfl + +/-- The space is that of the stack machine. -/ +@[simp] theorem contractionCertificate_space + (ev : NativeCertificate (fun q : T × List Bool => eval q.1 q.2) (encPair encT encBits) + encNat) : + (contractionCertificate eval ev).space = (sumCertificate eval ev).space := rfl + +/-! ### Resources -/ + +/-- The number of edges and the number of vertices are at most the encoded length. -/ +theorem length_numEdges_vertices_le (d : DescribedNetwork T) : + d.numEdges + d.vertices.length ≤ (encDescribed encT d).length := by + have h := length_le_length_encList (encPair (encList encNat) encT) d.vertices + change d.numEdges + d.vertices.length ≤ + (encPair encUnary (encList (encPair (encList encNat) encT)) (d.numEdges, d.vertices)).length + simp only [length_encPair, encUnary_apply, List.length_replicate] + omega + +/-- A node of the right shape is at most `5 n + 7` long, for `n` the length of the input. -/ +theorem length_encNode_le {q : ℕ × DescribedNetwork T} {x : Node T} (hx : NodeShape q x) : + (encNode encT x).length ≤ 5 * (encInput encT q).length + 7 := by + obtain ⟨hq, hk, hw, hv⟩ := hx + obtain ⟨k, ⟨P, d⟩, w, v⟩ := x + simp only at hq hk hw hv + subst hq + dsimp only at hw hv + have hd := length_numEdges_vertices_le (encT := encT) d + simp only [length_encPair, encUnary_apply, List.length_replicate, encBits_apply] + omega + +private theorem term_le {c a b d D z : ℕ} (hd : d ≤ D) : + c * (a * z + b) ^ d ≤ c * (a + b) ^ d * (z + 1) ^ D := + calc c * (a * z + b) ^ d ≤ c * ((a + b) * (z + 1)) ^ d := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by nlinarith) _) + _ = c * (a + b) ^ d * (z + 1) ^ d := by rw [Nat.mul_pow]; ring + _ ≤ c * (a + b) ^ d * (z + 1) ^ D := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (Nat.succ_pos _) hd) + +private theorem length_encNat_lt {y P : ℕ} (h : y < 2 ^ P) : (encNat y).length ≤ P := by + have h' := Nat.size_le.mpr h + rw [← Nat.size_eq_bits_len] at h' + exact h' + +/-- **The resources of direct summation over described networks.** There is `K` such that, for +an input `(P, d)` of length `n` with `m` edges and `k` vertices, if the evaluator takes time at +most `E` and space at most `ES` and outputs at most `Ev` bits on every vertex and every list of +bits on its ports, then the time is at most `2 ^ m (k + 1) + 1` times +`K (n + Ev + 1) ^ K + 2 E`, and the space at most `K (n + Ev + 1) ^ K + ES`. -/ +theorem contractionCertificate_le + (ev : NativeCertificate (fun q : T × List Bool => eval q.1 q.2) (encPair encT encBits) + encNat) : + ∃ K : ℕ, ∀ (q : ℕ × DescribedNetwork T) (E ES Ev : ℕ), + (∀ v ∈ q.2.vertices, ∀ bs : List Bool, bs.length = v.1.length → + ev.time (v.2, bs) ≤ E ∧ ev.space (v.2, bs) ≤ ES ∧ (encNat (eval v.2 bs)).length ≤ Ev) → + (contractionCertificate eval ev).time q ≤ + (2 ^ q.2.numEdges * (q.2.vertices.length + 1) + 1) * + (K * ((encInput encT q).length + Ev + 1) ^ K + 2 * E) ∧ + (contractionCertificate eval ev).space q ≤ + K * ((encInput encT q).length + Ev + 1) ^ K + ES := by + obtain ⟨K₀, hK₀⟩ := Scheme.certificate_le (sumScheme_polyTime (eval := eval) (encT := encT)) + (leafCertificate eval ev) + have hV : (vertexCertificate (encT := encT)).IsPolynomial := + NativeCertificate.ofPolyTime_isPolynomial _ + have hQ : (queryCertificate (encT := encT)).IsPolynomial := + NativeCertificate.ofPolyTime_isPolynomial _ + have hF := NativeCertificate.ofPolyTime_isPolynomial (fuel_polyTime (encT := encT)) + have hR := NativeCertificate.ofPolyTime_isPolynomial (sumRoot_polyTime (encT := encT)) + obtain ⟨cv, dv, hvt⟩ := hV.1.exists_le + obtain ⟨cv', dv', hvs⟩ := hV.2.exists_le + obtain ⟨cq, dq, hqt⟩ := hQ.1.exists_le + obtain ⟨cq', dq', hqs⟩ := hQ.2.exists_le + obtain ⟨cf, df, hft⟩ := hF.1.exists_le + obtain ⟨cf', df', hfs⟩ := hF.2.exists_le + obtain ⟨cr, dr, hrt⟩ := hR.1.exists_le + obtain ⟨cr', dr', hrs⟩ := hR.2.exists_le + obtain ⟨D, hD⟩ : ∃ D, D = K₀ + dv + dv' + dq + dq' + df + df' + dr + dr' + 2 := ⟨_, rfl⟩ + obtain ⟨G, hG⟩ : ∃ G, G = K₀ * 96 ^ K₀ + (2 * cv * 13 ^ dv + 24 + cq * 27 ^ dq) + 16 := + ⟨_, rfl⟩ + obtain ⟨G', hG'⟩ : ∃ G', G' = K₀ * 96 ^ K₀ + (2 * cv' * 13 ^ dv' + 24 + cq' * 27 ^ dq') := + ⟨_, rfl⟩ + obtain ⟨C, hC⟩ : ∃ C, C = cf + cr + cf' + cr' + 2 * G + G' + 4 := ⟨_, rfl⟩ + refine ⟨C + D, fun q E ES Ev hE => ?_⟩ + obtain ⟨P, d⟩ := q + obtain ⟨n, hn⟩ : ∃ n, n = (encInput encT (P, d)).length := ⟨_, rfl⟩ + obtain ⟨z, hz⟩ : ∃ z, z = n + Ev := ⟨_, rfl⟩ + obtain ⟨W, hW⟩ : ∃ W, W = (z + 1) ^ D := ⟨_, rfl⟩ + rw [← hn] + rw [show n + Ev + 1 = z + 1 by omega] + have hnP : 2 * P + 1 + (encDescribed encT d).length = n := by + rw [hn]; simp [encInput] + have hmk := length_numEdges_vertices_le (encT := encT) d + -- Every vertex is at most `n` long. + have hvlen (v : List ℕ × T) (hv : v ∈ d.vertices) : + (encPair (encList encNat) encT v).length ≤ n := by + have h1 := List.le_sum_of_mem (List.mem_map_of_mem (f := fun a => + (encPair (encList encNat) encT a).length) hv) + have h2 := sum_length_le_length_encList (encPair (encList encNat) encT) d.vertices + have h3 : (encList (encPair (encList encNat) encT) d.vertices).length ≤ + (encDescribed encT d).length := by + change _ ≤ (encPair encUnary (encList (encPair (encList encNat) encT)) + (d.numEdges, d.vertices)).length + simp only [length_encPair]; omega + omega + have hnode (x : Node T) (hx : (sumInvariant eval (P, d)).node x) : + (encNode encT x).length ≤ 5 * z + 7 := (length_encNode_le hx).trans (by omega) + have hleafT (x : Node T) (hx : (sumInvariant eval (P, d)).node x) : + (leafCertificate eval ev).time x ≤ + 2 * cv * (5 * z + 8) ^ dv + 2 * (5 * z + 7) + cq * (11 * z + 16) ^ dq + E := by + have h1 := hnode x hx + rw [leafCertificate_time] + have h2 : (vertexCertificate (encT := encT)).time x ≤ cv * (5 * z + 8) ^ dv := + (hvt x).trans (Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) _)) + have h2' : 2 * (vertexCertificate (encT := encT)).time x ≤ 2 * cv * (5 * z + 8) ^ dv := by + rw [Nat.mul_assoc]; exact Nat.mul_le_mul_left 2 h2 + cases hvx : x.2.1.2.vertices[x.2.2.2]? with + | none => simp only [Option.elim]; omega + | some v => + simp only [Option.elim] + have hmem : v ∈ x.2.1.2.vertices := List.mem_of_getElem? hvx + obtain ⟨hq, -, -, -⟩ := hx + rw [hq] at hmem + have h3 := hvlen v hmem + have h4 : (queryCertificate (encT := encT)).time (x, v) ≤ cq * (11 * z + 16) ^ dq := by + refine (hqt (x, v)).trans (Nat.mul_le_mul_left _ (Nat.pow_le_pow_left ?_ _)) + have := length_encPair (enc₁ := encNode encT) (enc₂ := encPair (encList encNat) encT) + (x, v) + dsimp only at this + omega + have h5 := (hE v hmem (wordBits x.2.2.1 v.1) (by simp [wordBits])).1 + omega + have hleafS (x : Node T) (hx : (sumInvariant eval (P, d)).node x) : + (leafCertificate eval ev).space x ≤ + 2 * cv' * (5 * z + 8) ^ dv' + 2 * (5 * z + 7) + cq' * (11 * z + 16) ^ dq' + ES := by + have h1 := hnode x hx + rw [leafCertificate_space] + have h2 : (vertexCertificate (encT := encT)).space x ≤ cv' * (5 * z + 8) ^ dv' := + (hvs x).trans (Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) _)) + have h2' : 2 * (vertexCertificate (encT := encT)).space x ≤ 2 * cv' * (5 * z + 8) ^ dv' := by + rw [Nat.mul_assoc]; exact Nat.mul_le_mul_left 2 h2 + cases hvx : x.2.1.2.vertices[x.2.2.2]? with + | none => simp only [Option.elim]; omega + | some v => + simp only [Option.elim] + have hmem : v ∈ x.2.1.2.vertices := List.mem_of_getElem? hvx + obtain ⟨hq, -, -, -⟩ := hx + rw [hq] at hmem + have h3 := hvlen v hmem + have h4 : (queryCertificate (encT := encT)).space (x, v) ≤ cq' * (11 * z + 16) ^ dq' := by + refine (hqs (x, v)).trans (Nat.mul_le_mul_left _ (Nat.pow_le_pow_left ?_ _)) + have := length_encPair (enc₁ := encNode encT) (enc₂ := encPair (encList encNat) encT) + (x, v) + dsimp only at this + omega + have h5 := (hE v hmem (wordBits x.2.2.1 v.1) (by simp [wordBits])).2.1 + omega + obtain ⟨h, hh, he⟩ := eval_sumRoot (eval := eval) P d + have hres := hK₀ (NativeCertificate.ofPolyTime fuel_polyTime) + (NativeCertificate.ofPolyTime sumRoot_polyTime) (sumInvariant eval (P, d)) (13 * z + 18) + (2 * cv * (5 * z + 8) ^ dv + 2 * (5 * z + 7) + cq * (11 * z + 16) ^ dq + E) + (2 * cv' * (5 * z + 8) ^ dv' + 2 * (5 * z + 7) + cq' * (11 * z + 16) ^ dq' + ES) + (fun x hx => ⟨(hnode x hx).trans (by omega), fun _ => ⟨hleafT x hx, hleafS x hx⟩⟩) + (fun x a ha => by + obtain ⟨hx, ha1, ha2⟩ := ha + have h1 := hnode x hx + have h2 : (encNat a.1).length ≤ d.numEdges + d.vertices.length + 1 := by + refine length_encNat_lt (lt_of_le_of_lt ha1 ?_) + calc 2 ^ d.numEdges + d.vertices.length + < 2 ^ d.numEdges + 2 ^ d.vertices.length := by + have := Nat.lt_two_pow_self (n := d.vertices.length); omega + _ ≤ 2 ^ (d.numEdges + d.vertices.length + 1) := by + rw [pow_succ, pow_add, Nat.mul_two] + exact Nat.add_le_add (Nat.le_mul_of_pos_right _ (Nat.two_pow_pos _)) + (Nat.le_mul_of_pos_left _ (Nat.two_pow_pos _)) + have h3 := length_encNat_lt ha2 + have h4 : (encPair (encNode encT) encAcc (x, a)).length = + 2 * (encNode encT x).length + 1 + (encAcc a).length := length_encPair (x, a) + have h5 : (encAcc a).length = 2 * (encNat a.1).length + 1 + (encNat a.2).length := + length_encPair a + omega) + (fun y hy => by + rcases hy with hy | ⟨v, hv, w, -, rfl⟩ + · have := length_encNat_lt hy; omega + · have := (hE v hv (wordBits w v.1) (by simp [wordBits])).2.2; omega) + (P, d) _ _ _ he + rw [← hn] at hres + -- The clock and the size of the fuel. + have hfuel : fuel (P, d) < 2 ^ (d.numEdges + d.vertices.length + 2) := by + have hk : d.vertices.length + 1 ≤ 2 ^ d.vertices.length := Nat.lt_two_pow_self + have h1 : 2 ^ d.numEdges * (d.vertices.length + 1) ≤ 2 ^ (d.numEdges + d.vertices.length) := + by rw [pow_add]; exact Nat.mul_le_mul_left _ hk + have h2 : 2 ^ (d.numEdges + d.vertices.length + 2) = 4 * 2 ^ (d.numEdges + d.vertices.length) := + by rw [pow_add]; ring + have h3 := Nat.two_pow_pos (d.numEdges + d.vertices.length) + simp only [fuel] + omega + have hfl := length_encNat_lt hfuel + obtain ⟨B, hB⟩ : ∃ B, B = 2 ^ d.numEdges * (d.vertices.length + 1) + 1 := ⟨_, rfl⟩ + have hfuel1 : fuel (P, d) + 1 = 2 * B := by rw [hB]; simp only [fuel]; ring + have hB1 : 1 ≤ B := by omega + rw [← hB] + -- The polynomial parts, each at most a constant times `W`. + have hW1 : z + 1 ≤ W := by + rw [hW] + calc z + 1 = (z + 1) ^ 1 := (pow_one _).symm + _ ≤ (z + 1) ^ D := Nat.pow_le_pow_right (Nat.succ_pos _) (by omega) + have hpoly {c e : ℕ} (he : e ≤ D) : c * (n + 1) ^ e ≤ c * W := by + rw [hW] + exact Nat.mul_le_mul_left _ ((Nat.pow_le_pow_left (by omega) _).trans + (Nat.pow_le_pow_right (Nat.succ_pos _) he)) + have hterm {c a b e : ℕ} (he : e ≤ D) : c * (a * z + b) ^ e ≤ c * (a + b) ^ e * W := by + rw [hW]; exact term_le he + have hT1 : K₀ * ((h + 1) * (13 * z + 18 + 1)) ^ K₀ ≤ K₀ * 96 ^ K₀ * W := by + have h3 : (h + 1) * (13 * z + 18 + 1) ≤ 39 * z + 57 := by + have := Nat.mul_le_mul_right (13 * z + 18 + 1) (show h + 1 ≤ 3 by omega); omega + exact (Nat.mul_le_mul_left _ (Nat.pow_le_pow_left h3 _)).trans (hterm (by omega)) + have hTL : 2 * cv * (5 * z + 8) ^ dv + 2 * (5 * z + 7) + cq * (11 * z + 16) ^ dq ≤ + (2 * cv * 13 ^ dv + 24 + cq * 27 ^ dq) * W := by + have a1 := hterm (c := 2 * cv) (a := 5) (b := 8) (show dv ≤ D by omega) + have a2 := hterm (c := cq) (a := 11) (b := 16) (show dq ≤ D by omega) + have e : (2 * cv * 13 ^ dv + 24 + cq * 27 ^ dq) * W = + 2 * cv * (5 + 8) ^ dv * W + 24 * W + cq * (11 + 16) ^ dq * W := by ring + omega + have hSL : 2 * cv' * (5 * z + 8) ^ dv' + 2 * (5 * z + 7) + cq' * (11 * z + 16) ^ dq' ≤ + (2 * cv' * 13 ^ dv' + 24 + cq' * 27 ^ dq') * W := by + have a1 := hterm (c := 2 * cv') (a := 5) (b := 8) (show dv' ≤ D by omega) + have a2 := hterm (c := cq') (a := 11) (b := 16) (show dq' ≤ D by omega) + have e : (2 * cv' * 13 ^ dv' + 24 + cq' * 27 ^ dq') * W = + 2 * cv' * (5 + 8) ^ dv' * W + 24 * W + cq' * (11 + 16) ^ dq' * W := by ring + omega + have hclock : ((encNat (fuel (P, d))).length + 1) ^ 2 ≤ 16 * W := by + have h3 : (encNat (fuel (P, d))).length + 1 ≤ 4 * (z + 1) := by omega + calc ((encNat (fuel (P, d))).length + 1) ^ 2 ≤ (4 * (z + 1)) ^ 2 := Nat.pow_le_pow_left h3 2 + _ = 16 * (z + 1) ^ 2 := by ring + _ ≤ 16 * W := by + rw [hW]; exact Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (Nat.succ_pos _) (by omega)) + have hCD : C * W ≤ (C + D) * (z + 1) ^ (C + D) := by + rw [hW]; exact Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right (Nat.succ_pos _) (by omega)) + obtain ⟨htime, hspace⟩ := hres + have hft' := hft (P, d) + have hrt' := hrt (P, d) + have hfs' := hfs (P, d) + have hrs' := hrs (P, d) + rw [← hn] at hft' hrt' hfs' hrs' + have hcf := hft'.trans (hpoly (c := cf) (show df ≤ D by omega)) + have hcr := hrt'.trans (hpoly (c := cr) (show dr ≤ D by omega)) + have hcf' := hfs'.trans (hpoly (c := cf') (show df' ≤ D by omega)) + have hcr' := hrs'.trans (hpoly (c := cr') (show dr' ≤ D by omega)) + constructor + · rw [hfuel1] at htime + obtain ⟨S, hS⟩ : ∃ S, S = K₀ * ((h + 1) * (13 * z + 18 + 1)) ^ K₀ + + (2 * cv * (5 * z + 8) ^ dv + 2 * (5 * z + 7) + cq * (11 * z + 16) ^ dq + E) + + ((encNat (fuel (P, d))).length + 1) ^ 2 := ⟨_, rfl⟩ + rw [← hS] at htime + have hstep : S ≤ G * W + E := by + have e : G * W = K₀ * 96 ^ K₀ * W + (2 * cv * 13 ^ dv + 24 + cq * 27 ^ dq) * W + 16 * W := by + rw [hG]; ring + omega + have hm := Nat.mul_le_mul_left (2 * B) hstep + calc (contractionCertificate eval ev).time (P, d) + ≤ cf * W + cr * W + 2 * W + 2 * B * (G * W + E) := by + rw [contractionCertificate_time]; unfold sumCertificate; omega + _ ≤ B * ((cf + cr + 2) * W) + B * (2 * G * W) + 2 * B * E := by + have e2 : 2 * B * (G * W + E) = B * (2 * G * W) + 2 * B * E := by ring + have e3 : cf * W + cr * W + 2 * W = (cf + cr + 2) * W := by ring + have e4 : (cf + cr + 2) * W ≤ B * ((cf + cr + 2) * W) := Nat.le_mul_of_pos_left _ hB1 + omega + _ = B * ((cf + cr + 2 + 2 * G) * W) + 2 * B * E := by ring + _ ≤ B * (C * W) + 2 * B * E := + Nat.add_le_add_right (Nat.mul_le_mul_left B (Nat.mul_le_mul_right W (by omega))) _ + _ = B * (C * W + 2 * E) := by ring + _ ≤ B * ((C + D) * (z + 1) ^ (C + D) + 2 * E) := + Nat.mul_le_mul_left _ (Nat.add_le_add_right hCD _) + · have h1 : (contractionCertificate eval ev).space (P, d) ≤ C * W + ES := by + rw [contractionCertificate_space] + unfold sumCertificate + have e : C * W = cf * W + cr * W + cf' * W + cr' * W + 2 * G * W + G' * W + 4 * W := by + rw [hC]; ring + have e' : G' * W = K₀ * 96 ^ K₀ * W + (2 * cv' * 13 ^ dv' + 24 + cq' * 27 ^ dq') * W := by + rw [hG']; ring + have hfl' : (encNat (fuel (P, d))).length ≤ W := by omega + omega + exact h1.trans (Nat.add_le_add_right hCD _) + +end Native + +end DescribedNetwork + +end Cslib.Circuits.Frontier diff --git a/ComplexityTests/DescribedContraction.lean b/ComplexityTests/DescribedContraction.lean new file mode 100644 index 000000000..7581ad62a --- /dev/null +++ b/ComplexityTests/DescribedContraction.lean @@ -0,0 +1,79 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Circuit.Frontier.TensorNetwork.DescribedContraction +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListBinaryLookup +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives + +/-! # Direct summation over described networks + +Tables as descriptors, with table lookup as the evaluator: the stack machine on a one-edge +network, the agreement with explicit networks, and one native machine for the contraction with +its resource theorem. -/ + +namespace ComplexityTests.DescribedContraction + +open Cslib.Circuits.Frontier Cslib.Circuits.Frontier.DescribedNetwork Cslib.BitString + Turing.MultiTapeTM + +/-- One edge between two vertices with tables `[2, 3]` and `[5, 7]`: contraction +`2 * 5 + 3 * 7 = 31`. -/ +def oneEdge : DescribedNetwork (List ℕ) := ⟨1, [([0], [2, 3]), ([0], [5, 7])]⟩ + +example : oneEdge.contraction ExplicitTensorNetwork.entry = 31 := by decide + +-- The stack machine, with fuel `2 (2 ^ 1 * 3) + 1 = 13`, returns `31 % 16 = 15`. +example : (sumScheme ExplicitTensorNetwork.entry).run fuel sumRoot (4, oneEdge) = some 15 := by + decide + +-- With one step fewer, the sum still waits for the second assignment's weight +-- `3 * 7 = 21 ≡ 5`. +example : (sumScheme ExplicitTensorNetwork.entry).run (fun _ => 12) sumRoot (4, oneEdge) = + some 5 := by + decide + +-- On every input, the run is the contraction modulo `2 ^ P`, for any evaluator. +example {T : Type} (eval : T → List Bool → ℕ) (q : ℕ × DescribedNetwork T) : + (sumScheme eval).run fuel sumRoot q = some (q.2.contraction eval % 2 ^ q.1) := + run_sumScheme q + +-- Explicit networks are described networks with their tables. +example (d : ExplicitTensorNetwork ℕ) : + (ofExplicit d).contraction ExplicitTensorNetwork.entry = d.contraction := + contraction_ofExplicit d + +/-- Table lookup is polynomial-time. -/ +theorem entry_polyTime : ComputableInPolyTime (fun q : List ℕ × List Bool => + ExplicitTensorNetwork.entry q.1 q.2) (encPair (encList encNat) encBits) encNat := by + have hindex := ComputableInPolyTime.bitsBinaryValue.comp + (ComputableInPolyTime.bitsReverse.comp (ComputableInPolyTime.snd (encList encNat) encBits)) + refine (ComputableInPolyTime.listGetD_binary (encA := encNat) (encL := encList encNat) 0 + (ComputableInPolyTime.fst (encList encNat) encBits) hindex).of_enc_eq fun q => ?_ + simp only [Function.comp_def, ExplicitTensorNetwork.entry, lsbValue_eq_binaryValue_reverse] + +/-- **One native machine contracts explicit networks** given as described networks with their +tables, from the table-lookup certificate. -/ +noncomputable def tableCertificate : + Cslib.GenericRAM.NativeCertificate + (fun q : ℕ × DescribedNetwork (List ℕ) => + q.2.contraction ExplicitTensorNetwork.entry % 2 ^ q.1) + (encInput (encList encNat)) encNat := + contractionCertificate ExplicitTensorNetwork.entry + (Cslib.GenericRAM.NativeCertificate.ofPolyTime entry_polyTime) + +-- The resource theorem applies to it. +example : ∃ K : ℕ, ∀ (q : ℕ × DescribedNetwork (List ℕ)) (E ES Ev : ℕ), + (∀ v ∈ q.2.vertices, ∀ bs : List Bool, bs.length = v.1.length → + (Cslib.GenericRAM.NativeCertificate.ofPolyTime entry_polyTime).time (v.2, bs) ≤ E ∧ + (Cslib.GenericRAM.NativeCertificate.ofPolyTime entry_polyTime).space (v.2, bs) ≤ ES ∧ + (encNat (ExplicitTensorNetwork.entry v.2 bs)).length ≤ Ev) → + tableCertificate.time q ≤ (2 ^ q.2.numEdges * (q.2.vertices.length + 1) + 1) * + (K * ((encInput (encList encNat) q).length + Ev + 1) ^ K + 2 * E) ∧ + tableCertificate.space q ≤ K * ((encInput (encList encNat) q).length + Ev + 1) ^ K + ES := + contractionCertificate_le _ + +end ComplexityTests.DescribedContraction