diff --git a/Complexity.lean b/Complexity.lean index d15259fc91..8a4957adf7 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -929,8 +929,13 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DescribedL public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DirectContraction public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContraction +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionDerivation +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionLeaf public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionMachine public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionPolyTime +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionSchedule +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionShape +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionSize public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionStep public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IntegralCoordinates public import Complexity.Computability.Circuit.Frontier.TensorNetwork.KernelProduct @@ -938,6 +943,7 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.LocalDefor public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ModeExpansion public import Complexity.Computability.Circuit.Frontier.TensorNetwork.NativeCall public import Complexity.Computability.Circuit.Frontier.TensorNetwork.NativeChild +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.NativeChildBounds public import Complexity.Computability.Circuit.Frontier.TensorNetwork.NativeChildPolyTime public import Complexity.Computability.Circuit.Frontier.TensorNetwork.NativeRecovery public import Complexity.Computability.Circuit.Frontier.TensorNetwork.PacketEntry @@ -1140,6 +1146,8 @@ public import Complexity.Computability.Complexity.Classes.CountingSimulation.Ass public import Complexity.Computability.Complexity.Classes.CountingSimulation.BlockNetworks public import Complexity.Computability.Complexity.Classes.CountingSimulation.Containments public import Complexity.Computability.Complexity.Classes.CountingSimulation.FastAlgorithm +public import Complexity.Computability.Complexity.Classes.CountingSimulation.FastAnalysis +public import Complexity.Computability.Complexity.Classes.CountingSimulation.FastLeaves public import Complexity.Computability.Complexity.Classes.CountingSimulation.Guarded public import Complexity.Computability.Complexity.Classes.CountingSimulation.Interfaces public import Complexity.Computability.Complexity.Classes.DP diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionDerivation.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionDerivation.lean new file mode 100644 index 0000000000..7d1f9b0e8d --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionDerivation.lean @@ -0,0 +1,198 @@ +/- +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.FastContraction +import Mathlib.Data.List.GetD + +/-! +# The derivations of the native contraction recursion + +The calls that the recursion of `Cslib.Circuits.Frontier.FastContraction.scheme` meets from a root +(`FastContraction.Reach`), and derivations of the root's value over them, with their height and, +given a bound on the children of each call, their number of nodes. This is the recursion tree of +Theorem D.1 of [OpenAI2026ETH] (Appendix D.4.7, p. 64), for any child builder. + +**The invariant** (`FastContraction.reachInv`). The nodes of a derivation from a root `x₀` are the +calls reached from `x₀`, its frames are the frames `FastContraction.frameAt` of a reached active +call along its children, and its values are the tagged values of reached calls. Every bound on +reached calls is a bound on the derivation. + +**The height.** The children of a call receive its number of edges as their bound, and an active +call has fewer edges than its bound, so the bound plus the depth never increases along the +recursion (`FastContraction.Reach.bound_add_depth_le`). From a root at depth `0` with edge bound +`B`, every active call has depth below `B - 1`, and the root has a derivation with at most `B` +stack levels (`FastContraction.exists_eval_reachInv`), whatever the schedule. + +**The node count.** If every reached active call has depth below `D` and at most `b d` children at +depth `d`, the derivation has at most `Nat.recursionBound b D 0` nodes and `D` stack levels +(`FastContraction.exists_eval_reachInv_count`). + +## Main definitions + +* `Cslib.Circuits.Frontier.FastContraction.Reach`: the calls reached from a root. +* `Cslib.Circuits.Frontier.FastContraction.reachInv`: the invariant of the derivations. + +## Main results + +* `Cslib.Circuits.Frontier.FastContraction.Reach.bound_add_depth_le`: the bound plus the depth + does not increase. +* `Cslib.Circuits.Frontier.FastContraction.exists_eval_reachInv`: a derivation of the root with its + height. +* `Cslib.Circuits.Frontier.FastContraction.exists_eval_reachInv_count`: a derivation of the root + with its node count. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Appendix D.4.7 (p. 64). +-/ + +public section + +namespace Cslib.Circuits.Frontier.FastContraction + +open ChildCursor Cslib.GenericRAM Cslib.GenericRAM.StackRecursion + +variable (mk : Call → State → ℕ × DescribedNetwork VertexDesc) + +/-- **The calls reached from a root** `x₀`: the root, and the children of reached active calls. -/ +inductive Reach (x₀ : Call) : Call → Prop + /-- The root is reached. -/ + | root : Reach x₀ x₀ + /-- The children of a reached active call are reached. -/ + | step {x : Call} (c : State) : Reach x₀ x → active x = true → c ∈ children x → + Reach x₀ (child x mk c) + +/-- **The invariant of the derivations from a root** `x₀`: the reached calls, the frames of reached +active calls along their children, and the tagged values of reached calls. -/ +@[expose] def reachInv (x₀ : Call) : Invariant Call Frame (ℕ × List ℕ) where + node := Reach mk x₀ + frame x a := Reach mk x₀ x ∧ active x = true ∧ + ∃ c ≤ (children x).length, a = frameAt x (fun c => value mk (child x mk c)) c + value y := ∃ x, Reach mk x₀ x ∧ y = (x.depth, value mk x) + +variable {mk} {x₀ : Call} + +namespace Reach + +/-- Reached calls keep the scale of the root. -/ +theorem scale_eq {x : Call} (h : Reach mk x₀ x) : x.scale = x₀.scale := by + induction h with + | root => rfl + | step c _ _ _ ih => exact ih + +/-- Reached calls keep the modulus of the root. -/ +theorem fl_eq {x : Call} (h : Reach mk x₀ x) : x.fl = x₀.fl := by + induction h with + | root => rfl + | step c _ _ _ ih => exact ih + +/-- **The bound plus the depth does not increase** along the recursion: a child's bound is its +parent's number of edges, which is below the parent's bound at an active call. -/ +theorem bound_add_depth_le {x : Call} (h : Reach mk x₀ x) : + x.bound + x.depth ≤ x₀.bound + x₀.depth := by + induction h with + | root => exact le_rfl + | step c _ ha _ ih => + rename_i x _ _ + have := edges_lt_bound_of_active ha + change x.edges + (x.depth + 1) ≤ _ + omega + +/-- **A reached active call lies above depth `B - 1`**, for the root's bound `B` plus its depth: +it has an edge and fewer edges than its bound. -/ +theorem depth_add_two_le_of_active {x : Call} (h : Reach mk x₀ x) (ha : active x = true) : + x.depth + 2 ≤ x₀.bound + x₀.depth := by + have h1 := h.bound_add_depth_le + have h2 := edges_lt_bound_of_active ha + have h3 := one_le_edges_of_active ha + omega + +/-- Reached calls lie at or below the root's depth. -/ +theorem depth_le {x : Call} (h : Reach mk x₀ x) : x₀.depth ≤ x.depth := by + induction h with + | root => exact le_rfl + | step c _ _ _ ih => change x₀.depth ≤ _ + 1; omega + +/-- A reached call at the root's depth is the root. -/ +theorem eq_root_of_depth_le {x : Call} (h : Reach mk x₀ x) (hd : x.depth ≤ x₀.depth) : + x = x₀ := by + cases h with + | root => rfl + | @step y c hx _ _ => + have := hx.depth_le + change y.depth + 1 ≤ x₀.depth at hd + omega + +end Reach + +/-- The derivation hypotheses of a reached active call: its frames along its children, which are +reached, smaller in the bound and one level deeper, and its value from the last frame. -/ +private theorem reach_call {x : Call} (hx : Reach mk x₀ x) (ha : active x = true) : + ∃ (acc : ℕ → Frame) (child' : ℕ → Call), acc 0 = (scheme mk).start x ∧ + (∀ c < (children x).length, (scheme mk).next x (acc c) = some (child' c)) ∧ + (scheme mk).next x (acc (children x).length) = none ∧ + (∀ c < (children x).length, (scheme mk).absorb x (acc c) + ((child' c).depth, value mk (child' c)) = acc (c + 1)) ∧ + (∀ c < (children x).length, (reachInv mk x₀).frame x (acc c) ∧ + Reach mk x₀ (child' c) ∧ (child' c).bound < x.bound ∧ (child' c).depth = x.depth + 1) ∧ + (x.depth, value mk x) = (scheme mk).finish x (acc (children x).length) := by + obtain ⟨h0, hnext, hdone, habs, hfin⟩ := walk mk ha fun c => value mk (child x mk c) + refine ⟨frameAt x fun c => value mk (child x mk c), + fun c => child x mk ((children x).getD c (0, 0, [], 0)), h0, hnext, hdone, + fun c hc => habs c hc, fun c hc => ⟨⟨hx, ha, c, hc.le, rfl⟩, ?_, ?_, rfl⟩, ?_⟩ + · exact Reach.step _ hx ha (List.getD_eq_getElem _ _ hc ▸ List.getElem_mem hc) + · exact edges_lt_bound_of_active ha + · simp only [scheme, Prod.mk.injEq, true_and] + rw [value_of_active mk ha, hfin] + +/-- The leaves and values of a derivation over the reached calls. -/ +private theorem reach_leaf {x : Call} (hl : (scheme mk).isLeaf x = true) : + (x.depth, value mk x) = (scheme mk).leaf x := by + have hl' : active x = false := by simpa [scheme] using hl + simp [scheme, value_of_not_active mk hl'] + +private theorem active_of_isLeaf_eq_false {x : Call} (hl : (scheme mk).isLeaf x = false) : + active x = true := by simpa [scheme] using hl + +/-- **A derivation of the root with its height.** A root at depth `0` with edge bound `B` has a +derivation of its tagged value over the reached calls with at most `B` stack levels, for every +child builder. -/ +theorem exists_eval_reachInv (hx₀ : x₀.depth = 0) : + ∃ N H, (scheme mk).Eval (reachInv mk x₀) x₀ (0, value mk x₀) N H ∧ H ≤ x₀.bound := by + obtain ⟨N, H, he, hH⟩ := Scheme.exists_eval_of_height (R := scheme mk) (I := reachInv mk x₀) + Call.bound Call.depth (fun x => (x.depth, value mk x)) x₀.bound (fun x _ hl => reach_leaf hl) + (fun x hx hl => by + have ha := active_of_isLeaf_eq_false hl + have hd := (show Reach mk x₀ x from hx).depth_add_two_le_of_active ha + obtain ⟨acc, child', h0, hnext, hdone, habs, hkids, hfin⟩ := reach_call hx ha + exact ⟨by omega, _, acc, child', h0, hnext, hdone, habs, hkids, hfin⟩) + (fun x hx => ⟨x, hx, rfl⟩) x₀ Reach.root (by omega) + rw [hx₀] at he hH + exact ⟨N, H, he, by omega⟩ + +/-- **A derivation of the root with its node count.** If every reached active call has depth below +`D` and at most `b d` children at depth `d`, a root at depth `0` has a derivation of its tagged +value over the reached calls with at most `Nat.recursionBound b D 0` nodes and `D` stack levels. -/ +theorem exists_eval_reachInv_count (hx₀ : x₀.depth = 0) (D : ℕ) (b : ℕ → ℕ) + (hcnt : ∀ x, Reach mk x₀ x → active x = true → + x.depth < D ∧ (children x).length ≤ b x.depth) : + ∃ N H, (scheme mk).Eval (reachInv mk x₀) x₀ (0, value mk x₀) N H ∧ + N ≤ Nat.recursionBound b D 0 ∧ H ≤ D := by + obtain ⟨N, H, he, hN, hH⟩ := Scheme.exists_eval_of_counted (R := scheme mk) (I := reachInv mk x₀) + Call.bound Call.depth (fun x => (x.depth, value mk x)) b D (fun x _ hl => reach_leaf hl) + (fun x hx hl => by + have ha := active_of_isLeaf_eq_false hl + obtain ⟨hd, hb⟩ := hcnt x hx ha + obtain ⟨acc, child', h0, hnext, hdone, habs, hkids, hfin⟩ := reach_call hx ha + exact ⟨hd, _, acc, child', hb, h0, hnext, hdone, habs, hkids, hfin⟩) + (fun x hx => ⟨x, hx, rfl⟩) x₀ Reach.root (by omega) + rw [hx₀] at he hN hH + exact ⟨N, H, he, hN, by omega⟩ + +end Cslib.Circuits.Frontier.FastContraction diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionLeaf.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionLeaf.lean new file mode 100644 index 0000000000..785b26d056 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionLeaf.lean @@ -0,0 +1,761 @@ +/- +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.FastContractionMachine +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionStep +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Lists +import Mathlib.Data.List.GetD +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length + +/-! +# The leaves of the fast contraction algorithm + +The cost of the leaves of the native recursion of Theorem D.1 of [OpenAI2026ETH] +(`Cslib.Circuits.Frontier.FastContraction.leafCertificate`), the leaf clause of the resource +analysis `Cslib.Complexity.CountingSimulation.FastAnalysis`. A leaf sums directly over the `2 ^ M` +edge assignments of a call with `M` edges (§D.4.7, p. 64), and the entry of a packet vertex costs +`(m + 2) ^ L` for `m` target modes and `L` row ports, the source's `exp(O(L log s))` (§D.4.6, +p. 63). + +**The cost of a leaf** (`FastContraction.leafCertificate_le`): with at most `R` target modes and +`Λ` row ports per vertex, time `K (n + R + 1) ^ K 2 ^ M (R + 2) ^ Λ` and space `K (n + R + 1) ^ K` +on a call of encoded length `n`, from the bounds of direct summation +(`DescribedNetwork.contractionCertificate_le`) and of the evaluator of descriptors +(`VertexDesc.entryCertificate_le`). + +**The packet shape** (`FastContraction.PacketShape`). Every packet vertex of a call of the +recursion has `i < a ≤ ⌊log₂ s⌋ / 32768`, `2 ^ (i + 1)` tiles, at most `p` exponents per tile, and +row ports in distinct slots below `2 ^ a`. So, with `A = 2 ^ (⌊log₂ s⌋ / 32768)`, it has at most +`A p` target modes and `A` row ports. The root has no packets, and the shape passes to the native +children of a well-formed active call (`FastContraction.packetShape_child`): a retained vertex +keeps its descriptor, and the row ports of a new packet are edges of one packet of the packing, +in distinct slots (`NativeChild.desc_of_mem_nativeChild`). + +**The leaf bound** (`FastContraction.exists_leafCertificate_le`). For `s ≤ m ≤ C s`, a leaf with +the packet shape and at most `2 m` edges takes time `K (n + 1) ^ K 2 ^ (K s / √⌊log₂ s⌋)` and space +`K (n + 1) ^ K`, provided that from some `s₀` on it has at most `leafSize m` edges and precision at +most `m ^ c`: then `2 ^ M ≤ 2 ^ (C s / √⌊log₂ s⌋)`, and `(A p + 2) ^ A` is +`2 ^ O(s ^ (1 / 32768) log s)` (`FastContraction.exists_packetFactor_le`). Below `s₀` everything +but a polynomial in `n` is a constant. + +## Main definitions + +* `Cslib.Circuits.Frontier.FastContraction.PacketShape`: the shape of the packets of a call. + +## Main results + +* `Cslib.Circuits.Frontier.FastContraction.leafCertificate_le`: the cost of a leaf. +* `Cslib.Circuits.Frontier.NativeChild.desc_of_mem_nativeChild`: the descriptors of a native + child. +* `Cslib.Circuits.Frontier.FastContraction.packetShape_root`, + `Cslib.Circuits.Frontier.FastContraction.packetShape_child`: the packet shape on the reached + calls. +* `Cslib.Circuits.Frontier.FastContraction.leafCertificate_le_of_packetShape`: the cost of a leaf + with the packet shape. +* `Cslib.Circuits.Frontier.FastContraction.exists_leafCertificate_le`: the leaf bound of the + resource analysis. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.6–§D.4.7, + pp. 63–64. +-/ + +public section + +namespace Cslib.Circuits.Frontier + +/-! ### The descriptors of the native children -/ + +namespace NativeChild + +open ChildNumbering + +variable {D : DescribedNetwork VertexDesc} {r : ℕ} + +/-- **The descriptors of the native child.** A vertex of the native child of a rows-first parent +with at least `64 ^ a` edges keeps the descriptor of a parent vertex, or is the packet `q`, with +the packet context of `q`, the slice of `β` at `q`, and tags whose slots are below `2 ^ a` and +distinct among its row ports. -/ +theorem desc_of_mem_nativeChild (hD : D.IsRowsFirstBipartite r) {fl : List ℕ} {a i : ℕ} + (hK : 64 ^ a ≤ D.numEdges) (hia : i < a) (pt : ℕ) (t : ℤ) (ζ β : List ℕ) (g : Fin 64) + {v : List ℕ × VertexDesc} + (hv : v ∈ (nativeChild fl a i pt t ζ r D (nativeParentPacking r a D) β g).vertices) : + (∃ w ∈ D.vertices, v.2 = w.2) ∨ + ∃ q tags, v.2 = .inr (packetCtx fl a i pt t ζ g q, tags, betaSlice i pt β q) ∧ + (∀ y ∈ tags, y.2 < 2 ^ a) ∧ ((tags.filter (·.1)).map (·.2)).Nodup := by + have hgroups := groupsOf_eq hD hK hia + have hpk1 : (nativeParentPacking r a D).2.1 = (parentPacking hD a).numPackets := by + rw [nativeParentPacking_eq hD hK] + have hpk2 : (nativeParentPacking r a D).2.2 = List.ofFn fun e => + (((parentPacking hD a).packet e : ℕ), ((parentPacking hD a).slot e : ℕ)) := by + rw [nativeParentPacking_eq hD hK] + rw [nativeChild_eq hD _ (parentPacking hD a).packet (fun e => ((parentPacking hD a).slot e : ℕ)) + g fl a i pt t ζ β _ hgroups hpk1 hpk2] at hv + simp only [List.mem_ofFn] at hv + obtain ⟨c, rfl⟩ := hv + rcases hc : (childVertexEquiv (P := (parentPacking hD a).numPackets) + (packingGroup (parentSide r) (parentPacking hD a) ⟨i, hia⟩) g).symm c with w | q + · left + refine ⟨D.vertices[(w.1 : ℕ)], List.getElem_mem _, ?_⟩ + simp only [numberedDesc, Sum.elim_inl] + · right + simp only [numberedDesc, Sum.elim_inr] + refine ⟨q, _, rfl, ?_, ?_⟩ + · intro y hy + simp only [List.mem_map] at hy + obtain ⟨e, -, rfl⟩ := hy + exact Fin.isLt _ + · rw [List.filter_map, List.map_map] + refine List.Nodup.map_on ?_ ((nodup_packetPorts hD _ _ g q).filter _) + intro c₁ hc₁ c₂ hc₂ heq + simp only [List.mem_filter, Function.comp_apply] at hc₁ hc₂ + obtain ⟨hm₁, hl₁⟩ := hc₁ + obtain ⟨hm₂, hl₂⟩ := hc₂ + rw [mem_packetPorts] at hm₁ hm₂ + rcases c₁ with e₁ | e₁ + · rcases c₂ with e₂ | e₂ + · simp only [Function.comp_apply, Sum.elim_inl] at heq hm₁ hm₂ + have hinj := (parentPacking hD a).injective (a₁ := e₁.1) (a₂ := e₂.1) + (Prod.ext (hm₁.trans hm₂.symm) (Fin.ext heq)) + rw [Subtype.ext hinj] + · simp at hl₂ + · simp at hl₁ + +end NativeChild + +namespace FastContraction + +open GaloisRingArith NativePacket ChildCursor NativeRecovery ContractionSchedule NativeChild + Cslib.GenericRAM Cslib.GenericRAM.StackRecursion Turing.MultiTapeTM + +/-! ### Encoded lengths -/ + +/-- The scale, the precision and the coefficients of the modulus are at most the encoded length +of a call. -/ +theorem scale_add_prec_add_length_fl_le (x : Call) : + x.scale + x.prec + x.fl.length ≤ (encCall x).length := by + have h := length_le_length_encList encNat x.fl + obtain ⟨⟨s, d, b, p, fl, r⟩, D⟩ := x + simp only [Call.scale, Call.prec, Call.fl, encCall, encParams, length_encPair, encUnary_apply, + List.length_replicate] at h ⊢ + omega + +/-- The network of a call is at most its encoded length. -/ +theorem length_net_le (x : Call) : + (DescribedNetwork.encDescribed VertexDesc.enc x.net).length ≤ (encCall x).length := by + obtain ⟨p, D⟩ := x + simp only [Call.net, encCall, length_encPair] + omega + +/-- A vertex of a call is at most its encoded length. -/ +theorem length_vertex_le {x : Call} {v : List ℕ × VertexDesc} (hv : v ∈ x.net.vertices) : + (encPair (encList encNat) VertexDesc.enc v).length ≤ (encCall x).length := by + have h := length_le_encList_of_mem (encPair (encList encNat) VertexDesc.enc) hv + have h2 : (encList (encPair (encList encNat) VertexDesc.enc) x.net.vertices).length ≤ + (DescribedNetwork.encDescribed VertexDesc.enc x.net).length := by + change _ ≤ (encPair encUnary (encList (encPair (encList encNat) VertexDesc.enc)) + (x.net.numEdges, x.net.vertices)).length + rw [length_encPair] + dsimp only + omega + have h3 := length_net_le x + omega + +/-- The number of vertices of a call is at most its encoded length. -/ +theorem length_vertices_le (x : Call) : x.net.vertices.length ≤ (encCall x).length := by + have h := DescribedNetwork.length_numEdges_vertices_le (encT := VertexDesc.enc) x.net + have h3 := length_net_le x + omega + +/-! ### The cost of a leaf -/ + +/-- `c (y + 1) ^ d ≤ c W ^ d` when `y + 1 ≤ W`. -/ +private theorem mul_pow_le_of_le {c y d W : ℕ} (hy : y + 1 ≤ W) : c * (y + 1) ^ d ≤ c * W ^ d := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hy _) + +/-- Raising the exponent of `W ≥ 1`. -/ +private theorem mul_pow_le_mul_pow {c W d E : ℕ} (hW : 1 ≤ W) (hd : d ≤ E) : + c * W ^ d ≤ c * W ^ E := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_right hW hd) + +/-- The reduced coefficient lists against `W`. -/ +private theorem rv_le {n W cf df cp dp ct dt : ℕ} (hnW : n + 1 ≤ W) : + n * (2 * n + 3) + cf * (n + 1) ^ df * (2 * (cp * (n + 1) ^ dp) + 3) + + ct * (3 * n + 2) ^ dt ≤ + (5 + cf * (2 * cp + 3) + ct * 3 ^ dt) * W ^ (2 + df + dp + dt) := by + have hW1 : 1 ≤ W := by omega + have h1 : n * (2 * n + 3) ≤ 5 * W ^ 2 := + calc n * (2 * n + 3) ≤ W * (5 * W) := Nat.mul_le_mul (by omega) (by omega) + _ = 5 * W ^ 2 := by ring + have h2 : cf * (n + 1) ^ df * (2 * (cp * (n + 1) ^ dp) + 3) ≤ + cf * (2 * cp + 3) * W ^ (df + dp) := by + have hb1 : (n + 1) ^ df ≤ W ^ df := Nat.pow_le_pow_left hnW _ + have hb2 : cp * (n + 1) ^ dp ≤ cp * W ^ dp := mul_pow_le_of_le hnW + have hW1' : 1 ≤ W ^ dp := Nat.one_le_pow _ _ (by omega) + have : 2 * (cp * (n + 1) ^ dp) + 3 ≤ (2 * cp + 3) * W ^ dp := by + rw [add_mul, Nat.mul_assoc]; omega + calc cf * (n + 1) ^ df * (2 * (cp * (n + 1) ^ dp) + 3) + ≤ cf * W ^ df * ((2 * cp + 3) * W ^ dp) := + Nat.mul_le_mul (Nat.mul_le_mul_left _ hb1) this + _ = cf * (2 * cp + 3) * W ^ (df + dp) := by rw [pow_add]; ring + have h3 : ct * (3 * n + 2) ^ dt ≤ ct * 3 ^ dt * W ^ dt := + calc ct * (3 * n + 2) ^ dt ≤ ct * (3 * W) ^ dt := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) _) + _ = ct * 3 ^ dt * W ^ dt := by rw [mul_pow]; ring + have l1 : 5 * W ^ 2 ≤ 5 * W ^ (2 + df + dp + dt) := mul_pow_le_mul_pow hW1 (by omega) + have l2 : cf * (2 * cp + 3) * W ^ (df + dp) ≤ cf * (2 * cp + 3) * W ^ (2 + df + dp + dt) := + mul_pow_le_mul_pow hW1 (by omega) + have l3 : ct * 3 ^ dt * W ^ dt ≤ ct * 3 ^ dt * W ^ (2 + df + dp + dt) := + mul_pow_le_mul_pow hW1 (by omega) + rw [add_mul, add_mul] + omega + +/-- The input of direct summation against `W`. -/ +private theorem sum_le_of_le {W a b c₀ d₀ cR E₀ : ℕ} (hW : 1 ≤ W) (ha : a ≤ c₀ * W ^ d₀) + (hd : d₀ ≤ E₀) (hb : b ≤ cR * W ^ E₀) : a + b + b + 1 ≤ (c₀ + 2 * cR + 1) * W ^ E₀ := by + have h1 : c₀ * W ^ d₀ ≤ c₀ * W ^ E₀ := mul_pow_le_mul_pow hW hd + have h2 : 1 ≤ W ^ E₀ := Nat.one_le_pow _ _ (by omega) + rw [add_mul, add_mul, Nat.mul_assoc 2] + omega + +/-- The bound on the entries' arguments against `W`. -/ +private theorem zb_le {W n R Rv cR E₀ : ℕ} (hW : 1 ≤ W) (hE : 1 ≤ E₀) (hRv : Rv ≤ cR * W ^ E₀) + (hnR : 3 * n + R + 3 ≤ 3 * W) : 3 * n + R + Rv + 3 ≤ (3 + cR) * W ^ E₀ := by + have h1 : W ≤ W ^ E₀ := + calc W = W ^ 1 := (pow_one W).symm + _ ≤ W ^ E₀ := Nat.pow_le_pow_right hW hE + rw [add_mul] + omega + +/-- The arithmetic of the time of a leaf. -/ +private theorem time_assemble {Td Ti Ts cd dd ci di P X k W A Zb c₁ c₂ E₀ K₁ K₂ : ℕ} + (hW : 1 ≤ W) (hP : 1 ≤ P) (hX : 1 ≤ X) (hd : Td ≤ cd * W ^ dd) (hi : Ti ≤ ci * W ^ di) + (hs : Ts ≤ (P * (k + 1) + 1) * (K₁ * (A + 1) ^ K₁ + 2 * (K₂ * X * Zb ^ K₂))) + (hk : k + 1 ≤ W) (hA : A + 1 ≤ c₁ * W ^ E₀) (hZ : Zb ≤ c₂ * W ^ E₀) : + Td + (Ti + Ts) ≤ (2 * (K₁ * c₁ ^ K₁ + 2 * (K₂ * c₂ ^ K₂)) + cd + ci) * + W ^ (1 + E₀ * (K₁ + K₂) + dd + di) * P * X := by + have hWF1 : W ^ (E₀ * K₁) ≤ W ^ (E₀ * (K₁ + K₂)) := + Nat.pow_le_pow_right hW (by rw [Nat.mul_add]; omega) + have hWF2 : W ^ (E₀ * K₂) ≤ W ^ (E₀ * (K₁ + K₂)) := + Nat.pow_le_pow_right hW (by rw [Nat.mul_add]; omega) + set F := E₀ * (K₁ + K₂) + set S := W ^ (1 + F + dd + di) + have hA' : K₁ * (A + 1) ^ K₁ ≤ K₁ * c₁ ^ K₁ * W ^ F := + calc K₁ * (A + 1) ^ K₁ ≤ K₁ * (c₁ * W ^ E₀) ^ K₁ := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hA _) + _ = K₁ * c₁ ^ K₁ * W ^ (E₀ * K₁) := by rw [mul_pow, ← pow_mul, Nat.mul_assoc] + _ ≤ K₁ * c₁ ^ K₁ * W ^ F := Nat.mul_le_mul_left _ hWF1 + have hZ' : K₂ * X * Zb ^ K₂ ≤ K₂ * c₂ ^ K₂ * X * W ^ F := + calc K₂ * X * Zb ^ K₂ ≤ K₂ * X * (c₂ * W ^ E₀) ^ K₂ := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hZ _) + _ = K₂ * c₂ ^ K₂ * X * W ^ (E₀ * K₂) := by rw [mul_pow, ← pow_mul]; ring + _ ≤ K₂ * c₂ ^ K₂ * X * W ^ F := Nat.mul_le_mul_left _ hWF2 + have hin : K₁ * (A + 1) ^ K₁ + 2 * (K₂ * X * Zb ^ K₂) ≤ + (K₁ * c₁ ^ K₁ + 2 * (K₂ * c₂ ^ K₂)) * X * W ^ F := by + have : K₁ * c₁ ^ K₁ * W ^ F ≤ K₁ * c₁ ^ K₁ * W ^ F * X := Nat.le_mul_of_pos_right _ hX + have e : (K₁ * c₁ ^ K₁ + 2 * (K₂ * c₂ ^ K₂)) * X * W ^ F = + K₁ * c₁ ^ K₁ * W ^ F * X + 2 * (K₂ * c₂ ^ K₂ * X * W ^ F) := by ring + omega + have hPk : P * (k + 1) + 1 ≤ 2 * P * W := by + have : P * (k + 1) ≤ P * W := Nat.mul_le_mul_left _ hk + have : 1 ≤ P * W := Nat.one_le_iff_ne_zero.mpr (by positivity) + rw [Nat.mul_assoc]; omega + have hs' : Ts ≤ 2 * (K₁ * c₁ ^ K₁ + 2 * (K₂ * c₂ ^ K₂)) * S * P * X := + calc Ts ≤ (2 * P * W) * ((K₁ * c₁ ^ K₁ + 2 * (K₂ * c₂ ^ K₂)) * X * W ^ F) := + hs.trans (Nat.mul_le_mul hPk hin) + _ = 2 * (K₁ * c₁ ^ K₁ + 2 * (K₂ * c₂ ^ K₂)) * W ^ (1 + F) * P * X := by + rw [pow_add, pow_one]; ring + _ ≤ 2 * (K₁ * c₁ ^ K₁ + 2 * (K₂ * c₂ ^ K₂)) * S * P * X := + Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ + (Nat.mul_le_mul_left _ (Nat.pow_le_pow_right hW (by omega)))) + have hPX : 1 ≤ P * X := Nat.one_le_iff_ne_zero.mpr (by positivity) + have hd' : Td ≤ cd * S * P * X := + calc Td ≤ cd * S := hd.trans (mul_pow_le_mul_pow hW (by omega)) + _ ≤ cd * S * (P * X) := Nat.le_mul_of_pos_right _ hPX + _ = cd * S * P * X := by ring + have hi' : Ti ≤ ci * S * P * X := + calc Ti ≤ ci * S := hi.trans (mul_pow_le_mul_pow hW (by omega)) + _ ≤ ci * S * (P * X) := Nat.le_mul_of_pos_right _ hPX + _ = ci * S * P * X := by ring + have e : (2 * (K₁ * c₁ ^ K₁ + 2 * (K₂ * c₂ ^ K₂)) + cd + ci) * S * P * X = + 2 * (K₁ * c₁ ^ K₁ + 2 * (K₂ * c₂ ^ K₂)) * S * P * X + cd * S * P * X + ci * S * P * X := by + ring + omega + +/-- The arithmetic of the space of a leaf. -/ +private theorem space_assemble {Sd Si Ss cd dd ci di W A Zb c₁ c₂ E₀ K₁ K₂ ES : ℕ} + (hW : 1 ≤ W) (hd : Sd ≤ cd * W ^ dd) (hi : Si ≤ ci * W ^ di) + (hs : Ss ≤ K₁ * (A + 1) ^ K₁ + ES) (hA : A + 1 ≤ c₁ * W ^ E₀) (hES : ES = K₂ * Zb ^ K₂) + (hZ : Zb ≤ c₂ * W ^ E₀) : + Sd + (Si + Ss) ≤ (K₁ * c₁ ^ K₁ + K₂ * c₂ ^ K₂ + cd + ci) * + W ^ (E₀ * (K₁ + K₂) + dd + di) := by + have hWF1 : W ^ (E₀ * K₁) ≤ W ^ (E₀ * (K₁ + K₂) + dd + di) := + Nat.pow_le_pow_right hW (by rw [Nat.mul_add]; omega) + have hWF2 : W ^ (E₀ * K₂) ≤ W ^ (E₀ * (K₁ + K₂) + dd + di) := + Nat.pow_le_pow_right hW (by rw [Nat.mul_add]; omega) + set F := E₀ * (K₁ + K₂) + set S := W ^ (F + dd + di) + have hA' : K₁ * (A + 1) ^ K₁ ≤ K₁ * c₁ ^ K₁ * S := + calc K₁ * (A + 1) ^ K₁ ≤ K₁ * (c₁ * W ^ E₀) ^ K₁ := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hA _) + _ = K₁ * c₁ ^ K₁ * W ^ (E₀ * K₁) := by rw [mul_pow, ← pow_mul, Nat.mul_assoc] + _ ≤ K₁ * c₁ ^ K₁ * S := Nat.mul_le_mul_left _ hWF1 + have hZ' : ES ≤ K₂ * c₂ ^ K₂ * S := + calc ES = K₂ * Zb ^ K₂ := hES + _ ≤ K₂ * (c₂ * W ^ E₀) ^ K₂ := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hZ _) + _ = K₂ * c₂ ^ K₂ * W ^ (E₀ * K₂) := by rw [mul_pow, ← pow_mul, Nat.mul_assoc] + _ ≤ K₂ * c₂ ^ K₂ * S := Nat.mul_le_mul_left _ hWF2 + have hd' : Sd ≤ cd * S := hd.trans (mul_pow_le_mul_pow hW (by omega)) + have hi' : Si ≤ ci * S := hi.trans (mul_pow_le_mul_pow hW (by omega)) + have e : (K₁ * c₁ ^ K₁ + K₂ * c₂ ^ K₂ + cd + ci) * S = + K₁ * c₁ ^ K₁ * S + K₂ * c₂ ^ K₂ * S + cd * S + ci * S := by ring + omega + +/-- **The cost of a leaf.** There is `K` such that, on a call of encoded length `n` with `M` edges +whose vertices have at most `R` target modes and at most `Λ` row ports on every bit list on their +ports, direct summation takes time at most `K (n + R + 1) ^ K 2 ^ M (R + 2) ^ Λ` and space at most +`K (n + R + 1) ^ K`, whatever the child builder. -/ +theorem leafCertificate_le : ∃ K : ℕ, ∀ (mk : Call → State → ℕ × DescribedNetwork VertexDesc) + (x : Call) (R Λ : ℕ), + (∀ v ∈ x.net.vertices, v.2.modes ≤ R ∧ + ∀ bs : List Bool, bs.length = v.1.length → v.2.rowPorts bs ≤ Λ) → + (leafCertificate mk).time x ≤ + K * ((encCall x).length + R + 1) ^ K * 2 ^ x.edges * (R + 2) ^ Λ ∧ + (leafCertificate mk).space x ≤ K * ((encCall x).length + R + 1) ^ K := by + obtain ⟨K₁, hK₁⟩ := DescribedNetwork.contractionCertificate_le (ops := SumOps.galois) + (eval := VertexDesc.entry) (encQ := encPair encUnary (encList encNat)) + (encY := encList encNat) (encT := VertexDesc.enc) SumOps.galois_polyTime + VertexDesc.entryCertificate + obtain ⟨K₂, hK₂⟩ := VertexDesc.entryCertificate_le + have hD := NativeCertificate.ofPolyTime_isPolynomial depth_polyTime + have hI := NativeCertificate.ofPolyTime_isPolynomial leafInput_polyTime + obtain ⟨cd, dd, hdt⟩ := hD.1.exists_le + obtain ⟨cd', dd', hds⟩ := hD.2.exists_le + obtain ⟨ci, di, hit⟩ := hI.1.exists_le + obtain ⟨ci', di', his⟩ := hI.2.exists_le + obtain ⟨cl, dl, hl⟩ := leafInput_polyTime.polyBounded_length.exists_le + obtain ⟨cp, dp, hp⟩ := PacketCtx.p_polyTime.polyBounded_length.exists_le + obtain ⟨cf, df, hf⟩ := PacketCtx.fl_polyTime.polyBounded_length.exists_le + obtain ⟨ct, dt, ht⟩ := VertexDesc.tableEntry_polyTime.polyBounded_length.exists_le + -- The constants. + obtain ⟨e, he⟩ : ∃ e, e = 2 + df + dp + dt := ⟨_, rfl⟩ + obtain ⟨cR, hcR⟩ : ∃ cR, cR = 5 + cf * (2 * cp + 3) + ct * 3 ^ dt := ⟨_, rfl⟩ + obtain ⟨E₀, hE₀⟩ : ∃ E₀, E₀ = dl + e := ⟨_, rfl⟩ + obtain ⟨c₁, hc₁⟩ : ∃ c₁, c₁ = cl + 2 * cR + 1 := ⟨_, rfl⟩ + obtain ⟨c₂, hc₂⟩ : ∃ c₂, c₂ = 3 + cR := ⟨_, rfl⟩ + obtain ⟨G, hG⟩ : ∃ G, G = 2 * (K₁ * c₁ ^ K₁ + 2 * (K₂ * c₂ ^ K₂)) + cd + ci + + (K₁ * c₁ ^ K₁ + K₂ * c₂ ^ K₂) + cd' + ci' := ⟨_, rfl⟩ + obtain ⟨Dg, hDg⟩ : ∃ Dg, Dg = 1 + E₀ * (K₁ + K₂) + dd + di + dd' + di' := ⟨_, rfl⟩ + refine ⟨G + Dg, fun mk x R Λ hRΛ => ?_⟩ + obtain ⟨n, hn⟩ : ∃ n, n = (encCall x).length := ⟨_, rfl⟩ + obtain ⟨W, hW⟩ : ∃ W, W = n + R + 1 := ⟨_, rfl⟩ + rw [← hn, show n + R + 1 = W from hW.symm] + have hW1 : 1 ≤ W := by omega + have hnW : n + 1 ≤ W := by omega + -- The precision and the modulus of the call. + have hpfl := scale_add_prec_add_length_fl_le x + rw [← hn] at hpfl + -- Every vertex and bit list on its ports is at most `3 n + 1` long. + have hq (v : List ℕ × VertexDesc) (hv : v ∈ x.net.vertices) (bs : List Bool) + (hbs : bs.length = v.1.length) : + (encPair VertexDesc.enc encBits (v.2, bs)).length ≤ 3 * n + 1 := by + have h1 := length_vertex_le hv + have h2 := length_le_length_encList encNat v.1 + rw [length_encPair] at h1 ⊢ + change 2 * (VertexDesc.enc v.2).length + 1 + bs.length ≤ 3 * n + 1 + omega + -- The reduced coefficient lists. + obtain ⟨Rv, hRv⟩ : ∃ Rv, Rv = n * (2 * n + 3) + + cf * (n + 1) ^ df * (2 * (cp * (n + 1) ^ dp) + 3) + ct * (3 * n + 2) ^ dt := ⟨_, rfl⟩ + have hred : ∀ y, SumOps.galois.Reduced (x.prec, x.fl) y → (encList encNat y).length ≤ Rv := by + intro y hy + have h := SumOps.length_encList_le_of_galois_reduced hy + simp only at h + have : x.fl.length * (2 * x.prec + 3) ≤ n * (2 * n + 3) := + Nat.mul_le_mul (by omega) (by omega) + omega + have hpacket (v : List ℕ × VertexDesc) (hv : v ∈ x.net.vertices) (d : PacketDesc) + (hd : v.2 = .inr d) : + ∀ y, SumOps.galois.Reduced (d.1.p, d.1.fl) y → (encList encNat y).length ≤ Rv := by + intro y hy + have h := SumOps.length_encList_le_of_galois_reduced hy + simp only at h + have h1 := length_vertex_le hv + rw [length_encPair, hd, length_encSum] at h1 + simp only [Sum.elim_inr] at h1 + have h2 : (PacketCtx.enc d.1).length ≤ n := by + have := length_encPair (enc₁ := PacketCtx.enc) + (enc₂ := encPair (encList (encPair encBool encNat)) (encList encUnary)) d + change (encPacketDesc d).length = _ at this + omega + have hpd : d.1.p ≤ cp * (n + 1) ^ dp := by + have := hp d.1 + rw [encUnary_apply, List.length_replicate] at this + exact this.trans (mul_pow_le_of_le (by omega)) + have hfd : d.1.fl.length ≤ cf * (n + 1) ^ df := + (length_le_length_encList encNat d.1.fl).trans ((hf d.1).trans (mul_pow_le_of_le (by omega))) + have : d.1.fl.length * (2 * d.1.p + 3) ≤ cf * (n + 1) ^ df * (2 * (cp * (n + 1) ^ dp) + 3) := + Nat.mul_le_mul hfd (by omega) + omega + -- The entries. + obtain ⟨Zb, hZb⟩ : ∃ Zb, Zb = 3 * n + R + Rv + 3 := ⟨_, rfl⟩ + have hentry : ∀ v ∈ ((x.prec, x.fl), x.net).2.vertices, ∀ bs : List Bool, + bs.length = v.1.length → + VertexDesc.entryCertificate.time (v.2, bs) ≤ K₂ * (R + 2) ^ Λ * Zb ^ K₂ ∧ + VertexDesc.entryCertificate.space (v.2, bs) ≤ K₂ * Zb ^ K₂ ∧ + (encList encNat (VertexDesc.entry v.2 bs)).length ≤ Rv := by + intro v hv bs hbs + have hlen := hq v hv bs hbs + obtain ⟨hmodes, hrows⟩ := hRΛ v hv + have hrows := hrows bs hbs + have hRLE : v.2.ReducedLE Rv := by + rcases hd : v.2 with t | d + · trivial + · exact hpacket v hv d hd + obtain ⟨hT, hS⟩ := hK₂ (v.2, bs) Rv hRLE + dsimp only at hT hS + have hZ : (encPair VertexDesc.enc encBits (v.2, bs)).length + v.2.modes + Rv + 2 ≤ Zb := by + omega + refine ⟨hT.trans ?_, hS.trans (Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hZ _)), ?_⟩ + · refine Nat.mul_le_mul (Nat.mul_le_mul_left _ ?_) (Nat.pow_le_pow_left hZ _) + exact (Nat.pow_le_pow_left (by omega) _).trans (Nat.pow_le_pow_right (by omega) hrows) + · rcases hd : v.2 with t | d + · have := ht (v.2, bs) + rw [hd] at this + refine this.trans ?_ + have h3 : (encPair VertexDesc.enc encBits (Sum.inl t, bs)).length + 1 ≤ 3 * n + 2 := by + rw [← hd]; omega + calc ct * ((encPair VertexDesc.enc encBits (Sum.inl t, bs)).length + 1) ^ dt + ≤ ct * (3 * n + 2) ^ dt := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left h3 _) + _ ≤ Rv := by omega + · exact hpacket v hv d hd _ (VertexDesc.reduced_entry_inr d bs) + obtain ⟨hsT, hsS⟩ := hK₁ ((x.prec, x.fl), x.net) (K₂ * (R + 2) ^ Λ * Zb ^ K₂) (K₂ * Zb ^ K₂) Rv + Rv hentry hred + -- Polynomial pieces against `W`. + have hk : x.net.vertices.length + 1 ≤ W := by have := length_vertices_le x; omega + have hRvW : Rv ≤ cR * W ^ e := by + rw [hRv, hcR, he]; exact rv_le hnW + have hWE : W ^ e ≤ W ^ E₀ := Nat.pow_le_pow_right hW1 (by omega) + have hA1 : (DescribedNetwork.encInput (encPair encUnary (encList encNat)) VertexDesc.enc + ((x.prec, x.fl), x.net)).length + Rv + Rv + 1 ≤ c₁ * W ^ E₀ := by + have h1 : (DescribedNetwork.encInput (encPair encUnary (encList encNat)) VertexDesc.enc + ((x.prec, x.fl), x.net)).length ≤ cl * W ^ dl := + (hl x).trans (by rw [← hn]; exact mul_pow_le_of_le hnW) + rw [hc₁] + exact sum_le_of_le hW1 h1 (by omega) (hRvW.trans (Nat.mul_le_mul_left _ hWE)) + have hZW : Zb ≤ c₂ * W ^ E₀ := by + rw [hc₂, hZb] + exact zb_le hW1 (by omega) (hRvW.trans (Nat.mul_le_mul_left _ hWE)) (by omega) + have hnW' : (encCall x).length + 1 ≤ W := by omega + have hdt' := (hdt x).trans (mul_pow_le_of_le (c := cd) (d := dd) hnW') + have hit' := (hit x).trans (mul_pow_le_of_le (c := ci) (d := di) hnW') + have hds' := (hds x).trans (mul_pow_le_of_le (c := cd') (d := dd') hnW') + have his' := (his x).trans (mul_pow_le_of_le (c := ci') (d := di') hnW') + have hP : 1 ≤ 2 ^ x.edges := Nat.one_le_two_pow + have hX : 1 ≤ (R + 2) ^ Λ := Nat.one_le_pow _ _ (by omega) + refine ⟨?_, ?_⟩ + · rw [leafCertificate_time] + refine (time_assemble hW1 hP hX hdt' hit' hsT hk hA1 hZW).trans ?_ + refine Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ (Nat.mul_le_mul (by omega) + (Nat.pow_le_pow_right hW1 (by omega)))) + · rw [leafCertificate_space] + refine (space_assemble hW1 hds' his' hsS hA1 rfl hZW).trans ?_ + exact Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right hW1 (by omega)) + +/-! ### The shape of the packets -/ + +/-- **The shape of the packets of a call**: every packet vertex has `i < a ≤ ⌊log₂ s⌋ / 32768`, +`2 ^ (i + 1)` tiles and at most `p` exponents per tile, and the slots of its ports are below +`2 ^ a` and distinct among its row ports. So it has at most `2 ^ (⌊log₂ s⌋ / 32768) p` target modes +and at most `2 ^ (⌊log₂ s⌋ / 32768)` row ports (`modes_le_of_packetShape`, +`rowPorts_le_of_packetShape`). -/ +def PacketShape (x : Call) : Prop := + ∀ v ∈ x.net.vertices, ∀ d : PacketDesc, v.2 = .inr d → + d.1.i < d.1.a ∧ d.1.a ≤ Nat.log 2 x.scale / 32768 ∧ d.1.tiles = 2 ^ (d.1.i + 1) ∧ + d.1.nb ≤ x.prec ∧ (∀ y ∈ d.2.1, y.2 < 2 ^ d.1.a) ∧ ((d.2.1.filter (·.1)).map (·.2)).Nodup + +/-- **The root has no packets.** -/ +theorem packetShape_root (q : ℕ × ℕ × ExplicitTensorNetwork ℕ) : PacketShape (root q) := by + intro v hv d hd + simp only [root, rootNet, Call.net, List.mem_map] at hv + obtain ⟨w, -, rfl⟩ := hv + cases hd + +/-- **The packet shape passes to the native children** of a well-formed active call: a retained +vertex keeps its descriptor, at a precision that only grows, and a new packet has `a` slot bits +(`slotBits_le`), `i < a` (the valuation of its node), `2 ^ (i + 1)` tiles, the child's precision +as its number of exponents per tile, and the slots of the packing, distinct within a packet. -/ +theorem packetShape_child {x : Call} (hx : WF x) (ha : active x = true) (hs : PacketShape x) + {c : State} (hc : c ∈ children x) : PacketShape (child x nativeMk c) := by + -- The builder at a cursor state of a well-formed active call: the uncapped native child. + have hmk : (nativeMk x c).2 = nativeChild x.fl (slots x) (level x ((nodes x).getD c.1 0)) + (nodePrec x c.1) (node (slots x) ((nodes x).getD c.1 0)) ((points x).getD c.2.1 []) x.rows + x.net (nativeParentPacking x.rows (slots x) x.net) c.2.2.1 c.2.2.2 := by + rw [nativeMk_eq hx ha hc] + obtain ⟨-, hD⟩ := hx + obtain ⟨hj, -, hg⟩ := lt_of_mem_children hc + have ha' := ha + simp only [active, decide_eq_true_eq] at ha' + obtain ⟨-, -, -, hua, -, -, -⟩ := ha' + have hkmem : (nodes x).getD c.1 0 ∈ nodes x := by + rw [List.getD_eq_getElem _ _ hj]; exact List.getElem_mem hj + obtain ⟨hk, -, hq⟩ := mem_nodes.mp hkmem + have hia : level x ((nodes x).getD c.1 0) < slots x := by + rw [level_eq hk] + exact padicValInt_lt_of_taperMult_pos (by rwa [← mult_eq _ _ hk]) hua + have hp : x.prec ≤ nodePrec x c.1 := by unfold nodePrec nodePrecision; omega + intro v hv d hd + have hv' : v ∈ (nativeChild x.fl (slots x) (level x ((nodes x).getD c.1 0)) (nodePrec x c.1) + (node (slots x) ((nodes x).getD c.1 0)) ((points x).getD c.2.1 []) x.rows x.net + (nativeParentPacking x.rows (slots x) x.net) c.2.2.1 (⟨c.2.2.2, hg⟩ : Fin 64)).vertices := by + change v ∈ (nativeMk x c).2.vertices at hv + rwa [hmk] at hv + rcases NativeChild.desc_of_mem_nativeChild hD (pow_slots_le_edges_of_active ha) hia _ _ _ _ _ + hv' with ⟨w, hw, hvw⟩ | ⟨q, tags, hvq, hslot, hnodup⟩ + · obtain ⟨h1, h2, h3, h4, h5, h6⟩ := hs w hw d (hvw ▸ hd) + exact ⟨h1, h2, h3, h4.trans hp, h5, h6⟩ + · rw [hvq] at hd + cases hd + exact ⟨hia, slotBits_le _ _, rfl, le_rfl, hslot, hnodup⟩ + +/-- The positions of a list satisfying a test are as many as its elements satisfying it. -/ +private theorem length_filter_range_getD {α : Type} (l : List α) (d : α) (p : α → Bool) : + ((List.range l.length).filter fun j => p (l.getD j d)).length = (l.filter p).length := by + have hl : (List.range l.length).map (fun j => l.getD j d) = l := by + refine List.ext_getElem (by simp) fun j h₁ h₂ => ?_ + simp only [List.getElem_map, List.getElem_range, List.getD_eq_getElem _ _ h₂] + conv_rhs => rw [← hl] + rw [List.filter_map, List.length_map] + rfl + +/-- `2 ^ (⌊log₂ s⌋ / 32768)` is at most `s + 1`. -/ +theorem two_pow_log_div_le (s : ℕ) : 2 ^ (Nat.log 2 s / 32768) ≤ s + 1 := by + rcases Nat.eq_zero_or_pos s with rfl | hs + · simp + · calc 2 ^ (Nat.log 2 s / 32768) ≤ 2 ^ Nat.log 2 s := + Nat.pow_le_pow_right (by norm_num) (Nat.div_le_self _ _) + _ ≤ s := Nat.pow_log_le_self 2 hs.ne' + _ ≤ s + 1 := Nat.le_succ s + +/-- **The target modes of a call with the packet shape**: at most `2 ^ (⌊log₂ s⌋ / 32768) p`. -/ +theorem modes_le_of_packetShape {x : Call} (hs : PacketShape x) {v : List ℕ × VertexDesc} + (hv : v ∈ x.net.vertices) : v.2.modes ≤ 2 ^ (Nat.log 2 x.scale / 32768) * x.prec := by + rcases hd : v.2 with t | d + · simp [VertexDesc.modes] + · obtain ⟨h1, h2, h3, h4, -, -⟩ := hs v hv d hd + simp only [VertexDesc.modes, targetModes] + calc ((List.range (d.1.tiles * d.1.nb)).filter _).length + ≤ (List.range (d.1.tiles * d.1.nb)).length := List.length_filter_le _ _ + _ = d.1.tiles * d.1.nb := List.length_range + _ ≤ 2 ^ (Nat.log 2 x.scale / 32768) * x.prec := by + rw [h3] + exact Nat.mul_le_mul (Nat.pow_le_pow_right (by norm_num) (by omega)) h4 + +/-- **The row ports of a call with the packet shape**: at most `2 ^ (⌊log₂ s⌋ / 32768)`, since +the slots of the row ports of a packet are distinct and below `2 ^ a`. -/ +theorem rowPorts_le_of_packetShape {x : Call} (hs : PacketShape x) {v : List ℕ × VertexDesc} + (hv : v ∈ x.net.vertices) (bs : List Bool) : + v.2.rowPorts bs ≤ 2 ^ (Nat.log 2 x.scale / 32768) := by + rcases hd : v.2 with t | d + · simp [VertexDesc.rowPorts] + · obtain ⟨-, h2, -, -, h5, h6⟩ := hs v hv d hd + simp only [VertexDesc.rowPorts, sidePorts, List.length_map] + have hlen := length_filter_range_getD d.2.1 (false, 0) (fun y => y.1 == true) + rw [hlen] + have hsub : ((d.2.1.filter (·.1)).map (·.2)).toFinset ⊆ Finset.range (2 ^ d.1.a) := by + intro y hy + simp only [List.mem_toFinset, List.mem_map, List.mem_filter] at hy + obtain ⟨z, ⟨hz, -⟩, rfl⟩ := hy + exact Finset.mem_range.mpr (h5 z hz) + have hcard := Finset.card_le_card hsub + rw [List.toFinset_card_of_nodup h6, Finset.card_range, List.length_map] at hcard + have hbeq : (d.2.1.filter fun y => y.1 == true) = d.2.1.filter (·.1) := by + congr 1 + rw [hbeq] + exact hcard.trans (Nat.pow_le_pow_right (by norm_num) h2) + +/-- **The cost of a leaf with the packet shape.** There is `K` such that, on a call of encoded +length `n` with `M` edges, scale `s` and precision `p` with the packet shape, writing +`A = 2 ^ (⌊log₂ s⌋ / 32768)`, direct summation takes time at most +`K (n + 1) ^ K 2 ^ M (A p + 2) ^ A` and space at most `K (n + 1) ^ K`. -/ +theorem leafCertificate_le_of_packetShape : ∃ K : ℕ, + ∀ (mk : Call → State → ℕ × DescribedNetwork VertexDesc) (x : Call), PacketShape x → + (leafCertificate mk).time x ≤ K * ((encCall x).length + 1) ^ K * 2 ^ x.edges * + (2 ^ (Nat.log 2 x.scale / 32768) * x.prec + 2) ^ 2 ^ (Nat.log 2 x.scale / 32768) ∧ + (leafCertificate mk).space x ≤ K * ((encCall x).length + 1) ^ K := by + obtain ⟨K, hK⟩ := leafCertificate_le + refine ⟨2 * K, fun mk x hs => ?_⟩ + obtain ⟨hT, hS⟩ := hK mk x (2 ^ (Nat.log 2 x.scale / 32768) * x.prec) + (2 ^ (Nat.log 2 x.scale / 32768)) fun v hv => + ⟨modes_le_of_packetShape hs hv, fun bs _ => rowPorts_le_of_packetShape hs hv bs⟩ + have hn := scale_add_prec_add_length_fl_le x + have hA := two_pow_log_div_le x.scale + have hR : (encCall x).length + 2 ^ (Nat.log 2 x.scale / 32768) * x.prec + 1 ≤ + ((encCall x).length + 1) ^ 2 := by + have : 2 ^ (Nat.log 2 x.scale / 32768) * x.prec ≤ + ((encCall x).length + 1) * (encCall x).length := Nat.mul_le_mul (by omega) (by omega) + nlinarith + have hpow : K * ((encCall x).length + 2 ^ (Nat.log 2 x.scale / 32768) * x.prec + 1) ^ K ≤ + 2 * K * ((encCall x).length + 1) ^ (2 * K) := + calc _ ≤ K * (((encCall x).length + 1) ^ 2) ^ K := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hR _) + _ = K * ((encCall x).length + 1) ^ (2 * K) := by rw [← pow_mul] + _ ≤ 2 * K * ((encCall x).length + 1) ^ (2 * K) := + Nat.mul_le_mul_right _ (by omega) + exact ⟨hT.trans (Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ hpow)), hS.trans hpow⟩ + +/-! ### The leaf bound of the analysis -/ + +/-- `(μ + 1) ^ 2 ≤ 16 · 2 ^ (μ / 2)`. -/ +private theorem succ_sq_le_two_pow (μ : ℕ) : (μ + 1) ^ 2 ≤ 16 * 2 ^ (μ / 2) := by + have hk : μ / 4 + 1 ≤ 2 ^ (μ / 4) := Nat.lt_two_pow_self + have h1 : μ + 1 ≤ 4 * 2 ^ (μ / 4) := by omega + calc (μ + 1) ^ 2 ≤ (4 * 2 ^ (μ / 4)) ^ 2 := Nat.pow_le_pow_left h1 2 + _ = 16 * 2 ^ (2 * (μ / 4)) := by rw [mul_pow, ← pow_mul, mul_comm (μ / 4)]; norm_num + _ ≤ 16 * 2 ^ (μ / 2) := Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (by norm_num) (by omega)) + +/-- **The packet factor is subexponential.** For `s ≤ m ≤ C s` and `p ≤ m ^ c`, with +`A = 2 ^ (⌊log₂ m⌋ / 32768)`, `(A p + 2) ^ A ≤ 2 ^ (K s / √⌊log₂ s⌋)` for a constant `K` depending +only on `C` and `c`: `A ≤ 2 ^ O(1) s ^ (1 / 32768)`, against `s / √⌊log₂ s⌋`. -/ +theorem exists_packetFactor_le (C c : ℕ) : ∃ K : ℕ, ∀ s m p : ℕ, 2 ≤ s → s ≤ m → m ≤ C * s → + p ≤ m ^ c → (2 ^ (Nat.log 2 m / 32768) * p + 2) ^ 2 ^ (Nat.log 2 m / 32768) ≤ + 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) := by + obtain ⟨c₀, hc₀⟩ : ∃ c₀, c₀ = Nat.log 2 C + 1 := ⟨_, rfl⟩ + refine ⟨16 * ((c₀ + 2) * (c + 1)) * 2 ^ c₀, fun s m p hs hsm hmC hp => ?_⟩ + set μ := Nat.log 2 s with hμ + set lam := Nat.log 2 m with hlam + set A := 2 ^ (lam / 32768) with hA + have hm2 : 2 ≤ m := hs.trans hsm + have hS1 : 1 ≤ Nat.sqrt μ := Nat.one_le_sqrt_log_two hs + -- `A ≤ m` and `m < 2 ^ (λ + 1)`. + have hAm : A ≤ m := (Nat.pow_le_pow_right (by norm_num) (Nat.div_le_self _ _)).trans + (Nat.pow_log_le_self 2 (by omega)) + have hmlam : m < 2 ^ (lam + 1) := Nat.lt_pow_succ_log_self (by norm_num) m + -- `λ ≤ c₀ + μ`. + have hlamμ : lam ≤ c₀ + μ := by + have hC : C < 2 ^ c₀ := hc₀ ▸ Nat.lt_pow_succ_log_self (by norm_num) C + have hs' : s < 2 ^ (μ + 1) := Nat.lt_pow_succ_log_self (by norm_num) s + have : m < 2 ^ (c₀ + μ + 1) := by + calc m ≤ C * s := hmC + _ < 2 ^ c₀ * 2 ^ (μ + 1) := Nat.mul_lt_mul'' hC hs' + _ = 2 ^ (c₀ + μ + 1) := by rw [← pow_add]; ring_nf + have := Nat.log_lt_of_lt_pow (by omega) this + omega + -- The base: `A p + 2 ≤ 2 ^ ((λ + 1) (c + 1) + 1)`. + have hbase : A * p + 2 ≤ 2 ^ ((lam + 1) * (c + 1) + 1) := by + have h1 : A * p ≤ m * m ^ c := Nat.mul_le_mul hAm hp + have h2 : 2 ≤ m * m ^ c := by + have : 1 ≤ m ^ c := Nat.one_le_pow _ _ (by omega) + nlinarith + have h3 : m * m ^ c = m ^ (c + 1) := by ring + have h4 : m ^ (c + 1) ≤ (2 ^ (lam + 1)) ^ (c + 1) := Nat.pow_le_pow_left hmlam.le _ + calc A * p + 2 ≤ 2 * m ^ (c + 1) := by omega + _ ≤ 2 * (2 ^ (lam + 1)) ^ (c + 1) := Nat.mul_le_mul_left _ h4 + _ = 2 ^ ((lam + 1) * (c + 1) + 1) := by rw [← pow_mul]; ring + -- The exponent. + have hA' : A ≤ 2 ^ c₀ * 2 ^ (μ / 32768) := by + rw [← pow_add]; exact Nat.pow_le_pow_right (by norm_num) (by omega) + have hE : ((lam + 1) * (c + 1) + 1) * A * Nat.sqrt μ ≤ + 16 * ((c₀ + 2) * (c + 1)) * 2 ^ c₀ * s := by + have h1 : (lam + 1) * (c + 1) + 1 ≤ (c₀ + 2) * (c + 1) * (μ + 1) := by + have : lam + 1 ≤ (c₀ + 1) * (μ + 1) := by nlinarith + nlinarith + have h2 : Nat.sqrt μ ≤ μ + 1 := (Nat.sqrt_le_self μ).trans (Nat.le_succ μ) + have h3 := succ_sq_le_two_pow μ + have h4 : 2 ^ (μ / 2) * 2 ^ (μ / 32768) ≤ 2 ^ μ := by + rw [← pow_add]; exact Nat.pow_le_pow_right (by norm_num) (by omega) + have h5 : 2 ^ μ ≤ s := Nat.pow_log_le_self 2 (by omega) + calc ((lam + 1) * (c + 1) + 1) * A * Nat.sqrt μ + ≤ ((c₀ + 2) * (c + 1) * (μ + 1)) * (2 ^ c₀ * 2 ^ (μ / 32768)) * (μ + 1) := + Nat.mul_le_mul (Nat.mul_le_mul h1 hA') h2 + _ = (c₀ + 2) * (c + 1) * 2 ^ c₀ * ((μ + 1) ^ 2 * 2 ^ (μ / 32768)) := by ring + _ ≤ (c₀ + 2) * (c + 1) * 2 ^ c₀ * (16 * 2 ^ (μ / 2) * 2 ^ (μ / 32768)) := + Nat.mul_le_mul_left _ (Nat.mul_le_mul_right _ h3) + _ = 16 * ((c₀ + 2) * (c + 1)) * 2 ^ c₀ * (2 ^ (μ / 2) * 2 ^ (μ / 32768)) := by ring + _ ≤ 16 * ((c₀ + 2) * (c + 1)) * 2 ^ c₀ * s := Nat.mul_le_mul_left _ (h4.trans h5) + have hE' : ((lam + 1) * (c + 1) + 1) * A ≤ 16 * ((c₀ + 2) * (c + 1)) * 2 ^ c₀ * s / Nat.sqrt μ := + (Nat.le_div_iff_mul_le (by omega)).mpr hE + calc (A * p + 2) ^ A ≤ (2 ^ ((lam + 1) * (c + 1) + 1)) ^ A := Nat.pow_le_pow_left hbase _ + _ = 2 ^ (((lam + 1) * (c + 1) + 1) * A) := by rw [← pow_mul] + _ ≤ 2 ^ (16 * ((c₀ + 2) * (c + 1)) * 2 ^ c₀ * s / Nat.sqrt μ) := + Nat.pow_le_pow_right (by norm_num) hE' + +/-- **The leaf bound of the resource analysis.** For all constants `C`, `c` and `s₀` there is `K` +such that a call with the packet shape, scale `m` with `s ≤ m ≤ C s` and at most `2 m` edges takes +time at most `K (n + 1) ^ K 2 ^ (K s / √⌊log₂ s⌋)` and space at most `K (n + 1) ^ K` at a leaf, +provided that from `s₀` on it has at most `leafSize m` edges and precision at most `m ^ c`. Below +`s₀`, the scale is bounded, so the packet factor is polynomial and `2 ^ M` is a constant; from +`s₀` on, `2 ^ M ≤ 2 ^ (C s / √⌊log₂ s⌋)` and the packet factor is subexponential +(`exists_packetFactor_le`). -/ +theorem exists_leafCertificate_le (C c s₀ : ℕ) : ∃ K : ℕ, + ∀ (mk : Call → State → ℕ × DescribedNetwork VertexDesc) (s : ℕ) (x : Call), 2 ≤ s → + s ≤ x.scale → x.scale ≤ C * s → PacketShape x → x.edges ≤ 2 * x.scale → + (s₀ ≤ s → x.edges ≤ leafSize x.scale ∧ x.prec ≤ x.scale ^ c) → + (leafCertificate mk).time x ≤ + K * ((encCall x).length + 1) ^ K * 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) ∧ + (leafCertificate mk).space x ≤ K * ((encCall x).length + 1) ^ K := by + obtain ⟨K₀, hK₀⟩ := leafCertificate_le_of_packetShape + obtain ⟨K₁, hK₁⟩ := exists_packetFactor_le C c + obtain ⟨Ks, hKs⟩ : ∃ Ks, Ks = K₀ * 2 ^ (2 * (C * s₀)) * (C * s₀ + 2) ^ (C * s₀) := ⟨_, rfl⟩ + refine ⟨Ks + K₀ + C * s₀ + C + K₁, fun mk s x hs hsm hmC hshape hM hbig => ?_⟩ + obtain ⟨hT, hS⟩ := hK₀ mk x hshape + set n := (encCall x).length with hn + set K := Ks + K₀ + C * s₀ + C + K₁ with hK + set S := Nat.sqrt (Nat.log 2 s) with hSdef + have hS1 : 1 ≤ S := Nat.one_le_sqrt_log_two hs + have hB1 : 1 ≤ n + 1 := by omega + have hX1 : 1 ≤ 2 ^ (K * s / S) := Nat.one_le_two_pow + have hnK : (n + 1) ^ K₀ ≤ (n + 1) ^ K := Nat.pow_le_pow_right hB1 (by omega) + refine ⟨?_, hS.trans (Nat.mul_le_mul (by omega) hnK)⟩ + set A := 2 ^ (Nat.log 2 x.scale / 32768) with hA + have hAm : A ≤ x.scale := (Nat.pow_le_pow_right (by norm_num) (Nat.div_le_self _ _)).trans + (Nat.pow_log_le_self 2 (by omega)) + rcases lt_or_ge s s₀ with hsmall | hlarge + · -- Below `s₀`: constants and a polynomial. + have hmC' : x.scale ≤ C * s₀ := hmC.trans (Nat.mul_le_mul_left _ hsmall.le) + have hp : x.prec ≤ n := by have := scale_add_prec_add_length_fl_le x; omega + have h2M : 2 ^ x.edges ≤ 2 ^ (2 * (C * s₀)) := + Nat.pow_le_pow_right (by norm_num) (by omega) + have hbase : A * x.prec + 2 ≤ (C * s₀ + 2) * (n + 1) := by + have : A * x.prec ≤ C * s₀ * n := Nat.mul_le_mul (hAm.trans hmC') hp + nlinarith + have hfac : (A * x.prec + 2) ^ A ≤ (C * s₀ + 2) ^ (C * s₀) * (n + 1) ^ (C * s₀) := by + calc (A * x.prec + 2) ^ A ≤ ((C * s₀ + 2) * (n + 1)) ^ A := Nat.pow_le_pow_left hbase _ + _ ≤ ((C * s₀ + 2) * (n + 1)) ^ (C * s₀) := + Nat.pow_le_pow_right (Nat.one_le_iff_ne_zero.mpr (by positivity)) (hAm.trans hmC') + _ = (C * s₀ + 2) ^ (C * s₀) * (n + 1) ^ (C * s₀) := mul_pow _ _ _ + calc (leafCertificate mk).time x ≤ K₀ * (n + 1) ^ K₀ * 2 ^ x.edges * (A * x.prec + 2) ^ A := hT + _ ≤ K₀ * (n + 1) ^ K₀ * 2 ^ (2 * (C * s₀)) * + ((C * s₀ + 2) ^ (C * s₀) * (n + 1) ^ (C * s₀)) := + Nat.mul_le_mul (Nat.mul_le_mul_left _ h2M) hfac + _ = Ks * (n + 1) ^ (K₀ + C * s₀) := by rw [hKs, pow_add]; ring + _ ≤ K * (n + 1) ^ K := Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right hB1 (by omega)) + _ ≤ K * (n + 1) ^ K * 2 ^ (K * s / S) := Nat.le_mul_of_pos_right _ hX1 + · -- From `s₀` on: the leaf size and the packet factor. + obtain ⟨hleaf, hp⟩ := hbig hlarge + have hlog : S ≤ Nat.sqrt (Nat.log 2 x.scale) := Nat.sqrt_log_two_mono hsm + have hMs : x.edges ≤ C * s / S := + calc x.edges ≤ x.scale / Nat.sqrt (Nat.log 2 x.scale) := hleaf + _ ≤ x.scale / S := Nat.div_le_div_left hlog hS1 + _ ≤ C * s / S := Nat.div_le_div_right hmC + have hfac := hK₁ s x.scale x.prec hs hsm hmC hp + have hCK : (C + K₁) * s ≤ K * s := Nat.mul_le_mul_right _ (by omega) + have hexp : C * s / S + K₁ * s / S ≤ K * s / S := + Nat.div_add_div_le_add_div.trans (Nat.div_le_div_right (by rw [← add_mul]; exact hCK)) + calc (leafCertificate mk).time x ≤ K₀ * (n + 1) ^ K₀ * 2 ^ x.edges * (A * x.prec + 2) ^ A := hT + _ ≤ K₀ * (n + 1) ^ K₀ * 2 ^ (C * s / S) * 2 ^ (K₁ * s / S) := + Nat.mul_le_mul (Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (by norm_num) hMs)) hfac + _ = K₀ * (n + 1) ^ K₀ * 2 ^ (C * s / S + K₁ * s / S) := by rw [pow_add]; ring + _ ≤ K * (n + 1) ^ K * 2 ^ (K * s / S) := + Nat.mul_le_mul (Nat.mul_le_mul (by omega) hnK) (Nat.pow_le_pow_right (by norm_num) hexp) + +end FastContraction + +end Cslib.Circuits.Frontier diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionMachine.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionMachine.lean index f93e9b6050..922fff07f2 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionMachine.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionMachine.lean @@ -118,12 +118,28 @@ variable (mk : Call → State → ℕ × DescribedNetwork VertexDesc) /-- **The leaf certificate**: direct summation over the coefficient lists of `A_p`, with the native evaluator of the vertex descriptors, tagged with the depth. -/ -noncomputable def leafCertificate : NativeCertificate (scheme mk).leaf encCall encValue := +@[expose] noncomputable def leafCertificate : NativeCertificate (scheme mk).leaf encCall encValue := ((NativeCertificate.ofPolyTime depth_polyTime).prod ((DescribedNetwork.contractionCertificate VertexDesc.entry SumOps.galois_polyTime VertexDesc.entryCertificate).comp (NativeCertificate.ofPolyTime leafInput_polyTime))).congr fun _ => rfl +/-- The time of a leaf: the depth, the input of direct summation, and direct summation. -/ +theorem leafCertificate_time (x : Call) : + (leafCertificate mk).time x = + (NativeCertificate.ofPolyTime depth_polyTime).time x + + ((NativeCertificate.ofPolyTime leafInput_polyTime).time x + + (DescribedNetwork.contractionCertificate VertexDesc.entry SumOps.galois_polyTime + VertexDesc.entryCertificate).time ((x.prec, x.fl), x.net)) := rfl + +/-- The space of a leaf. -/ +theorem leafCertificate_space (x : Call) : + (leafCertificate mk).space x = + (NativeCertificate.ofPolyTime depth_polyTime).space x + + ((NativeCertificate.ofPolyTime leafInput_polyTime).space x + + (DescribedNetwork.contractionCertificate VertexDesc.entry SumOps.galois_polyTime + VertexDesc.entryCertificate).space ((x.prec, x.fl), x.net)) := rfl + /-! ### The root -/ /-- The exponent `t` of the modulus, with `2 ^ (t + 1) > 4 ⌊log₂ m⌋ + 2`. -/ diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSchedule.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSchedule.lean new file mode 100644 index 0000000000..e367f44adf --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSchedule.lean @@ -0,0 +1,335 @@ +/- +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.FastContractionDerivation +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionMachine +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionStep +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.NativeChildBounds +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ScheduleCount +import Mathlib.Data.List.GetD + +/-! +# The native contraction recursion follows the schedule + +For a root with `m` edges, the calls of the native recursion +(`FastContraction.scheme FastContraction.nativeMk`) follow the parameter schedule of +`Cslib.Circuits.Frontier.ContractionSchedule` at scale `m` (§D.4.2 of [OpenAI2026ETH], p. 58): +once `m` is large enough for the schedule's certificate `ContractionSchedule.ActiveBounds`, every +reached call either has at most `leafSize m` edges or is an active call of the schedule +(`ContractionSchedule.Active`), and every reached call of the second kind passes the test +`FastContraction.active` of the machine. + +**The invariant** (`FastContraction.OnSchedule`): the call keeps the root's scale and modulus, is +well-formed, has maximum degree at most `degreeBound m`, has fewer edges than its bound, and is +small or active in the schedule. It passes from an active call to its native children +(`FastContraction.OnSchedule.child`) by round 10's child facts in the native numbering: at most +`M / 16` edges (`NativeChild.sixteen_mul_numEdges_nativeChild_le`), the degree bound +(`NativeChild.length_le_of_mem_vertices_nativeChild`), and the schedule's precisions +(`ContractionSchedule.ActiveBounds.nodePrecision_le`). + +**Consequences** for the reached calls: a call that the machine treats as a leaf has at most +`leafSize m` edges (`FastContraction.OnSchedule.edges_le_leafSize`), an active one lies above +depth `⌊log₂ m⌋ - 2` (`FastContraction.OnSchedule.depth_add_two_le`) and has at most +`2 ^ (2 ⌊log₂ m⌋ + e_d)` children (`FastContraction.OnSchedule.length_children_le`), by the mode +count (D.15). So the root has a derivation with at most `2 ^ ((245760 C + 37) m / √⌊log₂ m⌋)` nodes +(`FastContraction.exists_eval_onSchedule`, by +`ContractionSchedule.recursionBound_le_two_pow_div_sqrt_log_two`). + +## Main definitions + +* `Cslib.Circuits.Frontier.FastContraction.OnSchedule`: the invariant. + +## Main results + +* `Cslib.Circuits.Frontier.FastContraction.OnSchedule.active_eq_true`: an active call of the + schedule passes the machine's test. +* `Cslib.Circuits.Frontier.FastContraction.OnSchedule.child`: the invariant passes to the native + children. +* `Cslib.Circuits.Frontier.FastContraction.Reach.onSchedule`: every reached call satisfies it. +* `Cslib.Circuits.Frontier.FastContraction.OnSchedule.edges_le_leafSize`: the leaves are small. +* `Cslib.Circuits.Frontier.FastContraction.OnSchedule.length_children_le`: the number of children. +* `Cslib.Circuits.Frontier.FastContraction.exists_eval_onSchedule`: the derivation of the root with + its node count. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.2 (p. 58) and + §D.4.6–§D.4.7 (pp. 63–64). +-/ + +public section + +namespace Cslib.Circuits.Frontier.FastContraction + +open ContractionSchedule ChildCursor NativeRecovery NativeChild + +/-- **A call on the schedule** of a root with `m` edges, for the constant `C`: it keeps the root's +scale and modulus, is well-formed, has maximum degree at most `degreeBound m` and fewer edges than +its bound, and has at most `leafSize m` edges or is an active call of the schedule. -/ +structure OnSchedule (C m : ℕ) (x : Call) : Prop where + /-- The scale is the root's number of edges. -/ + scale_eq : x.scale = m + /-- The modulus is the root's. -/ + fl_eq : x.fl = modulus m + /-- The call is well-formed. -/ + wf : WF x + /-- The maximum degree is at most `degreeBound m`. -/ + degree_le : ∀ v ∈ x.net.vertices, v.1.length ≤ degreeBound m + /-- The call has fewer edges than its bound. -/ + edges_lt_bound : x.edges < x.bound + /-- The call is small, or an active call of the schedule. -/ + small_or_active : x.edges ≤ leafSize m ∨ Active C m x.depth x.edges x.prec + +/-- `4 ⌊log₂ m⌋ ≤ 2 ⬝ 3 ^ t` for the exponent `t` of the modulus. -/ +theorem four_mul_log_le_length_modulus (m : ℕ) : 4 * Nat.log 2 m ≤ (modulus m).length := by + rw [length_modulus] + set t := modulusExp m + have h1 : 4 * Nat.log 2 m + 2 < 2 ^ (t + 1) := Nat.lt_pow_succ_log_self one_lt_two _ + have h2 : 2 ^ t ≤ 3 ^ t := Nat.pow_le_pow_left (by norm_num) t + rw [pow_succ] at h1 + omega + +variable {C m : ℕ} {x : Call} + +namespace OnSchedule + +/-- **An active call of the schedule passes the machine's test** once the schedule's certificate +holds: the certificate gives `1 ≤ u ≤ M`, `u ≤ a` and the number of points, and the invariant gives +the degrees and the edge bound. -/ +theorem active_eq_true (hB : ∀ d M p, Active C m d M p → ActiveBounds C m d M p) + (h : OnSchedule C m x) (hA : Active C m x.depth x.edges x.prec) : active x = true := by + have hb := hB _ _ _ hA + have hpts : numPoints x ≤ 2 ^ x.fl.length := by + unfold numPoints slots + rw [h.scale_eq, h.fl_eq] + exact hb.points_le.trans (Nat.pow_le_pow_right (by norm_num) + (four_mul_log_le_length_modulus m)) + simp only [active, decide_eq_true_eq, levels, slots, h.scale_eq] + refine ⟨hA.leafSize_lt, hb.one_le_taper, hb.taper_le_edges, ?_, h.degree_le, ?_, + h.edges_lt_bound⟩ + · rw [slotBits_eq]; omega + · simpa only [numPoints, slots, h.scale_eq] using hpts + +/-- An active call on the schedule is active in the schedule: it has more than `leafSize m` +edges. -/ +theorem active_of_active (h : OnSchedule C m x) (ha : active x = true) : + Active C m x.depth x.edges x.prec := by + have ha' := ha + simp only [active, decide_eq_true_eq] at ha' + rcases h.small_or_active with hs | hA + · rw [h.scale_eq] at ha' + omega + · exact hA + +/-- **The leaves are small**: a call on the schedule that the machine treats as a leaf has at most +`leafSize m` edges, once the schedule's certificate holds. -/ +theorem edges_le_leafSize (hB : ∀ d M p, Active C m d M p → ActiveBounds C m d M p) + (h : OnSchedule C m x) (hl : active x = false) : x.edges ≤ leafSize m := by + rcases h.small_or_active with hs | hA + · exact hs + · rw [h.active_eq_true hB hA] at hl + cases hl + +/-- **An active call lies above depth `⌊log₂ m⌋ - 2`**, once the schedule's certificate holds. -/ +theorem depth_add_two_le (hB : ∀ d M p, Active C m d M p → ActiveBounds C m d M p) + (h : OnSchedule C m x) (ha : active x = true) : x.depth + 2 ≤ Nat.log 2 m := + (hB _ _ _ (h.active_of_active ha)).depth_add_two_le + +/-- The level of the `j`-th node of positive multiplicity is below `u`. -/ +theorem level_lt_levels_of_lt {j : ℕ} (hj : j < (nodes x).length) : + level x ((nodes x).getD j 0) < levels x := by + have hkmem : (nodes x).getD j 0 ∈ nodes x := by + rw [List.getD_eq_getElem _ _ hj]; exact List.getElem_mem hj + obtain ⟨hk, -, hq⟩ := mem_nodes.mp hkmem + rw [level_eq hk] + exact padicValInt_lt_of_taperMult_pos_left (by rwa [← mult_eq _ _ hk]) + +/-- The level of the node of a child of an active call is below `u`. -/ +theorem level_lt_levels {c : State} (hc : c ∈ children x) : + level x ((nodes x).getD c.1 0) < levels x := + level_lt_levels_of_lt (lt_of_mem_children hc).1 + +/-- **The invariant passes to the native children** of an active call, once the schedule's +certificate holds: a child has at most a sixteenth of the edges, keeps the degree bound, and its +precision is within the schedule. -/ +theorem child (hB : ∀ d M p, Active C m d M p → ActiveBounds C m d M p) (h : OnSchedule C m x) + (ha : active x = true) {c : State} (hc : c ∈ children x) : + OnSchedule C m (FastContraction.child x nativeMk c) := by + have hA := h.active_of_active ha + have hb := hB _ _ _ hA + obtain ⟨-, -, hg⟩ := lt_of_mem_children hc + have hK := pow_slots_le_edges_of_active ha + have hu := level_lt_levels hc + have ha' := ha + simp only [active, decide_eq_true_eq] at ha' + obtain ⟨-, -, -, hua, -, -, -⟩ := ha' + have hia : level x ((nodes x).getD c.1 0) < slots x := hu.trans_le hua + have hslots : slots x = slotBits m x.depth := by rw [slots, h.scale_eq] + have hlevels : levels x = taper m x.depth := by rw [levels, h.scale_eq] + -- The child's edges. + have h16 : 16 * (FastContraction.child x nativeMk c).edges ≤ x.edges := by + have := sixteen_mul_numEdges_nativeChild_le h.wf.2 hK hia h.degree_le + (Δ := degreeBound m) (by rw [hslots]; exact hb.degree_mul_pairs_sq_le) x.fl + (nodePrec x c.1) (node (slots x) ((nodes x).getD c.1 0)) ((points x).getD c.2.1 []) + c.2.2.1 ⟨c.2.2.2, hg⟩ + simpa only [FastContraction.child, nativeMk_eq h.wf ha hc, Call.edges] using this + have hM := one_le_edges_of_active ha + refine ⟨h.scale_eq, h.fl_eq, wfChildren_nativeMk x h.wf ha c hc, fun v hv => ?_, ?_, ?_⟩ + · refine length_le_of_mem_vertices_nativeChild h.wf.2 hK hia h.degree_le + (by rw [hslots]; exact hb.two_mul_slots_le) x.fl (nodePrec x c.1) + (node (slots x) ((nodes x).getD c.1 0)) ((points x).getD c.2.1 []) c.2.2.1 ⟨c.2.2.2, hg⟩ ?_ + simpa only [FastContraction.child, nativeMk_eq h.wf ha hc] using hv + · change _ < x.edges + omega + · by_cases hs : (FastContraction.child x nativeMk c).edges ≤ leafSize m + · exact Or.inl hs + · refine Or.inr (hA.child h16 (by omega) ?_) + change nodePrec x c.1 ≤ _ + unfold nodePrec + rw [hslots] + refine hb.nodePrecision_le _ _ (by rw [← hlevels]; exact hu) ?_ + have := taperStep_mul_le x.scale x.depth x.edges + rw [h.scale_eq] at this + simpa only [step, h.scale_eq] using this + +end OnSchedule + +/-- **Every reached call is on the schedule**, from a root on the schedule, once the schedule's +certificate holds. -/ +theorem Reach.onSchedule (hB : ∀ d M p, Active C m d M p → ActiveBounds C m d M p) {x₀ : Call} + (h₀ : OnSchedule C m x₀) (h : Reach nativeMk x₀ x) : OnSchedule C m x := by + induction h with + | root => exact h₀ + | step c _ ha hc ih => exact ih.child hB ha hc + +/-- **The root is on the schedule**: a well-formed root with `m` edges, at scale `m` with the +modulus of `m`, of maximum degree at most `degreeBound m`, with edge bound `m + 1` and precision at +most `C m` for `1 ≤ C`. -/ +theorem onSchedule_root {x₀ : Call} (hC : 1 ≤ C) (hs : x₀.scale = m) (he : x₀.edges = m) + (hfl : x₀.fl = modulus m) (hwf : WF x₀) + (hdeg : ∀ v ∈ x₀.net.vertices, v.1.length ≤ degreeBound m) + (hb : x₀.bound = m + 1) (hd : x₀.depth = 0) (hp : x₀.prec ≤ C * m) : OnSchedule C m x₀ := by + refine ⟨hs, hfl, hwf, hdeg, by omega, ?_⟩ + by_cases hl : x₀.edges ≤ leafSize m + · exact Or.inl hl + · refine Or.inr ?_ + rw [hd, he] + exact Active.root (Nat.le_mul_of_pos_left m hC) (by omega) hp + +/-! ### The number of children -/ + +/-- **The tuples of weight below `p` of the modes** are the mode budget of the weights `b + 1`. -/ +theorem length_budgetTuples_modeWeights (P T p : ℕ) : + (BudgetTuples.budgetTuples (modeWeights P T p) p).length = + Finset.card (TensorNetwork.modeBudget + (fun Z : Fin P × Fin T × Fin p => (Z.2.2 : ℕ) + 1) p) := by + have h := BudgetTuples.sum_filter_weight_lt_eq (nodup_modeList P T p) mem_modeList + (w := fun Z : Fin P × Fin T × Fin p => (Z.2.2 : ℕ) + 1) (fun _ => Nat.succ_pos _) p + (S := ℕ) (fun _ => 1) + rw [map_modeList_weight] at h + simp only [Finset.sum_const, smul_eq_mul, mul_one, List.map_const', List.sum_replicate] at h + rw [TensorNetwork.modeBudget, h] + +/-- **The length of the cursor's list**: at most `T n B r` for `T` nodes, `n` points, at most `B` +tuples at each node and `r` groups. -/ +theorem length_cursorList_le {ws : ℕ → List ℕ} {ps : ℕ → ℕ} {T n r B : ℕ} + (hB : ∀ t < T, (BudgetTuples.budgetTuples (ws t) (ps t)).length ≤ B) : + (cursorList ws ps T n r).length ≤ T * n * B * r := by + have hnode : ∀ t < T, (nodeBlock ws ps n r t).length ≤ n * B * r := fun t ht => by + simp only [nodeBlock, pointBlock, groupBlock, List.length_flatMap, List.length_map, + List.length_range, List.map_const', List.sum_replicate, smul_eq_mul] + have : ((List.range n).map fun _ => + (BudgetTuples.budgetTuples (ws t) (ps t)).length * r).sum ≤ n * (B * r) := by + rw [List.map_const', List.sum_replicate, smul_eq_mul, List.length_range] + exact Nat.mul_le_mul_left _ (Nat.mul_le_mul_right _ (hB t ht)) + simpa [Nat.mul_assoc] using this + simp only [cursorList, List.length_flatMap] + calc ((List.range T).map fun t => (nodeBlock ws ps n r t).length).sum + ≤ ((List.range T).map fun _ => n * B * r).sum := + List.sum_le_sum fun t ht => hnode t (List.mem_range.mp ht) + _ = T * n * B * r := by + rw [List.map_const', List.sum_replicate, smul_eq_mul, List.length_range]; ring + +/-- The nodes of positive multiplicity are at most `2 ^ (a + 1)`. -/ +theorem length_nodes_le (x : Call) : (nodes x).length ≤ 2 ^ (slots x + 1) := + (List.length_filter_le _ _).trans List.length_range.le + +namespace OnSchedule + +/-- **The number of children of an active call** on the schedule is at most +`2 ^ (2 ⌊log₂ m⌋ + e_d)`, `e_d = branchExponent C m d`, once the schedule's certificate holds: the +nodes, points and `64` groups contribute `2 ^ (2 ⌊log₂ m⌋)`, and each node has at most `2 ^ e_d` +tuples of exponents (the mode count (D.15)). -/ +theorem length_children_le (hB : ∀ d M p, Active C m d M p → ActiveBounds C m d M p) + (h : OnSchedule C m x) (ha : active x = true) : + (children x).length ≤ 2 ^ (2 * Nat.log 2 m + branchExponent C m x.depth) := by + have hA := h.active_of_active ha + have hb := hB _ _ _ hA + have hK := pow_slots_le_edges_of_active ha + have hslots : slots x = slotBits m x.depth := by rw [slots, h.scale_eq] + have hlevels : levels x = taper m x.depth := by rw [levels, h.scale_eq] + have hr := rows_le_of_isRowsFirstBipartite h.wf.2 (one_le_edges_of_active ha) + have hP : (packing x).2.1 * 2 ^ slots x ≤ 3 * x.edges := + packing_eq hr ▸ numPackets_nativeParentPacking_mul_le h.wf.2 hK h.degree_le + (by rw [hslots]; exact hb.degree_mul_pairs_sq_le) + (by rw [hslots]; exact hb.slots_mul_pairs_le) + have hT : ∀ j < (nodes x).length, (BudgetTuples.budgetTuples (weights x j) + (nodePrec x j)).length ≤ 2 ^ branchExponent C m x.depth := fun j hj => by + have hu := level_lt_levels_of_lt hj + set i := level x ((nodes x).getD j 0) + have e1 : nodePrec x j = nodePrecision x.prec (step x) (slotBits m x.depth) x.edges i := by + rw [nodePrec, hslots] + have e2 : weights x j = modeWeights (packing x).2.1 (2 ^ (i + 1)) + (nodePrecision x.prec (step x) (slotBits m x.depth) x.edges i) := by + rw [weights, ← e1] + have hh : step x * taper m x.depth ≤ 3 * x.edges + taper m x.depth := by + have := taperStep_mul_le x.scale x.depth x.edges + rw [h.scale_eq] at this + rw [step, h.scale_eq] + exact this + have hP' : Fintype.card (Fin (packing x).2.1) * 2 ^ slotBits m x.depth ≤ 3 * x.edges := by + rw [Fintype.card_fin, ← hslots]; exact hP + rw [e1, e2, length_budgetTuples_modeWeights] + exact hb.card_modeBudget_le hA (by rw [← hlevels]; exact hu) hh hP' + have hc := length_cursorList_le (n := numPoints x) (r := 64) hT + have hbr := hb.branching_le + have hN := length_nodes_le x + rw [hslots, pow_succ] at hN + rw [children] + calc (cursorList (weights x) (nodePrec x) (nodes x).length (numPoints x) 64).length + ≤ (nodes x).length * numPoints x * 2 ^ branchExponent C m x.depth * 64 := hc + _ ≤ 2 * 2 ^ slotBits m x.depth * numPoints x * 64 * 2 ^ branchExponent C m x.depth := by + have : (nodes x).length * numPoints x ≤ 2 * 2 ^ slotBits m x.depth * numPoints x := + Nat.mul_le_mul_right _ (by omega) + calc _ = (nodes x).length * numPoints x * 64 * 2 ^ branchExponent C m x.depth := by ring + _ ≤ _ := Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ this) + _ ≤ 2 ^ (2 * Nat.log 2 m) * 2 ^ branchExponent C m x.depth := by + refine Nat.mul_le_mul_right _ ?_ + simpa only [numPoints, slots, h.scale_eq] using hbr + _ = 2 ^ (2 * Nat.log 2 m + branchExponent C m x.depth) := (pow_add _ _ _).symm + +end OnSchedule + +/-! ### The derivation on the schedule -/ + +/-- **The derivation of a root on the schedule, with its node count** (§D.4.7, p. 64): once the +schedule's certificate holds at scale `m ≥ 2`, a root on the schedule at depth `0` has a derivation +of its tagged value over the reached calls with at most `2 ^ ((245760 C + 37) m / √⌊log₂ m⌋)` nodes +and `⌊log₂ m⌋` stack levels. -/ +theorem exists_eval_onSchedule (hB : ∀ d M p, Active C m d M p → ActiveBounds C m d M p) + {x₀ : Call} (h₀ : OnSchedule C m x₀) (hd : x₀.depth = 0) (hm : 2 ≤ m) : + ∃ N H, (scheme nativeMk).Eval (reachInv nativeMk x₀) x₀ (0, value nativeMk x₀) N H ∧ + N ≤ 2 ^ ((245760 * C + 37) * m / Nat.sqrt (Nat.log 2 m)) ∧ H ≤ Nat.log 2 m := by + obtain ⟨N, H, he, hN, hH⟩ := exists_eval_reachInv_count hd (Nat.log 2 m) + (fun d => 2 ^ (2 * Nat.log 2 m + branchExponent C m d)) fun x hx ha => by + have h := hx.onSchedule hB h₀ + exact ⟨by have := h.depth_add_two_le hB ha; omega, h.length_children_le hB ha⟩ + exact ⟨N, H, he, hN.trans (recursionBound_le_two_pow_div_sqrt_log_two C hm le_rfl), hH⟩ + +end Cslib.Circuits.Frontier.FastContraction diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionShape.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionShape.lean new file mode 100644 index 0000000000..76f982e9f8 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionShape.lean @@ -0,0 +1,316 @@ +/- +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.FastContractionSchedule +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.NativeChildPolyTime +import Mathlib.Data.List.GetD + +/-! +# The shapes of the calls of the native contraction recursion + +Structural bounds on every call reached from a root of the native recursion +(`FastContraction.scheme FastContraction.nativeMk`) with `m` edges, valid for every input, whatever +the schedule: they are what makes the calls, frames and values polynomially long. + +**The invariant** (`FastContraction.Shape`). A reached call at depth `d` keeps the root's scale and +modulus, is well-formed, has at most `2 m` edges, precision at most `p₀ + 40 m² d` for the root's +precision `p₀`, at most `V₀ + m² d` vertices for the root's `V₀` vertices, as many rows (unless it +is the root), and every vertex descriptor is a table of the root or a packet descriptor whose fields +are bounded (`FastContraction.PacketBound`). It passes to the native children +(`FastContraction.Shape.child`): a child has at most twice the edges of its parent +(`NativeChild.numEdges_nativeChild_le`), its precision `p_t = p + 8 h 2 ^ (a - i) + 8 M (a + 1)` is +at most `p + 40 m²` since `2 ^ a ≤ m`, and it adds at most `M (2 ^ a) ^ 12 ≤ m²` packet vertices +(`NativeChild.numPackets_nativeParentPacking_le`). + +## Main definitions + +* `Cslib.Circuits.Frontier.FastContraction.PacketBound`: the bounded packet descriptors. +* `Cslib.Circuits.Frontier.FastContraction.Shape`: the invariant. + +## Main results + +* `Cslib.Circuits.Frontier.FastContraction.Shape.child`: the invariant passes to the native + children. +* `Cslib.Circuits.Frontier.FastContraction.Reach.shape`: every reached call satisfies it. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.6–§D.4.7 (pp. 63–64). +-/ + +public section + +namespace Cslib.Circuits.Frontier.FastContraction + +open ContractionSchedule ChildCursor NativeRecovery NativeChild + +/-- **A bounded packet descriptor** for a root with modulus `fl` and `m` edges, at precision at most +`P`, on a vertex with `k` ports: its precision is at most `P` and is its number of exponents per +tile, its modulus is `fl`, it has `2 ^ a` slots with `a ≤ ⌊log₂ m⌋`, `2 ^ (i + 1)` tiles with +`i ≤ a`, a grid point of size at most `2 ^ a`, no column list, a 0/1 interpolation value with at +most `e` coordinates, `k` tags with slots below `2 ^ a`, and at most `2 ^ (i + 1) p` exponents, each +at most `p`. -/ +@[expose] def PacketBound (fl : List ℕ) (m P k : ℕ) (d : NativePacket.PacketDesc) : Prop := + d.1.p ≤ P ∧ d.1.nb = d.1.p ∧ d.1.fl = fl ∧ d.1.a ≤ Nat.log 2 m ∧ d.1.L = 2 ^ d.1.a ∧ + d.1.i ≤ d.1.a ∧ d.1.tiles = 2 ^ (d.1.i + 1) ∧ d.1.t.natAbs ≤ 2 ^ d.1.a ∧ d.1.cols = [] ∧ + d.1.ζ.length ≤ fl.length ∧ (∀ z ∈ d.1.ζ, z ≤ 1) ∧ d.2.1.length = k ∧ + (∀ b ∈ d.2.1, b.2 < 2 ^ d.1.a) ∧ d.2.2.length ≤ d.1.tiles * d.1.p ∧ ∀ b ∈ d.2.2, b ≤ d.1.p + +theorem PacketBound.mono {fl : List ℕ} {m P P' k : ℕ} {d : NativePacket.PacketDesc} + (h : PacketBound fl m P k d) (hP : P ≤ P') : PacketBound fl m P' k d := + ⟨h.1.trans hP, h.2⟩ + +/-- **The shape of a call** reached from a root `x₀` with `m` edges, precision `p₀` and `V₀` +vertices, at depth `d`. -/ +structure Shape (x₀ x : Call) : Prop where + /-- The scale is the root's. -/ + scale_eq : x.scale = x₀.scale + /-- The modulus is the root's. -/ + fl_eq : x.fl = x₀.fl + /-- The call is well-formed. -/ + wf : WF x + /-- The bound plus the depth does not exceed the root's. -/ + bound_add_depth_le : x.bound + x.depth ≤ x₀.bound + x₀.depth + /-- At most twice the root's number of edges. -/ + edges_le : x.edges ≤ 2 * x₀.edges + /-- The precision grows by at most `40 m²` per level. -/ + prec_le : x.prec ≤ x₀.prec + x.depth * (40 * x₀.edges ^ 2) + /-- The vertices grow by at most `m²` per level. -/ + vertices_le : x.net.vertices.length ≤ x₀.net.vertices.length + x.depth * x₀.edges ^ 2 + /-- The rows are the root's or at most the vertices of a parent. -/ + rows_le : x = x₀ ∨ x.rows ≤ x₀.net.vertices.length + x.depth * x₀.edges ^ 2 + /-- Every descriptor is a descriptor of the root or a bounded packet descriptor. -/ + desc : ∀ v ∈ x.net.vertices, (∃ w ∈ x₀.net.vertices, v.2 = w.2) ∨ + ∃ d, v.2 = .inr d ∧ + PacketBound x₀.fl x₀.edges (x₀.prec + x.depth * (40 * x₀.edges ^ 2)) v.1.length d + +/-- The exponent tuple of a child of an active call has entries below the node's precision. -/ +theorem lt_nodePrec_of_mem_children {x : Call} {c : State} (hc : c ∈ children x) : + ∀ b ∈ c.2.2.1, b < nodePrec x c.1 := by + simp only [children, cursorList, nodeBlock, pointBlock, groupBlock, List.mem_flatMap, + List.mem_range, List.mem_map] at hc + obtain ⟨j, -, i, -, β, hβ, g, -, rfl⟩ := hc + exact fun b hb => BudgetTuples.lt_of_mem_budgetTuples (weights_pos j) hβ hb + +/-- The ports of a vertex of a well-formed call are at most its edges. -/ +theorem length_le_edges_of_wf {x : Call} (hx : WF x) {v : List ℕ × VertexDesc} + (hv : v ∈ x.net.vertices) : v.1.length ≤ x.edges := by + obtain ⟨k, hk, rfl⟩ := List.getElem_of_mem hv + have hnd : (x.net.vertices[k]).1.Nodup := nodup_ports hx.2 ⟨k, hk⟩ + have hsub : (x.net.vertices[k]).1.toFinset ⊆ Finset.range x.edges := fun j hj => + Finset.mem_range.mpr (hx.2.1 _ (List.getElem_mem hk) j (List.mem_toFinset.mp hj)) + have := Finset.card_le_card hsub + rw [List.toFinset_card_of_nodup hnd, Finset.card_range] at this + simpa using this + +section Child + +variable {x₀ x : Call} + +/-- The schedule's numbers at an active call at scale `m`: `a ≤ ⌊log₂ m⌋`, `2 ^ (12 a) ≤ m`, +`u ≤ ⌊log₂ m⌋ < m`, and `h ≤ 3 M + u`. -/ +theorem slots_facts (ha : active x = true) : + slots x ≤ Nat.log 2 x.scale ∧ (2 ^ slots x) ^ 12 ≤ x.scale ∧ 2 ^ slots x ≤ x.scale ∧ + levels x ≤ Nat.log 2 x.scale ∧ Nat.log 2 x.scale < x.scale ∧ + step x ≤ 3 * x.edges + levels x := by + have ha' := ha + simp only [active, decide_eq_true_eq] at ha' + obtain ⟨-, hu, -, -, -, -, -⟩ := ha' + set L := Nat.log 2 x.scale + have hL1 : 1 ≤ L := by + have : levels x = L / 2 ^ (17 + x.depth) := rfl + rcases Nat.eq_zero_or_pos L with h0 | h0 + · rw [this, h0, Nat.zero_div] at hu; omega + · exact h0 + have hs0 : x.scale ≠ 0 := by + intro h0; simp only [L, h0, Nat.log_zero_right] at hL1; omega + have hsL : 2 ^ L ≤ x.scale := Nat.pow_log_le_self 2 hs0 + have ha32 : slots x ≤ L / 32768 := slotBits_le _ _ + have h12 : (2 ^ slots x) ^ 12 ≤ x.scale := by + rw [← pow_mul] + exact (Nat.pow_le_pow_right (by norm_num) (by omega)).trans hsL + refine ⟨by omega, h12, (Nat.pow_le_pow_right (by norm_num) (by omega)).trans hsL, + Nat.div_le_self _ _, Nat.log_lt_self 2 hs0, ?_⟩ + unfold step taperStep + rw [show taper x.scale x.depth = levels x from rfl] + rcases Nat.eq_zero_or_pos (levels x) with h0 | h0 + · rw [h0, Nat.div_zero]; exact Nat.zero_le _ + · exact (Nat.div_le_self _ _).trans (by omega) + +/-- **The node precisions grow by at most `40 m²`**, at an active call at scale `m` with at most +`m` edges. -/ +theorem nodePrec_le_add (ha : active x = true) (hM : x.edges ≤ x.scale) (j : ℕ) : + nodePrec x j ≤ x.prec + 40 * x.scale ^ 2 := by + obtain ⟨haL, -, hL, huL, hLs, hh⟩ := slots_facts ha + unfold nodePrec nodePrecision + set m := x.scale + have h1 : 2 ^ (slots x - level x ((nodes x).getD j 0)) ≤ m := + (Nat.pow_le_pow_right (by norm_num) (Nat.sub_le _ _)).trans hL + have h2 : step x ≤ 4 * m := by omega + have h3 : 8 * step x * 2 ^ (slots x - level x ((nodes x).getD j 0)) ≤ 32 * m ^ 2 := + calc 8 * step x * 2 ^ (slots x - level x ((nodes x).getD j 0)) ≤ 8 * (4 * m) * m := + Nat.mul_le_mul (Nat.mul_le_mul_left _ h2) h1 + _ = 32 * m ^ 2 := by ring + have h4 : 8 * x.edges * (slots x + 1) ≤ 8 * m ^ 2 := + calc 8 * x.edges * (slots x + 1) ≤ 8 * m * m := Nat.mul_le_mul (Nat.mul_le_mul_left _ hM) + (by omega) + _ = 8 * m ^ 2 := by ring + omega + +/-- The level of a node index is at most `a`, and its node has size at most `2 ^ a`. -/ +theorem level_le_slots_of_mem_children (ha : active x = true) {c : State} (hc : c ∈ children x) : + level x ((nodes x).getD c.1 0) < slots x ∧ + (node (slots x) ((nodes x).getD c.1 0)).natAbs ≤ 2 ^ slots x := by + have hu := OnSchedule.level_lt_levels hc + have ha' := ha + simp only [active, decide_eq_true_eq] at ha' + obtain ⟨-, -, -, hua, -, -, -⟩ := ha' + refine ⟨hu.trans_le hua, ?_⟩ + obtain ⟨hj, -, -⟩ := lt_of_mem_children hc + have hkmem : (nodes x).getD c.1 0 ∈ nodes x := by + rw [List.getD_eq_getElem _ _ hj]; exact List.getElem_mem hj + obtain ⟨hk, -, -⟩ := mem_nodes.mp hkmem + rw [pow_succ] at hk + unfold node + have e : (2 : ℤ) ^ slots x = ((2 ^ slots x : ℕ) : ℤ) := by push_cast; rfl + rw [e] + omega + +/-- The interpolation points are 0/1 lists with `e` coordinates. -/ +theorem getD_points_facts (x : Call) (i : ℕ) : + ((points x).getD i []).length ≤ x.fl.length ∧ ∀ z ∈ (points x).getD i [], z ≤ 1 := by + by_cases hi : i < (points x).length + · rw [List.getD_eq_getElem _ _ hi] + simp only [points, List.getElem_map, digits, List.length_map, List.length_range, le_refl, + List.mem_map, List.mem_range, true_and, forall_exists_index, and_imp] + rintro z j - rfl + split_ifs <;> omega + · rw [List.getD_eq_default _ _ (by omega)] + simp + +/-- The rows of a native child are at most the parent's vertices. -/ +theorem childRows_le (r i : ℕ) (D : DescribedNetwork VertexDesc) + (pk : (List (List ℕ) × List (List ℕ)) × ℕ × List (ℕ × ℕ)) (g : ℕ) : + childRows r i D pk g ≤ D.vertices.length := by + unfold childRows + refine (List.count_le_length).trans ?_ + simp [groupsOf] + +/-- A packet descriptor built from a packet context with bounded fields is bounded. -/ +theorem packetBound_packetCtx {fl ζ β : List ℕ} {m P k a i pt g q : ℕ} {t : ℤ} + {tags : List (Bool × ℕ)} (hpt : pt ≤ P) (ha : a ≤ Nat.log 2 m) (hi : i ≤ a) + (ht : t.natAbs ≤ 2 ^ a) (hζ : ζ.length ≤ fl.length) (hζ1 : ∀ z ∈ ζ, z ≤ 1) + (htags : tags.length = k) (hslots : ∀ b ∈ tags, b.2 < 2 ^ a) + (hβ : β.length ≤ 2 ^ (i + 1) * pt) (hβ' : ∀ b ∈ β, b ≤ pt) : + PacketBound fl m P k (packetCtx fl a i pt t ζ g q, tags, β) := + ⟨hpt, rfl, rfl, ha, rfl, hi, rfl, ht, rfl, hζ, hζ1, htags, hslots, hβ, hβ'⟩ + +/-- **The shape passes to the native children** of an active call, from a root `x₀` at scale `m` +equal to its number of edges, with bound plus depth `m + 1`. -/ +theorem Shape.child (h₀s : x₀.scale = x₀.edges) (h₀b : x₀.bound + x₀.depth = x₀.edges + 1) + (h : Shape x₀ x) (ha : active x = true) {c : State} (hc : c ∈ children x) : + Shape x₀ (FastContraction.child x nativeMk c) := by + set m := x₀.edges + have hsc : x.scale = m := h.scale_eq.trans h₀s + have hM : x.edges ≤ m := by + have := edges_lt_bound_of_active ha + have := h.bound_add_depth_le + omega + obtain ⟨haL, h12, hL, -, -, -⟩ := slots_facts ha + rw [hsc] at haL h12 hL + have hK := pow_slots_le_edges_of_active ha + obtain ⟨hlev, hnode⟩ := level_le_slots_of_mem_children ha hc + have hprec : nodePrec x c.1 ≤ x.prec + 40 * m ^ 2 := by + have := nodePrec_le_add ha (hsc ▸ hM) c.1 + rwa [hsc] at this + have hmk := nativeMk_eq h.wf ha hc + set pk := nativeParentPacking x.rows (slots x) x.net + have hpk : pk.2.1 ≤ m ^ 2 := by + have := numPackets_nativeParentPacking_le x.rows (slots x) x.net + calc pk.2.1 ≤ x.edges * (2 ^ slots x) ^ 12 := this + _ ≤ m * m := Nat.mul_le_mul hM h12 + _ = m ^ 2 := by ring + have hslot : ∀ y ∈ pk.2.2, y.2 < 2 ^ slots x := by + intro y hy + rw [show pk = nativeParentPacking x.rows (slots x) x.net from rfl, + nativeParentPacking_eq h.wf.2 hK] at hy + obtain ⟨e, rfl⟩ := List.mem_ofFn.mp hy + exact ((parentPacking h.wf.2 (slots x)).slot e).2 + have hvert : (FastContraction.child x nativeMk c).net.vertices.length ≤ + x.net.vertices.length + m ^ 2 := by + change (nativeMk x c).2.vertices.length ≤ _ + rw [hmk, length_vertices_nativeChild] + have := childRows_le x.rows (level x ((nodes x).getD c.1 0)) x.net pk c.2.2.2 + omega + refine ⟨h.scale_eq, h.fl_eq, wfChildren_nativeMk x h.wf ha c hc, ?_, ?_, ?_, ?_, ?_, ?_⟩ + · have := edges_lt_bound_of_active ha + have := h.bound_add_depth_le + change x.edges + (x.depth + 1) ≤ _ + omega + · change (nativeMk x c).2.numEdges ≤ 2 * m + rw [hmk] + exact (numEdges_nativeChild_le _ _ _ _ _ _ _ _ _ _ _).trans (Nat.mul_le_mul_left 2 hM) + · change nodePrec x c.1 ≤ x₀.prec + (x.depth + 1) * (40 * m ^ 2) + have : x.prec ≤ x₀.prec + x.depth * (40 * m ^ 2) := h.prec_le + rw [add_one_mul] + omega + · change _ ≤ x₀.net.vertices.length + (x.depth + 1) * m ^ 2 + have : x.net.vertices.length ≤ x₀.net.vertices.length + x.depth * m ^ 2 := + h.vertices_le + rw [add_one_mul] + omega + · refine Or.inr ?_ + change (nativeMk x c).1 ≤ x₀.net.vertices.length + (x.depth + 1) * m ^ 2 + rw [hmk] + have := childRows_le x.rows (level x ((nodes x).getD c.1 0)) x.net pk c.2.2.2 + have : x.net.vertices.length ≤ x₀.net.vertices.length + x.depth * m ^ 2 := + h.vertices_le + rw [add_one_mul] + omega + · intro v hv + change v ∈ (nativeMk x c).2.vertices at hv + rw [hmk] at hv + rcases mem_vertices_nativeChild _ _ _ _ _ _ _ _ _ _ _ hv with ⟨w, hw, hd, hl⟩ | + ⟨q, -, tags, hd, htl, hts⟩ + · rcases h.desc w hw with ⟨u, hu, hu'⟩ | ⟨d, hwd, hb⟩ + · exact Or.inl ⟨u, hu, hd.trans hu'⟩ + · refine Or.inr ⟨d, hd.trans hwd, ?_⟩ + rw [hl] + refine hb.mono ?_ + change x₀.prec + x.depth * (40 * m ^ 2) ≤ x₀.prec + (x.depth + 1) * (40 * m ^ 2) + rw [add_one_mul] + omega + · refine Or.inr ⟨_, hd, ?_⟩ + have hζ := getD_points_facts x c.2.1 + have hβ := lt_nodePrec_of_mem_children hc + have hp : nodePrec x c.1 ≤ x₀.prec + (x.depth + 1) * (40 * m ^ 2) := by + have : x.prec ≤ x₀.prec + x.depth * (40 * m ^ 2) := h.prec_le + rw [add_one_mul] + omega + have hfl : x.fl.length = x₀.fl.length := by rw [h.fl_eq] + rw [h.fl_eq] at hζ ⊢ + refine packetBound_packetCtx hp haL hlev.le hnode (hfl ▸ hζ.1) hζ.2 htl (fun b hb => ?_) + (length_betaSlice_le _ _ _ _) fun b hb => (hβ b (mem_of_mem_betaSlice _ _ _ hb)).le + rcases hts b hb with h0 | ⟨y, hy, hy'⟩ + · rw [h0]; exact Nat.two_pow_pos _ + · rw [hy']; exact hslot y hy + +/-- **Every reached call has the shape** of a root `x₀` that is well-formed, at scale its number of +edges, with bound plus depth `m + 1`. -/ +theorem Reach.shape (h₀s : x₀.scale = x₀.edges) (h₀b : x₀.bound + x₀.depth = x₀.edges + 1) + (h₀ : WF x₀) (h : Reach nativeMk x₀ x) : Shape x₀ x := by + induction h with + | root => + exact ⟨rfl, rfl, h₀, le_rfl, by omega, Nat.le_add_right _ _, Nat.le_add_right _ _, + Or.inl rfl, fun v hv => Or.inl ⟨v, hv, rfl⟩⟩ + | step c _ ha hc ih => exact ih.child h₀s h₀b ha hc + +end Child + +end Cslib.Circuits.Frontier.FastContraction diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSize.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSize.lean new file mode 100644 index 0000000000..0fd1f563a8 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSize.lean @@ -0,0 +1,529 @@ +/- +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.FastContractionShape +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length +import Mathlib.Data.List.GetD + +/-! +# The encoded sizes of the calls of the native contraction recursion + +Bounds on the encoded lengths of the calls (`FastContraction.encCall`) of the native recursion +from bounds on their numbers: the length of an encoded call is at most `64 (B + 1) ^ 3 + 2 B R` when +its numbers, lists and ports are at most `B` and its descriptors at most `R` long +(`FastContraction.length_encCall_le`), and a bounded packet descriptor is at most +`200 (B + 1) ^ 2` long (`FastContraction.length_enc_inr_le`). The values are reduced at their +precision (`FastContraction.reducedAt_value`), and the frames of an active call with at most `m` +edges at scale `m` and precision `p` are at most `64 (B + 1) ^ 3` long for +`B = 256 (m + 1) ^ 5 (p + 1) + e` (`FastContraction.length_encFrame_frameAt_le`): the accumulator +stays reduced at the common precision and stores at most one value per node and point. + +## Main results + +* `Cslib.Circuits.Frontier.FastContraction.length_encList_le`: lists of bounded elements. +* `Cslib.Circuits.Frontier.FastContraction.length_enc_packetCtx_le`: packet contexts. +* `Cslib.Circuits.Frontier.FastContraction.length_enc_inr_le`: bounded packet descriptors. +* `Cslib.Circuits.Frontier.FastContraction.length_encCall_le`: calls. +* `Cslib.Circuits.Frontier.FastContraction.reducedAt_value`, + `Cslib.Circuits.Frontier.FastContraction.length_encValue_le`: values. +* `Cslib.Circuits.Frontier.FastContraction.length_encFrame_frameAt_le`: the frames of an active + call. +-/ + +public section + +namespace Cslib.Circuits.Frontier.FastContraction + +open Turing.MultiTapeTM NativePacket + +/-- A number at most `b` has at most `b` binary digits. -/ +theorem length_encNat_le {a b : ℕ} (h : a ≤ b) : (encNat a).length ≤ b := by + rw [encNat_apply, Nat.size_eq_bits_len] + exact Nat.size_le.mpr (h.trans_lt Nat.lt_two_pow_self) + +/-- A number below `2 ^ p` has at most `p` binary digits. -/ +theorem length_encNat_le_of_lt_two_pow {a p : ℕ} (h : a < 2 ^ p) : (encNat a).length ≤ p := by + rw [encNat_apply, Nat.size_eq_bits_len] + exact Nat.size_le.mpr h + +/-- **A list of elements of encoded length at most `B`** has encoded length at most +`k (2 B + 1)` for `k` elements. -/ +theorem length_encList_le {α : Type*} (enc : α ↪ List Bool) {l : List α} {B : ℕ} + (h : ∀ a ∈ l, (enc a).length ≤ B) : (encList enc l).length ≤ l.length * (2 * B + 1) := by + rw [length_encList] + calc (l.map fun a => 2 * (enc a).length + 1).sum ≤ (l.map fun _ => 2 * B + 1).sum := + List.sum_le_sum fun a ha => by have := h a ha; omega + _ = l.length * (2 * B + 1) := by simp + +/-- A list of numbers at most `1` has encoded length at most `3 k` for `k` numbers. -/ +theorem length_encList_le_of_le_one {l : List ℕ} (h : ∀ z ∈ l, z ≤ 1) : + (encList encNat l).length ≤ 3 * l.length := by + have := length_encList_le encNat (B := 1) fun z hz => length_encNat_le (h z hz) + omega + +/-- **A packet context with fields at most `B`** and no column list has encoded length at most +`64 (B + 1)`. -/ +theorem length_enc_packetCtx_le (c : PacketCtx) {B : ℕ} (hp : c.p ≤ B) (hfl : c.fl.length ≤ B) + (hfl1 : ∀ z ∈ c.fl, z ≤ 1) (ha : c.a ≤ B) (hL : c.L ≤ B) (hi : c.i ≤ B) (htl : c.tiles ≤ B) + (ht : c.t.natAbs ≤ B) (hnb : c.nb ≤ B) (hcols : c.cols = []) (hζ : c.ζ.length ≤ B) + (hζ1 : ∀ z ∈ c.ζ, z ≤ 1) : (PacketCtx.enc c).length ≤ 64 * (B + 1) := by + have h1 := length_encList_le_of_le_one hfl1 + have h2 := length_encList_le_of_le_one hζ1 + have h3 : c.t.natAbs.size ≤ B := (Nat.size_le.mpr (Nat.lt_two_pow_self)).trans ht + simp only [PacketCtx.enc, encOfEquiv, Function.Embedding.trans_apply, Equiv.coe_toEmbedding, + PacketCtx.equivProd, Equiv.coe_fn_mk, length_encPair, encUnary_apply, List.length_replicate, + length_encIntBin, encBool_apply, List.length_singleton, hcols, length_encList, List.map_nil, + List.sum_nil] at h1 h2 ⊢ + omega + +/-- `2 ^ a ≤ m` for `a ≤ ⌊log₂ m⌋` and `m ≠ 0`. -/ +theorem two_pow_le_of_le_log {a m : ℕ} (ha : a ≤ Nat.log 2 m) (hm : m ≠ 0) : 2 ^ a ≤ m := + (Nat.pow_le_pow_right (by norm_num) ha).trans (Nat.pow_log_le_self 2 hm) + +/-- **A bounded packet descriptor has encoded length at most `200 (B + 1) ^ 2`**, when +`2 (m + 1) (P + 1)`, the modulus's length and the number of ports are at most `B` and the +modulus has 0/1 coefficients. -/ +theorem length_enc_inr_le {fl : List ℕ} {m P k : ℕ} {d : PacketDesc} (h : PacketBound fl m P k d) + {B : ℕ} (hB : 2 * (m + 1) * (P + 1) ≤ B) (hfl : fl.length ≤ B) (hfl1 : ∀ z ∈ fl, z ≤ 1) + (hk : k ≤ B) : (VertexDesc.enc (.inr d)).length ≤ 200 * (B + 1) ^ 2 := by + obtain ⟨hp, hnb, hfl', ha, hL, hi, htl, ht, hcols, hζ, hζ1, htags, hslots, hβ, hβ'⟩ := h + have h2m : 2 * (m + 1) ≤ B := le_trans (Nat.le_mul_of_pos_right _ (by omega)) hB + have hP1 : P + 1 ≤ B := le_trans (Nat.le_mul_of_pos_left _ (by omega)) hB + have hLm : 2 ^ d.1.a ≤ m + 1 := by + rcases Nat.eq_zero_or_pos m with h0 | h0 + · rw [h0, Nat.log_zero_right, Nat.le_zero] at ha; rw [ha, h0]; simp + · exact (two_pow_le_of_le_log ha (by omega)).trans (Nat.le_succ _) + have htiles : d.1.tiles ≤ 2 * (m + 1) := by + rw [htl, pow_succ] + have := Nat.pow_le_pow_right (n := 2) (by norm_num) hi + omega + have haL := Nat.lt_two_pow_self (n := d.1.a) + have hiL := Nat.lt_two_pow_self (n := d.1.i) + have hiL' : 2 ^ d.1.i ≤ 2 ^ d.1.a := Nat.pow_le_pow_right (by norm_num) hi + have hflB : d.1.fl.length ≤ B := by rw [hfl']; exact hfl + have hfl1' : ∀ z ∈ d.1.fl, z ≤ 1 := by rw [hfl']; exact hfl1 + have hctx := length_enc_packetCtx_le d.1 (B := B) (by omega) hflB hfl1' (by omega) (by omega) + (by omega) (by omega) (by omega) (by omega) hcols (hζ.trans hfl) hζ1 + have htg : (encList (encPair encBool encNat) d.2.1).length ≤ B * (2 * (B + 3) + 1) := by + refine (length_encList_le _ (B := B + 3) fun b hb => ?_).trans + (Nat.mul_le_mul_right _ (htags ▸ hk)) + rw [length_encPair, encBool_apply, List.length_singleton] + have := length_encNat_le_of_lt_two_pow (hslots b hb) + have := Nat.lt_two_pow_self (n := d.1.a) + omega + have hbeta : (encList encUnary d.2.2).length ≤ B * (2 * B + 1) := by + refine (length_encList_le _ (B := B) fun b hb => ?_).trans (Nat.mul_le_mul_right _ ?_) + · rw [encUnary_apply, List.length_replicate] + exact (hβ' b hb).trans (hp.trans (by omega)) + · calc d.2.2.length ≤ d.1.tiles * d.1.p := hβ + _ ≤ 2 * (m + 1) * (P + 1) := Nat.mul_le_mul htiles (hp.trans (Nat.le_succ _)) + _ ≤ B := hB + rw [length_encSum] + simp only [Sum.elim_inr, encPacketDesc, length_encPair] + nlinarith + +/-- **The encoded length of a call** is at most `64 (B + 1) ^ 3 + 2 B R` when its scale, depth, +bound, precision, number of edges, number of vertices, modulus length, the binary length of its +rows and its ports are at most `B`, the modulus has 0/1 coefficients, and its descriptors are at +most `R` long. -/ +theorem length_encCall_le {x : Call} {B R : ℕ} (hs : x.scale ≤ B) (hd : x.depth ≤ B) + (hb : x.bound ≤ B) (hp : x.prec ≤ B) (hfl : x.fl.length ≤ B) (hfl1 : ∀ z ∈ x.fl, z ≤ 1) + (hr : (encNat x.rows).length ≤ B) (hE : x.edges ≤ B) (hV : x.net.vertices.length ≤ B) + (hports : ∀ v ∈ x.net.vertices, v.1.length ≤ B ∧ ∀ i ∈ v.1, i ≤ B) + (hdesc : ∀ v ∈ x.net.vertices, (VertexDesc.enc v.2).length ≤ R) : + (encCall x).length ≤ 64 * (B + 1) ^ 3 + 2 * B * R := by + have h1 := length_encList_le_of_le_one hfl1 + have hv : ∀ v ∈ x.net.vertices, (encPair (encList encNat) VertexDesc.enc v).length ≤ + 2 * (B * (2 * B + 1)) + 1 + R := fun v hv => by + rw [length_encPair] + have := (length_encList_le encNat (B := B) fun i hi => length_encNat_le + ((hports v hv).2 i hi)).trans (Nat.mul_le_mul_right _ (hports v hv).1) + have := hdesc v hv + omega + have hvs := (length_encList_le _ hv).trans (Nat.mul_le_mul_right _ hV) + simp only [encCall, encParams, length_encPair, encUnary_apply, List.length_replicate, + DescribedNetwork.encDescribed, encOfEquiv, Function.Embedding.trans_apply, + Equiv.coe_toEmbedding, DescribedNetwork.equivProd, Equiv.coe_fn_mk] at hvs ⊢ + have h2 : B * (2 * (2 * (B * (2 * B + 1)) + 1 + R) + 1) = + 8 * B ^ 3 + 4 * B ^ 2 + 3 * B + 2 * B * R := by ring + rw [h2] at hvs + nlinarith + +/-! ### Values -/ + +/-- A reduced coefficient list: `e` coordinates, each at most `2 ^ p`. -/ +@[expose] def ReducedAt (p : ℕ) (fl c : List ℕ) : Prop := c.length = fl.length ∧ ∀ z ∈ c, z ≤ 2 ^ p + +theorem reducedAt_add (p : ℕ) (fl c d : List ℕ) : ReducedAt p fl (GaloisRingArith.add p fl c d) := + ⟨GaloisRingArith.length_add _ _ _ _, fun _ hz => (GaloisRingArith.lt_of_mem_add hz).le⟩ + +theorem reducedAt_mul (p : ℕ) (fl c d : List ℕ) : ReducedAt p fl (GaloisRingArith.mul p fl c d) := + ⟨GaloisRingArith.length_mul _ _ _ _, fun _ hz => (GaloisRingArith.lt_of_mem_mul hz).le⟩ + +theorem reducedAt_zero (p : ℕ) (fl : List ℕ) : ReducedAt p fl (GaloisRingArith.zero fl) := + (SumOps.galois.reduced_zero (p, fl)) + +theorem reducedAt_one (p : ℕ) (fl : List ℕ) : ReducedAt p fl (GaloisRingArith.one fl) := + (SumOps.galois.reduced_one (p, fl)) + +/-- A reduced list at precision `p` has encoded length at most `e (2 (p + 1) + 1)`. -/ +theorem length_encList_le_of_reducedAt {p : ℕ} {fl c : List ℕ} (h : ReducedAt p fl c) : + (encList encNat c).length ≤ fl.length * (2 * (p + 1) + 1) := by + rw [← h.1] + exact length_encList_le _ fun z hz => length_encNat_le_of_lt_two_pow + ((h.2 z hz).trans_lt (Nat.pow_lt_pow_right (by norm_num) (Nat.lt_succ_self p))) + +/-- **The values of the calls are reduced** at their precision, for every child builder. -/ +theorem reducedAt_value (mk : Call → ChildCursor.State → ℕ × DescribedNetwork VertexDesc) + (x : Call) : + ReducedAt x.prec x.fl (value mk x) := by + cases ha : active x + · rw [value_of_not_active mk ha] + exact DescribedNetwork.reduced_sumValue (ops := SumOps.galois) (eval := VertexDesc.entry) + (x.prec, x.fl) x.net + · rw [value_of_active mk ha, finishValue, NativeRecovery.recover] + set W := table x (runLoop x fun c => value mk (child x mk c)).2.2 + have hfold : ∀ (l : List ℕ) (S : List ℕ), ReducedAt (x.prec + shift x) x.fl S → + ReducedAt (x.prec + shift x) x.fl (l.foldl (fun S k => if k = 2 ^ slots x then S else + GaloisRingArith.add (x.prec + shift x) x.fl S + (NativeRecovery.nodeTerm (x.prec + shift x) x.fl + (slots x) (levels x) (step x) (shift x) (points x) k (W.getD k []))) S) := by + intro l + induction l with + | nil => exact fun S hS => hS + | cons k l ih => + intro S hS + rw [List.foldl_cons] + refine ih _ ?_ + split_ifs + · exact hS + · exact reducedAt_add _ _ _ _ + obtain ⟨hl, hz⟩ := hfold (List.range (2 ^ (slots x + 1))) _ (reducedAt_zero _ _) + refine ⟨by rw [GaloisRingArith.shiftDown, List.length_map, hl], fun z hzm => ?_⟩ + simp only [GaloisRingArith.shiftDown, List.mem_map] at hzm + obtain ⟨w, hw, rfl⟩ := hzm + have := hz w hw + rw [pow_add] at this + exact Nat.le_of_lt_succ (Nat.lt_succ_of_le (Nat.div_le_of_le_mul (by linarith))) + +/-- **The encoded length of a tagged value** of a call. -/ +theorem length_encValue_le (mk : Call → ChildCursor.State → ℕ × DescribedNetwork VertexDesc) + (x : Call) : + (encValue (x.depth, value mk x)).length ≤ + 2 * x.depth + 1 + x.fl.length * (2 * (x.prec + 1) + 1) := by + rw [length_encPair, encUnary_apply, List.length_replicate] + have := length_encList_le_of_reducedAt (reducedAt_value mk x) + simp only at this ⊢ + omega + +/-! ### Frames -/ + +section Frames + +variable {ws : ℕ → List ℕ} {ps : ℕ → ℕ} {N : ℕ} {fl : List ℕ} + +/-- An accumulator whose product, sum and stored values are reduced at precision `N`. -/ +@[expose] def AccReduced (N : ℕ) (fl : List ℕ) (acc : ChildCursor.Acc (List ℕ)) : Prop := + ReducedAt N fl acc.1 ∧ ReducedAt N fl acc.2.1 ∧ ∀ y ∈ acc.2.2, ReducedAt N fl y + +/-- **The accumulator stays reduced** along the children, and its stored values only grow. -/ +theorem accReduced_runAcc (vals : ChildCursor.State → List ℕ) (l : List ChildCursor.State) + {acc : ChildCursor.Acc (List ℕ)} (h : AccReduced N fl acc) : + AccReduced N fl (ChildCursor.runAcc ws ps 64 (GaloisRingArith.mul N fl) + (GaloisRingArith.add N fl) (GaloisRingArith.one fl) (GaloisRingArith.zero fl) vals l acc) ∧ + acc.2.2.length ≤ (ChildCursor.runAcc ws ps 64 (GaloisRingArith.mul N fl) + (GaloisRingArith.add N fl) (GaloisRingArith.one fl) (GaloisRingArith.zero fl) vals l + acc).2.2.length := by + induction l generalizing acc with + | nil => exact ⟨h, le_rfl⟩ + | cons s l ih => + simp only [ChildCursor.runAcc, List.foldl_cons] at ih ⊢ + have hstep : AccReduced N fl (ChildCursor.absorbAt ws ps 64 (GaloisRingArith.mul N fl) + (GaloisRingArith.add N fl) (GaloisRingArith.one fl) (GaloisRingArith.zero fl) s acc + (vals s)) ∧ acc.2.2.length ≤ (ChildCursor.absorbAt ws ps 64 (GaloisRingArith.mul N fl) + (GaloisRingArith.add N fl) (GaloisRingArith.one fl) (GaloisRingArith.zero fl) s acc + (vals s)).2.2.length := by + unfold ChildCursor.absorbAt + split_ifs + · exact ⟨⟨reducedAt_mul _ _ _ _, h.2.1, h.2.2⟩, le_rfl⟩ + · refine ⟨⟨reducedAt_one _ _, reducedAt_zero _ _, fun y hy => ?_⟩, by simp⟩ + rcases List.mem_append.mp hy with hy | hy + · exact h.2.2 y hy + · rw [List.mem_singleton.mp hy]; exact reducedAt_add _ _ _ _ + · exact ⟨⟨reducedAt_one _ _, reducedAt_add _ _ _ _, h.2.2⟩, le_rfl⟩ + obtain ⟨h1, h2⟩ := ih hstep.1 + exact ⟨h1, hstep.2.trans h2⟩ + +/-- **The encoded length of a frame** is at most `64 (B + 1) ^ 3` when its cursor state's numbers +and exponents, the number of stored values, `N + 1` and `e` are at most `B`, and its accumulator is +reduced at precision `N`. -/ +theorem length_encFrame_le {o : Option ChildCursor.State} {acc : ChildCursor.Acc (List ℕ)} + {B : ℕ} (hst : ∀ s, o = some s → s.1 ≤ B ∧ s.2.1 ≤ B ∧ s.2.2.1.length ≤ B ∧ + (∀ b ∈ s.2.2.1, b ≤ B) ∧ s.2.2.2 ≤ B) + (hacc : AccReduced N fl acc) (hst' : acc.2.2.length ≤ B) (hN : N + 1 ≤ B) + (he : fl.length ≤ B) : (encFrame (o, acc)).length ≤ 64 * (B + 1) ^ 3 := by + have hred : ∀ c, ReducedAt N fl c → (encList encNat c).length ≤ B * (2 * B + 1) := fun c hc => + (length_encList_le_of_reducedAt hc).trans (Nat.mul_le_mul he (by omega)) + have hopt : (encOption ChildCursor.encState o).length ≤ 4 * B ^ 2 + 7 * B + 4 := by + rcases o with _ | s + · simp [encOption] + · obtain ⟨h1, h2, h3, h4, h5⟩ := hst s rfl + have hβ := (length_encList_le encNat (B := B) fun b hb => length_encNat_le (h4 b hb)).trans + (Nat.mul_le_mul_right _ h3) + simp only [encOption, Function.Embedding.coeFn_mk, Option.elim_some, List.length_cons, + ChildCursor.encState, length_encPair, encUnary_apply, List.length_replicate] + nlinarith + have hstored := (length_encList_le (encList encNat) (B := B * (2 * B + 1)) fun y hy => + hred y (hacc.2.2 y hy)).trans (Nat.mul_le_mul_right _ hst') + have h1 := hred _ hacc.1 + have h2 := hred _ hacc.2.1 + simp only [encFrame, length_encPair] + nlinarith + +end Frames + +/-! ### The frames of an active call -/ + +section ActiveFrames + +variable {x : Call} + +/-- The bound `256 (m + 1) ^ 5 (p + 1) + e` on the numbers of the frames of an active call at scale +`m` with precision `p`. -/ +@[expose] def frameBound (x : Call) : ℕ := 256 * (x.scale + 1) ^ 5 * (x.prec + 1) + x.fl.length + +/-- The numbers of an active call with at most `m` edges at scale `m`. -/ +theorem active_numbers (ha : active x = true) (hM : x.edges ≤ x.scale) : + (nodes x).length ≤ 2 * x.scale ∧ numPoints x ≤ 2 * x.scale ^ 2 + 1 ∧ + (packing x).2.1 ≤ x.scale ^ 2 ∧ shift x ≤ 48 * (x.scale + 1) ^ 4 ∧ + ∀ j, nodePrec x j ≤ x.prec + 40 * x.scale ^ 2 ∧ + 2 ^ (level x ((nodes x).getD j 0) + 1) ≤ 4 * x.scale := by + obtain ⟨haL, h12, hL, huL, hLs, hh⟩ := slots_facts ha + have ha1 : slots x + 1 ≤ x.scale := by omega + have hu : levels x ≤ x.scale := by omega + have hstep : step x ≤ 4 * x.scale := by omega + have h2a : 2 ^ (slots x + 1) ≤ 2 * x.scale := by rw [pow_succ]; omega + refine ⟨(length_nodes_le x).trans h2a, ?_, ?_, ?_, fun j => ⟨nodePrec_le_add ha hM j, ?_⟩⟩ + · unfold numPoints + have : x.edges * (2 * 2 ^ slots x - 1) ≤ x.scale * (2 * x.scale) := + Nat.mul_le_mul hM (by omega) + nlinarith + · calc (packing x).2.1 ≤ x.edges * (2 ^ slots x) ^ 12 := + NativeChild.numPackets_nativeParentPacking_le _ _ _ + _ ≤ x.scale * x.scale := Nat.mul_le_mul hM h12 + _ = x.scale ^ 2 := by ring + · unfold shift + have e1 : (slots x + 1) * 2 ^ (slots x + 1) * step x * levels x ≤ + x.scale * (2 * x.scale) * (4 * x.scale) * x.scale := + Nat.mul_le_mul (Nat.mul_le_mul (Nat.mul_le_mul ha1 h2a) hstep) hu + have e2 : 8 * step x * 2 ^ slots x ≤ 8 * (4 * x.scale) * x.scale := + Nat.mul_le_mul (Nat.mul_le_mul_left _ hstep) hL + have e3 : 8 * x.edges * (slots x + 1) ≤ 8 * x.scale * x.scale := + Nat.mul_le_mul (Nat.mul_le_mul_left _ hM) ha1 + have h4 : x.scale ^ 4 ≤ (x.scale + 1) ^ 4 := Nat.pow_le_pow_left (Nat.le_succ _) 4 + have h2 : x.scale ^ 2 ≤ (x.scale + 1) ^ 4 := + (Nat.pow_le_pow_left (Nat.le_succ _) 2).trans (Nat.pow_le_pow_right (by omega) (by omega)) + have e4 : x.scale * (2 * x.scale) * (4 * x.scale) * x.scale + 8 * (4 * x.scale) * x.scale + + 8 * x.scale * x.scale = 8 * x.scale ^ 4 + 40 * x.scale ^ 2 := by ring + omega + · have : level x ((nodes x).getD j 0) ≤ slots x + 1 := by + unfold level NativeRecovery.twoVal + split_ifs + · omega + · exact (List.length_filter_le _ _).trans List.length_range.le + calc 2 ^ (level x ((nodes x).getD j 0) + 1) ≤ 2 ^ (slots x + 1 + 1) := + Nat.pow_le_pow_right (by norm_num) (by omega) + _ ≤ 4 * x.scale := by rw [pow_succ]; omega + +/-- The exponent tuple of a child of an active call is a tuple of weight below its node's +precision. -/ +theorem mem_budgetTuples_of_mem_children {c : ChildCursor.State} (hc : c ∈ children x) : + c.2.2.1 ∈ BudgetTuples.budgetTuples (weights x c.1) (nodePrec x c.1) := by + simp only [children, ChildCursor.cursorList, ChildCursor.nodeBlock, ChildCursor.pointBlock, + ChildCursor.groupBlock, List.mem_flatMap, List.mem_range, List.mem_map] at hc + obtain ⟨j, -, i, -, β, hβ, g, -, rfl⟩ := hc + exact hβ + +/-- **The frames of an active call** with at most `m` edges at scale `m` have encoded length at +most `64 (B + 1) ^ 3` for `B = frameBound x`. -/ +theorem length_encFrame_frameAt_le (ha : active x = true) (hM : x.edges ≤ x.scale) + (vals : ChildCursor.State → List ℕ) (c : ℕ) : + (encFrame (frameAt x vals c)).length ≤ 64 * (frameBound x + 1) ^ 3 := by + obtain ⟨hT, hn, hP, hsh, hj⟩ := active_numbers ha hM + have hM1 := one_le_edges_of_active ha + set m := x.scale with hm + set p := x.prec with hp + have hBf : 256 * ((m + 1) ^ 5 * (p + 1)) ≤ frameBound x := by + rw [← Nat.mul_assoc]; exact Nat.le_add_right _ _ + have hm5 : 1 ≤ (m + 1) ^ 5 := Nat.one_le_pow _ _ (by omega) + have hm1 : m + 1 ≤ (m + 1) ^ 5 := Nat.le_self_pow (by norm_num) _ + have hm2 : (m + 1) ^ 2 ≤ (m + 1) ^ 5 := Nat.pow_le_pow_right (by omega) (by norm_num) + have hm3 : (m + 1) ^ 3 ≤ (m + 1) ^ 5 := Nat.pow_le_pow_right (by omega) (by norm_num) + have hm4 : (m + 1) ^ 4 ≤ (m + 1) ^ 5 := Nat.pow_le_pow_right (by omega) (by norm_num) + have hsq : m ^ 2 ≤ (m + 1) ^ 2 := Nat.pow_le_pow_left (Nat.le_succ _) 2 + have hcu : m ^ 3 ≤ (m + 1) ^ 3 := Nat.pow_le_pow_left (Nat.le_succ _) 3 + have hP5 : (m + 1) ^ 5 ≤ (m + 1) ^ 5 * (p + 1) := Nat.le_mul_of_pos_right _ (by omega) + have hpq : p + 1 ≤ (m + 1) ^ 5 * (p + 1) := Nat.le_mul_of_pos_left _ (by omega) + -- The stored values. + obtain ⟨qs, hqs, hrun⟩ := ChildCursor.runAcc_cursorList (ws := weights x) (ps := nodePrec x) + (T := (nodes x).length) (n := numPoints x) (r := 64) (GaloisRingArith.mul (wide x) x.fl) + (GaloisRingArith.add (wide x) x.fl) (GaloisRingArith.one x.fl) (GaloisRingArith.zero x.fl) + (GaloisRingArith.val (wide x) x.fl) (fun a b => GaloisRingArith.val_mul a b) + (fun a b => GaloisRingArith.val_add a b) GaloisRingArith.val_one GaloisRingArith.val_zero + (by norm_num) (nodePrec_pos hM1) weights_pos vals + have hqlen : qs.length = (nodes x).length * numPoints x := by + have := congrArg List.length hqs + simpa [List.length_flatMap, List.sum_replicate] using this + have hinit : AccReduced (wide x) x.fl (GaloisRingArith.one x.fl, GaloisRingArith.zero x.fl, []) := + ⟨reducedAt_one _ _, reducedAt_zero _ _, by simp⟩ + have hpre := accReduced_runAcc (ws := weights x) (ps := nodePrec x) vals + ((children x).take c) hinit + have hsuf := accReduced_runAcc (ws := weights x) (ps := nodePrec x) vals + ((children x).drop c) hpre.1 + have hfull : ChildCursor.runAcc (weights x) (nodePrec x) 64 + (GaloisRingArith.mul (wide x) x.fl) (GaloisRingArith.add (wide x) x.fl) + (GaloisRingArith.one x.fl) (GaloisRingArith.zero x.fl) vals (children x) + (GaloisRingArith.one x.fl, GaloisRingArith.zero x.fl, []) = + (GaloisRingArith.one x.fl, GaloisRingArith.zero x.fl, qs) := by + rw [children]; exact hrun + rw [← ChildCursor.runAcc_append, List.take_append_drop, hfull] at hsuf + have hstored : (ChildCursor.runAcc (weights x) (nodePrec x) 64 + (GaloisRingArith.mul (wide x) x.fl) (GaloisRingArith.add (wide x) x.fl) + (GaloisRingArith.one x.fl) (GaloisRingArith.zero x.fl) vals ((children x).take c) + (GaloisRingArith.one x.fl, GaloisRingArith.zero x.fl, [])).2.2.length ≤ frameBound x := by + refine hsuf.2.trans ?_ + rw [hqlen] + have : (nodes x).length * numPoints x ≤ 2 * m * (2 * m ^ 2 + 1) := Nat.mul_le_mul hT hn + have : 2 * m * (2 * m ^ 2 + 1) = 4 * m ^ 3 + 2 * m := by ring + omega + refine length_encFrame_le (N := wide x) (fl := x.fl) (fun s hs => ?_) hpre.1 hstored ?_ + (Nat.le_add_left _ _) + · have hsm : s ∈ children x := List.mem_of_getElem? hs + obtain ⟨hj1, hi1, hg1⟩ := lt_of_mem_children hsm + have hβ := mem_budgetTuples_of_mem_children hsm + have hlen := ((BudgetTuples.mem_budgetTuples (weights_pos _)).mp hβ).1 + obtain ⟨hpj, hlj⟩ := hj s.1 + refine ⟨by omega, by omega, ?_, fun b hb => ?_, by omega⟩ + · rw [hlen, weights, NativeChild.modeWeights, List.length_map, List.length_range] + have h1 : (packing x).2.1 * (2 ^ (level x ((nodes x).getD s.1 0) + 1) * nodePrec x s.1) ≤ + m ^ 2 * (4 * m * (p + 40 * m ^ 2)) := + Nat.mul_le_mul hP (Nat.mul_le_mul hlj hpj) + have h2 : m ^ 2 * (4 * m * (p + 40 * m ^ 2)) = 4 * (m ^ 3 * p) + 160 * m ^ 5 := by ring + have h3 : m ^ 5 ≤ (m + 1) ^ 5 := Nat.pow_le_pow_left (Nat.le_succ _) 5 + have h4 : m ^ 3 * p ≤ (m + 1) ^ 5 * (p + 1) := + Nat.mul_le_mul (hcu.trans hm3) (Nat.le_succ _) + omega + · have := BudgetTuples.lt_of_mem_budgetTuples (weights_pos _) hβ hb + have : m ^ 2 ≤ (m + 1) ^ 5 := hsq.trans hm2 + omega + · unfold wide + omega + +end ActiveFrames + +/-! ### The sizes along the recursion -/ + +section Sizes + +variable {x₀ x : Call} + +/-- **The sizes of a call of a given shape**: from a root `x₀` at depth `0`, at scale its number +`m` of edges, with bound `m + 1`, a 0/1 modulus and descriptors at most `200 (Z + 1) ^ 2` long, a +call of its shape, its tagged value and, if it is active, its frames are at most +`1000 (Z + 1) ^ 3` long, once `Z` dominates `256 (m + 1) ^ 5 (P + 1) + e` for the precision bound +`P = p₀ + 40 m² (m + 1)` and the vertices, rows and their growth. -/ +theorem Shape.length_le (h₀s : x₀.scale = x₀.edges) (h₀b : x₀.bound = x₀.edges + 1) + (h₀d : x₀.depth = 0) (h : Shape x₀ x) {Z : ℕ} + (hZ1 : 256 * (x₀.edges + 1) ^ 5 * (x₀.prec + (x₀.edges + 1) * (40 * x₀.edges ^ 2) + 1) + + x₀.fl.length ≤ Z) + (hZ2 : x₀.net.vertices.length + (x₀.edges + 1) * x₀.edges ^ 2 + (encNat x₀.rows).length ≤ Z) + (hfl1 : ∀ z ∈ x₀.fl, z ≤ 1) + (hR₀ : ∀ w ∈ x₀.net.vertices, (VertexDesc.enc w.2).length ≤ 200 * (Z + 1) ^ 2) : + (encCall x).length ≤ 1000 * (Z + 1) ^ 3 ∧ + (encValue (x.depth, value nativeMk x)).length ≤ 1000 * (Z + 1) ^ 3 ∧ + (active x = true → ∀ vals c, + (encPair encCall encFrame (x, frameAt x vals c)).length ≤ 1000 * (Z + 1) ^ 3) := by + set m := x₀.edges with hm + set P := x₀.prec + (m + 1) * (40 * m ^ 2) with hP + -- The numbers of `x`. + have hbd := h.bound_add_depth_le + rw [h₀b, h₀d] at hbd + have hd : x.depth ≤ m + 1 := by omega + have hprec : x.prec ≤ P := h.prec_le.trans (Nat.add_le_add_left + (Nat.mul_le_mul_right _ hd) _) + have hV : x.net.vertices.length ≤ x₀.net.vertices.length + (m + 1) * m ^ 2 := + h.vertices_le.trans (Nat.add_le_add_left (Nat.mul_le_mul_right _ hd) _) + have hm5 : m + 1 ≤ (m + 1) ^ 5 := Nat.le_self_pow (by norm_num) _ + have hP1 : P + 1 ≤ (m + 1) ^ 5 * (P + 1) := Nat.le_mul_of_pos_left _ (by positivity) + have hmP : 2 * (m + 1) * (P + 1) ≤ 256 * (m + 1) ^ 5 * (P + 1) := by + have : (m + 1) * (P + 1) ≤ (m + 1) ^ 5 * (P + 1) := Nat.mul_le_mul_right _ hm5 + nlinarith + have hmZ : 2 * (m + 1) ≤ Z := by + have : 2 * (m + 1) ≤ 2 * (m + 1) * (P + 1) := Nat.le_mul_of_pos_right _ (by omega) + omega + have hPZ : P + 1 ≤ Z := by + have : P + 1 ≤ 2 * (m + 1) * (P + 1) := Nat.le_mul_of_pos_left _ (by omega) + omega + have hflZ : x₀.fl.length ≤ Z := by omega + have hsc : x.scale = m := h.scale_eq.trans h₀s + have hE : x.edges ≤ 2 * m := h.edges_le + have hports : ∀ v ∈ x.net.vertices, v.1.length ≤ Z ∧ ∀ i ∈ v.1, i ≤ Z := fun v hv => + ⟨(length_le_edges_of_wf h.wf hv).trans (hE.trans (by omega)), + fun i hi => (h.wf.2.1 v hv i hi).le.trans (hE.trans (by omega))⟩ + have hR : ∀ v ∈ x.net.vertices, (VertexDesc.enc v.2).length ≤ 200 * (Z + 1) ^ 2 := by + intro v hv + rcases h.desc v hv with ⟨w, hw, hvw⟩ | ⟨d, hvd, hb⟩ + · rw [hvw]; exact hR₀ w hw + · rw [hvd] + refine length_enc_inr_le (hb.mono (Nat.add_le_add_left (Nat.mul_le_mul_right _ hd) _)) + (show 2 * (m + 1) * (P + 1) ≤ Z by omega) hflZ hfl1 (hports v hv).1 + have hrows : (encNat x.rows).length ≤ Z := by + rcases h.rows_le with rfl | hr + · omega + · exact (length_encNat_le (hr.trans (Nat.add_le_add_left + (Nat.mul_le_mul_right _ hd) _))).trans + (show x₀.net.vertices.length + (m + 1) * m ^ 2 ≤ Z by omega) + have hcall := length_encCall_le (B := Z) (R := 200 * (Z + 1) ^ 2) (x := x) + (by rw [hsc]; omega) (hd.trans (by omega)) (by omega) (hprec.trans (by omega)) + (h.fl_eq ▸ hflZ) (h.fl_eq ▸ hfl1) hrows (hE.trans (by omega)) (hV.trans (by omega)) hports hR + have hcall' : (encCall x).length ≤ 464 * (Z + 1) ^ 3 := by + have : 2 * Z * (200 * (Z + 1) ^ 2) ≤ 400 * (Z + 1) ^ 3 := by + have : Z ≤ Z + 1 := Nat.le_succ _ + calc 2 * Z * (200 * (Z + 1) ^ 2) = 400 * (Z * (Z + 1) ^ 2) := by ring + _ ≤ 400 * ((Z + 1) * (Z + 1) ^ 2) := Nat.mul_le_mul_left _ (Nat.mul_le_mul_right _ this) + _ = 400 * (Z + 1) ^ 3 := by ring + omega + have hZ3 : (Z + 1) ^ 2 ≤ (Z + 1) ^ 3 := Nat.pow_le_pow_right (by omega) (by norm_num) + have hZ1' : Z + 1 ≤ (Z + 1) ^ 3 := Nat.le_self_pow (by norm_num) _ + refine ⟨hcall'.trans (by omega), ?_, fun ha vals c => ?_⟩ + · have hv := length_encValue_le nativeMk x + rw [h.fl_eq] at hv + have : x₀.fl.length * (2 * (x.prec + 1) + 1) ≤ Z * (2 * Z + 1) := + Nat.mul_le_mul hflZ (by omega) + have : Z * (2 * Z + 1) ≤ 3 * (Z + 1) ^ 2 := by nlinarith + omega + · have hM : x.edges ≤ x.scale := by + have := edges_lt_bound_of_active ha + omega + have hf := length_encFrame_frameAt_le ha hM vals c + have hfb : frameBound x ≤ Z := by + unfold frameBound + rw [hsc, h.fl_eq] + have : 256 * (m + 1) ^ 5 * (x.prec + 1) ≤ 256 * (m + 1) ^ 5 * (P + 1) := + Nat.mul_le_mul_left _ (by omega) + omega + have hfZ : (frameBound x + 1) ^ 3 ≤ (Z + 1) ^ 3 := Nat.pow_le_pow_left (by omega) 3 + have hl := length_encPair (enc₁ := encCall) (enc₂ := encFrame) (x, frameAt x vals c) + simp only at hl + rw [hl] + omega + +end Sizes + +end Cslib.Circuits.Frontier.FastContraction diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChildBounds.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChildBounds.lean new file mode 100644 index 0000000000..57b93e560b --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChildBounds.lean @@ -0,0 +1,262 @@ +/- +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.NativeChild +import Mathlib.Data.List.GetD + +/-! +# The sizes of the native child networks + +The native child (`NativeChild.nativeChild`) of a rows-first parent with the native packing of its +edges keeps the two invariants of the recursion of [OpenAI2026ETH] (§D.4.6, p. 63) that its +running time needs: + +* **at most `M / 16` edges** (`NativeChild.sixteen_mul_numEdges_nativeChild_le`) under the size + hypothesis `2 Δ D² ≤ M` of (D.6), `D = 64 ^ (2 a)`, for a parent with `M` edges and maximum + degree `Δ`: the child has one edge per port of its group, and each group has at most `2 M / 64` + ports on each side (`PacketPacking.row_ports_packing_le`). This is + `TensorNetwork.mul_card_edges_child_callSplitting_le` for the native numbering; +* **the degree bound** (`NativeChild.length_le_of_mem_vertices_nativeChild`): a vertex of the + parent keeps its ports, and a packet vertex has at most `2 L` ports, `L = 2 ^ a`, so the child + again has maximum degree at most `Δ` when `2 L ≤ Δ`. This is + `TensorNetwork.ModeSplitting.rowsToColumnsLE_child` for the native numbering. + +Both need `64 ^ a ≤ M`, under which the native packing is the packing of Lemma D.3 +(`NativeChild.nativeParentPacking_eq`), and a node of valuation `i < a`. + +## Main results + +* `Cslib.Circuits.Frontier.NativeChild.numEdges_nativeChild_eq`: the edges of the child are the + ports of its group. +* `Cslib.Circuits.Frontier.NativeChild.sixteen_mul_numEdges_nativeChild_le`: at most `M / 16` + edges. +* `Cslib.Circuits.Frontier.NativeChild.length_le_of_mem_vertices_nativeChild`: the degree bound. +* `Cslib.Circuits.Frontier.NativeChild.numPackets_nativeParentPacking_mul_le`: at most `3 M / L` + packets. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Lemma D.3 (pp. 58–59) and + §D.4.6 (p. 63). +-/ + +public section + +namespace Cslib.Circuits.Frontier.NativeChild + +open Finset ChildNumbering + +variable {r a i : ℕ} {D : DescribedNetwork VertexDesc} (hD : D.IsRowsFirstBipartite r) + +/-- The group of a vertex of the parent in coordinate `i < a` of its packing. -/ +noncomputable abbrev parentGroup (a : ℕ) {i : ℕ} (hia : i < a) : + Fin D.vertices.length → Fin 64 := + packingGroup (parentSide r) (parentPacking hD a) ⟨i, hia⟩ + +/-- **The native child is the numbered child** of the packing of the parent, when `64 ^ a ≤ M` and +`i < a`. -/ +theorem nativeChild_nativeParentPacking_eq (hK : 64 ^ a ≤ D.numEdges) (hia : i < a) + (fl : List ℕ) (pt : ℕ) (t : ℤ) (ζ β : List ℕ) (g : Fin 64) : + nativeChild fl a i pt t ζ r D (nativeParentPacking r a D) β g = + ⟨(members fun e => parentGroup hD a hia (D.srcFin hD e) = g).length + + (members fun e => parentGroup hD a hia (D.tgtFin hD e) = g).length, + List.ofFn fun c => + ((numberedPorts hD (parentGroup hD a hia) (parentPacking hD a).packet g + ((childVertexEquiv (P := (parentPacking hD a).numPackets) (parentGroup hD a hia) + g).symm c)).map + fun e => (childEdgeEquiv (D.srcFin hD) (D.tgtFin hD) (parentGroup hD a hia) g e : ℕ), + numberedDesc hD (parentGroup hD a hia) (parentPacking hD a).packet + (fun e => ((parentPacking hD a).slot e : ℕ)) g fl a i pt t ζ β + ((childVertexEquiv (P := (parentPacking hD a).numPackets) (parentGroup hD a hia) + g).symm c))⟩ := + nativeChild_eq hD _ _ _ g fl a i pt t ζ β _ (groupsOf_eq hD hK hia) + (by rw [nativeParentPacking_eq hD hK]) (by rw [nativeParentPacking_eq hD hK]) + +/-- The members of a predicate are as many as its elements. -/ +theorem length_members {n : ℕ} (p : Fin n → Prop) [DecidablePred p] : + (members p).length = #{v | p v} := by + rw [← Fintype.card_subtype, Fintype.card_congr (rankEquiv p), Fintype.card_fin] + +/-- **The edges of the native child are the ports of its group**: the row ports of group `g`, then +its column ports. -/ +theorem numEdges_nativeChild_eq (hK : 64 ^ a ≤ D.numEdges) (hia : i < a) (fl : List ℕ) (pt : ℕ) + (t : ℤ) (ζ β : List ℕ) (g : Fin 64) : + (nativeChild fl a i pt t ζ r D (nativeParentPacking r a D) β g).numEdges = + #{e | (parentPacking hD a).rowLabel (D.srcFin hD e) ⟨i, hia⟩ = g} + + #{e | (parentPacking hD a).colLabel (D.tgtFin hD e) ⟨i, hia⟩ = g} := by + rw [nativeChild_nativeParentPacking_eq hD hK hia] + simp only [length_members] + rw [card_packingGroup_src (parentSide r) (parentSide_src hD), + card_packingGroup_tgt (parentSide r) (parentSide_tgt hD)] + +/-- A row of a rows-first network is the row of at most as many edges as it has ports. -/ +theorem card_rowOfP_le (v : Fin r) : + #{e | rowOfP hD e = v} ≤ (D.vertices.getD v ([], .inl [])).1.length := by + by_cases hv : (v : ℕ) < D.vertices.length + · rw [List.getD_eq_getElem _ _ hv] + calc #{e | rowOfP hD e = v} + ≤ #((D.vertices[(v : ℕ)]'hv).1.toFinset) := by + refine card_le_card_of_injOn (fun e => (e : ℕ)) (fun e he => ?_) + (fun e _ e' _ h => Fin.ext h) + simp only [coe_filter, Set.mem_ofPred_eq, mem_univ, true_and] at he + rw [mem_coe, List.mem_toFinset] + exact (DescribedNetwork.mem_ports_iff hD ⟨v, hv⟩ e).mpr + (Or.inl (Fin.ext (show (D.srcFin hD e : ℕ) = v from congrArg Fin.val he))) + _ ≤ _ := List.toFinset_card_le _ + · have : #{e | rowOfP hD e = v} = 0 := by + refine card_eq_zero.mpr (filter_eq_empty_iff.mpr fun e _ he => hv ?_) + have := (D.srcFin hD e).2 + rw [show (D.srcFin hD e : ℕ) = v from congrArg Fin.val he] at this + exact this + omega + +/-- A column of a rows-first network is the column of at most as many edges as it has ports. -/ +theorem card_colOfP_le (w : Fin (D.vertices.length - r)) : + #{e | colOfP hD e = w} ≤ (D.vertices.getD (r + w) ([], .inl [])).1.length := by + have hv : r + (w : ℕ) < D.vertices.length := by have := w.2; omega + rw [List.getD_eq_getElem _ _ hv] + calc #{e | colOfP hD e = w} + ≤ #((D.vertices[r + (w : ℕ)]'hv).1.toFinset) := by + refine card_le_card_of_injOn (fun e => (e : ℕ)) (fun e he => ?_) + (fun e _ e' _ h => Fin.ext h) + simp only [coe_filter, Set.mem_ofPred_eq, mem_univ, true_and] at he + rw [mem_coe, List.mem_toFinset] + have hle := DescribedNetwork.le_tgtFin hD e + have hw : (D.tgtFin hD e : ℕ) - r = w := congrArg Fin.val he + exact (DescribedNetwork.mem_ports_iff hD ⟨r + w, hv⟩ e).mpr + (Or.inr (Fin.ext (by simp only; omega))) + _ ≤ _ := List.toFinset_card_le _ + +include hD in +/-- **At most `M / 16` edges in a native child**, under the size hypothesis `2 Δ D² ≤ M` of (D.6), +`D = 64 ^ (2 a)`, for a rows-first parent with `M ≥ 64 ^ a` edges and maximum degree `Δ`, at a node +of valuation `i < a`. -/ +theorem sixteen_mul_numEdges_nativeChild_le (hK : 64 ^ a ≤ D.numEdges) (hia : i < a) {Δ : ℕ} + (hdeg : ∀ v ∈ D.vertices, v.1.length ≤ Δ) (hM : 2 * Δ * (64 ^ (2 * a)) ^ 2 ≤ D.numEdges) + (fl : List ℕ) (pt : ℕ) (t : ℤ) (ζ β : List ℕ) (g : Fin 64) : + 16 * (nativeChild fl a i pt t ζ r D (nativeParentPacking r a D) β g).numEdges ≤ + D.numEdges := by + have hdeg' (v : ℕ) : (D.vertices.getD v ([], .inl [])).1.length ≤ Δ := by + by_cases hv : v < D.vertices.length + · rw [List.getD_eq_getElem _ _ hv] + exact hdeg _ (List.getElem_mem hv) + · rw [List.getD_eq_default _ _ (by omega)] + exact Nat.zero_le _ + have hrow : ∀ v, #{e | rowOfP hD e = v} ≤ Δ := fun v => (card_rowOfP_le hD v).trans (hdeg' _) + have hcol : ∀ w, #{e | colOfP hD e = w} ≤ Δ := fun w => (card_colOfP_le hD w).trans (hdeg' _) + have hM' : 2 * Δ * (64 ^ (2 * a)) ^ 2 ≤ Fintype.card (Fin D.numEdges) := by + rwa [Fintype.card_fin] + have h1 := PacketPacking.row_ports_packing_le (rowOfP hD) (colOfP hD) a 64 hrow hcol hM' + ⟨i, hia⟩ g + have h2 := PacketPacking.col_ports_packing_le (rowOfP hD) (colOfP hD) a 64 hrow hcol hM' + ⟨i, hia⟩ g + rw [Fintype.card_fin] at h1 h2 + rw [numEdges_nativeChild_eq hD hK hia] + have e1 : #{e | (parentPacking hD a).rowLabel (D.srcFin hD e) ⟨i, hia⟩ = g} = + #{e | (PacketPacking.packing (rowOfP hD) (colOfP hD) a 64).rowLabel (rowOfP hD e) + ⟨i, hia⟩ = g} := by + congr 1 + refine filter_congr fun e _ => ?_ + simp only [parentPacking, PacketPacking.Packing.relabel, + dite_eq_left (DescribedNetwork.srcFin_lt hD e)] + rfl + have e2 : #{e | (parentPacking hD a).colLabel (D.tgtFin hD e) ⟨i, hia⟩ = g} = + #{e | (PacketPacking.packing (rowOfP hD) (colOfP hD) a 64).colLabel (colOfP hD e) + ⟨i, hia⟩ = g} := by + congr 1 + refine filter_congr fun e _ => ?_ + simp only [parentPacking, PacketPacking.Packing.relabel, + dite_eq_left (DescribedNetwork.le_tgtFin hD e)] + rfl + rw [e1, e2] + omega + +include hD in +/-- **At most `3 M / L` packets** (Lemma D.3 (1)) in the native packing of a rows-first parent with +`M ≥ 64 ^ a` edges and maximum degree `Δ`, under (D.6): `2 Δ D² ≤ M` and `L D ≤ M`, +`D = 64 ^ (2 a)`, `L = 2 ^ a`. -/ +theorem numPackets_nativeParentPacking_mul_le (hK : 64 ^ a ≤ D.numEdges) {Δ : ℕ} + (hdeg : ∀ v ∈ D.vertices, v.1.length ≤ Δ) (hM : 2 * Δ * (64 ^ (2 * a)) ^ 2 ≤ D.numEdges) + (hL : 2 ^ a * 64 ^ (2 * a) ≤ D.numEdges) : + (nativeParentPacking r a D).2.1 * 2 ^ a ≤ 3 * D.numEdges := by + have hdeg' (v : ℕ) : (D.vertices.getD v ([], .inl [])).1.length ≤ Δ := by + by_cases hv : v < D.vertices.length + · rw [List.getD_eq_getElem _ _ hv] + exact hdeg _ (List.getElem_mem hv) + · rw [List.getD_eq_default _ _ (by omega)] + exact Nat.zero_le _ + have h := PacketPacking.numPackets_packing_mul_le (rowOfP hD) (colOfP hD) a 64 + (fun v => (card_rowOfP_le hD v).trans (hdeg' _)) + (fun w => (card_colOfP_le hD w).trans (hdeg' _)) + (by rwa [Fintype.card_fin]) (by rwa [Fintype.card_fin]) + rw [Fintype.card_fin] at h + rw [nativeParentPacking_eq hD hK] + exact h + +/-- At most `2 ^ a` edges lie in a packet of a packing. -/ +theorem card_packet_le {E R C : Type*} [Fintype E] {rowOf : E → R} {colOf : E → C} {r : ℕ} + (Q : PacketPacking.Packing rowOf colOf a r) (q : Fin Q.numPackets) : + #{e | Q.packet e = q} ≤ 2 ^ a := by + calc #{e | Q.packet e = q} ≤ #(univ : Finset (Fin (2 ^ a))) := + card_le_card_of_injOn Q.slot (fun _ _ => mem_coe.mpr (mem_univ _)) fun e he e' he' h => by + simp only [coe_filter, Set.mem_ofPred_eq, mem_univ, true_and] at he he' + exact Q.injective (Prod.ext (he.trans he'.symm) h) + _ = 2 ^ a := by rw [card_univ, Fintype.card_fin] + +/-- Counting the elements of a sum type with a property. -/ +private theorem card_filter_sum {A B : Type*} [Fintype A] [Fintype B] (p : A ⊕ B → Prop) + [DecidablePred p] : + #{x | p x} = #{a | p (.inl a)} + #{b | p (.inr b)} := by + rw [← Fintype.card_subtype, Fintype.card_congr Equiv.subtypeSum, Fintype.card_sum, + Fintype.card_subtype, Fintype.card_subtype] + +include hD in +/-- **The degree bound passes to the native child**: if the parent has maximum degree at most `Δ` +and `2 · 2 ^ a ≤ Δ`, every vertex of the child has at most `Δ` ports. A parent vertex keeps its +ports, and a packet vertex has one port per end in group `g` of an edge of its packet, of which +there are at most `2 ^ a`. -/ +theorem length_le_of_mem_vertices_nativeChild (hK : 64 ^ a ≤ D.numEdges) (hia : i < a) {Δ : ℕ} + (hdeg : ∀ v ∈ D.vertices, v.1.length ≤ Δ) (hL : 2 * 2 ^ a ≤ Δ) (fl : List ℕ) (pt : ℕ) (t : ℤ) + (ζ β : List ℕ) (g : Fin 64) {v : List ℕ × VertexDesc} + (hv : v ∈ (nativeChild fl a i pt t ζ r D (nativeParentPacking r a D) β g).vertices) : + v.1.length ≤ Δ := by + rw [nativeChild_nativeParentPacking_eq hD hK hia] at hv + obtain ⟨c, rfl⟩ := List.mem_ofFn.mp hv + simp only [List.length_map] + rcases (childVertexEquiv (P := (parentPacking hD a).numPackets) (parentGroup hD a hia) g).symm c + with u | q + · simp only [numberedPorts, Sum.elim_inl] + exact (List.length_filterMap_le _ _).trans (hdeg _ (List.getElem_mem _)) + · simp only [numberedPorts, Sum.elim_inr, packetPorts, List.length_map] + set E := childEdgeEquiv (D.srcFin hD) (D.tgtFin hD) (parentGroup hD a hia) g + have hcount : ((List.finRange _).filter fun j => + decide (childTgt (D.srcFin hD) (D.tgtFin hD) (parentGroup hD a hia) + (parentPacking hD a).packet g (E.symm j) = .inr q)).length = + #{c | childTgt (D.srcFin hD) (D.tgtFin hD) (parentGroup hD a hia) + (parentPacking hD a).packet g c = .inr q} := by + rw [show ((List.finRange _).filter fun j => + decide (childTgt (D.srcFin hD) (D.tgtFin hD) (parentGroup hD a hia) + (parentPacking hD a).packet g (E.symm j) = .inr q)) = + members (fun j => childTgt (D.srcFin hD) (D.tgtFin hD) (parentGroup hD a hia) + (parentPacking hD a).packet g (E.symm j) = .inr q) from rfl, length_members, + ← Fintype.card_subtype, ← Fintype.card_subtype] + exact Fintype.card_congr (E.symm.subtypeEquiv fun _ => Iff.rfl) + rw [hcount, card_filter_sum] + simp only [childTgt, Sum.elim_inl, Sum.elim_inr, Sum.inr.injEq] + have h1 : ∀ (P : Fin D.numEdges → Prop) [DecidablePred P], + #{e : {e // P e} | (parentPacking hD a).packet e.1 = q} ≤ 2 ^ a := fun P _ => + (card_le_card_of_injOn Subtype.val (fun e he => by + simp only [coe_filter, Set.mem_ofPred_eq, mem_univ, true_and] at he ⊢ + exact he) + fun e _ e' _ h => Subtype.ext h).trans (card_packet_le _ q) + have := h1 (fun e => parentGroup hD a hia (D.srcFin hD e) = g) + have := h1 (fun e => parentGroup hD a hia (D.tgtFin hD e) = g) + omega + +end Cslib.Circuits.Frontier.NativeChild diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAnalysis.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAnalysis.lean new file mode 100644 index 0000000000..9e69bf87bf --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAnalysis.lean @@ -0,0 +1,460 @@ +/- +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.Complexity.Classes.CountingSimulation.FastAlgorithm +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionSchedule +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionSize +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length + +/-! +# The resource analysis of the native recursion: the recursion tree and the sizes + +The resource analysis `CountingSimulation.FastAnalysis` of the native recursion +(`FastContraction.nativeMk`) of Theorem D.1 of [OpenAI2026ETH] (Appendix D.4.7, p. 64), reduced to +the leaf bounds (`CountingSimulation.fastAnalysis_nativeMk`): direct summation at a reached leaf +takes time `poly(n) 2 ^ O(s / √⌊log₂ s⌋)` and polynomial space (`CountingSimulation.FastLeaves`). + +The rest of the analysis is proved here: + +* **the derivation** of the root over the reached calls (`FastContraction.reachInv`), with at most + `m + 1` stack levels for every input (`FastContraction.exists_eval_reachInv`), and, from some size + on, with at most `2 ^ ((245760 C' + 37) m / √⌊log₂ m⌋)` nodes for `C' = ⌊p / m⌋ + 1` + (`FastContraction.exists_eval_onSchedule`), which fit in the clock + (`CountingSimulation.two_mul_sub_one_le_fuel`). The clock's fixed constant serves every precision + because the call count's exponent is linear in `C'`; +* **the sizes** (`CountingSimulation.fastSizes`): the reached calls, their frames and their values + are at most `2 ^ 55 (n + 1) ^ 24` long, from the structural shapes of the calls + (`FastContraction.Reach.shape`) and the encoded lengths of `FastContraction.Shape.length_le`. + +`CountingSimulation.reach_facts` collects what the leaf bounds may use about a reached call: its +scale `m` with `s ≤ m ≤ C s`, at most `2 m` edges, and, from some size on, precision at most `m ^ 4` +and at most `leafSize m` edges at a leaf. + +## Main definitions + +* `Cslib.Complexity.CountingSimulation.FastSizes`: polynomial sizes along the recursion. +* `Cslib.Complexity.CountingSimulation.FastLeaves`: the leaf bounds, the remaining obligation. + +## Main results + +* `Cslib.Complexity.CountingSimulation.two_mul_sub_one_le_fuel`: the call count fits in the clock. +* `Cslib.Complexity.CountingSimulation.onSchedule_root_capPrecision`: guarded roots are on the + schedule. +* `Cslib.Complexity.CountingSimulation.fastAnalysis_nativeMk_of`: the resource analysis from the + sizes and the leaf bounds. +* `Cslib.Complexity.CountingSimulation.fastSizes`: the sizes. +* `Cslib.Complexity.CountingSimulation.fastAnalysis_nativeMk`: the resource analysis from the leaf + bounds. +* `Cslib.Complexity.CountingSimulation.reach_facts`: the facts at the reached calls that the leaf + bounds use. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Theorem D.1 (p. 53) and + Appendix D.4.7 (p. 64). +-/ + +public section + +namespace Cslib.Complexity.CountingSimulation + +open Cslib.Circuits.Frontier Cslib.Circuits.Frontier.ContractionSchedule + Cslib.Circuits.Frontier.FastContraction Cslib.GenericRAM Cslib.GenericRAM.StackRecursion + Turing.MultiTapeTM + +/-! ### The clock -/ + +/-- **The call count fits in the clock.** For a root with `m ≥ D + 2` edges and precision +`p ≤ D m`, a derivation with at most `2 ^ ((245760 C' + 37) m / √⌊log₂ m⌋)` nodes, +`C' = ⌊p / m⌋ + 1`, has `2 N - 1` at most the clock `2 ^ (K₀ (m + p) / √⌊log₂ (m + p)⌋)`: the +exponent is at most `245797 (m + p) / √⌊log₂ m⌋`, and `⌊log₂ (m + p)⌋ ≤ 3 ⌊log₂ m⌋`. -/ +theorem two_mul_sub_one_le_fuel {m p N D : ℕ} (hm : D + 2 ≤ m) (hp : p ≤ D * m) + (hN : N ≤ 2 ^ ((245760 * (p / m + 1) + 37) * m / Nat.sqrt (Nat.log 2 m))) : + 2 * N - 1 ≤ 2 ^ (fuelConst * (m + p) / Nat.sqrt (Nat.log 2 (m + p))) := by + set L := Nat.log 2 m with hLdef + set σ := Nat.sqrt L with hσdef + set Y := m + p with hYdef + have hm2 : 2 ≤ m := by omega + have hσ : 1 ≤ σ := Nat.one_le_sqrt_log_two hm2 + -- The exponent of the count. + have hCm : (p / m + 1) * m ≤ Y := by + have := Nat.div_mul_le_self p m + rw [add_mul, one_mul] + omega + have hX : (245760 * (p / m + 1) + 37) * m ≤ 245797 * Y := by nlinarith + -- `⌊log₂ (m + p)⌋ ≤ 3 ⌊log₂ m⌋`. + have hYm : Y ≤ m * m := by nlinarith + have hL1 : 1 ≤ L := Nat.le_log_of_pow_le one_lt_two (by simpa using hm2) + have hL' : Nat.log 2 Y ≤ 3 * L := by + have h1 : m < 2 ^ (L + 1) := Nat.lt_pow_succ_log_self one_lt_two m + have h2 : Y < 2 ^ (2 * L + 2) := + calc Y ≤ m * m := hYm + _ < 2 ^ (L + 1) * 2 ^ (L + 1) := Nat.mul_self_lt_mul_self h1 + _ = 2 ^ (2 * L + 2) := by rw [← pow_add]; ring_nf + have := Nat.log_lt_of_lt_pow (by omega) h2 + omega + have hσ' : Nat.sqrt (Nat.log 2 Y) ≤ 3 * σ := by + have h1 : Nat.sqrt (Nat.log 2 Y) ≤ Nat.sqrt (3 * L) := Nat.sqrt_le_sqrt hL' + have h2 : Nat.sqrt (3 * L) < 2 * σ + 2 := by + rw [Nat.sqrt_lt'] + have := Nat.lt_succ_sqrt' L + nlinarith + omega + have hσ'0 : 0 < Nat.sqrt (Nat.log 2 Y) := + Nat.sqrt_pos.mpr ((Nat.log_mono_right (show m ≤ Y by omega)).trans_lt' hL1) + -- Comparing the exponents. + set k := Y / σ with hkdef + have hk : 1 ≤ k := by + refine (Nat.le_div_iff_mul_le hσ).mpr ?_ + have h1 : σ ≤ L := Nat.sqrt_le_self L + have h2 : L < m := Nat.log_lt_self 2 (by omega) + omega + have hE1 : (245760 * (p / m + 1) + 37) * m / σ ≤ 245797 * k + 245797 := + (Nat.div_le_div_right hX).trans (Nat.mul_div_le_mul_div_add _ _ _) + have hE2 : 1398101 * k ≤ fuelConst * Y / Nat.sqrt (Nat.log 2 Y) := by + have h1 : fuelConst * Y / (3 * σ) ≤ fuelConst * Y / Nat.sqrt (Nat.log 2 Y) := + Nat.div_le_div_left hσ' hσ'0 + have h2 : fuelConst * Y / (3 * σ) = fuelConst * Y / σ / 3 := by + rw [Nat.div_div_eq_div_mul, Nat.mul_comm σ 3] + have h3 : fuelConst * k ≤ fuelConst * Y / σ := by + rw [Nat.le_div_iff_mul_le hσ, Nat.mul_assoc] + exact Nat.mul_le_mul_left _ (Nat.div_mul_le_self Y σ) + have h4 : 1398101 * k ≤ fuelConst * k / 3 := by + rw [Nat.le_div_iff_mul_le (by norm_num)] + simp only [fuelConst] + nlinarith + omega + have hpow : 2 * N ≤ 2 ^ (fuelConst * Y / Nat.sqrt (Nat.log 2 Y)) := + calc 2 * N ≤ 2 * 2 ^ ((245760 * (p / m + 1) + 37) * m / σ) := Nat.mul_le_mul_left 2 hN + _ = 2 ^ ((245760 * (p / m + 1) + 37) * m / σ + 1) := by rw [pow_succ]; ring + _ ≤ 2 ^ (fuelConst * Y / Nat.sqrt (Nat.log 2 Y)) := + Nat.pow_le_pow_right (by norm_num) (by omega) + omega + +/-- The schedule's certificate for every constant up to `D + 1`, from some size on. -/ +theorem exists_activeBounds_le (D : ℕ) : + ∃ s₀, ∀ s, s₀ ≤ s → ∀ C ≤ D + 1, ∀ d M p, Active C s d M p → ActiveBounds C s d M p := by + choose f hf using exists_activeBounds + exact ⟨(Finset.range (D + 2)).sup f, fun s hs C hC d M p hA => + ((hf C) s ((Finset.le_sup (Finset.mem_range.mpr (by omega))).trans hs)).2 d M p hA⟩ + +/-! ### The root -/ + +/-- **Guarded roots are on the schedule**, for every constant `C ≥ 1` with precision at most +`C m`. -/ +theorem onSchedule_root_capPrecision {P C : ℕ} {G : ℕ × ExplicitTensorNetwork ℕ} + (hg : fastGuard G = true) (hC : 1 ≤ C) + (hp : (ExplicitTensorNetwork.capPrecision (P, G)).1 ≤ C * G.2.numEdges) : + OnSchedule C G.2.numEdges (root (ExplicitTensorNetwork.capPrecision (P, G))) := by + have hdeg : G.2.maxDegree ≤ degreeBound G.2.numEdges := by + simp only [fastGuard, decide_eq_true_eq] at hg + exact hg.2.2 + rw [ExplicitTensorNetwork.maxDegree_le_iff] at hdeg + refine FastContraction.onSchedule_root hC rfl rfl rfl (wf_root P hg) (fun v hv => ?_) rfl rfl hp + simp only [root, ExplicitTensorNetwork.capPrecision, rootNet, List.mem_map] at hv + obtain ⟨w, hw, rfl⟩ := hv + exact hdeg w hw + +/-- The number of edges of an explicit network is below the length of an encoded input. -/ +theorem numEdges_lt_length_encInput (P : ℕ) (G : ℕ × ExplicitTensorNetwork ℕ) : + G.2.numEdges < (FastContraction.encInput (P, G)).length := by + simp only [FastContraction.encInput, length_encPair, ExplicitTensorNetwork.encExplicitNetwork, + encOfEquiv, Function.Embedding.trans_apply, Equiv.coe_toEmbedding] + simp only [DescribedNetwork.equivProd, Equiv.coe_fn_mk, encUnary_apply, List.length_replicate] + omega + +/-! ### The analysis from the sizes and the leaves -/ + +/-- **Polynomial sizes along the recursion**: for all constants `C` and `D` there are `c` and `d` +such that on every guarded input admissible at size `s ≥ 2` with constant `C` and with precision +`1 ≤ P ≤ D s`, every call reached from the root, its frames and its value are at most +`c (n + 1) ^ d` long, for the input length `n`. -/ +@[expose] def FastSizes : Prop := + ∀ C D : ℕ, ∃ c d : ℕ, ∀ (s P : ℕ) (G : ℕ × ExplicitTensorNetwork ℕ), 2 ≤ s → 1 ≤ P → + P ≤ D * s → ExplicitAdmissible C s G → fastGuard G = true → + ∀ x, Reach nativeMk (root (ExplicitTensorNetwork.capPrecision (P, G))) x → + (encCall x).length ≤ c * ((FastContraction.encInput (P, G)).length + 1) ^ d ∧ + (∀ a, (reachInv nativeMk (root (ExplicitTensorNetwork.capPrecision (P, G)))).frame x a → + (encPair encCall encFrame (x, a)).length ≤ + c * ((FastContraction.encInput (P, G)).length + 1) ^ d) ∧ + (encValue (x.depth, value nativeMk x)).length ≤ + c * ((FastContraction.encInput (P, G)).length + 1) ^ d + +/-- **The leaf bounds**: for all constants `C` and `D` there is `K` such that on every guarded +input admissible at size `s ≥ 2` with constant `C` and with precision `1 ≤ P ≤ D s`, direct +summation at every reached call that the machine treats as a leaf takes time at most +`K (n + 1) ^ K 2 ^ (K s / √⌊log₂ s⌋)` and space at most `K (n + 1) ^ K`. -/ +@[expose] def FastLeaves : Prop := + ∀ C D : ℕ, ∃ K : ℕ, ∀ (s P : ℕ) (G : ℕ × ExplicitTensorNetwork ℕ), 2 ≤ s → 1 ≤ P → + P ≤ D * s → ExplicitAdmissible C s G → fastGuard G = true → + ∀ x, Reach nativeMk (root (ExplicitTensorNetwork.capPrecision (P, G))) x → active x = false → + (leafCertificate nativeMk).time x ≤ + K * ((FastContraction.encInput (P, G)).length + 1) ^ K * + 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) ∧ + (leafCertificate nativeMk).space x ≤ + K * ((FastContraction.encInput (P, G)).length + 1) ^ K + +/-- `a B ^ a ≤ a B ^ K` for `1 ≤ B` and `a ≤ K`. -/ +private theorem mul_pow_le_mul_pow {a B K : ℕ} (hB : 1 ≤ B) (ha : a ≤ K) : + a * B ^ a ≤ a * B ^ K := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_right hB ha) + +/-- **The resource analysis of the native recursion**, from polynomial sizes along the recursion +and the leaf bounds. The derivation of the root over the reached calls has at most `m + 1` stack +levels, and, from some size on, its nodes fit in the clock. -/ +theorem fastAnalysis_nativeMk_of (hS : FastSizes) (hL : FastLeaves) : FastAnalysis nativeMk := by + intro C D + obtain ⟨cS, dS, hKS⟩ := hS C D + obtain ⟨KL, hKL⟩ := hL C D + obtain ⟨sA, hsA⟩ := exists_activeBounds_le D + refine ⟨cS + dS + KL + 1, max sA (D + 2), fun s P G hs hP hPD hA hg => ?_⟩ + set q := ExplicitTensorNetwork.capPrecision (P, G) with hq + set x₀ := root q with hx₀ + set m := G.2.numEdges with hm + set n := (FastContraction.encInput (P, G)).length with hn + have hsm : s ≤ m := hA.2.2.2.2.2 + have hmn : m < n := numEdges_lt_length_encInput P G + have hp₀ : q.1 ≤ D * m := + (min_le_right _ _).trans (hPD.trans (Nat.mul_le_mul_left _ hsm)) + -- The derivation. + obtain ⟨N, H, he, hN, hH⟩ : ∃ N H, (scheme nativeMk).Eval (reachInv nativeMk x₀) x₀ + (0, value nativeMk x₀) N H ∧ (max sA (D + 2) ≤ s → 2 * N - 1 ≤ fuel q) ∧ H ≤ m + 1 := by + by_cases hs₀ : max sA (D + 2) ≤ s + · have hm2 : D + 2 ≤ m := by omega + have hC1 : q.1 / m + 1 ≤ D + 1 := by + have := Nat.div_le_div_right (c := m) hp₀ + rw [Nat.mul_div_cancel _ (by omega)] at this + omega + have hB := hsA m (by omega) (q.1 / m + 1) hC1 + have hpC : q.1 ≤ (q.1 / m + 1) * m := + (Nat.lt_div_mul_add (a := q.1) (b := m) (by omega)).le.trans (by rw [add_mul, one_mul]) + obtain ⟨N, H, he, hN, hH⟩ := exists_eval_onSchedule hB + (onSchedule_root_capPrecision hg (Nat.le_add_left 1 _) hpC) rfl (by omega) + refine ⟨N, H, he, fun _ => ?_, hH.trans ((Nat.log_lt_self 2 (by omega)).le.trans + (Nat.le_succ _))⟩ + exact two_mul_sub_one_le_fuel hm2 hp₀ hN + · obtain ⟨N, H, he, hH⟩ := exists_eval_reachInv (mk := nativeMk) (x₀ := x₀) rfl + exact ⟨N, H, he, fun h => absurd h hs₀, hH⟩ + -- The bounds. + obtain hKS' := hKS s P G hs hP hPD hA hg + obtain hKL' := hKL s P G hs hP hPD hA hg + set K := cS + dS + KL + 1 + have hB1 : 1 ≤ n + 1 := by omega + refine ⟨reachInv nativeMk x₀, N, H, cS * (n + 1) ^ dS, KL * (n + 1) ^ KL * 2 ^ (KL * s / + Nat.sqrt (Nat.log 2 s)), KL * (n + 1) ^ KL, he, hN, fun x hx => ⟨(hKS' x hx).1, fun hl => ?_⟩, + fun x a ha => (hKS' x ha.1).2.1 a ha, fun v ⟨x, hx, hv⟩ => hv ▸ (hKS' x hx).2.2, ?_, ?_⟩ + · have hl' : active x = false := by simpa [scheme] using hl + exact hKL' x hx hl' + · have h1 : H ≤ 1 * (n + 1) ^ K := by + have : n + 1 ≤ (n + 1) ^ K := Nat.le_self_pow (by omega) _ + omega + have h2 : cS * (n + 1) ^ dS ≤ cS * (n + 1) ^ K := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_right hB1 (by omega)) + have h3 := mul_pow_le_mul_pow (a := KL) hB1 (show KL ≤ K by omega) + calc H + cS * (n + 1) ^ dS + KL * (n + 1) ^ KL + ≤ 1 * (n + 1) ^ K + cS * (n + 1) ^ K + KL * (n + 1) ^ K := by omega + _ ≤ K * (n + 1) ^ K := by + rw [← add_mul, ← add_mul] + exact Nat.mul_le_mul_right _ (by omega) + · refine Nat.mul_le_mul (mul_pow_le_mul_pow' hB1 (show KL ≤ K by omega)) + (Nat.pow_le_pow_right (by norm_num) (Nat.div_le_div_right (Nat.mul_le_mul_right _ + (by omega)))) +where + /-- `a B ^ a ≤ K B ^ K` for `1 ≤ B` and `a ≤ K`. -/ + mul_pow_le_mul_pow' {a B K : ℕ} (hB : 1 ≤ B) (ha : a ≤ K) : a * B ^ a ≤ K * B ^ K := + Nat.mul_le_mul ha (Nat.pow_le_pow_right hB ha) + +/-! ### The sizes -/ + +/-- The modulus has at most `32 (m + 1) ^ 2` coefficients. -/ +theorem length_modulus_le (m : ℕ) : (modulus m).length ≤ 32 * (m + 1) ^ 2 := by + rw [length_modulus] + set t := modulusExp m + have h1 : 2 ^ t ≤ 4 * Nat.log 2 m + 2 := Nat.pow_log_le_self 2 (by omega) + have h2 : Nat.log 2 m ≤ m := by + rcases Nat.eq_zero_or_pos m with h | h + · simp [h] + · exact (Nat.log_lt_self 2 h.ne').le + have h3 : 3 ^ t ≤ (2 ^ t) ^ 2 := by + rw [← pow_mul, mul_comm, pow_mul] + exact Nat.pow_le_pow_left (by norm_num) t + have h4 : (2 ^ t) ^ 2 ≤ (4 * (m + 1)) ^ 2 := Nat.pow_le_pow_left (by omega) 2 + nlinarith + +/-- The coefficients of the modulus are `0` or `1`. -/ +theorem le_one_of_mem_modulus {m z : ℕ} (hz : z ∈ modulus m) : z ≤ 1 := by + simp only [modulus, List.mem_map, List.mem_range] at hz + obtain ⟨i, -, rfl⟩ := hz + split_ifs <;> omega + +/-- The encoded network is at most the encoded input long. -/ +theorem length_encExplicitNetwork_le (P : ℕ) (G : ℕ × ExplicitTensorNetwork ℕ) : + (ExplicitTensorNetwork.encExplicitNetwork G.2).length ≤ + (FastContraction.encInput (P, G)).length := by + simp only [FastContraction.encInput, length_encPair] + omega + +/-- The vertices of an explicit network, encoded, are at most the encoded network long. -/ +theorem length_vertices_le (G : ExplicitTensorNetwork ℕ) : + G.vertices.length ≤ (ExplicitTensorNetwork.encExplicitNetwork G).length ∧ + ∀ v ∈ G.vertices, (encList encNat v.2).length + 1 ≤ + (ExplicitTensorNetwork.encExplicitNetwork G).length := by + have hl : (ExplicitTensorNetwork.encExplicitNetwork G).length = 2 * G.numEdges + 1 + + (G.vertices.map fun v => + 2 * (encPair (encList encNat) (encList encNat) v).length + 1).sum := by + simp only [ExplicitTensorNetwork.encExplicitNetwork, encOfEquiv, Function.Embedding.trans_apply, + Equiv.coe_toEmbedding, DescribedNetwork.equivProd, Equiv.coe_fn_mk, length_encPair, + encUnary_apply, List.length_replicate, length_encList] + refine ⟨?_, fun v hv => ?_⟩ + · have := List.length_le_sum_of_one_le (G.vertices.map fun v => + 2 * (encPair (encList encNat) (encList encNat) v).length + 1) (fun i hi => by + obtain ⟨v, -, rfl⟩ := List.mem_map.mp hi + omega) + rw [List.length_map] at this + omega + · have := List.le_sum_of_mem (List.mem_map_of_mem (f := fun v => + 2 * (encPair (encList encNat) (encList encNat) v).length + 1) hv) + have h2 := length_encPair (enc₁ := encList encNat) (enc₂ := encList encNat) v + omega + +/-- **Polynomial sizes along the recursion**: every call reached from the root of a guarded input, +its frames and its tagged value are at most `2 ^ 55 (n + 1) ^ 24` long. -/ +theorem fastSizes : FastSizes := by + intro C D + refine ⟨2 ^ 55, 24, fun s P G _ _ _ _ hg x hx => ?_⟩ + set q := ExplicitTensorNetwork.capPrecision (P, G) with hq + set x₀ := root q with hx₀ + set m := G.2.numEdges with hm + set n := (FastContraction.encInput (P, G)).length with hn + set Y := n + 1 with hY + have hmn : m < n := numEdges_lt_length_encInput P G + have hnet := length_encExplicitNetwork_le P G + obtain ⟨hV, hdesc⟩ := length_vertices_le G.2 + have hp₀ : x₀.prec ≤ n := (min_le_left _ _).trans hnet + have hrows : (encNat x₀.rows).length ≤ n := by + change (encNat G.1).length ≤ n + simp only [hn, FastContraction.encInput, length_encPair] + omega + have hV₀ : x₀.net.vertices.length ≤ n := by + change (List.map _ G.2.vertices).length ≤ n + rw [List.length_map]; omega + have hsh := Reach.shape (x₀ := x₀) rfl rfl (wf_root P hg) hx + set Z := 2 ^ 14 * Y ^ 8 with hZ + have hY1 : 1 ≤ Y := by omega + have hmY : m + 1 ≤ Y := by omega + have hY3 : Y ≤ Y ^ 3 := Nat.le_self_pow (by norm_num) _ + have hY8 : Y ^ 3 ≤ Y ^ 8 := Nat.pow_le_pow_right hY1 (by norm_num) + have hY2 : Y ^ 2 ≤ Y ^ 3 := Nat.pow_le_pow_right hY1 (by norm_num) + have hm2 : m ^ 2 ≤ Y ^ 2 := Nat.pow_le_pow_left (by omega) 2 + have hm5 : (m + 1) ^ 5 ≤ Y ^ 5 := Nat.pow_le_pow_left hmY 5 + have hPm : x₀.prec + (x₀.edges + 1) * (40 * x₀.edges ^ 2) + 1 ≤ 41 * Y ^ 3 := by + change x₀.prec + (m + 1) * (40 * m ^ 2) + 1 ≤ 41 * Y ^ 3 + have : (m + 1) * (40 * m ^ 2) ≤ Y * (40 * Y ^ 2) := Nat.mul_le_mul hmY (by omega) + have : Y * (40 * Y ^ 2) = 40 * Y ^ 3 := by ring + omega + have hZ1 : 256 * (x₀.edges + 1) ^ 5 * (x₀.prec + (x₀.edges + 1) * (40 * x₀.edges ^ 2) + 1) + + x₀.fl.length ≤ Z := by + have h1 : 256 * (x₀.edges + 1) ^ 5 * (x₀.prec + (x₀.edges + 1) * (40 * x₀.edges ^ 2) + 1) ≤ + 256 * Y ^ 5 * (41 * Y ^ 3) := Nat.mul_le_mul (Nat.mul_le_mul_left _ hm5) hPm + have h2 : 256 * Y ^ 5 * (41 * Y ^ 3) = 10496 * Y ^ 8 := by ring + have h3 : x₀.fl.length ≤ 32 * Y ^ 8 := (length_modulus_le m).trans + (by have := Nat.pow_le_pow_left hmY 2; omega) + omega + have hZ2 : x₀.net.vertices.length + (x₀.edges + 1) * x₀.edges ^ 2 + (encNat x₀.rows).length ≤ + Z := by + have : (x₀.edges + 1) * x₀.edges ^ 2 ≤ Y * Y ^ 2 := Nat.mul_le_mul hmY hm2 + have : Y * Y ^ 2 = Y ^ 3 := by ring + omega + have hR₀ : ∀ w ∈ x₀.net.vertices, (VertexDesc.enc w.2).length ≤ 200 * (Z + 1) ^ 2 := by + intro w hw + change w ∈ List.map _ G.2.vertices at hw + obtain ⟨v, hv, rfl⟩ := List.mem_map.mp hw + rw [length_encSum] + simp only [Sum.elim_inl] + have := hdesc v hv + have : Z ≤ (Z + 1) ^ 2 := (Nat.le_succ Z).trans (Nat.le_self_pow (by norm_num) _) + omega + obtain ⟨hc, hv, hf⟩ := hsh.length_le rfl rfl rfl hZ1 hZ2 + (fun z hz => le_one_of_mem_modulus hz) hR₀ + -- `1000 (Z + 1) ^ 3 ≤ 2 ^ 55 (n + 1) ^ 24`. + have hfin : 1000 * (Z + 1) ^ 3 ≤ 2 ^ 55 * Y ^ 24 := by + have h1 : Z + 1 ≤ 2 ^ 15 * Y ^ 8 := by + have : 1 ≤ Y ^ 8 := Nat.one_le_pow _ _ hY1 + omega + have h2 : (Z + 1) ^ 3 ≤ (2 ^ 15 * Y ^ 8) ^ 3 := Nat.pow_le_pow_left h1 3 + have h3 : (2 ^ 15 * Y ^ 8) ^ 3 = 2 ^ 45 * Y ^ 24 := by ring + rw [h3] at h2 + have h4 : 1000 * (2 ^ 45 * Y ^ 24) ≤ 2 ^ 55 * Y ^ 24 := by + rw [← Nat.mul_assoc] + exact Nat.mul_le_mul_right _ (by norm_num) + exact (Nat.mul_le_mul_left 1000 h2).trans h4 + refine ⟨hc.trans hfin, fun a ⟨_, ha, c, _, hac⟩ => ?_, hv.trans hfin⟩ + rw [hac] + exact (hf ha _ c).trans hfin + +/-- **The resource analysis of the native recursion**, given the leaf bounds. -/ +theorem fastAnalysis_nativeMk (hL : FastLeaves) : FastAnalysis nativeMk := + fastAnalysis_nativeMk_of fastSizes hL + +/-! ### Facts at the leaves -/ + +/-- `D m + 40 m ^ 2 (m + 1) ≤ m ^ 4` from `m = D + 81` on. -/ +private theorem prec_arith {m D : ℕ} (hm : D + 81 ≤ m) : + D * m + (m + 1) * (40 * m ^ 2) ≤ m ^ 4 := by + have h1 : D * m ≤ m * m := Nat.mul_le_mul_right _ (by omega) + have h2 : 81 * m ^ 3 ≤ m ^ 4 := by + rw [pow_succ m 3, mul_comm (m ^ 3) m] + exact Nat.mul_le_mul_right _ (by omega) + have h3 : m * m ≤ m ^ 3 := by nlinarith + have h4 : m ^ 2 ≤ m ^ 3 := Nat.pow_le_pow_right (by omega) (by norm_num) + have e : (m + 1) * (40 * m ^ 2) = 40 * m ^ 3 + 40 * m ^ 2 := by ring + have h5 : m * m = m ^ 2 := by ring + omega + +/-- **The facts at the reached calls that the leaf bounds use.** For all constants `C` and `D` there +is `s₀` such that on every guarded input admissible at size `s ≥ 2` with constant `C` and with +precision `1 ≤ P ≤ D s`, every call reached from the root has scale `m` with `s ≤ m ≤ C s`, at most +`2 m` edges, and, from `s₀` on, precision at most `m ^ 4`, and at most `leafSize m` edges if the +machine treats it as a leaf. -/ +theorem reach_facts (C D : ℕ) : ∃ s₀, ∀ (s P : ℕ) (G : ℕ × ExplicitTensorNetwork ℕ), 2 ≤ s → + 1 ≤ P → P ≤ D * s → ExplicitAdmissible C s G → fastGuard G = true → + ∀ x, Reach nativeMk (root (ExplicitTensorNetwork.capPrecision (P, G))) x → + s ≤ x.scale ∧ x.scale ≤ C * s ∧ x.edges ≤ 2 * x.scale ∧ + (s₀ ≤ s → x.prec ≤ x.scale ^ 4 ∧ (active x = false → x.edges ≤ leafSize x.scale)) := by + obtain ⟨sA, hsA⟩ := exists_activeBounds_le D + refine ⟨max sA (D + 81), fun s P G hs hP hPD hA hg x hx => ?_⟩ + set q := ExplicitTensorNetwork.capPrecision (P, G) with hq + set m := G.2.numEdges with hm + have hsm : s ≤ m := hA.2.2.2.2.2 + have hmC : m ≤ C * s := hA.2.1 + have hp₀ : q.1 ≤ D * m := + (min_le_right _ _).trans (hPD.trans (Nat.mul_le_mul_left _ hsm)) + have hsh := Reach.shape (x₀ := root q) rfl rfl (wf_root P hg) hx + have hsc : x.scale = m := hsh.scale_eq + refine ⟨hsc ▸ hsm, hsc ▸ hmC, hsc ▸ hsh.edges_le, fun hs₀ => ⟨?_, fun hl => ?_⟩⟩ + · have hbd := hsh.bound_add_depth_le + change x.bound + x.depth ≤ (m + 1) + 0 at hbd + have hprec : x.prec ≤ q.1 + x.depth * (40 * m ^ 2) := hsh.prec_le + have : x.depth * (40 * m ^ 2) ≤ (m + 1) * (40 * m ^ 2) := Nat.mul_le_mul_right _ (by omega) + have := prec_arith (m := m) (D := D) (by omega) + rw [hsc] + omega + · have hm2 : D + 2 ≤ m := by omega + have hC1 : q.1 / m + 1 ≤ D + 1 := by + have := Nat.div_le_div_right (c := m) hp₀ + rw [Nat.mul_div_cancel _ (by omega)] at this + omega + have hB := hsA m (by omega) (q.1 / m + 1) hC1 + have hpC : q.1 ≤ (q.1 / m + 1) * m := + (Nat.lt_div_mul_add (a := q.1) (b := m) (by omega)).le.trans (by rw [add_mul, one_mul]) + have h := hx.onSchedule hB (onSchedule_root_capPrecision hg (Nat.le_add_left 1 _) hpC) + rw [hsc] + exact h.edges_le_leafSize hB hl + +end Cslib.Complexity.CountingSimulation diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastLeaves.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastLeaves.lean new file mode 100644 index 0000000000..f5b6d411c6 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastLeaves.lean @@ -0,0 +1,146 @@ +/- +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.Complexity.Classes.CountingSimulation.FastAnalysis +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionLeaf + +/-! +# The leaf bounds of the native recursion + +The leaf clause of the resource analysis of the native recursion of Theorem D.1 of +[OpenAI2026ETH] (`Cslib.Complexity.CountingSimulation.FastLeaves`), from the cost of a leaf with +the packet shape (`Cslib.Circuits.Frontier.FastContraction.exists_leafCertificate_le`), the sizes +of the reached calls (`Cslib.Complexity.CountingSimulation.FastSizes`) and three facts about the +reached calls: at most twice the scale in edges and, from some size on, at most the leaf size in +edges at a leaf and precision at most the fourth power of the scale. Those facts and the sizes are +proved (`FastContraction.Reach.edges_le_two_mul_scale`, `CountingSimulation.reach_facts`, +`CountingSimulation.fastSizes`), so the resource analysis of the native recursion holds +(`CountingSimulation.fastAnalysis_nativeMk_holds`). + +Every reached call is well-formed and has the packet shape (`FastContraction.Reach.wf_packetShape`), +by `FastContraction.wfChildren_nativeMk` and `FastContraction.packetShape_child`. + +## Main results + +* `Cslib.Circuits.Frontier.FastContraction.Reach.wf_packetShape`: the reached calls are + well-formed and have the packet shape. +* `Cslib.Complexity.CountingSimulation.fastLeaves_of`: the leaf bounds from the reached-call facts. +* `Cslib.Circuits.Frontier.FastContraction.Reach.edges_le_two_mul_scale`: at most twice the scale + in edges. +* `Cslib.Complexity.CountingSimulation.fastLeaves`: the leaf bounds. +* `Cslib.Complexity.CountingSimulation.fastAnalysis_nativeMk_holds`: the resource analysis of the + native recursion. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.6–§D.4.7, + pp. 63–64. +-/ + +public section + +namespace Cslib.Circuits.Frontier.FastContraction + +/-- **The reached calls are well-formed and have the packet shape**, from a well-formed root with +the packet shape. -/ +theorem Reach.wf_packetShape {x₀ x : Call} (h : Reach nativeMk x₀ x) (hw : WF x₀) + (hs : PacketShape x₀) : WF x ∧ PacketShape x := by + induction h with + | root => exact ⟨hw, hs⟩ + | step c _ ha hc ih => + exact ⟨wfChildren_nativeMk _ ih.1 ha c hc, packetShape_child ih.1 ha ih.2 hc⟩ + +/-- **Reached calls have at most twice the scale in edges**, from a root at scale its number of +edges with bound plus depth one more, for every input: a child has at most twice its parent's +edges (`NativeChild.numEdges_nativeChild_le`), and an active parent has at most the root's. -/ +theorem Reach.edges_le_two_mul_scale {x₀ x : Call} (h₀s : x₀.scale = x₀.edges) + (h₀b : x₀.bound + x₀.depth = x₀.edges + 1) (h : Reach nativeMk x₀ x) : + x.edges ≤ 2 * x.scale := by + have key : x.edges ≤ 2 * x₀.edges := by + induction h with + | root => omega + | @step y c hy ha _ _ => + have h1 : (nativeMk y c).2.numEdges ≤ 2 * y.edges := by + unfold nativeMk + exact NativeChild.numEdges_nativeChild_le _ _ _ _ _ _ _ _ _ _ _ + have h2 := hy.bound_add_depth_le + have h3 := edges_lt_bound_of_active ha + change (nativeMk y c).2.numEdges ≤ 2 * x₀.edges + omega + rw [h.scale_eq, h₀s] + exact key + +end Cslib.Circuits.Frontier.FastContraction + +namespace Cslib.Complexity.CountingSimulation + +open Cslib.Circuits.Frontier Cslib.Circuits.Frontier.ContractionSchedule + Cslib.Circuits.Frontier.FastContraction + +/-- **The leaf bounds of the native recursion**, from the sizes of the reached calls and three +facts about them on admissible guarded inputs: every reached call has at most twice its scale in +edges, and for each `C` and `D`, from some size on, every reached leaf has at most the leaf size in +edges and precision at most the fourth power of its scale. -/ +theorem fastLeaves_of (hS : FastSizes) + (hE : ∀ (P : ℕ) (G : ℕ × ExplicitTensorNetwork ℕ) (x : Call), + Reach nativeMk (root (ExplicitTensorNetwork.capPrecision (P, G))) x → + x.edges ≤ 2 * x.scale) + (hbig : ∀ C D : ℕ, ∃ s₀ : ℕ, ∀ (s P : ℕ) (G : ℕ × ExplicitTensorNetwork ℕ), 2 ≤ s → 1 ≤ P → + P ≤ D * s → ExplicitAdmissible C s G → fastGuard G = true → s₀ ≤ s → + ∀ x, Reach nativeMk (root (ExplicitTensorNetwork.capPrecision (P, G))) x → + active x = false → x.edges ≤ leafSize x.scale ∧ x.prec ≤ x.scale ^ 4) : + FastLeaves := by + intro C D + obtain ⟨cS, dS, hKS⟩ := hS C D + set KS := cS + dS + obtain ⟨s₀, hs₀⟩ := hbig C D + obtain ⟨KB, hKB⟩ := exists_leafCertificate_le C 4 s₀ + refine ⟨KB * (KS + 1) ^ KB + KS * KB + KB, fun s P G hs hP hPD hA hg x hx hl => ?_⟩ + set n := (FastContraction.encInput (P, G)).length with hn + have hscale : x.scale = G.2.numEdges := hx.scale_eq + have hsm : s ≤ x.scale := hscale ▸ hA.2.2.2.2.2 + have hmC : x.scale ≤ C * s := hscale ▸ hA.2.1 + obtain ⟨-, hshape⟩ := hx.wf_packetShape (wf_root P hg) (packetShape_root _) + obtain ⟨hT, hSp⟩ := hKB nativeMk s x hs hsm hmC hshape (hE P G x hx) + fun h => hs₀ s P G hs hP hPD hA hg h x hx hl + have hlen' := (hKS s P G hs hP hPD hA hg x hx).1 + rw [← hn] at hlen' + have hlen : (encCall x).length ≤ KS * (n + 1) ^ KS := + hlen'.trans (Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right (by omega) (by omega))) + -- `n_x + 1 ≤ (KS + 1) (n + 1) ^ KS`. + have hB1 : 1 ≤ (n + 1) ^ KS := Nat.one_le_pow _ _ (by omega) + have hx1 : (encCall x).length + 1 ≤ (KS + 1) * (n + 1) ^ KS := by + rw [add_mul, one_mul]; omega + set K := KB * (KS + 1) ^ KB + KS * KB + KB + have hpoly : KB * ((encCall x).length + 1) ^ KB ≤ K * (n + 1) ^ K := + calc KB * ((encCall x).length + 1) ^ KB ≤ KB * ((KS + 1) * (n + 1) ^ KS) ^ KB := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hx1 _) + _ = KB * (KS + 1) ^ KB * (n + 1) ^ (KS * KB) := by rw [mul_pow, ← pow_mul]; ring + _ ≤ K * (n + 1) ^ K := + Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right (by omega) (by omega)) + have hexp : KB * s / Nat.sqrt (Nat.log 2 s) ≤ K * s / Nat.sqrt (Nat.log 2 s) := + Nat.div_le_div_right (Nat.mul_le_mul_right _ (by omega)) + exact ⟨hT.trans (Nat.mul_le_mul hpoly (Nat.pow_le_pow_right (by norm_num) hexp)), + hSp.trans hpoly⟩ + +/-- **The leaf bounds of the native recursion.** -/ +theorem fastLeaves : FastLeaves := + fastLeaves_of fastSizes (fun _ _ _ hx => hx.edges_le_two_mul_scale rfl rfl) fun C D => by + obtain ⟨s₀, hs₀⟩ := reach_facts C D + refine ⟨s₀, fun s P G hs hP hPD hA hg h x hx hl => ?_⟩ + obtain ⟨hp, hlf⟩ := (hs₀ s P G hs hP hPD hA hg x hx).2.2.2 h + exact ⟨hlf hl, hp⟩ + +/-- **The resource analysis of the native recursion holds**: the derivation of the root over the +reached calls has polynomial height, sizes and leaf space, leaf time `poly(n) 2 ^ O(s / √⌊log₂ s⌋)`, +and, from some size on, its nodes fit in the clock. -/ +theorem fastAnalysis_nativeMk_holds : FastAnalysis nativeMk := + fastAnalysis_nativeMk fastLeaves + +end Cslib.Complexity.CountingSimulation diff --git a/Complexity/Computability/GenericRAM/Native/StackRecursionTree.lean b/Complexity/Computability/GenericRAM/Native/StackRecursionTree.lean index 0f72261147..2eb5616ba5 100644 --- a/Complexity/Computability/GenericRAM/Native/StackRecursionTree.lean +++ b/Complexity/Computability/GenericRAM/Native/StackRecursionTree.lean @@ -41,6 +41,8 @@ small to vouch for the run. recursion. * `Cslib.GenericRAM.StackRecursion.Scheme.exists_eval_of_counted`: derivations with the node count of the recursion tree. +* `Cslib.GenericRAM.StackRecursion.Scheme.exists_eval_of_height`: derivations with their height + alone. * `Cslib.GenericRAM.StackRecursion.Scheme.value_of_run_eq_some`: a returned value satisfies the invariant. @@ -179,6 +181,43 @@ theorem exists_eval_of_counted (μ depth : X → ℕ) (value : X → Y) (b : ℕ rw [hleaf x hx hl] exact Eval.leaf hx hl (hleaf x hx hl ▸ hvalue x hx) +/-- **Derivations with their height.** Let `value` assign values to the nodes satisfying `I.node`, +all satisfying `I.value`, such that a leaf has its leaf value, and a call at depth `d` has +`d < D` and counted children, as in `exists_eval_of_counted`, at depth `d + 1`. Then every node at +depth `d ≤ D` has a derivation of its value with at most `D - d` stack levels. This is +`exists_eval_of_counted` without a bound on the number of children. -/ +theorem exists_eval_of_height (μ depth : X → ℕ) (value : X → Y) (D : ℕ) + (hleaf : ∀ x, I.node x → R.isLeaf x = true → value x = R.leaf x) + (hcall : ∀ x, I.node x → R.isLeaf x = false → depth x < D ∧ + ∃ (cnt : ℕ) (acc : ℕ → A) (child : ℕ → X), acc 0 = R.start x ∧ + (∀ c < cnt, R.next x (acc c) = some (child c)) ∧ R.next x (acc cnt) = none ∧ + (∀ c < cnt, R.absorb x (acc c) (value (child c)) = acc (c + 1)) ∧ + (∀ c < cnt, I.frame x (acc c) ∧ I.node (child c) ∧ μ (child c) < μ x ∧ + depth (child c) = depth x + 1) ∧ + value x = R.finish x (acc cnt)) + (hvalue : ∀ x, I.node x → I.value (value x)) (x : X) (hx : I.node x) (hxD : depth x ≤ D) : + ∃ n h, R.Eval I x (value x) n h ∧ h ≤ D - depth x := by + induction hμ : μ x using Nat.strong_induction_on generalizing x with + | _ k ih => + cases hl : R.isLeaf x + · obtain ⟨hd, cnt, acc, child, h0, hnext, hdone, habs, hkids, hfin⟩ := hcall x hx hl + have hev : ∀ c < cnt, ∃ n h, R.Eval I (child c) (value (child c)) n h ∧ + h ≤ D - (depth x + 1) := fun c hc => by + obtain ⟨-, hn, hμc, hdc⟩ := hkids c hc + obtain ⟨n, h, he, hhb⟩ := ih (μ (child c)) (hμ ▸ hμc) (child c) hn (by omega) rfl + rw [hdc] at hhb + exact ⟨n, h, he, hhb⟩ + choose! nodes height hev using hev + obtain ⟨h, hh, hloop⟩ := Loop.counted (I := I) (val := fun c => value (child c)) cnt + (D - (depth x + 1)) hnext hdone habs (fun c hc => (hev c hc).1) + (fun c hc => (hkids c hc).1) (fun c hc => (hev c hc).2) + rw [h0] at hloop + have hv : I.value (R.finish x (acc cnt)) := hfin ▸ hvalue x hx + exact ⟨(∑ c ∈ range cnt, nodes c) + 1, h + 1, hfin ▸ Eval.call hx hl hloop hv, by omega⟩ + · refine ⟨1, 0, ?_, Nat.zero_le _⟩ + rw [hleaf x hx hl] + exact Eval.leaf hx hl (hleaf x hx hl ▸ hvalue x hx) + /-- **What a clocked run returns.** For any fuel, a value returned by the run satisfies the invariant of a derivation of the root. -/ theorem value_of_run_eq_some {J : Type} {fuel : J → ℕ} {root : J → X} {a : J} {y y' : Y} diff --git a/ComplexityTests/FastContractionAnalysis.lean b/ComplexityTests/FastContractionAnalysis.lean new file mode 100644 index 0000000000..29eb99127e --- /dev/null +++ b/ComplexityTests/FastContractionAnalysis.lean @@ -0,0 +1,70 @@ +/- +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.Complexity.Classes.CountingSimulation.FastAnalysis + +/-! # The resource analysis of the native recursion: checked instances + +The derivation invariant and the shape invariant at a small root, the reduced values, the clock +arithmetic at a concrete size, and the statement of the remaining obligation. -/ + +namespace ComplexityTests.FastContractionAnalysis + +open Cslib.Circuits.Frontier Cslib.Circuits.Frontier.FastContraction + Cslib.Complexity.CountingSimulation Cslib.Circuits.Frontier.ContractionSchedule + +/-- One row `0` and one column `1` joined by edge `0`, with full tables. -/ +def tiny : ℕ × ExplicitTensorNetwork ℕ := (1, ⟨1, [([0], [1, 2]), ([0], [3, 4])]⟩) + +example : fastGuard tiny = true := by decide + +/-- The root of `tiny` at precision `3`. -/ +abbrev tinyRoot : Call := root (ExplicitTensorNetwork.capPrecision (3, tiny)) + +-- The root is reached, and it is the only reached call at depth `0`. +example : Reach nativeMk tinyRoot tinyRoot := .root +example (x : Call) (hx : Reach nativeMk tinyRoot x) (h0 : x.depth = 0) : x = tinyRoot := + hx.eq_root_of_depth_le (by rw [h0]; rfl) + +-- The root is a leaf, so its derivation has one node and no open call. +example : active tinyRoot = false := by decide + +-- The shape invariant holds at every reached call; at the root it is the root itself. +example : Shape tinyRoot tinyRoot := + Reach.shape rfl rfl (wf_root 3 (by decide)) .root + +-- The root is on the schedule for `C = 3`: its precision `3` is at most `3 ⬝ 1`. +example : OnSchedule 3 tiny.2.numEdges tinyRoot := + onSchedule_root_capPrecision (by decide) (by norm_num) (by decide) + +-- Values are reduced at their precision: at most `e` coordinates below `2 ^ p`. +example : ReducedAt tinyRoot.prec tinyRoot.fl (value nativeMk tinyRoot) := + reducedAt_value nativeMk tinyRoot + +-- The modulus at `m = 1` has `2 ⬝ 3 ^ 1 = 6` coefficients, within `32 (m + 1) ^ 2`. +example : (modulus 1).length = 6 := by decide +example : (modulus 1).length ≤ 32 * (1 + 1) ^ 2 := length_modulus_le 1 + +-- The clock arithmetic: with `m = 100` edges, precision `p = 50 ≤ 1 ⬝ m` and `D = 1`, a derivation +-- within the call count of `C' = ⌊50 / 100⌋ + 1 = 1` fits in the clock. +example (N : ℕ) (hN : N ≤ 2 ^ ((245760 * (50 / 100 + 1) + 37) * 100 / Nat.sqrt (Nat.log 2 100))) : + 2 * N - 1 ≤ 2 ^ (fuelConst * (100 + 50) / Nat.sqrt (Nat.log 2 (100 + 50))) := + two_mul_sub_one_le_fuel (D := 1) (by norm_num) (by norm_num) hN + +-- A child of a parent with `M` edges under (D.6) has at most `M / 16` edges. +example {r a i Δ : ℕ} {D : DescribedNetwork VertexDesc} (hD : D.IsRowsFirstBipartite r) + (hK : 64 ^ a ≤ D.numEdges) (hia : i < a) (hdeg : ∀ v ∈ D.vertices, v.1.length ≤ Δ) + (hM : 2 * Δ * (64 ^ (2 * a)) ^ 2 ≤ D.numEdges) (fl : List ℕ) (pt : ℕ) (t : ℤ) + (ζ β : List ℕ) (g : Fin 64) : + 16 * (NativeChild.nativeChild fl a i pt t ζ r D (NativeChild.nativeParentPacking r a D) β + g).numEdges ≤ D.numEdges := + NativeChild.sixteen_mul_numEdges_nativeChild_le hD hK hia hdeg hM fl pt t ζ β g + +-- The sizes are proved; the resource analysis needs only the leaf bounds. +example : FastSizes := fastSizes +example (hL : FastLeaves) : FastAnalysis nativeMk := fastAnalysis_nativeMk hL + +end ComplexityTests.FastContractionAnalysis diff --git a/ComplexityTests/FastContractionLeaf.lean b/ComplexityTests/FastContractionLeaf.lean new file mode 100644 index 0000000000..5a2370278f --- /dev/null +++ b/ComplexityTests/FastContractionLeaf.lean @@ -0,0 +1,85 @@ +/- +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.FastContractionLeaf + +/-! # The leaves of the fast contraction machine: checked instances + +The packet shape on a root and on a call with a packet vertex, the row ports and target modes it +bounds, and an input meeting every hypothesis of the leaf bound. -/ + +namespace ComplexityTests.FastContractionLeaf + +open Cslib.Circuits.Frontier Cslib.Circuits.Frontier.FastContraction + Cslib.Circuits.Frontier.NativePacket Cslib.Circuits.Frontier.ContractionSchedule + +/-- Two rows `0, 1` and two columns `2, 3`, joined by edges `0 : 0 → 2` and `1 : 1 → 3`. -/ +def pair : ℕ × ExplicitTensorNetwork ℕ := + (2, ⟨2, [([0], [1, 2]), ([1], [3, 4]), ([0], [1, 1]), ([1], [1, 0])]⟩) + +-- The root of `(1, pair)`: scale `2`, two edges, precision `1`. +example : (root (1, pair)).scale = 2 ∧ (root (1, pair)).edges = 2 ∧ + (root (1, pair)).prec = 1 := by decide + +-- The root has the packet shape: its vertices are tables. +example : PacketShape (root (1, pair)) := packetShape_root _ + +-- At `s = 2`, the root meets every hypothesis of `exists_leafCertificate_le` with `C = 1` and +-- `c = 2`, for every `s₀`: `leafSize 2 = 2` and `1 ≤ 2 ^ 2`. +example (s₀ : ℕ) : 2 ≤ 2 ∧ 2 ≤ (root (1, pair)).scale ∧ (root (1, pair)).scale ≤ 1 * 2 ∧ + PacketShape (root (1, pair)) ∧ (root (1, pair)).edges ≤ 2 * (root (1, pair)).scale ∧ + (s₀ ≤ 2 → (root (1, pair)).edges ≤ leafSize (root (1, pair)).scale ∧ + (root (1, pair)).prec ≤ (root (1, pair)).scale ^ 2) := + ⟨le_rfl, by decide, by decide, packetShape_root _, by decide, fun _ => by decide⟩ + +/-- A packet context with `a = 1` slot bit, `i = 0`, two tiles, precision `1` and one exponent per +tile. -/ +def ctx : PacketCtx where + p := 1 + fl := [1] + a := 1 + L := 2 + i := 0 + tiles := 2 + t := 1 + nb := 1 + e₁ := true + e₂ := false + differ := true + cols := [] + ζ := [0] + +/-- A packet vertex with a row port in slot `0` and a column port in slot `1`. -/ +def packetVertex : List ℕ × VertexDesc := ([0, 1], .inr (ctx, [(true, 0), (false, 1)], [0, 0])) + +/-- A call at scale `4` and precision `1` whose network is the packet vertex alone. -/ +def packetCall : Call := ((4, 1, 3, 1, [1], 0), ⟨2, [packetVertex]⟩) + +-- The packet vertex has one row port, and at most `2 ⬝ 1` target modes. +example : packetVertex.2.rowPorts [true, false] = 1 := by decide +example : packetVertex.2.modes ≤ 2 := by decide + +-- The packet shape is not vacuous on packets. Here `a = 1` exceeds `⌊log₂ 4⌋ / 32768 = 0`, so the +-- shape fails; a call one level down the schedule has `a ≤ ⌊log₂ s⌋ / 32768`. +example : ¬ PacketShape packetCall := by + intro h + have h1 : 1 ≤ Nat.log 2 4 / 32768 := (h packetVertex (by simp [packetCall]) _ rfl).2.1 + rw [show (4 : ℕ) = 2 ^ 2 by norm_num, Nat.log_pow (by norm_num)] at h1 + omega + +-- From scale `2 ^ 32768` on, the same vertex has the packet shape. +example (s : ℕ) (hs : 32768 ≤ Nat.log 2 s) : + PacketShape ((s, 1, 3, 1, [1], 0), ⟨2, [packetVertex]⟩) := by + intro v hv d hd + simp only [List.mem_singleton] at hv + subst hv + simp only [packetVertex, Sum.inr.injEq] at hd + subst hd + refine ⟨by decide, ?_, by decide, le_rfl, by decide, by decide⟩ + change 1 ≤ Nat.log 2 s / 32768 + omega + +end ComplexityTests.FastContractionLeaf diff --git a/ComplexityTests/FastLeaves.lean b/ComplexityTests/FastLeaves.lean new file mode 100644 index 0000000000..03914e3872 --- /dev/null +++ b/ComplexityTests/FastLeaves.lean @@ -0,0 +1,39 @@ +/- +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.Complexity.Classes.CountingSimulation.FastLeaves + +/-! # The leaf bounds of the native recursion: checked instances + +A guarded input whose root is reached, well-formed and has the packet shape; the edge bound on +reached calls; and the resource analysis. -/ + +namespace ComplexityTests.FastLeaves + +open Cslib.Circuits.Frontier Cslib.Circuits.Frontier.FastContraction + Cslib.Complexity.CountingSimulation + +/-- Two rows `0, 1` and two columns `2, 3`, joined by edges `0 : 0 → 2` and `1 : 1 → 3`. -/ +def pair : ℕ × ExplicitTensorNetwork ℕ := + (2, ⟨2, [([0], [1, 2]), ([1], [3, 4]), ([0], [1, 1]), ([1], [1, 0])]⟩) + +example : fastGuard pair = true := by decide + +-- The root of a guarded input is reached, well-formed, and has the packet shape. +example : WF (root (ExplicitTensorNetwork.capPrecision (1, pair))) ∧ + PacketShape (root (ExplicitTensorNetwork.capPrecision (1, pair))) := + (Reach.root (mk := nativeMk)).wf_packetShape (wf_root 1 (by decide)) (packetShape_root _) + +-- Reached calls have at most twice the scale in edges, on every input. +example (P : ℕ) (G : ℕ × ExplicitTensorNetwork ℕ) (x : Call) + (hx : Reach nativeMk (root (ExplicitTensorNetwork.capPrecision (P, G))) x) : + x.edges ≤ 2 * x.scale := + hx.edges_le_two_mul_scale rfl rfl + +-- The resource analysis of the native recursion holds, with no remaining hypothesis. +example : FastAnalysis nativeMk := fastAnalysis_nativeMk_holds + +end ComplexityTests.FastLeaves