diff --git a/Complexity.lean b/Complexity.lean index 85d501bae..854323aeb 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -937,6 +937,8 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Deformatio public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DescribedContraction public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DescribedLift public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DirectContraction +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.EntryContraction +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.EntryContractionMachine public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContraction public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionDerivation @@ -962,6 +964,7 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.PacketTerm public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Recursion public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ReductionLift public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Reindex +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.RowsFirstPolyTime public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Schedule public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ScheduleCount public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ScheduledRecursion @@ -1165,6 +1168,7 @@ public import Complexity.Computability.Complexity.Classes.CountingSimulation.Blo public import Complexity.Computability.Complexity.Classes.CountingSimulation.Containments public import Complexity.Computability.Complexity.Classes.CountingSimulation.Count public import Complexity.Computability.Complexity.Classes.CountingSimulation.CountingClasses +public import Complexity.Computability.Complexity.Classes.CountingSimulation.EntryAnalysis public import Complexity.Computability.Complexity.Classes.CountingSimulation.FastAlgorithm public import Complexity.Computability.Complexity.Classes.CountingSimulation.FastAnalysis public import Complexity.Computability.Complexity.Classes.CountingSimulation.FastLeaves diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/EntryContraction.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/EntryContraction.lean new file mode 100644 index 000000000..eeeb0d439 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/EntryContraction.lean @@ -0,0 +1,568 @@ +/- +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.Schedule +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimePrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Lists +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListBinaryLookup +import Complexity.Foundations.Data.BitString.Binary +import Complexity.Foundations.Data.Nat.Asymptotics + +/-! +# Contraction with entry procedures: the interface + +Theorem D.1 of [OpenAI2026ETH] (p. 53) contracts Boolean tensor networks whose entries are not +given as tables but computed: it assumes, uniformly over the vertices and the Boolean choices of +their ports, that each entry is computable from the description in time +`(s + L) ^ b 2 ^ (A s ^ (9/10))` and space `(s + L) ^ b` (a paraphrase), with maximum degree at +most `⌈s ^ (9/10)⌉`. At that degree a table has +`2 ^ ⌈s ^ (9/10)⌉` entries, so Lemma D.2 (p. 56), which applies the theorem with entries computed +by procedures, needs this form for its polynomial-space bound. This file states the interface +that the contraction algorithm provides for such networks, milestone E1 of #1538. + +**Entry procedures.** A network is a described network `DescribedNetwork T` (the record shared +with explicit networks), with descriptors in a type `T` encoded by `encT`. An *entry procedure* +is a function `entry : T → List Bool → List ℕ`, the coefficient list over +`A_P = (ℤ / 2 ^ P)[U] / (f)` of the entry of a descriptor at the bits on its ports, with a native +certificate `ce` on `encPair encT encBits`. This is the evaluator of direct summation +(`DescribedNetwork.contractionCertificate`). Explicit networks are the case of tables, and the +specialized networks of the truncation-order reduction (#1538, E2) are another instance. + +**Admissible networks** (`EntryAdmissible`). Theorem D.1's hypotheses with one constant `C` for +the theorem's `C`, `A` and `b`: rows-first bipartite, between `s` and `C s` edges, maximum degree +at most `⌈s ^ (9/10)⌉` (`ceilNineTenths`), and every entry within time +`C (s + L + 1) ^ C 2 ^ (C ⌈s ^ (9/10)⌉)` and space `C (s + L + 1) ^ C`, where `L` is the encoded +length of the network. Entry outputs need no separate size condition, because a native +certificate's space bound charges its encoded output. As for explicit networks +(`Cslib.Complexity.CountingSimulation.ExplicitAdmissible`), admissibility asks for at least `s` +edges; a caller can pad with disjoint edges whose row tensor is `[x = 0]` and column tensor `1`, +which leave the contraction unchanged. The number of vertices is not bounded separately: the +encoded length bounds it. + +**The interface** (`EntryContractionAlgorithm`). One native certificate maps an input +`(P, fl, r, G)`, with the precision `P` in unary and the coefficients `fl` of a modulus, to a +coefficient list whose value in `A_P` at the modulus `FastContraction.modulus m`, for `m` the +number of edges, is the contraction of the entries' values, on every input. On admissible inputs +at that modulus it runs in time `K (n + 1) ^ K 2 ^ (K s / √⌊log₂ s⌋)` and space `K (n + 1) ^ K`, +the bound shape of `Cslib.Complexity.CountingSimulation.ContractionAlgorithm`. The input format is +that of the truncation-order reduction's contractions of specialized networks. + +**Direct summation** (`EntryContraction.directCore`). Summing over all edge assignments with the +entry procedure computes the contraction on every input (`EntryContraction.val_directCore`), in +time `(2 ^ m (k + 1) + 1) (K (n + ES + 1) ^ K + 2 E)` and space `K (n + ES + 1) ^ K + ES` when the +procedure takes time `E` and space `ES` on the vertices (`EntryContraction.directCore_le`). On +admissible inputs that is `K (n + 1) ^ K 2 ^ (K s)` and polynomial space +(`EntryContraction.exists_directCore_le`): the fallback of the contraction algorithm for small `s`. + +**Instances.** A polynomial-time entry procedure meets the entry bounds from some constant on +(`EntryContraction.exists_entryAdmissible_of_isPolynomial`), so admissibility reduces to the +shape of the network. Tables are the entry procedure `tableEntry` (`VertexDesc.lean`), and direct +summation with it is the contraction of the explicit network +(`EntryContraction.val_directCore_tableEntry`). + +## Main definitions + +* `Cslib.Circuits.Frontier.ceilNineTenths`: `⌈s ^ (9/10)⌉`. +* `Cslib.Circuits.Frontier.EntryContraction.encInput`: the encoding of an input. +* `Cslib.Circuits.Frontier.EntryAdmissible`: Theorem D.1's hypotheses. +* `Cslib.Circuits.Frontier.EntryContractionAlgorithm`: the interface. +* `Cslib.Circuits.Frontier.EntryContraction.directCore`: direct summation with an entry procedure. + +## Main results + +* `Cslib.Circuits.Frontier.le_ceilNineTenths_iff`: `x ≤ ⌈s ^ (9/10)⌉` iff `(x - 1) ^ 10 < s ^ 9`. +* `Cslib.Circuits.Frontier.ceilNineTenths_le_degreeBound`: the degree bound of the schedule is at + least `⌈s ^ (9/10)⌉`. +* `Cslib.Circuits.Frontier.exists_mul_ceilNineTenths_le`: `A ⌈s ^ (9/10)⌉ ≤ s / √⌊log₂ s⌋` from + some size on, so entry costs fit the time budget. +* `Cslib.Circuits.Frontier.EntryContraction.val_directCore`: direct summation is correct. +* `Cslib.Circuits.Frontier.EntryContraction.directCore_le`, + `Cslib.Circuits.Frontier.EntryContraction.exists_directCore_le`: its resources. +* `Cslib.Circuits.Frontier.EntryContraction.exists_entryAdmissible_of_isPolynomial`: + polynomial-time entry procedures meet the entry bounds. +* `Cslib.Circuits.Frontier.EntryContraction.val_directCore_tableEntry`: direct summation of an + explicit network. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Theorem D.1 (p. 53), + Lemma D.2 (pp. 54–56) and Appendix D.4.6–D.4.7 (pp. 63–64). +-/ + +public section + +namespace Cslib.Circuits.Frontier + +open GaloisRingArith Cslib.GenericRAM Turing.MultiTapeTM + +/-! ### The nine-tenths power -/ + +/-- `s ^ 9 ≤ s ^ 10`. -/ +theorem pow_nine_le_pow_ten_self (s : ℕ) : s ^ 9 ≤ s ^ 10 := by + rcases Nat.eq_zero_or_pos s with rfl | hs + · simp + · exact Nat.pow_le_pow_right hs (by norm_num) + +/-- Some `x` has `s ^ 9 ≤ x ^ 10`. -/ +theorem exists_pow_nine_le_pow_ten (s : ℕ) : ∃ x, s ^ 9 ≤ x ^ 10 := + ⟨s, pow_nine_le_pow_ten_self s⟩ + +/-- **`⌈s ^ (9/10)⌉`**, the least `x` with `s ^ 9 ≤ x ^ 10`. -/ +@[expose] def ceilNineTenths (s : ℕ) : ℕ := Nat.find (exists_pow_nine_le_pow_ten s) + +/-- `s ^ 9 ≤ ⌈s ^ (9/10)⌉ ^ 10`. -/ +theorem pow_nine_le_ceilNineTenths_pow_ten (s : ℕ) : s ^ 9 ≤ ceilNineTenths s ^ 10 := + Nat.find_spec (exists_pow_nine_le_pow_ten s) + +/-- `⌈s ^ (9/10)⌉ ≤ x` whenever `s ^ 9 ≤ x ^ 10`. -/ +theorem ceilNineTenths_le {s x : ℕ} (h : s ^ 9 ≤ x ^ 10) : ceilNineTenths s ≤ x := + Nat.find_min' _ h + +/-- **`x ≤ ⌈s ^ (9/10)⌉` iff `(x - 1) ^ 10 < s ^ 9`**: the condition of a degree at most +`⌈s ^ (9/10)⌉`, for `s ≥ 1`. -/ +theorem le_ceilNineTenths_iff {s x : ℕ} (hs : 1 ≤ s) : + x ≤ ceilNineTenths s ↔ (x - 1) ^ 10 < s ^ 9 := by + constructor + · intro hx + by_contra h + rw [not_lt] at h + have h1 := ceilNineTenths_le h + rcases Nat.eq_zero_or_pos x with rfl | hx0 + · have : 1 ≤ s ^ 9 := Nat.one_le_pow _ _ hs + rw [Nat.zero_sub, zero_pow (by norm_num)] at h + omega + · omega + · intro h + by_contra hx + rw [not_le] at hx + have h1 : ceilNineTenths s ≤ x - 1 := by omega + have h2 := (pow_nine_le_ceilNineTenths_pow_ten s).trans (Nat.pow_le_pow_left h1 10) + omega + +/-- `⌈s ^ (9/10)⌉ ≤ s`. -/ +theorem ceilNineTenths_le_self (s : ℕ) : ceilNineTenths s ≤ s := + ceilNineTenths_le (pow_nine_le_pow_ten_self s) + +/-- **The degree bound of the schedule is at least `⌈s ^ (9/10)⌉`** +(`ContractionSchedule.pow_nine_le_degreeBound_pow_ten`). -/ +theorem ceilNineTenths_le_degreeBound (s : ℕ) : + ceilNineTenths s ≤ ContractionSchedule.degreeBound s := + ceilNineTenths_le (ContractionSchedule.pow_nine_le_degreeBound_pow_ten s) + +/-- **Entry costs fit the budget**: for every `A`, from some size on, +`A ⌈s ^ (9/10)⌉ ≤ s / √⌊log₂ s⌋`. So the entry time `2 ^ (A s ^ (9/10))` allowed by Theorem D.1 +is within the `2 ^ O(s / √log s)` budget of a leaf (§D.4.7, p. 64). -/ +theorem exists_mul_ceilNineTenths_le (A : ℕ) : + ∃ s₀ : ℕ, ∀ s, s₀ ≤ s → A * ceilNineTenths s ≤ s / Nat.sqrt (Nat.log 2 s) := by + obtain ⟨L₀, hL₀⟩ := Filter.eventually_atTop.mp + (Nat.eventually_mul_add_one_pow_le_pow_div (4 * A) 1 10 one_lt_two (by norm_num)) + refine ⟨2 ^ (L₀ + 1), fun s hs => ?_⟩ + obtain ⟨L, hLdef⟩ : ∃ L, L = Nat.log 2 s := ⟨_, rfl⟩ + have hs0 : s ≠ 0 := by have := Nat.one_le_two_pow (n := L₀ + 1); omega + have hL : L₀ + 1 ≤ L := hLdef ▸ Nat.le_log_of_pow_le one_lt_two hs + have h1 := hL₀ L (by omega) + rw [pow_one] at h1 + have hsq : Nat.sqrt L ≤ L + 1 := (Nat.sqrt_le_self L).trans (Nat.le_succ L) + have hsq0 : 0 < Nat.sqrt L := Nat.sqrt_pos.2 (by omega) + have hD : ceilNineTenths s ≤ 2 ^ (9 * L / 10 + 2) := by + have := ceilNineTenths_le_degreeBound s + rwa [ContractionSchedule.degreeBound, ← hLdef] at this + have hpow : 2 ^ L ≤ s := hLdef ▸ Nat.pow_log_le_self 2 hs0 + rw [← hLdef, Nat.le_div_iff_mul_le hsq0] + calc A * ceilNineTenths s * Nat.sqrt L ≤ A * 2 ^ (9 * L / 10 + 2) * (L + 1) := + Nat.mul_le_mul (Nat.mul_le_mul_left _ hD) hsq + _ = 2 ^ (9 * L / 10) * (4 * A * (L + 1)) := by rw [pow_add]; ring + _ ≤ 2 ^ (9 * L / 10) * 2 ^ (L / 10) := Nat.mul_le_mul_left _ h1 + _ = 2 ^ (9 * L / 10 + L / 10) := (pow_add _ _ _).symm + _ ≤ 2 ^ L := Nat.pow_le_pow_right (by norm_num) (by omega) + _ ≤ s := hpow + +/-! ### The interface -/ + +namespace EntryContraction + +/-- **The encoding of an input `(P, fl, r, G)`**: the precision `P` in unary, the coefficients of +the modulus and the number of rows in binary, then the network. -/ +abbrev encInput {T : Type} (encT : T ↪ List Bool) : + ℕ × List ℕ × ℕ × DescribedNetwork T ↪ List Bool := + encPair encUnary (encPair (encList encNat) (encPair encNat (DescribedNetwork.encDescribed encT))) + +end EntryContraction + +variable {T : Type} {encT : T ↪ List Bool} {entry : T → List Bool → List ℕ} + +/-- **Admissible networks with an entry procedure** at size `s` with constant `C` (Theorem D.1's +hypotheses, with `C` for its constants `C`, `A` and `b`): the network `G` with `r` row vertices is +rows-first bipartite, has between `s` and `C s` edges, every vertex has at most +`⌈s ^ (9/10)⌉` ports, and on every vertex and bits on its ports the entry procedure's certificate +takes time at most `C (s + L + 1) ^ C 2 ^ (C ⌈s ^ (9/10)⌉)` and space at most `C (s + L + 1) ^ C`, +for `L` the encoded length of `G`. -/ +@[expose] def EntryAdmissible + (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)) (C s : ℕ) (G : ℕ × DescribedNetwork T) : Prop := + G.2.IsRowsFirstBipartite G.1 ∧ s ≤ G.2.numEdges ∧ G.2.numEdges ≤ C * s ∧ + (∀ v ∈ G.2.vertices, v.1.length ≤ ceilNineTenths s) ∧ + ∀ v ∈ G.2.vertices, ∀ bs : List Bool, bs.length = v.1.length → + ce.time (v.2, bs) ≤ + C * (s + (DescribedNetwork.encDescribed encT G.2).length + 1) ^ C * + 2 ^ (C * ceilNineTenths s) ∧ + ce.space (v.2, bs) ≤ C * (s + (DescribedNetwork.encDescribed encT G.2).length + 1) ^ C + +variable (encT entry) in +/-- **The contraction interface for entry procedures** (Theorem D.1 with `ℓ = 1`, entries in +`A_P`). A native certificate maps `(P, fl, r, G)` to a coefficient list `core (P, fl, r, G)`. At +the modulus `fl = FastContraction.modulus m`, for `m` the number of edges of `G`, its value in +`A_P` is the contraction of the values of the entries, on every input. For all constants `C` and +`D` there is `K` such that on every network admissible at a size `s ≥ 2` with constant `C`, and +every precision `1 ≤ P ≤ D s`, at that modulus the certificate takes time at most +`K (n + 1) ^ K 2 ^ (K s / √⌊log₂ s⌋)` and space at most `K (n + 1) ^ K`, for `n` the encoded length +of the input. -/ +structure EntryContractionAlgorithm (Admissible : ℕ → ℕ → ℕ × DescribedNetwork T → Prop) where + /-- The output on an input `(P, fl, r, G)`. -/ + core : ℕ × List ℕ × ℕ × DescribedNetwork T → List ℕ + /-- Its native certificate. -/ + certificate : NativeCertificate core (EntryContraction.encInput encT) (encList encNat) + /-- **Correctness**: at the modulus of the number of edges, the value is the contraction. -/ + val_core : ∀ (P r : ℕ) (G : DescribedNetwork T), + val P (FastContraction.modulus G.numEdges) + (core (P, FastContraction.modulus G.numEdges, r, G)) = + G.contraction fun t bs => val P (FastContraction.modulus G.numEdges) (entry t bs) + /-- Its time and space on admissible inputs at the modulus of the number of edges. -/ + bound : ∀ C D : ℕ, ∃ K : ℕ, ∀ (s P r : ℕ) (G : DescribedNetwork T), 2 ≤ s → 1 ≤ P → + P ≤ D * s → Admissible C s (r, G) → + certificate.time (P, FastContraction.modulus G.numEdges, r, G) ≤ + K * ((EntryContraction.encInput encT + (P, FastContraction.modulus G.numEdges, r, G)).length + 1) ^ K * + 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) ∧ + certificate.space (P, FastContraction.modulus G.numEdges, r, G) ≤ + K * ((EntryContraction.encInput encT + (P, FastContraction.modulus G.numEdges, r, G)).length + 1) ^ K + +/-! ### Direct summation -/ + +namespace EntryContraction + +/-- The input of direct summation, `((P, fl), G)`, from `(P, fl, r, G)`. -/ +theorem sumInput_polyTime : + ComputableInPolyTime + (fun ((P, fl, _, G) : ℕ × List ℕ × ℕ × DescribedNetwork T) => ((P, fl), G)) (encInput encT) + (DescribedNetwork.encInput (encPair encUnary (encList encNat)) encT) := + ((ComputableInPolyTime.fst _ _).prod + ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _))).prod + ((ComputableInPolyTime.snd _ _).comp ((ComputableInPolyTime.snd _ _).comp + (ComputableInPolyTime.snd _ _))) + +variable (entry) in +/-- **Direct summation with an entry procedure**: on `(P, fl, r, G)`, the sum over all edge +assignments of the products of the entries, with the operations of `A_P` at the modulus `fl`. -/ +@[expose] noncomputable def directCore + (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)) : + NativeCertificate + (fun ((P, fl, _, G) : ℕ × List ℕ × ℕ × DescribedNetwork T) => + DescribedNetwork.sumValue SumOps.galois entry (P, fl) G) + (encInput encT) (encList encNat) := + ((DescribedNetwork.contractionCertificate entry SumOps.galois_polyTime ce).comp + (NativeCertificate.ofPolyTime sumInput_polyTime)).congr fun _ => rfl + +/-- **Direct summation is correct**: at every modulus, the value is the contraction. -/ +theorem val_directCore (P : ℕ) (fl : List ℕ) (G : DescribedNetwork T) : + val P fl (DescribedNetwork.sumValue SumOps.galois entry (P, fl) G) = + G.contraction fun t bs => val P fl (entry t bs) := + DescribedNetwork.val_sumValue_galois entry (P, fl) G + +/-- The time of direct summation: the input of the sum, then the sum. -/ +theorem directCore_time + (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)) (P : ℕ) (fl : List ℕ) (r : ℕ) (G : DescribedNetwork T) : + (directCore entry ce).time (P, fl, r, G) = + (NativeCertificate.ofPolyTime (sumInput_polyTime (encT := encT))).time (P, fl, r, G) + + (DescribedNetwork.contractionCertificate entry SumOps.galois_polyTime ce).time + ((P, fl), G) := rfl + +/-- The space of direct summation. -/ +theorem directCore_space + (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)) (P : ℕ) (fl : List ℕ) (r : ℕ) (G : DescribedNetwork T) : + (directCore entry ce).space (P, fl, r, G) = + (NativeCertificate.ofPolyTime (sumInput_polyTime (encT := encT))).space (P, fl, r, G) + + (DescribedNetwork.contractionCertificate entry SumOps.galois_polyTime ce).space + ((P, fl), G) := rfl + +/-- The precision, the modulus and the input of the sum against the encoded input. -/ +private theorem lengths_le (P : ℕ) (fl : List ℕ) (r : ℕ) (G : DescribedNetwork T) : + P + fl.length ≤ (encInput encT (P, fl, r, G)).length ∧ + (DescribedNetwork.encInput (encPair encUnary (encList encNat)) encT + ((P, fl), G)).length ≤ 2 * (encInput encT (P, fl, r, G)).length := by + have h := length_le_length_encList encNat fl + simp only [encInput, DescribedNetwork.encInput, length_encPair, encUnary_apply, + List.length_replicate] at h ⊢ + omega + +private theorem mul_pow_le {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 resources of direct summation with an entry procedure.** There is `K` such that on an +input `(P, fl, r, G)` of encoded length `n`, with `m` edges and `k` vertices in `G`, if the entry +procedure takes time at most `E` and space at most `ES` on every vertex and bits on its ports, +then direct summation takes time at most `(2 ^ m (k + 1) + 1) (K (n + ES + 1) ^ K + 2 E)` and +space at most `K (n + ES + 1) ^ K + ES`. -/ +theorem directCore_le + (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)) : + ∃ K : ℕ, ∀ (P : ℕ) (fl : List ℕ) (r : ℕ) (G : DescribedNetwork T) (E ES : ℕ), + (∀ v ∈ G.vertices, ∀ bs : List Bool, bs.length = v.1.length → + ce.time (v.2, bs) ≤ E ∧ ce.space (v.2, bs) ≤ ES) → + (directCore entry ce).time (P, fl, r, G) ≤ + (2 ^ G.numEdges * (G.vertices.length + 1) + 1) * + (K * ((encInput encT (P, fl, r, G)).length + ES + 1) ^ K + 2 * E) ∧ + (directCore entry ce).space (P, fl, r, G) ≤ + K * ((encInput encT (P, fl, r, G)).length + ES + 1) ^ K + ES := by + obtain ⟨K₁, hK₁⟩ := DescribedNetwork.contractionCertificate_le (ops := SumOps.galois) + (eval := entry) (encQ := encPair encUnary (encList encNat)) (encY := encList encNat) + (encT := encT) SumOps.galois_polyTime ce + obtain ⟨c, -, hout⟩ := ce.computes + have hI := NativeCertificate.ofPolyTime_isPolynomial (sumInput_polyTime (encT := encT)) + obtain ⟨ct, dt, hit⟩ := hI.1.exists_le + obtain ⟨cs, ds, his⟩ := hI.2.exists_le + obtain ⟨c₁, hc₁⟩ : ∃ c₁, c₁ = K₁ * (c + 6) ^ K₁ := ⟨_, rfl⟩ + refine ⟨ct + cs + c₁ + dt + ds + 2 * K₁, fun P fl r G E ES hE => ?_⟩ + obtain ⟨n, hn⟩ : ∃ n, n = (encInput encT (P, fl, r, G)).length := ⟨_, rfl⟩ + obtain ⟨W, hW⟩ : ∃ W, W = n + ES + 1 := ⟨_, rfl⟩ + rw [← hn, show n + ES + 1 = W from hW.symm] + have hW1 : 1 ≤ W := by omega + obtain ⟨hPfl, hproj⟩ := lengths_le P fl r G + rw [← hn] at hPfl hproj + have hRv : ∀ y, SumOps.galois.Reduced (P, fl) y → + (encList encNat y).length ≤ n * (2 * n + 3) := fun y hy => + (SumOps.length_encList_le_of_galois_reduced hy).trans (Nat.mul_le_mul (by simp only; omega) + (by simp only; omega)) + have hEv : ∀ v ∈ G.vertices, ∀ bs : List Bool, + bs.length = v.1.length → ce.time (v.2, bs) ≤ E ∧ ce.space (v.2, bs) ≤ ES ∧ + (encList encNat (entry v.2 bs)).length ≤ c * (ES + 1) := fun v hv bs hbs => + ⟨(hE v hv bs hbs).1, (hE v hv bs hbs).2, + (hout (v.2, bs)).trans (Nat.mul_le_mul_left _ (by have := (hE v hv bs hbs).2; omega))⟩ + obtain ⟨hT, hS⟩ := hK₁ ((P, fl), G) E ES (c * (ES + 1)) (n * (2 * n + 3)) hEv hRv + -- The argument of direct summation's polynomial against `W ^ 2`. + have hA : (DescribedNetwork.encInput (encPair encUnary (encList encNat)) encT + ((P, fl), G)).length + c * (ES + 1) + n * (2 * n + 3) + 1 ≤ (c + 6) * W ^ 2 := by + have h1 : c * (ES + 1) ≤ c * W := Nat.mul_le_mul_left _ (by omega) + have h2 : c * W ≤ c * W ^ 2 := Nat.mul_le_mul_left _ (by nlinarith) + have h3 : n * (2 * n + 3) + 2 * n + 1 ≤ 6 * W ^ 2 := by nlinarith + nlinarith + have hpoly : K₁ * ((DescribedNetwork.encInput (encPair encUnary (encList encNat)) encT + ((P, fl), G)).length + c * (ES + 1) + n * (2 * n + 3) + 1) ^ K₁ ≤ + c₁ * W ^ (2 * K₁) := by + rw [hc₁, pow_mul, Nat.mul_assoc, ← Nat.mul_pow] + exact Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hA _) + have hnW : n + 1 ≤ W := by omega + have hit' : (NativeCertificate.ofPolyTime (sumInput_polyTime (encT := encT))).time + (P, fl, r, G) ≤ ct * W ^ dt := by + have h := hit (P, fl, r, G) + rw [← hn] at h + exact h.trans (Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hnW _)) + have his' : (NativeCertificate.ofPolyTime (sumInput_polyTime (encT := encT))).space + (P, fl, r, G) ≤ cs * W ^ ds := by + have h := his (P, fl, r, G) + rw [← hn] at h + exact h.trans (Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hnW _)) + obtain ⟨K, hK⟩ : ∃ K, K = ct + cs + c₁ + dt + ds + 2 * K₁ := ⟨_, rfl⟩ + rw [← hK] + have hct : ct * W ^ dt ≤ ct * W ^ K := mul_pow_le hW1 (by omega) + have hcs : cs * W ^ ds ≤ cs * W ^ K := mul_pow_le hW1 (by omega) + have hc1 : c₁ * W ^ (2 * K₁) ≤ c₁ * W ^ K := mul_pow_le hW1 (by omega) + have hsum : ct * W ^ K + cs * W ^ K + c₁ * W ^ K ≤ K * W ^ K := by + rw [← Nat.add_mul, ← Nat.add_mul]; exact Nat.mul_le_mul_right _ (by omega) + have hP1 : 1 ≤ 2 ^ G.numEdges * (G.vertices.length + 1) + 1 := by omega + constructor + · rw [directCore_time] + calc _ ≤ ct * W ^ dt + (2 ^ G.numEdges * (G.vertices.length + 1) + 1) * + (c₁ * W ^ (2 * K₁) + 2 * E) := + Nat.add_le_add hit' (hT.trans (Nat.mul_le_mul_left _ (Nat.add_le_add_right hpoly _))) + _ ≤ (2 ^ G.numEdges * (G.vertices.length + 1) + 1) * + (ct * W ^ K + (c₁ * W ^ K + 2 * E)) := by + rw [Nat.mul_add _ (ct * W ^ K)] + refine Nat.add_le_add ((hct.trans (Nat.le_mul_of_pos_left _ hP1))) ?_ + exact Nat.mul_le_mul_left _ (by omega) + _ ≤ _ := Nat.mul_le_mul_left _ (by omega) + · rw [directCore_space] + calc _ ≤ cs * W ^ ds + (c₁ * W ^ (2 * K₁) + ES) := + Nat.add_le_add his' (hS.trans (Nat.add_le_add_right hpoly _)) + _ ≤ _ := by omega + +/-- **Direct summation on admissible inputs** takes time `K (n + 1) ^ K 2 ^ (K s)` and space +`K (n + 1) ^ K`, at the modulus of the number of edges, for `K` depending only on the constants: +the fallback of the contraction algorithm for small sizes. -/ +theorem exists_directCore_le + (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)) (C : ℕ) : + ∃ K : ℕ, ∀ (s P r : ℕ) (G : DescribedNetwork T), EntryAdmissible ce C s (r, G) → + (directCore entry ce).time (P, FastContraction.modulus G.numEdges, r, G) ≤ + K * ((encInput encT (P, FastContraction.modulus G.numEdges, r, G)).length + 1) ^ K * + 2 ^ (K * s) ∧ + (directCore entry ce).space (P, FastContraction.modulus G.numEdges, r, G) ≤ + K * ((encInput encT (P, FastContraction.modulus G.numEdges, r, G)).length + 1) ^ K := by + obtain ⟨K₀, hK₀⟩ := directCore_le (entry := entry) ce + obtain ⟨c₀, hc₀⟩ : ∃ c₀, c₀ = C * 3 ^ C + 1 := ⟨_, rfl⟩ + obtain ⟨K, hK⟩ : ∃ K, K = 4 * (K₀ * (c₀ + 1) ^ K₀ + c₀ + 1) * 2 + K₀ * (C + 1) + C + 3 := + ⟨_, rfl⟩ + refine ⟨K, fun s P r G hA => ?_⟩ + obtain ⟨-, hsm, hmC, -, hent⟩ := hA + simp only at hsm hmC hent + obtain ⟨n, hn⟩ : ∃ n, n = (encInput encT (P, FastContraction.modulus G.numEdges, r, G)).length := + ⟨_, rfl⟩ + rw [← hn] + -- The size, the network and the vertices against `n`. + have hG : (DescribedNetwork.encDescribed encT G).length ≤ n := by + rw [hn]; simp only [encInput, length_encPair]; omega + have hmk := DescribedNetwork.length_numEdges_vertices_le (encT := encT) G + have hsn : s ≤ n := by omega + have hB : s + (DescribedNetwork.encDescribed encT G).length + 1 ≤ 3 * (n + 1) := by omega + -- The entry bounds. + obtain ⟨E, hE⟩ : ∃ E, E = c₀ * (n + 1) ^ C * 2 ^ (C * s) := ⟨_, rfl⟩ + obtain ⟨ES, hES⟩ : ∃ ES, ES = c₀ * (n + 1) ^ C := ⟨_, rfl⟩ + have hpowB : C * (s + (DescribedNetwork.encDescribed encT G).length + 1) ^ C ≤ ES := by + rw [hES] + calc C * (s + (DescribedNetwork.encDescribed encT G).length + 1) ^ C + ≤ C * (3 * (n + 1)) ^ C := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hB _) + _ = C * 3 ^ C * (n + 1) ^ C := by rw [Nat.mul_pow, Nat.mul_assoc] + _ ≤ c₀ * (n + 1) ^ C := Nat.mul_le_mul_right _ (by omega) + have hbnd : ∀ v ∈ G.vertices, ∀ bs : List Bool, bs.length = v.1.length → + ce.time (v.2, bs) ≤ E ∧ ce.space (v.2, bs) ≤ ES := by + intro v hv bs hbs + obtain ⟨ht, hs⟩ := hent v hv bs hbs + refine ⟨ht.trans ?_, hs.trans hpowB⟩ + rw [hE, show c₀ * (n + 1) ^ C * 2 ^ (C * s) = (c₀ * (n + 1) ^ C) * 2 ^ (C * s) from rfl] + exact Nat.mul_le_mul (hES ▸ hpowB) (Nat.pow_le_pow_right (by norm_num) + (Nat.mul_le_mul_left _ (ceilNineTenths_le_self s))) + obtain ⟨hT, hS⟩ := hK₀ P (FastContraction.modulus G.numEdges) r G E ES hbnd + rw [← hn] at hT hS + -- Arithmetic. + have hn1 : 1 ≤ n + 1 := by omega + have hWES : n + ES + 1 ≤ (c₀ + 1) * (n + 1) ^ (C + 1) := by + have h1 : n + 1 ≤ (n + 1) ^ (C + 1) := by + calc n + 1 = (n + 1) ^ 1 := (pow_one _).symm + _ ≤ (n + 1) ^ (C + 1) := Nat.pow_le_pow_right hn1 (by omega) + have h2 : ES ≤ c₀ * (n + 1) ^ (C + 1) := by + rw [hES]; exact Nat.mul_le_mul_left _ (Nat.pow_le_pow_right hn1 (by omega)) + rw [Nat.add_mul, one_mul]; omega + obtain ⟨A₀, hA₀⟩ : ∃ A₀, A₀ = K₀ * (c₀ + 1) ^ K₀ := ⟨_, rfl⟩ + obtain ⟨X, hX⟩ : ∃ X, X = n + 1 := ⟨_, rfl⟩ + obtain ⟨Y, hY⟩ : ∃ Y, Y = 2 ^ (C * s) := ⟨_, rfl⟩ + obtain ⟨e, he⟩ : ∃ e, e = (C + 1) * K₀ + C := ⟨_, rfl⟩ + rw [← hX] at hn1 hWES hE hES ⊢ + rw [← hY] at hE + have hX1 : 1 ≤ X := hn1 + have hY1 : 1 ≤ Y := hY ▸ Nat.one_le_two_pow + have hpoly : K₀ * (n + ES + 1) ^ K₀ ≤ A₀ * X ^ ((C + 1) * K₀) := by + rw [hA₀, pow_mul, Nat.mul_assoc, ← Nat.mul_pow] + exact Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hWES _) + have hXe1 : X ^ ((C + 1) * K₀) ≤ X ^ e := Nat.pow_le_pow_right hX1 (by omega) + have hXe2 : X ^ C ≤ X ^ e := Nat.pow_le_pow_right hX1 (by omega) + -- The number of assignments and vertices. + have hk : G.vertices.length + 1 ≤ X := by omega + have hm : 2 ^ G.numEdges ≤ Y := hY ▸ Nat.pow_le_pow_right (by norm_num) hmC + have hcount : 2 ^ G.numEdges * (G.vertices.length + 1) + 1 ≤ 2 * (Y * X) := by + have := Nat.mul_le_mul hm hk + have : 1 ≤ Y * X := Nat.one_le_iff_ne_zero.mpr (by positivity) + omega + have hinner : K₀ * (n + ES + 1) ^ K₀ + 2 * E ≤ (A₀ + 2 * c₀) * X ^ e * Y := by + have h1 : A₀ * X ^ ((C + 1) * K₀) ≤ A₀ * X ^ e * Y := + (Nat.mul_le_mul_left _ hXe1).trans (Nat.le_mul_of_pos_right _ hY1) + have h2 : 2 * E ≤ 2 * c₀ * X ^ e * Y := by + rw [hE, Nat.mul_assoc 2 c₀, Nat.mul_assoc, Nat.mul_assoc, Nat.mul_assoc] + exact Nat.mul_le_mul_left _ (Nat.mul_le_mul_left _ (Nat.mul_le_mul_right _ hXe2)) + have e3 : (A₀ + 2 * c₀) * X ^ e * Y = A₀ * X ^ e * Y + 2 * c₀ * X ^ e * Y := by ring + omega + have hCc : C ≤ c₀ := by + have : C ≤ C * 3 ^ C := Nat.le_mul_of_pos_right _ (by positivity) + omega + have hKc : 2 * (A₀ + 2 * c₀) ≤ K := by rw [hK, ← hA₀]; omega + have hKe : e + 1 ≤ K := by + have : (C + 1) * K₀ = K₀ * (C + 1) := Nat.mul_comm _ _ + rw [hK, he]; omega + have hKY : Y * Y ≤ 2 ^ (K * s) := by + have h2C : 2 * C ≤ K := by rw [hK]; omega + rw [hY, ← pow_add] + refine Nat.pow_le_pow_right (by norm_num) ?_ + calc C * s + C * s = 2 * C * s := by ring + _ ≤ K * s := Nat.mul_le_mul_right _ h2C + constructor + · calc _ ≤ 2 * (Y * X) * ((A₀ + 2 * c₀) * X ^ e * Y) := hT.trans (Nat.mul_le_mul hcount hinner) + _ = 2 * (A₀ + 2 * c₀) * X ^ (e + 1) * (Y * Y) := by rw [pow_succ]; ring + _ ≤ K * X ^ K * 2 ^ (K * s) := + Nat.mul_le_mul (Nat.mul_le_mul hKc (Nat.pow_le_pow_right hX1 hKe)) hKY + · have h1 : ES ≤ c₀ * X ^ e := hES ▸ Nat.mul_le_mul_left _ hXe2 + calc _ ≤ A₀ * X ^ e + c₀ * X ^ e := + hS.trans (Nat.add_le_add (hpoly.trans (Nat.mul_le_mul_left _ hXe1)) h1) + _ = (A₀ + c₀) * X ^ e := by ring + _ ≤ K * X ^ K := Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right hX1 (by omega)) + +/-! ### Polynomial-time entry procedures and tables -/ + +/-- **Polynomial-time entry procedures meet the entry bounds.** For a polynomial certificate of the +entry procedure there is `C₀` such that, for every `C ≥ C₀`, a rows-first network with between +`s` and `C s` edges and degree at most `⌈s ^ (9/10)⌉` is admissible at size `s` with constant +`C`. -/ +theorem exists_entryAdmissible_of_isPolynomial + {ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)} (hce : ce.IsPolynomial) : + ∃ C₀ : ℕ, ∀ (C s r : ℕ) (G : DescribedNetwork T), C₀ ≤ C → G.IsRowsFirstBipartite r → + s ≤ G.numEdges → G.numEdges ≤ C * s → (∀ v ∈ G.vertices, v.1.length ≤ ceilNineTenths s) → + EntryAdmissible ce C s (r, G) := by + obtain ⟨ct, dt, ht⟩ := hce.1.exists_le + obtain ⟨cs, ds, hs⟩ := hce.2.exists_le + refine ⟨ct * 3 ^ dt + cs * 3 ^ ds + dt + ds + 1, fun C s r G hC hrows hsm hmC hdeg => + ⟨hrows, hsm, hmC, hdeg, fun v hv bs hbs => ?_⟩⟩ + change v ∈ G.vertices at hv + obtain ⟨B, hB⟩ : ∃ B, B = s + (DescribedNetwork.encDescribed encT G).length + 1 := ⟨_, rfl⟩ + rw [← hB] + have hB1 : 1 ≤ B := by omega + -- The argument of the procedure is at most `3 B`. + have hq : (encPair encT encBits (v.2, bs)).length + 1 ≤ 3 * B := by + have h1 := length_le_encList_of_mem (encPair (encList encNat) encT) hv + have h2 : (encList (encPair (encList encNat) encT) G.vertices).length ≤ + (DescribedNetwork.encDescribed encT G).length := by + change _ ≤ (encPair encUnary (encList (encPair (encList encNat) encT)) + (G.numEdges, G.vertices)).length + rw [length_encPair] + dsimp only + omega + have h3 := length_le_length_encList encNat v.1 + rw [length_encPair] at h1 ⊢ + change 2 * (encT v.2).length + 1 + bs.length + 1 ≤ 3 * B + omega + have hpow {c d : ℕ} : c * ((encPair encT encBits (v.2, bs)).length + 1) ^ d ≤ + c * 3 ^ d * B ^ d := by + rw [Nat.mul_assoc, ← Nat.mul_pow] + exact Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hq _) + have hBC {c d : ℕ} (hc : c ≤ C) (hd : d ≤ C) : c * B ^ d ≤ C * B ^ C := + Nat.mul_le_mul hc (Nat.pow_le_pow_right hB1 hd) + refine ⟨(ht _).trans (hpow.trans ((hBC (by omega) (by omega)).trans + (Nat.le_mul_of_pos_right _ Nat.one_le_two_pow))), (hs _).trans (hpow.trans + (hBC (by omega) (by omega)))⟩ + +/-- **Direct summation of a table network is its contraction**, in `A_P` at every modulus. -/ +theorem val_directCore_tableEntry (P : ℕ) (fl : List ℕ) (G : ExplicitTensorNetwork ℕ) : + val P fl (DescribedNetwork.sumValue SumOps.galois tableEntry (P, fl) G) = + (G.contraction : GaloisRingArith.Ring P fl) := by + rw [val_directCore, ← DescribedNetwork.contraction_entry] + have h := DescribedNetwork.map_contraction (Nat.castRingHom (GaloisRingArith.Ring P fl)) + ExplicitTensorNetwork.entry G + simp only [Nat.coe_castRingHom] at h + rw [h] + congr 1 + funext t bs + exact VertexDesc.val_entry_inl P fl t bs + +end EntryContraction + +end Cslib.Circuits.Frontier diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/EntryContractionMachine.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/EntryContractionMachine.lean new file mode 100644 index 000000000..c23f6e016 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/EntryContractionMachine.lean @@ -0,0 +1,355 @@ +/- +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.EntryContraction +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionPolyTime +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionLeaf +import Complexity.Computability.Circuit.Frontier.TensorNetwork.RowsFirstPolyTime +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.SqrtLog +import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeNatFrontends +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimePrimitives + +/-! +# The native machine of the contraction with entry procedures + +The machine behind the instance of the contraction interface for entry procedures +(`Cslib.Circuits.Frontier.EntryContractionAlgorithm`, milestone E1.3 of #1538): the recursion of +Theorem D.1 of [OpenAI2026ETH] (`FastContraction.scheme` with the native child builder) run from +a root call whose descriptors are the vertex descriptors of the input network, read by the entry +procedure, with direct summation as the fallback. + +**The input** `(P, fl, r, G)` has the precision `P` in unary (`EntryContraction.encInput`), so the +precision is not capped: the cap at the encoded length of the network that the explicit machine +uses (`ExplicitTensorNetwork.capPrecision`) keeps the residue only for tables of natural numbers. + +**The guard** (`EntryContraction.guard`) checks that `fl` is the modulus `FastContraction.modulus m` +of the number `m` of edges, that the network is rows-first bipartite, and that every vertex has at +most `degreeBound m` ports. It is polynomial-time (`EntryContraction.guard_polyTime`), with the +rows-first test `DescribedNetwork.rowsFirst_polyTime`, and every admissible input at the modulus +passes it (`EntryContraction.guard_of_entryAdmissible`), since +`⌈s ^ (9/10)⌉ ≤ degreeBound s ≤ degreeBound m` (`ContractionSchedule.degreeBound_mono`). + +**The root and the clock.** The root call (`EntryContraction.rootCall`) has scale `m`, depth `0`, +edge bound `m + 1`, precision `P`, modulus `fl`, `r` rows and the network +`FastContraction.rootNet G`. The clock (`EntryContraction.clock`) is +`2 ^ (K₀ (m + P) / √⌊log₂ (m + P)⌋)`, as for explicit networks. On guarded inputs the root is +well-formed (`EntryContraction.wf_rootCall`), and it has no packets +(`EntryContraction.packetShape_rootCall`). + +**The result** (`EntryContraction.coreValue`): on guarded inputs, the coefficient list of a value +tagged `0` returned by the clocked run, and direct summation otherwise. It is correct at the modulus +of the number of edges for every fuel (`EntryContraction.val_coreValue`), from the correctness of +the recursion (`FastContraction.val_value`) and the root (`FastContraction.contraction_rootNet`). +Its native certificate is `EntryContraction.fastCore`; its resources are analyzed in +`Cslib.Complexity.CountingSimulation.EntryAnalysis`. + +## Main definitions + +* `Cslib.Circuits.Frontier.EntryContraction.guard`: the guard. +* `Cslib.Circuits.Frontier.EntryContraction.rootCall`, `EntryContraction.clock`: the root call and + the clock. +* `Cslib.Circuits.Frontier.EntryContraction.coreValue`: the result of the machine. +* `Cslib.Circuits.Frontier.EntryContraction.runCore`, `EntryContraction.fastCore`: the clocked run + and the machine. + +## Main results + +* `Cslib.Circuits.Frontier.FastContraction.contraction_rootNet`: the root network computes the + contraction of the network, for every entry procedure. +* `Cslib.Circuits.Frontier.EntryContraction.guard_polyTime`: the guard is polynomial-time. +* `Cslib.Circuits.Frontier.EntryContraction.guard_of_entryAdmissible`: admissible inputs pass it. +* `Cslib.Circuits.Frontier.EntryContraction.wf_rootCall`: guarded roots are well-formed. +* `Cslib.Circuits.Frontier.EntryContraction.packetShape_rootCall`: the root has no packets. +* `Cslib.Circuits.Frontier.EntryContraction.val_coreValue`: the machine is correct. + +## 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.Circuits.Frontier + +open GaloisRingArith Cslib.GenericRAM Cslib.GenericRAM.StackRecursion Turing.MultiTapeTM + ContractionSchedule + +variable {T : Type} + +/-! ### The root network -/ + +/-- **The root network computes the contraction**, for every entry procedure `ev` and every map +`f` of its outputs to a commutative semiring: reading the root descriptors through +`VertexDesc.entry ev` is reading the descriptors of `G` through `ev`. -/ +theorem FastContraction.contraction_rootNet {R : Type*} [CommSemiring R] (f : List ℕ → R) + (ev : T → List Bool → List ℕ) (G : DescribedNetwork T) : + (FastContraction.rootNet G).contraction (fun d bs => f (VertexDesc.entry ev d bs)) = + G.contraction fun t bs => f (ev t bs) := by + simp only [DescribedNetwork.contraction, FastContraction.rootNet, List.map_map] + rfl + +namespace EntryContraction + +open FastContraction (Call scheme nativeMk value rootNet modulus fuelConst encCall encValue + leafCertificate irreducible_modulus) + +variable {encT : T ↪ List Bool} {entry : T → List Bool → List ℕ} + +/-! ### The guard -/ + +/-- **The guard** on an input `(P, fl, r, G)`: `fl` is the modulus of the number `m` of edges of +`G`, `G` is rows-first bipartite at `r` rows, and every vertex has at most `degreeBound m` +ports. -/ +@[expose] def guard : ℕ × List ℕ × ℕ × DescribedNetwork T → Bool + | (_, fl, r, G) => decide (fl = modulus G.numEdges ∧ G.IsRowsFirstBipartite r ∧ + ∀ v ∈ G.vertices, v.1.length ≤ degreeBound G.numEdges) + +/-- The network of an input, from `(P, fl, r, G)`. -/ +private theorem network_polyTime : + ComputableInPolyTime (fun ((_, _, _, G) : ℕ × List ℕ × ℕ × DescribedNetwork T) => G) + (encInput encT) (DescribedNetwork.encDescribed encT) := + (ComputableInPolyTime.snd _ _).comp + ((ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.snd _ _)) + +/-- The number of edges of an input, in unary. -/ +private theorem numEdges_polyTime : + ComputableInPolyTime (fun ((_, _, _, G) : ℕ × List ℕ × ℕ × DescribedNetwork T) => G.numEdges) + (encInput encT) encUnary := + DescribedNetwork.numEdges_polyTime.comp network_polyTime + +/-- The network of an input with its number of rows, from `(P, fl, r, G)`. -/ +private theorem rowsNet_polyTime : + ComputableInPolyTime (fun ((_, _, r, G) : ℕ × List ℕ × ℕ × DescribedNetwork T) => (r, G)) + (encInput encT) (encPair encNat (DescribedNetwork.encDescribed encT)) := + (ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.snd _ _) + +/-- **The guard is polynomial-time.** -/ +theorem guard_polyTime : ComputableInPolyTime (guard (T := T)) (encInput encT) encBool := by + have hm := numEdges_polyTime (encT := encT) + have hfl : ComputableInPolyTime (fun ((_, fl, _, G) : ℕ × List ℕ × ℕ × DescribedNetwork T) => + decide (fl = modulus G.numEdges)) (encInput encT) encBool := + ComputableInPolyTime.decide_eq' ((ComputableInPolyTime.fst _ _).comp + (ComputableInPolyTime.snd _ _)) (FastContraction.modulus_polyTime.comp hm) + have hrows := (DescribedNetwork.rowsFirst_polyTime (encT := encT)).comp rowsNet_polyTime + have hvs := (DescribedNetwork.vertices_polyTime (encT := encT)).comp network_polyTime + have hdeg : ComputableInPolyTime (fun ((_, _, _, G) : ℕ × List ℕ × ℕ × DescribedNetwork T) => + G.vertices.all (fun v => decide (v.1.length ≤ degreeBound G.numEdges))) + (encInput encT) encBool := by + refine ComputableInPolyTime.allWithInput hvs ?_ + exact ComputableInPolyTime.binary_le' + (ComputableInPolyTime.unary_to_binary.comp ((ComputableInPolyTime.length_list _).comp + ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _)))) + (degreeBound_polyTime.comp (hm.comp (ComputableInPolyTime.fst _ _))) + refine (ComputableInPolyTime.bool_and.comp (hfl.prod (ComputableInPolyTime.bool_and.comp + (hrows.prod hdeg)))).of_enc_eq fun ⟨P, fl, r, G⟩ => ?_ + simp only [guard, Function.comp_apply, Bool.decide_and, List.all_eq, decide_eq_true_eq] + +/-- **Admissible inputs pass the guard** at the modulus of the number of edges: their degree is at +most `⌈s ^ (9/10)⌉ ≤ degreeBound s ≤ degreeBound m`, for `s ≤ m`. -/ +theorem guard_of_entryAdmissible + {ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)} {C s P r : ℕ} {G : DescribedNetwork T} + (hA : EntryAdmissible ce C s (r, G)) : guard (P, modulus G.numEdges, r, G) = true := by + obtain ⟨hrows, hsm, -, hdeg, -⟩ := hA + simp only [guard, decide_eq_true_eq, true_and] + exact ⟨hrows, fun v hv => + (hdeg v hv).trans ((ceilNineTenths_le_degreeBound s).trans (degreeBound_mono hsm))⟩ + +/-! ### The root and the clock -/ + +/-- **The root call** of an input `(P, fl, r, G)`: scale `m`, depth `0`, edge bound `m + 1`, +precision `P`, modulus `fl`, `r` rows and the descriptors of `G`. -/ +@[expose] def rootCall : ℕ × List ℕ × ℕ × DescribedNetwork T → Call T + | (P, fl, r, G) => ((G.numEdges, 0, G.numEdges + 1, P, fl, r), rootNet G) + +/-- **The clock** of an input `(P, fl, r, G)`: `2 ^ (K₀ (m + P) / √⌊log₂ (m + P)⌋)`. -/ +@[expose] def clock : ℕ × List ℕ × ℕ × DescribedNetwork T → ℕ + | (P, _, _, G) => 2 ^ (fuelConst * (G.numEdges + P) / Nat.sqrt (Nat.log 2 (G.numEdges + P))) + +/-- **The root call is polynomial-time.** -/ +theorem rootCall_polyTime : + ComputableInPolyTime (rootCall (T := T)) (encInput encT) (encCall encT) := by + have hm := numEdges_polyTime (encT := encT) + have hP := ComputableInPolyTime.fst encUnary + (encPair (encList encNat) (encPair encNat (DescribedNetwork.encDescribed encT))) + have hfl := (ComputableInPolyTime.fst (encList encNat) + (encPair encNat (DescribedNetwork.encDescribed encT))).comp + (ComputableInPolyTime.snd encUnary _) + have hr := (ComputableInPolyTime.fst encNat (DescribedNetwork.encDescribed encT)).comp + rowsNet_polyTime + exact (hm.prod ((ComputableInPolyTime.const 0).prod + ((ComputableInPolyTime.unary_add' hm (ComputableInPolyTime.const 1)).prod + (hP.prod (hfl.prod hr))))).prod + ((FastContraction.rootNet_polyTime encT).comp network_polyTime) + +/-- **The clock is polynomial-time.** -/ +theorem clock_polyTime : ComputableInPolyTime (clock (T := T)) (encInput encT) encNat := + (ComputableInPolyTime.unary_two_pow_div_sqrt_log_two fuelConst).comp + (ComputableInPolyTime.unary_add' numEdges_polyTime (ComputableInPolyTime.fst _ _)) + +/-- **Guarded roots are well-formed**: the modulus is irreducible modulo `2`, and the descriptors +of `G` keep its rows-first ports. -/ +theorem wf_rootCall {x : ℕ × List ℕ × ℕ × DescribedNetwork T} (hg : guard x = true) : + FastContraction.WF (rootCall x) := by + obtain ⟨P, fl, r, G⟩ := x + simp only [guard, decide_eq_true_eq] at hg + obtain ⟨hfl, ⟨h1, h2⟩, -⟩ := hg + refine ⟨?_, fun v hv i hi => ?_, fun i hi => ?_⟩ + · change Irreducible ((monicOf fl).map (Int.castRingHom (ZMod 2))) + rw [hfl] + exact irreducible_modulus _ + · simp only [rootCall, rootNet, List.mem_map] at hv + obtain ⟨w, hw, rfl⟩ := hv + exact h1 w hw i hi + · simp only [rootCall, rootNet, ← List.map_take, ← List.map_drop, List.map_map, + Function.comp_def] at hi ⊢ + exact h2 i hi + +/-- **The root call has no packets**: its descriptors are those of the input network. -/ +theorem packetShape_rootCall (x : ℕ × List ℕ × ℕ × DescribedNetwork T) : + FastContraction.PacketShape (rootCall x) := by + obtain ⟨P, fl, r, G⟩ := x + exact FastContraction.packetShape_of_net_eq_rootNet rfl + +/-! ### The result -/ + +variable (entry) in +/-- **The result of the machine** on an input `(P, fl, r, G)`: on guarded inputs, the coefficient +list of a value tagged `0` returned by the clocked run from the root call, and direct summation +otherwise. -/ +noncomputable def coreValue : ℕ × List ℕ × ℕ × DescribedNetwork T → List ℕ + | x@(P, fl, _, G) => + if guard x then + ((scheme entry nativeMk).run clock rootCall x).elim + (DescribedNetwork.sumValue SumOps.galois entry (P, fl) G) + fun (tag, coeffs) => if tag = 0 then coeffs + else DescribedNetwork.sumValue SumOps.galois entry (P, fl) G + else DescribedNetwork.sumValue SumOps.galois entry (P, fl) G + +/-- **The machine is correct**: at the modulus of the number of edges, the value of the result is +the contraction of the values of the entries, on every input and for every fuel. A value tagged +`0` returned by the run is the root's value (`FastContraction.eq_value_of_run`), which is the +contraction on well-formed roots (`FastContraction.val_value`). -/ +theorem val_coreValue (P r : ℕ) (G : DescribedNetwork T) : + val P (modulus G.numEdges) (coreValue entry (P, modulus G.numEdges, r, G)) = + G.contraction fun t bs => val P (modulus G.numEdges) (entry t bs) := by + rw [coreValue] + split_ifs with hg + · rcases hrun : (scheme entry nativeMk).run clock rootCall (P, modulus G.numEdges, r, G) with + _ | ⟨d, y⟩ + · exact val_directCore _ _ _ + · simp only [Option.elim_some] + split_ifs with hd + · subst hd + have hy := FastContraction.eq_value_of_run entry nativeMk (fuel := clock) + (root := rootCall) rfl hrun + rw [hy] + exact (FastContraction.val_value entry nativeMk (FastContraction.stepCorrect_nativeMk entry) + FastContraction.wfChildren_nativeMk _ (wf_rootCall hg)).trans + (FastContraction.contraction_rootNet (val P (modulus G.numEdges)) entry G) + · exact val_directCore _ _ _ + · exact val_directCore _ _ _ + +/-! ### The machine -/ + +/-- Whether a returned value is tagged `0`. -/ +theorem valueTag_polyTime : + ComputableInPolyTime + (fun ((_, (tag, _)) : (ℕ × List ℕ × ℕ × DescribedNetwork T) × (ℕ × List ℕ)) => + decide (tag = 0)) (encPair (encInput encT) encValue) encBool := + ComputableInPolyTime.decide_eq' ((ComputableInPolyTime.fst encUnary (encList encNat)).comp + (ComputableInPolyTime.snd (encInput encT) encValue)) (ComputableInPolyTime.const 0) + +/-- The coefficient list of a returned value. -/ +theorem valueList_polyTime : + ComputableInPolyTime + (fun ((_, (_, coeffs)) : (ℕ × List ℕ × ℕ × DescribedNetwork T) × (ℕ × List ℕ)) => coeffs) + (encPair (encInput encT) encValue) (encList encNat) := + (ComputableInPolyTime.snd encUnary (encList encNat)).comp + (ComputableInPolyTime.snd (encInput encT) encValue) + +variable (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)) + +/-- **The clocked run** from the root call, as one native machine, with direct summation through +the entry procedure's certificate `ce` at the leaves. -/ +@[expose] noncomputable def runCore : + NativeCertificate ((scheme entry nativeMk).run clock rootCall) (encInput encT) + (encOption encValue) := + Scheme.certificate (FastContraction.scheme_nativeMk_polyTime entry) (leafCertificate ce nativeMk) + (NativeCertificate.ofPolyTime clock_polyTime) (NativeCertificate.ofPolyTime rootCall_polyTime) + +/-- **The machine**: branch on the guard; on guarded inputs run the recursion, and on a value +tagged `0` output its coefficient list; otherwise sum directly (`EntryContraction.directCore`). It +computes `coreValue`. -/ +@[expose] noncomputable def fastCore : + NativeCertificate (coreValue entry) (encInput encT) (encList encNat) := + (NativeCertificate.branch (NativeCertificate.ofPolyTime guard_polyTime) + (NativeCertificate.option (runCore ce) (directCore entry ce) + (NativeCertificate.branch (NativeCertificate.ofPolyTime valueTag_polyTime) + (NativeCertificate.ofPolyTime valueList_polyTime) + ((directCore entry ce).comp + (NativeCertificate.ofPolyTime (ComputableInPolyTime.fst (encInput encT) encValue))))) + (directCore entry ce)).congr fun ⟨P, fl, r, G⟩ => by + simp only [coreValue, Function.comp_apply] + split + · cases (scheme entry nativeMk).run clock rootCall (P, fl, r, G) with + | none => rfl + | some v => + obtain ⟨tag, coeffs⟩ := v + simp only [Option.elim_some, decide_eq_true_eq] + · rfl + +/-- The time of the machine, unfolded: the guard, and on guarded inputs the run twice, the input, +and the output or direct summation. -/ +theorem fastCore_time (x : ℕ × List ℕ × ℕ × DescribedNetwork T) : + (fastCore ce).time x = + (NativeCertificate.ofPolyTime (guard_polyTime (encT := encT))).time x + + if guard x = true then + 2 * (runCore ce).time x + (encInput encT x).length + + ((scheme entry nativeMk).run clock rootCall x).elim ((directCore entry ce).time x) + fun (tag, coeffs) => + (NativeCertificate.ofPolyTime (valueTag_polyTime (encT := encT))).time + (x, (tag, coeffs)) + + if decide (tag = 0) = true then + (NativeCertificate.ofPolyTime (valueList_polyTime (encT := encT))).time + (x, (tag, coeffs)) + else (NativeCertificate.ofPolyTime + (ComputableInPolyTime.fst (encInput encT) encValue)).time (x, (tag, coeffs)) + + (directCore entry ce).time x + else (directCore entry ce).time x := rfl + +/-- The space of the machine, unfolded. -/ +theorem fastCore_space (x : ℕ × List ℕ × ℕ × DescribedNetwork T) : + (fastCore ce).space x = + (NativeCertificate.ofPolyTime (guard_polyTime (encT := encT))).space x + + if guard x = true then + 2 * (runCore ce).space x + (encInput encT x).length + + ((scheme entry nativeMk).run clock rootCall x).elim ((directCore entry ce).space x) + fun (tag, coeffs) => + (NativeCertificate.ofPolyTime (valueTag_polyTime (encT := encT))).space + (x, (tag, coeffs)) + + if decide (tag = 0) = true then + (NativeCertificate.ofPolyTime (valueList_polyTime (encT := encT))).space + (x, (tag, coeffs)) + else (NativeCertificate.ofPolyTime + (ComputableInPolyTime.fst (encInput encT) encValue)).space (x, (tag, coeffs)) + + (directCore entry ce).space x + else (directCore entry ce).space x := rfl + +end EntryContraction + +end Cslib.Circuits.Frontier diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionLeaf.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionLeaf.lean index 4fba5a66f..fa8f9ecdb 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionLeaf.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionLeaf.lean @@ -47,7 +47,10 @@ the packet shape and at most `2 m` edges takes time `K (n + 1) ^ K 2 ^ (K s / `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. +but a polynomial in `n` is a constant (`FastContraction.exists_leafFactor_le`). With an entry +procedure whose roots cost time `E` and space `ES`, the leaf takes time +`K (n + ES + 1) ^ K 2 ^ (K s / √⌊log₂ s⌋) (E + 1)` and space `K (n + ES + 1) ^ K` +(`FastContraction.exists_leafCertificate_le_of_entry`). ## Main definitions @@ -62,8 +65,11 @@ but a polynomial in `n` is a constant. * `Cslib.Circuits.Frontier.FastContraction.leafCertificate_le_of_packetShape`, `Cslib.Circuits.Frontier.FastContraction.leafCertificate_tableEntry_le_of_packetShape`: the cost of a leaf with the packet shape, and over tables. -* `Cslib.Circuits.Frontier.FastContraction.exists_leafCertificate_le`: the leaf bound of the - resource analysis. +* `Cslib.Circuits.Frontier.FastContraction.exists_leafFactor_le`: the factor `2 ^ M (A p + 2) ^ A` + is subexponential. +* `Cslib.Circuits.Frontier.FastContraction.exists_leafCertificate_le`, + `Cslib.Circuits.Frontier.FastContraction.exists_leafCertificate_le_of_entry`: the leaf bound of + the resource analysis, over tables and with the costs of the root entries. ## References @@ -469,13 +475,20 @@ def PacketShape (x : Call T) : Prop := 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 +/-- **A call on a root network has no packets**: its descriptors are those of a network +`G`, by `rootNet G`. -/ +theorem packetShape_of_net_eq_rootNet {x : Call T} {G : DescribedNetwork T} + (h : x.net = rootNet G) : PacketShape x := by intro v hv d hd - simp only [root, rootNet, Call.net, List.mem_map] at hv + rw [h] at hv + simp only [rootNet, List.mem_map] at hv obtain ⟨w, -, rfl⟩ := hv cases hd +/-- **The root has no packets.** -/ +theorem packetShape_root (q : ℕ × ℕ × ExplicitTensorNetwork ℕ) : PacketShape (root q) := + packetShape_of_net_eq_rootNet rfl + /-- **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 @@ -757,78 +770,143 @@ theorem exists_packetFactor_le (C c : ℕ) : ∃ K : ℕ, ∀ s m p : ℕ, 2 ≤ _ ≤ 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 (List ℕ) → State → ℕ × DescribedNetwork (VertexDesc (List ℕ))) (s : ℕ) - (x : Call (List ℕ)), 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 tableEntryCertificate mk).time x ≤ - K * ((encCall (encList encNat) x).length + 1) ^ K * 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) ∧ - (leafCertificate tableEntryCertificate mk).space x ≤ - K * ((encCall (encList encNat) x).length + 1) ^ K := by - obtain ⟨K₀, hK₀⟩ := leafCertificate_tableEntry_le_of_packetShape +/-- **The leaf factor is subexponential.** For all constants `C`, `c` and `s₀` there is `K` such +that, for `s ≤ m ≤ C s`, `M ≤ 2 m` and `p ≤ n`, writing `A = 2 ^ (⌊log₂ m⌋ / 32768)`, +`2 ^ M (A p + 2) ^ A ≤ K (n + 1) ^ K 2 ^ (K s / √⌊log₂ s⌋)`, provided that from `s₀` on +`M ≤ leafSize m` and `p ≤ m ^ c`. Below `s₀`, `m` is bounded, so the packet factor is polynomial +in `n` 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`). This is the factor of the cost of a leaf with +the packet shape (`leafCertificate_le_of_packetShape`) that is not polynomial. -/ +theorem exists_leafFactor_le (C c s₀ : ℕ) : ∃ K : ℕ, ∀ s m M p n : ℕ, 2 ≤ s → s ≤ m → + m ≤ C * s → M ≤ 2 * m → p ≤ n → (s₀ ≤ s → M ≤ leafSize m ∧ p ≤ m ^ c) → + 2 ^ M * (2 ^ (Nat.log 2 m / 32768) * p + 2) ^ 2 ^ (Nat.log 2 m / 32768) ≤ + K * (n + 1) ^ K * 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) := by 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 (encList encNat) x).length with hn - set K := Ks + K₀ + C * s₀ + C + K₁ with hK + obtain ⟨Ks, hKs⟩ : ∃ Ks, Ks = 2 ^ (2 * (C * s₀)) * (C * s₀ + 2) ^ (C * s₀) := ⟨_, rfl⟩ + have hKs1 : 1 ≤ Ks := by rw [hKs]; exact Nat.one_le_iff_ne_zero.mpr (by positivity) + refine ⟨Ks + C * s₀ + C + K₁, fun s m M p n hs hsm hmC hM hp hbig => ?_⟩ + set K := Ks + C * s₀ + C + K₁ with hK set S := Nat.sqrt (Nat.log 2 s) with hSdef + set A := 2 ^ (Nat.log 2 m / 32768) with hA 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 + 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)) 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 (encList encNat) 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 + have hmC' : m ≤ C * s₀ := hmC.trans (Nat.mul_le_mul_left _ hsmall.le) + have h2M : 2 ^ M ≤ 2 ^ (2 * (C * s₀)) := Nat.pow_le_pow_right (by norm_num) (by omega) + have hbase : A * p + 2 ≤ (C * s₀ + 2) * (n + 1) := by + have : A * p ≤ 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 _ + have hfac : (A * p + 2) ^ A ≤ (C * s₀ + 2) ^ (C * s₀) * (n + 1) ^ (C * s₀) := by + calc (A * p + 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 tableEntryCertificate 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 + calc 2 ^ M * (A * p + 2) ^ A + ≤ 2 ^ (2 * (C * s₀)) * ((C * s₀ + 2) ^ (C * s₀) * (n + 1) ^ (C * s₀)) := + Nat.mul_le_mul h2M hfac + _ = Ks * (n + 1) ^ (C * s₀) := by rw [hKs]; 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 + obtain ⟨hleaf, hpm⟩ := hbig hlarge + have hlog : S ≤ Nat.sqrt (Nat.log 2 m) := Nat.sqrt_log_two_mono hsm + have hMs : M ≤ C * s / S := + calc M ≤ m / Nat.sqrt (Nat.log 2 m) := hleaf + _ ≤ m / 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 hfac : (A * p + 2) ^ A ≤ 2 ^ (K₁ * s / S) := hK₁ s m p hs hsm hmC hpm 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 tableEntryCertificate 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) + have hKn : 1 ≤ K * (n + 1) ^ K := Nat.mul_pos (by omega) (Nat.pos_of_ne_zero (by positivity)) + calc 2 ^ M * (A * p + 2) ^ A ≤ 2 ^ (C * s / S) * 2 ^ (K₁ * s / S) := + Nat.mul_le_mul (Nat.pow_le_pow_right (by norm_num) hMs) hfac + _ = 2 ^ (C * s / S + K₁ * s / S) := by rw [pow_add] + _ ≤ 2 ^ (K * s / S) := Nat.pow_le_pow_right (by norm_num) hexp + _ ≤ K * (n + 1) ^ K * 2 ^ (K * s / S) := Nat.le_mul_of_pos_left _ hKn + +/-- A polynomial factor `K₀ B ^ K₀` absorbed into a leaf bound `K₁ B ^ K₁ 2 ^ (K₁ s / S)`. -/ +private theorem mul_leafBound_le {K₀ K₁ B s S : ℕ} (hB : 1 ≤ B) : + K₀ * B ^ K₀ * (K₁ * B ^ K₁ * 2 ^ (K₁ * s / S)) ≤ + (K₀ * K₁ + K₀ + K₁) * B ^ (K₀ * K₁ + K₀ + K₁) * 2 ^ ((K₀ * K₁ + K₀ + K₁) * s / S) := + calc K₀ * B ^ K₀ * (K₁ * B ^ K₁ * 2 ^ (K₁ * s / S)) + = K₀ * K₁ * B ^ (K₀ + K₁) * 2 ^ (K₁ * s / S) := by rw [pow_add]; ring + _ ≤ _ := Nat.mul_le_mul (Nat.mul_le_mul (Nat.le_add_right _ _ |>.trans (Nat.le_add_right _ _)) + (Nat.pow_le_pow_right hB (by omega))) + (Nat.pow_le_pow_right (by norm_num) (Nat.div_le_div_right + (Nat.mul_le_mul_right _ (by omega)))) + +/-- **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`: the +cost of a leaf over tables with the packet shape +(`leafCertificate_tableEntry_le_of_packetShape`), with its factor `2 ^ M (A p + 2) ^ A` bounded by +`exists_leafFactor_le`. -/ +theorem exists_leafCertificate_le (C c s₀ : ℕ) : ∃ K : ℕ, + ∀ (mk : Call (List ℕ) → State → ℕ × DescribedNetwork (VertexDesc (List ℕ))) (s : ℕ) + (x : Call (List ℕ)), 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 tableEntryCertificate mk).time x ≤ + K * ((encCall (encList encNat) x).length + 1) ^ K * 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) ∧ + (leafCertificate tableEntryCertificate mk).space x ≤ + K * ((encCall (encList encNat) x).length + 1) ^ K := by + obtain ⟨K₀, hK₀⟩ := leafCertificate_tableEntry_le_of_packetShape + obtain ⟨K₁, hK₁⟩ := exists_leafFactor_le C c s₀ + refine ⟨K₀ * K₁ + K₀ + K₁, fun mk s x hs hsm hmC hshape hM hbig => ?_⟩ + obtain ⟨hT, hS⟩ := hK₀ mk x hshape + set n := (encCall (encList encNat) x).length with hn + have hB1 : 1 ≤ n + 1 := by omega + have hp : x.prec ≤ n := by have := scale_add_prec_add_length_fl_le (encList encNat) x; omega + have hF := hK₁ s x.scale x.edges x.prec n hs hsm hmC hM hp hbig + refine ⟨hT.trans ?_, hS.trans (Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right hB1 (by omega)))⟩ + rw [Nat.mul_assoc] + exact (Nat.mul_le_mul_left _ hF).trans (mul_leafBound_le hB1) + +/-- **The leaf bound with the costs of the root entries.** For a native certificate `ce` of the +entry procedure and 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, whose root entries take time at most +`E` and space at most `ES`, takes time at most `K (n + ES + 1) ^ K 2 ^ (K s / √⌊log₂ s⌋) (E + 1)` +and space at most `K (n + ES + 1) ^ K` at a leaf, provided that from `s₀` on it has at most +`leafSize m` edges and precision at most `m ^ c`: the cost of a leaf with the packet shape +(`leafCertificate_le_of_packetShape`), with its factor `2 ^ M (A p + 2) ^ A` bounded as for tables +by `exists_leafFactor_le`. -/ +theorem exists_leafCertificate_le_of_entry + (ce : NativeCertificate (fun q : T × List Bool => ev q.1 q.2) (encPair encT encBits) + (encList encNat)) (C c s₀ : ℕ) : ∃ K : ℕ, + ∀ (mk : Call T → State → ℕ × DescribedNetwork (VertexDesc T)) (s : ℕ) (x : Call T) + (E ES : ℕ), 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) → + (∀ v ∈ x.net.vertices, ∀ t, v.2 = .inl t → ∀ bs : List Bool, bs.length = v.1.length → + ce.time (t, bs) ≤ E ∧ ce.space (t, bs) ≤ ES) → + (leafCertificate ce mk).time x ≤ K * ((encCall encT x).length + ES + 1) ^ K * + 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) * (E + 1) ∧ + (leafCertificate ce mk).space x ≤ K * ((encCall encT x).length + ES + 1) ^ K := by + obtain ⟨K₀, hK₀⟩ := leafCertificate_le_of_packetShape ce + obtain ⟨K₁, hK₁⟩ := exists_leafFactor_le C c s₀ + refine ⟨K₀ * K₁ + K₀ + K₁, fun mk s x E ES hs hsm hmC hshape hM hbig hroot => ?_⟩ + obtain ⟨hT, hS⟩ := hK₀ mk x E ES hshape hroot + set W := (encCall encT x).length + ES + 1 with hW + have hB1 : 1 ≤ W := by omega + have hp : x.prec ≤ (encCall encT x).length + ES := by + have := scale_add_prec_add_length_fl_le encT x; omega + have hF := hK₁ s x.scale x.edges x.prec _ hs hsm hmC hM hp hbig + rw [← hW] at hF + set Pk := (2 ^ (Nat.log 2 x.scale / 32768) * x.prec + 2) ^ 2 ^ (Nat.log 2 x.scale / 32768) + refine ⟨?_, hS.trans (Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right hB1 (by omega)))⟩ + have hPE : Pk + E ≤ Pk * (E + 1) := by + have : 1 ≤ Pk := Nat.one_le_pow _ _ (by omega) + nlinarith + calc _ ≤ K₀ * W ^ K₀ * 2 ^ x.edges * (Pk + E) := hT + _ ≤ K₀ * W ^ K₀ * (2 ^ x.edges * Pk) * (E + 1) := by + rw [Nat.mul_assoc (K₀ * W ^ K₀), Nat.mul_assoc (K₀ * W ^ K₀), Nat.mul_assoc (2 ^ x.edges)] + exact Nat.mul_le_mul_left _ (Nat.mul_le_mul_left _ hPE) + _ ≤ _ := Nat.mul_le_mul_right _ ((Nat.mul_le_mul_left _ hF).trans (mul_leafBound_le hB1)) end FastContraction diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionShape.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionShape.lean index 84b65a919..f0570881c 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionShape.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionShape.lean @@ -28,6 +28,10 @@ fields are bounded (`FastContraction.PacketBound`). It passes to the native chil 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`). +**Root descriptors** keep their number of ports along the recursion +(`FastContraction.Reach.exists_root_of_inl`), since the native child renumbers the ports of the +vertices it keeps (`NativeChild.exists_mem_of_mem_nativeChild_inl`). + ## Main definitions * `Cslib.Circuits.Frontier.FastContraction.PacketBound`: the bounded packet descriptors. @@ -38,6 +42,8 @@ at most `p + 40 m²` since `2 ^ a ≤ m`, and it adds at most `M (2 ^ a) ^ 12 * `Cslib.Circuits.Frontier.FastContraction.Shape.child`: the invariant passes to the native children. * `Cslib.Circuits.Frontier.FastContraction.Reach.shape`: every reached call satisfies it. +* `Cslib.Circuits.Frontier.FastContraction.Reach.exists_root_of_inl`: root descriptors keep their + number of ports. ## References @@ -315,4 +321,17 @@ theorem Reach.shape (h₀s : x₀.scale = x₀.edges) (h₀b : x₀.bound + x₀ end Child +/-- **Root descriptors keep their number of ports along the recursion**: every root descriptor of a +call reached by the native child builder is the descriptor of a vertex of the root with as many +ports. -/ +theorem Reach.exists_root_of_inl {x₀ x : Call T} (h : Reach nativeMk x₀ x) + {v : List ℕ × VertexDesc T} (hv : v ∈ x.net.vertices) {t : T} (ht : v.2 = .inl t) : + ∃ w ∈ x₀.net.vertices, w.2 = .inl t ∧ w.1.length = v.1.length := by + induction h generalizing v with + | root => exact ⟨v, hv, ht, rfl⟩ + | step c _ _ _ ih => + obtain ⟨u, hu, hut, hlen⟩ := NativeChild.exists_mem_of_mem_nativeChild_inl hv ht + obtain ⟨w, hw, hwt, hwlen⟩ := ih hu hut + exact ⟨w, hw, hwt, hwlen.trans hlen⟩ + end Cslib.Circuits.Frontier.FastContraction diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChild.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChild.lean index ab503a6a6..fa553d228 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChild.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChild.lean @@ -69,6 +69,8 @@ vertices as rows (`NativeChild.isRowsFirstBipartite_nativeChild`). * `Cslib.Circuits.Frontier.NativeChild.isRowsFirstBipartite_nativeChild`: it is rows-first. * `Cslib.Circuits.Frontier.NativeChild.desc_of_mem_nativeChild`: its retained and packet descriptors. +* `Cslib.Circuits.Frontier.NativeChild.exists_mem_of_mem_nativeChild_inl`: a retained vertex keeps + its number of ports. ## References @@ -1081,6 +1083,20 @@ theorem desc_of_mem_nativeChild (hD : D.IsRowsFirstBipartite r) {fl : List ℕ} · simp at hl₂ · simp at hl₁ +/-- **A kept vertex of the native child keeps its descriptor and its number of ports**: every root +descriptor of the native child is the descriptor of a parent vertex with as many ports. -/ +theorem exists_mem_of_mem_nativeChild_inl {fl : List ℕ} {a i pt : ℕ} {τ : ℤ} {ζ : List ℕ} + {pk : (List (List ℕ) × List (List ℕ)) × ℕ × List (ℕ × ℕ)} {β : List ℕ} {g : ℕ} + {v : List ℕ × VertexDesc T} (hv : v ∈ (nativeChild fl a i pt τ ζ r D pk β g).vertices) + {t : T} (ht : v.2 = .inl t) : + ∃ u ∈ D.vertices, u.2 = .inl t ∧ u.1.length = v.1.length := by + simp only [nativeChild, List.mem_append, List.mem_map, List.mem_filter, List.mem_range] at hv + rcases hv with ⟨k, ⟨hk, -⟩, rfl⟩ | ⟨q, -, rfl⟩ + · refine ⟨D.vertices[k], List.getElem_mem hk, ?_, ?_⟩ + · simpa only [List.getD_eq_getElem _ _ hk] using ht + · simp only [List.length_map, List.getD_eq_getElem _ _ hk] + · cases ht + end NativeChild end Cslib.Circuits.Frontier diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/RowsFirstPolyTime.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/RowsFirstPolyTime.lean new file mode 100644 index 000000000..785a9fa64 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/RowsFirstPolyTime.lean @@ -0,0 +1,136 @@ +/- +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.DescribedContraction +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeNatFrontends +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimePrimitives + +/-! +# Rows-first bipartiteness in polynomial time + +Rows-first bipartiteness of a described network at a number of rows +(`DescribedNetwork.IsRowsFirstBipartite`) is decidable in polynomial time, from the number of rows +in binary and the network as encoded by `DescribedNetwork.encDescribed`. The test checks that every +port names an edge and counts, for each edge, its ports among the first `r` vertices and among the +others. It is the rows-first part of the guards of the contraction machines, for explicit networks +and for entry procedures. + +## Main results + +* `Cslib.Circuits.Frontier.DescribedNetwork.rowsFirst_polyTime`: rows-first bipartiteness is + decidable in polynomial time. +-/ + +public section + +namespace Cslib.Circuits.Frontier.DescribedNetwork + +open Turing.MultiTapeTM + +variable {T : Type} {encT : T ↪ List Bool} + +/-- Rows-first bipartiteness as a conjunction of list tests. -/ +private def rowsTest (r : ℕ) (d : DescribedNetwork T) : Bool := + d.vertices.all (fun v => v.1.all fun i => decide (i < d.numEdges)) && + (List.range d.numEdges).all (fun i => + decide (((d.vertices.take r).flatMap Prod.fst).count i = 1) && + decide (((d.vertices.drop r).flatMap Prod.fst).count i = 1)) + +private theorem decide_eq_rowsTest (r : ℕ) (d : DescribedNetwork T) : + decide (d.IsRowsFirstBipartite r) = rowsTest r d := by + refine Bool.eq_iff_iff.mpr ?_ + simp only [rowsTest, IsRowsFirstBipartite, decide_eq_true_eq, Bool.and_eq_true, + List.all_eq_true, List.mem_range, List.count_flatMap, Function.comp_def] + +/-- Taking or dropping `min |l| r` elements is taking or dropping `r`. -/ +private theorem take_drop_min {α : Type} (l : List α) (r : ℕ) : + l.take (min l.length r) = l.take r ∧ l.drop (min l.length r) = l.drop r := by + rcases le_total l.length r with hle | hle + · rw [min_eq_left hle, List.take_length, List.take_of_length_le hle, List.drop_length, + List.drop_of_length_le hle] + exact ⟨rfl, rfl⟩ + · rw [min_eq_right hle] + exact ⟨rfl, rfl⟩ + +/-- **Rows-first bipartiteness is decidable in polynomial time**, from the number of rows and the +network. -/ +theorem rowsFirst_polyTime : + ComputableInPolyTime + (fun ((r, d) : ℕ × DescribedNetwork T) => decide (d.IsRowsFirstBipartite r)) + (encPair encNat (encDescribed encT)) encBool := by + have hr := ComputableInPolyTime.fst encNat (encDescribed encT) + have hm : ComputableInPolyTime (fun G : ℕ × DescribedNetwork T => G.2.numEdges) + (encPair encNat (encDescribed encT)) encUnary := + numEdges_polyTime.comp (ComputableInPolyTime.snd _ _) + have hvs : ComputableInPolyTime (fun G : ℕ × DescribedNetwork T => G.2.vertices) + (encPair encNat (encDescribed encT)) (encList (encPair (encList encNat) encT)) := + vertices_polyTime.comp (ComputableInPolyTime.snd _ _) + -- Ports in range. + have h1 : ComputableInPolyTime (fun G : ℕ × DescribedNetwork T => + G.2.vertices.all (fun v => v.1.all fun i => decide (i < G.2.numEdges))) + (encPair encNat (encDescribed encT)) encBool := by + refine ComputableInPolyTime.allWithInput hvs ?_ + refine ComputableInPolyTime.allWithInput + ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _)) ?_ + exact ComputableInPolyTime.binary_lt.comp ((ComputableInPolyTime.snd _ _).prod + (ComputableInPolyTime.unary_to_binary.comp (hm.comp ((ComputableInPolyTime.fst _ _).comp + (ComputableInPolyTime.fst _ _))))) + -- Each edge has one row port and one column port. + have hlen := (ComputableInPolyTime.length_list _).comp hvs + have hcap := ComputableInPolyTime.binary_min_unary' hlen hr + have htake : ComputableInPolyTime (fun G : ℕ × DescribedNetwork T => + G.2.vertices.take (min G.2.vertices.length G.1)) (encPair encNat (encDescribed encT)) + (encList (encPair (encList encNat) encT)) := + .of_tidy (ComputableTidilyInPolyTime.listTakeWithInput hvs.tidy hcap.tidy) + have hdrop : ComputableInPolyTime (fun G : ℕ × DescribedNetwork T => + G.2.vertices.drop (min G.2.vertices.length G.1)) (encPair encNat (encDescribed encT)) + (encList (encPair (encList encNat) encT)) := + .of_tidy (ComputableTidilyInPolyTime.listDropWithInput hvs.tidy hcap.tidy) + have hflat {l : ℕ × DescribedNetwork T → List (List ℕ × T)} + (hl : ComputableInPolyTime l (encPair encNat (encDescribed encT)) + (encList (encPair (encList encNat) encT))) : + ComputableInPolyTime (fun G => (l G).flatMap Prod.fst) (encPair encNat (encDescribed encT)) + (encList encNat) := + ComputableInPolyTime.flatMapWithInput (f := fun _ v => v.1) hl + ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _)) + have hcount {l : ℕ × DescribedNetwork T → List ℕ} + (hl : ComputableInPolyTime l (encPair encNat (encDescribed encT)) (encList encNat)) : + ComputableInPolyTime (fun p : (ℕ × DescribedNetwork T) × ℕ => + decide ((l p.1).count p.2 = 1)) + (encPair (encPair encNat (encDescribed encT)) encUnary) encBool := by + have hc := ComputableInPolyTime.countPWithInput (test := fun p a => decide (a = p.2)) + (hl.comp (ComputableInPolyTime.fst (encPair encNat (encDescribed encT)) encUnary)) + (ComputableInPolyTime.decide_eq' (ComputableInPolyTime.snd _ _) + (ComputableInPolyTime.unary_to_binary.comp ((ComputableInPolyTime.snd _ _).comp + (ComputableInPolyTime.fst _ _)))) + refine (ComputableInPolyTime.decide_eq' hc (ComputableInPolyTime.const 1)).of_enc_eq + fun p => ?_ + simp only [Function.comp_apply, List.count_eq_countP] + congr 3 + have h2 : ComputableInPolyTime (fun G : ℕ × DescribedNetwork T => + (List.range G.2.numEdges).all (fun i => + decide (((G.2.vertices.take (min G.2.vertices.length G.1)).flatMap Prod.fst).count i = + 1) && + decide (((G.2.vertices.drop (min G.2.vertices.length G.1)).flatMap Prod.fst).count i = + 1))) (encPair encNat (encDescribed encT)) encBool := + ComputableInPolyTime.allWithInput (ComputableInPolyTime.range.comp hm) + (ComputableInPolyTime.bool_and.comp ((hcount (hflat htake)).prod (hcount (hflat hdrop)))) + refine (ComputableInPolyTime.bool_and.comp (h1.prod h2)).of_enc_eq fun ⟨r, d⟩ => ?_ + obtain ⟨ht, hdr⟩ := take_drop_min d.vertices r + dsimp only + rw [decide_eq_rowsTest, rowsTest] + simp only [Function.comp_apply, ht, hdr] + +end Cslib.Circuits.Frontier.DescribedNetwork diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Schedule.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Schedule.lean index 66eafea95..4bde8f16f 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Schedule.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Schedule.lean @@ -32,7 +32,8 @@ p. 64). * Labels have `a_d = 2 ∑_{j ≤ d} u_j` coordinates (`slotBits`), packets `L = 2 ^ a_d` slots, and there are `D_arr = 64 ^ (2 a_d)` pairs of labels (`r = 64`). * The degree bound is `Δ = 2 ^ (⌊9 λ / 10⌋ + 2)` (`degreeBound`), a power of two that is at least - `s ^ (9/10)` (`pow_nine_le_degreeBound_pow_ten`) and at most `2 ^ 20 s ^ 9` in tenth power. + `s ^ (9/10)` (`pow_nine_le_degreeBound_pow_ten`) and at most `2 ^ 20 s ^ 9` in tenth power, + and monotone in `s` (`degreeBound_mono`). * The node `t` of valuation `i` is recovered from its children at precision `p_t = p + 8 h 2 ^ (a - i) + 8 M (a + 1)` (`nodePrecision`), as in Lemma D.5, where `D_t = L / 2 ^ i`. @@ -209,6 +210,10 @@ theorem degreeBound_pow_ten_le {s : ℕ} (hs : s ≠ 0) : degreeBound s ^ 10 ≤ _ = 2 ^ 20 * (2 ^ Nat.log 2 s) ^ 9 := by rw [← pow_mul, ← pow_add]; ring_nf _ ≤ 2 ^ 20 * s ^ 9 := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left h2 9) +/-- **The degree bound is monotone.** -/ +theorem degreeBound_mono {a b : ℕ} (h : a ≤ b) : degreeBound a ≤ degreeBound b := + Nat.pow_le_pow_right (by norm_num) (by have := Nat.log_mono_right (b := 2) h; omega) + /-- **The precision bound** of (D.11), `p ≤ s λ^{O(1)} 2 ^ (a_{d - 1})`: `precisionBound C s d ≤ C s 2 ^ (a_{d - 1}) (1 + d (8 λ + 40))`. -/ theorem precisionBound_le (C s d : ℕ) : diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/EntryAnalysis.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/EntryAnalysis.lean new file mode 100644 index 000000000..44f0e9c8a --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/EntryAnalysis.lean @@ -0,0 +1,754 @@ +/- +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.FastLeaves +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.EntryContractionMachine +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length + +/-! +# Theorem D.1 for entry procedures: the resource analysis + +The instance of the contraction interface for entry procedures +(`Cslib.Circuits.Frontier.EntryContractionAlgorithm`) given by the native machine +`EntryContraction.fastCore` (milestone E1.3 of #1538): for every native certificate `ce` of an +entry procedure, `CountingSimulation.entryContractionAlgorithm ce` contracts the networks admissible +for `ce` (`Cslib.Circuits.Frontier.EntryAdmissible`) in time `poly(n) 2 ^ O(s / √⌊log₂ s⌋)` and +polynomial space. This is Theorem D.1 of [OpenAI2026ETH] (p. 53) at truncation order `1`, with +the entries given by procedures. + +The analysis follows the one for explicit networks (`CountingSimulation.FastAnalysis`, +`CountingSimulation.fastSizes`, `CountingSimulation.fastLeaves`), with the root call of +`EntryContraction.rootCall`, the precision in unary and the guard `EntryContraction.guard`, which +every admissible input at the modulus passes. The one new ingredient is the cost of the root +entries at a leaf (§D.4.7, p. 64): + +* **root descriptors stay with their ports** (`FastContraction.Reach.exists_root_of_inl`): every + root descriptor of a reached call is the descriptor of a vertex of the input network with as many + ports, since the native child renumbers the ports of the vertices it keeps. So the entry bounds of + admissibility apply at every reached leaf; +* **the leaf bound with entry costs** (`FastContraction.exists_leafCertificate_le_of_entry`): a + leaf whose root entries take time `E` and space `ES` takes time + `K (n + ES + 1) ^ K 2 ^ (K s / √⌊log₂ s⌋) (E + 1)`; +* **the entry costs fit the budget**: `E ≤ C (s + L + 1) ^ C 2 ^ (C ⌈s ^ (9/10)⌉)`, and + `C ⌈s ^ (9/10)⌉ ≤ s / √⌊log₂ s⌋` from some size on (`exists_mul_ceilNineTenths_le`). + +## Main results + +* `Cslib.Complexity.CountingSimulation.entry_length_le_of_reach`: polynomial sizes along the + recursion from a guarded input. +* `Cslib.Complexity.CountingSimulation.exists_entryLeaves_le`: the leaf bounds on admissible + inputs. +* `Cslib.Complexity.CountingSimulation.exists_entryAnalysis`: the resource analysis of the + recursion on admissible inputs. +* `Cslib.Complexity.CountingSimulation.exists_fastCore_le`: the machine within the interface's + bounds. +* `Cslib.Complexity.CountingSimulation.entryContractionAlgorithm`: the contraction algorithm for + entry procedures. + +## 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.EntryContraction Cslib.GenericRAM Cslib.GenericRAM.StackRecursion + Turing.MultiTapeTM +open Cslib.Circuits.Frontier.FastContraction (Call Reach reachInv scheme nativeMk value encCall + encFrame encValue leafCertificate modulus active OnSchedule fuelConst) + +variable {T : Type} {encT : T ↪ List Bool} {entry : T → List Bool → List ℕ} + +/-! ### The root -/ + +/-- The parts of an encoded input `(P, fl, r, G)` against its length. -/ +theorem length_parts_le_encInput (P : ℕ) (fl : List ℕ) (r : ℕ) (G : DescribedNetwork T) : + P + fl.length + (encNat r).length + (DescribedNetwork.encDescribed encT G).length ≤ + (encInput encT (P, fl, r, G)).length := by + have h := length_le_length_encList encNat fl + simp only [encInput, length_encPair, encUnary_apply, List.length_replicate] at h ⊢ + omega + +/-- **Guarded roots are on the schedule**, for every constant `C ≥ 1` with precision at most +`C m`. -/ +theorem onSchedule_rootCall {P C r : ℕ} {G : DescribedNetwork T} + (hg : EntryContraction.guard (P, modulus G.numEdges, r, G) = true) (hC : 1 ≤ C) + (hp : P ≤ C * G.numEdges) : + OnSchedule C G.numEdges (rootCall (P, modulus G.numEdges, r, G)) := by + have hdeg : ∀ v ∈ G.vertices, v.1.length ≤ degreeBound G.numEdges := by + simp only [EntryContraction.guard, decide_eq_true_eq] at hg + exact hg.2.2 + refine FastContraction.onSchedule_root hC rfl rfl rfl (wf_rootCall hg) (fun v hv => ?_) rfl rfl + hp + simp only [rootCall, FastContraction.rootNet, List.mem_map] at hv + obtain ⟨w, hw, rfl⟩ := hv + exact hdeg w hw + +/-- **The clock is subexponential on admissible inputs**: with `s ≤ m ≤ C s` edges and precision +`P ≤ D s`, it is at most `2 ^ (K₀ (C + D) s / √⌊log₂ s⌋)`. -/ +theorem clock_le {C D s P r : ℕ} {fl : List ℕ} {G : DescribedNetwork T} (hs : 2 ≤ s) + (hsm : s ≤ G.numEdges) (hmC : G.numEdges ≤ C * s) (hP : P ≤ D * s) : + clock (P, fl, r, G) ≤ 2 ^ (fuelConst * (C + D) * s / Nat.sqrt (Nat.log 2 s)) := by + simp only [clock] + refine Nat.pow_le_pow_right (by norm_num) ?_ + set y := G.numEdges + P + have hy : y ≤ (C + D) * s := by rw [add_mul]; omega + have hsy : s ≤ y := by omega + have hq : 1 ≤ Nat.sqrt (Nat.log 2 s) := Nat.one_le_sqrt_log_two hs + have hq' : Nat.sqrt (Nat.log 2 s) ≤ Nat.sqrt (Nat.log 2 y) := Nat.sqrt_log_two_mono hsy + calc fuelConst * y / Nat.sqrt (Nat.log 2 y) ≤ fuelConst * y / Nat.sqrt (Nat.log 2 s) := + Nat.div_le_div_left hq' hq + _ ≤ fuelConst * (C + D) * s / Nat.sqrt (Nat.log 2 s) := by + refine Nat.div_le_div_right ?_ + rw [Nat.mul_assoc] + exact Nat.mul_le_mul_left _ hy + +/-! ### The sizes -/ + +/-- **Polynomial sizes along the recursion**: every call reached from the root of a guarded input +of encoded length `n`, its frames and its tagged value are at most `2 ^ 55 (n + 1) ^ 24` long. -/ +theorem entry_length_le_of_reach {x : ℕ × List ℕ × ℕ × DescribedNetwork T} + (hg : EntryContraction.guard x = true) {y : Call T} (hy : Reach nativeMk (rootCall x) y) : + (encCall encT y).length ≤ 2 ^ 55 * ((encInput encT x).length + 1) ^ 24 ∧ + (∀ a, (reachInv entry nativeMk (rootCall x)).frame y a → + (encPair (encCall encT) encFrame (y, a)).length ≤ + 2 ^ 55 * ((encInput encT x).length + 1) ^ 24) ∧ + (encValue (y.depth, value entry nativeMk y)).length ≤ + 2 ^ 55 * ((encInput encT x).length + 1) ^ 24 := by + obtain ⟨P, fl, r, G⟩ := x + set x₀ := rootCall (P, fl, r, G) with hx₀ + set m := G.numEdges with hm + set n := (encInput encT (P, fl, r, G)).length with hn + set Y := n + 1 with hY + have hparts := length_parts_le_encInput (encT := encT) P fl r G + have hmv := DescribedNetwork.length_numEdges_vertices_le (encT := encT) G + rw [← hn] at hparts + have hfl : fl = modulus m := by + simp only [EntryContraction.guard, decide_eq_true_eq] at hg + exact hg.1 + have hsh := FastContraction.Reach.shape (x₀ := x₀) rfl rfl (wf_rootCall hg) hy + 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 P + (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 := by + change fl.length ≤ 32 * Y ^ 8 + 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 + have hV : x₀.net.vertices.length = G.vertices.length := List.length_map _ + change _ + _ + (encNat r).length ≤ Z + omega + have hR₀ : ∀ w ∈ x₀.net.vertices, + (VertexDesc.enc encT w.2).length ≤ 200 * (Z + 1) ^ 2 := by + intro w hw + change w ∈ List.map _ G.vertices at hw + obtain ⟨u, hu, rfl⟩ := List.mem_map.mp hw + rw [length_encSum] + simp only [Sum.elim_inl] + have h1 := length_le_encList_of_mem (encPair (encList encNat) encT) hu + have h2 : (encList (encPair (encList encNat) encT) G.vertices).length ≤ + (DescribedNetwork.encDescribed encT G).length := by + change _ ≤ (encPair encUnary (encList (encPair (encList encNat) encT)) + (G.numEdges, G.vertices)).length + rw [length_encPair] + dsimp only + omega + rw [length_encPair] at h1 + 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 entry rfl rfl rfl hZ1 hZ2 + (fun z hz => by + change z ∈ fl at hz + rw [hfl] at hz + exact 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 leaves -/ + +/-- **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 at the modulus with `s ≤ m ≤ C s` edges and +precision `P ≤ D s`, every reached call has scale `m`, 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 entry_reach_facts (C D : ℕ) : ∃ s₀, ∀ (s P r : ℕ) (G : DescribedNetwork T), 2 ≤ s → + P ≤ D * s → s ≤ G.numEdges → G.numEdges ≤ C * s → + EntryContraction.guard (P, modulus G.numEdges, r, G) = true → + ∀ y, Reach nativeMk (rootCall (P, modulus G.numEdges, r, G)) y → + y.scale = G.numEdges ∧ y.edges ≤ 2 * y.scale ∧ + (s₀ ≤ s → y.prec ≤ y.scale ^ 4 ∧ (active y = false → y.edges ≤ leafSize y.scale)) := by + obtain ⟨sA, hsA⟩ := exists_activeBounds_le D + refine ⟨max sA (D + 81), fun s P r G hs hPD hsm hmC hg y hy => ?_⟩ + set m := G.numEdges with hm + have hp₀ : P ≤ D * m := hPD.trans (Nat.mul_le_mul_left _ hsm) + have hsh := FastContraction.Reach.shape (x₀ := rootCall (P, modulus m, r, G)) rfl rfl + (wf_rootCall hg) hy + have hsc : y.scale = m := hsh.scale_eq + refine ⟨hsc, hsc ▸ hsh.edges_le, fun hs₀ => ⟨?_, fun hl => ?_⟩⟩ + · have hbd := hsh.bound_add_depth_le + change y.bound + y.depth ≤ (m + 1) + 0 at hbd + have hprec : y.prec ≤ P + y.depth * (40 * m ^ 2) := hsh.prec_le + have : y.depth * (40 * m ^ 2) ≤ (m + 1) * (40 * m ^ 2) := Nat.mul_le_mul_right _ (by omega) + have h4 : D * m + (m + 1) * (40 * m ^ 2) ≤ m ^ 4 := by + have hm81 : D + 81 ≤ m := by omega + 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 + rw [hsc] + omega + · have hm2 : D + 2 ≤ m := by omega + have hC1 : P / 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) (P / m + 1) hC1 + have hpC : P ≤ (P / m + 1) * m := + (Nat.lt_div_mul_add (a := P) (b := m) (by omega)).le.trans (by rw [add_mul, one_mul]) + have h := hy.onSchedule hB (onSchedule_rootCall hg (Nat.le_add_left 1 _) hpC) + rw [hsc] + exact h.edges_le_leafSize hB hl + +/-- `2 ^ (C ⌈s ^ (9/10)⌉) ≤ 2 ^ (C s₁) 2 ^ (s / √⌊log₂ s⌋)` once `C ⌈s ^ (9/10)⌉` fits the budget +from `s₁` on. -/ +private theorem two_pow_mul_ceilNineTenths_le {C s₁ : ℕ} + (hs₁ : ∀ s, s₁ ≤ s → C * ceilNineTenths s ≤ s / Nat.sqrt (Nat.log 2 s)) (s : ℕ) : + 2 ^ (C * ceilNineTenths s) ≤ 2 ^ (C * s₁) * 2 ^ (s / Nat.sqrt (Nat.log 2 s)) := by + rw [← pow_add] + refine Nat.pow_le_pow_right (by norm_num) ?_ + rcases le_or_gt s₁ s with h | h + · have := hs₁ s h + omega + · exact (Nat.mul_le_mul_left C ((ceilNineTenths_le_self s).trans h.le)).trans + (Nat.le_add_right _ _) + +/-- **The leaf bounds on admissible inputs**: for a native certificate `ce` of the entry procedure +and all constants `C` and `D` there is `K` such that on every input at the modulus 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`. The root entries take time at most +`C (s + L + 1) ^ C 2 ^ (C ⌈s ^ (9/10)⌉)` at every reached leaf +(`FastContraction.Reach.exists_root_of_inl`), within the budget from some size on +(`exists_mul_ceilNineTenths_le`). -/ +theorem exists_entryLeaves_le + (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)) (C D : ℕ) : + ∃ K : ℕ, ∀ (s P r : ℕ) (G : DescribedNetwork T), 2 ≤ s → 1 ≤ P → P ≤ D * s → + EntryAdmissible ce C s (r, G) → + ∀ y, Reach nativeMk (rootCall (P, modulus G.numEdges, r, G)) y → active y = false → + (leafCertificate ce nativeMk).time y ≤ + K * ((encInput encT (P, modulus G.numEdges, r, G)).length + 1) ^ K * + 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) ∧ + (leafCertificate ce nativeMk).space y ≤ + K * ((encInput encT (P, modulus G.numEdges, r, G)).length + 1) ^ K := by + obtain ⟨s₀, hs₀⟩ := entry_reach_facts (T := T) C D + obtain ⟨KB, hKB⟩ := FastContraction.exists_leafCertificate_le_of_entry ce C 4 s₀ + obtain ⟨s₁, hs₁⟩ := exists_mul_ceilNineTenths_le C + obtain ⟨cW, hcW⟩ : ∃ cW, cW = 2 ^ 55 + C * 2 ^ C + 1 := ⟨_, rfl⟩ + obtain ⟨cE, hcE⟩ : ∃ cE, cE = (C * 2 ^ C + 1) * 2 ^ (C * s₁) := ⟨_, rfl⟩ + obtain ⟨K, hK⟩ : ∃ K, K = KB * cW ^ KB * cE + (24 + C) * KB + C + KB + 1 := ⟨_, rfl⟩ + refine ⟨K, fun s P r G hs hP hPD hA y hy hl => ?_⟩ + have hg : EntryContraction.guard (P, modulus G.numEdges, r, G) = true := + guard_of_entryAdmissible hA + obtain ⟨-, hsm, hmC, -, hent⟩ := hA + simp only at hsm hmC hent + set n := (encInput encT (P, modulus G.numEdges, r, G)).length with hn + set Y := n + 1 with hY + set S := Nat.sqrt (Nat.log 2 s) with hS + set L := (DescribedNetwork.encDescribed encT G).length with hL + have hparts := length_parts_le_encInput (encT := encT) P (modulus G.numEdges) r G + have hmv := DescribedNetwork.length_numEdges_vertices_le (encT := encT) G + rw [← hn] at hparts + obtain ⟨hsc, hE2, hbig⟩ := hs₀ s P r G hs hPD hsm hmC hg y hy + obtain ⟨-, hshape⟩ := hy.wf_packetShape (wf_rootCall hg) (packetShape_rootCall _) + -- The root entries at the leaf. + have hroot : ∀ v ∈ y.net.vertices, ∀ t, v.2 = .inl t → ∀ bs : List Bool, + bs.length = v.1.length → + ce.time (t, bs) ≤ C * (s + L + 1) ^ C * 2 ^ (C * ceilNineTenths s) ∧ + ce.space (t, bs) ≤ C * (s + L + 1) ^ C := by + intro v hv t ht bs hbs + obtain ⟨w, hw, hwt, hwlen⟩ := hy.exists_root_of_inl hv ht + change w ∈ List.map _ G.vertices at hw + obtain ⟨u, hu, rfl⟩ := List.mem_map.mp hw + simp only [Sum.inl.injEq] at hwt + subst hwt + exact hent u hu bs (hbs.trans hwlen.symm) + obtain ⟨hT, hSp⟩ := hKB nativeMk s y _ _ hs (hsc ▸ hsm) (hsc ▸ hmC) hshape hE2 + (fun h => ⟨(hbig h).2 hl, (hbig h).1⟩) hroot + have hny := (entry_length_le_of_reach (encT := encT) (entry := entry) hg hy).1 + rw [← hn] at hny + change _ ≤ 2 ^ 55 * Y ^ 24 at hny + -- The arithmetic against `Y = n + 1`. + have hY1 : 1 ≤ Y := by omega + have hsLY : s + L + 1 ≤ 2 * Y := by omega + have hES : C * (s + L + 1) ^ C ≤ C * 2 ^ C * Y ^ C := by + calc C * (s + L + 1) ^ C ≤ C * (2 * Y) ^ C := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hsLY _) + _ = C * 2 ^ C * Y ^ C := by rw [mul_pow, Nat.mul_assoc] + have hYC : Y ^ C ≤ Y ^ (24 + C) := Nat.pow_le_pow_right hY1 (by omega) + have hY24 : Y ^ 24 ≤ Y ^ (24 + C) := Nat.pow_le_pow_right hY1 (by omega) + have hW : (encCall encT y).length + C * (s + L + 1) ^ C + 1 ≤ cW * Y ^ (24 + C) := by + have h1 : 2 ^ 55 * Y ^ 24 ≤ 2 ^ 55 * Y ^ (24 + C) := Nat.mul_le_mul_left _ hY24 + have h2 : C * 2 ^ C * Y ^ C ≤ C * 2 ^ C * Y ^ (24 + C) := Nat.mul_le_mul_left _ hYC + have h3 : 1 ≤ Y ^ (24 + C) := Nat.one_le_pow _ _ hY1 + have e : cW * Y ^ (24 + C) = 2 ^ 55 * Y ^ (24 + C) + C * 2 ^ C * Y ^ (24 + C) + + Y ^ (24 + C) := by rw [hcW]; ring + omega + have hWK : KB * ((encCall encT y).length + C * (s + L + 1) ^ C + 1) ^ KB ≤ + KB * cW ^ KB * Y ^ ((24 + C) * KB) := by + calc _ ≤ KB * (cW * Y ^ (24 + C)) ^ KB := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hW _) + _ = KB * cW ^ KB * Y ^ ((24 + C) * KB) := by rw [mul_pow, ← pow_mul]; ring + have hE1 : C * (s + L + 1) ^ C * 2 ^ (C * ceilNineTenths s) + 1 ≤ + cE * Y ^ C * 2 ^ (s / S) := by + have h1 := two_pow_mul_ceilNineTenths_le hs₁ s + have h2 : C * (s + L + 1) ^ C * 2 ^ (C * ceilNineTenths s) ≤ + C * 2 ^ C * Y ^ C * (2 ^ (C * s₁) * 2 ^ (s / S)) := Nat.mul_le_mul hES h1 + have h3 : 1 ≤ Y ^ C * (2 ^ (C * s₁) * 2 ^ (s / S)) := + Nat.one_le_iff_ne_zero.mpr (by positivity) + have e : cE * Y ^ C * 2 ^ (s / S) = C * 2 ^ C * Y ^ C * (2 ^ (C * s₁) * 2 ^ (s / S)) + + Y ^ C * (2 ^ (C * s₁) * 2 ^ (s / S)) := by rw [hcE]; ring + omega + have hexp : KB * s / S + s / S ≤ K * s / S := + Nat.div_add_div_le_add_div.trans (Nat.div_le_div_right (by + rw [← Nat.add_one_mul]; exact Nat.mul_le_mul_right _ (by omega))) + constructor + · calc _ ≤ KB * ((encCall encT y).length + C * (s + L + 1) ^ C + 1) ^ KB * + 2 ^ (KB * s / S) * (C * (s + L + 1) ^ C * 2 ^ (C * ceilNineTenths s) + 1) := hT + _ ≤ KB * cW ^ KB * Y ^ ((24 + C) * KB) * 2 ^ (KB * s / S) * (cE * Y ^ C * 2 ^ (s / S)) := + Nat.mul_le_mul (Nat.mul_le_mul_right _ hWK) hE1 + _ = KB * cW ^ KB * cE * Y ^ ((24 + C) * KB + C) * 2 ^ (KB * s / S + s / S) := by + rw [pow_add, pow_add]; ring + _ ≤ K * Y ^ K * 2 ^ (K * s / S) := + Nat.mul_le_mul (Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right hY1 (by omega))) + (Nat.pow_le_pow_right (by norm_num) hexp) + · calc _ ≤ KB * ((encCall encT y).length + C * (s + L + 1) ^ C + 1) ^ KB := hSp + _ ≤ KB * cW ^ KB * Y ^ ((24 + C) * KB) := hWK + _ ≤ K * Y ^ K := by + have hcE1 : 1 ≤ cE := by rw [hcE]; exact Nat.one_le_iff_ne_zero.mpr (by positivity) + refine Nat.mul_le_mul ?_ (Nat.pow_le_pow_right hY1 (by omega)) + calc KB * cW ^ KB ≤ KB * cW ^ KB * cE := Nat.le_mul_of_pos_right _ hcE1 + _ ≤ K := by omega + +/-! ### The resource analysis -/ + +/-- **The resource analysis of the recursion on admissible inputs.** For a native certificate `ce` +of the entry procedure and all constants `C` and `D` there are `K` and `s₀` such that on every input +at the modulus admissible at size `s ≥ 2` with constant `C` and with precision `1 ≤ P ≤ D s`, the +root call has a derivation whose nodes, frames and values are at most `F` long, whose leaves take +time at most `TL` and space at most `SL`, with `H` open calls, such that +`H + F + SL ≤ K (n + 1) ^ K` and `TL ≤ K (n + 1) ^ K 2 ^ (K s / √⌊log₂ s⌋)` for the input length +`n`; and from `s₀` on its `N` nodes fit in the clock, `2 N - 1 ≤ clock`. -/ +theorem exists_entryAnalysis + (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)) (C D : ℕ) : + ∃ K s₀ : ℕ, ∀ (s P r : ℕ) (G : DescribedNetwork T), 2 ≤ s → 1 ≤ P → P ≤ D * s → + EntryAdmissible ce C s (r, G) → + ∃ N H F TL SL : ℕ, + (scheme entry nativeMk).Eval + (reachInv entry nativeMk (rootCall (P, modulus G.numEdges, r, G))) + (rootCall (P, modulus G.numEdges, r, G)) + (0, value entry nativeMk (rootCall (P, modulus G.numEdges, r, G))) N H ∧ + (s₀ ≤ s → 2 * N - 1 ≤ clock (P, modulus G.numEdges, r, G)) ∧ + (∀ y, (reachInv entry nativeMk (rootCall (P, modulus G.numEdges, r, G))).node y → + (encCall encT y).length ≤ F ∧ + ((scheme entry nativeMk).isLeaf y = true → + (leafCertificate ce nativeMk).time y ≤ TL ∧ + (leafCertificate ce nativeMk).space y ≤ SL)) ∧ + (∀ y a, (reachInv entry nativeMk (rootCall (P, modulus G.numEdges, r, G))).frame y a → + (encPair (encCall encT) encFrame (y, a)).length ≤ F) ∧ + (∀ v, (reachInv entry nativeMk (rootCall (P, modulus G.numEdges, r, G))).value v → + (encValue v).length ≤ F) ∧ + H + F + SL ≤ K * ((encInput encT (P, modulus G.numEdges, r, G)).length + 1) ^ K ∧ + TL ≤ K * ((encInput encT (P, modulus G.numEdges, r, G)).length + 1) ^ K * + 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) := by + obtain ⟨KL, hKL⟩ := exists_entryLeaves_le ce C D + obtain ⟨sA, hsA⟩ := exists_activeBounds_le D + refine ⟨2 ^ 55 + 24 + KL + 1, max sA (D + 2), fun s P r G hs hP hPD hA => ?_⟩ + have hg : EntryContraction.guard (P, modulus G.numEdges, r, G) = true := + guard_of_entryAdmissible hA + have hsm : s ≤ G.numEdges := hA.2.1 + have hKL' := hKL s P r G hs hP hPD hA + set x := (P, modulus G.numEdges, r, G) with hx + set x₀ := rootCall x with hx₀ + set m := G.numEdges with hm + set n := (encInput encT x).length with hn + have hparts := length_parts_le_encInput (encT := encT) P (modulus G.numEdges) r G + have hmv := DescribedNetwork.length_numEdges_vertices_le (encT := encT) G + rw [← hx, ← hn] at hparts + have hmn : m ≤ n := by omega + have hp₀ : P ≤ D * m := hPD.trans (Nat.mul_le_mul_left _ hsm) + -- The derivation. + obtain ⟨N, H, he, hN, hH⟩ : ∃ N H, (scheme entry nativeMk).Eval (reachInv entry nativeMk x₀) x₀ + (0, value entry nativeMk x₀) N H ∧ (max sA (D + 2) ≤ s → 2 * N - 1 ≤ clock x) ∧ + H ≤ m + 1 := by + by_cases hs₀ : max sA (D + 2) ≤ s + · have hm2 : D + 2 ≤ m := by omega + have hC1 : P / 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) (P / m + 1) hC1 + have hpC : P ≤ (P / m + 1) * m := + (Nat.lt_div_mul_add (a := P) (b := m) (by omega)).le.trans (by rw [add_mul, one_mul]) + obtain ⟨N, H, he, hN, hH⟩ := FastContraction.exists_eval_onSchedule entry hB + (onSchedule_rootCall hg (Nat.le_add_left 1 _) hpC) rfl (by omega) + exact ⟨N, H, he, fun _ => two_mul_sub_one_le_fuel hm2 hp₀ hN, + hH.trans ((Nat.log_lt_self 2 (by omega)).le.trans (Nat.le_succ _))⟩ + · obtain ⟨N, H, he, hH⟩ := FastContraction.exists_eval_reachInv (ev := entry) (mk := nativeMk) + (x₀ := x₀) rfl + exact ⟨N, H, he, fun h => absurd h hs₀, hH⟩ + -- The bounds. + set K := 2 ^ 55 + 24 + KL + 1 with hK + have hB1 : 1 ≤ n + 1 := by omega + refine ⟨N, H, 2 ^ 55 * (n + 1) ^ 24, + KL * (n + 1) ^ KL * 2 ^ (KL * s / Nat.sqrt (Nat.log 2 s)), KL * (n + 1) ^ KL, he, hN, + fun y hy => ⟨(entry_length_le_of_reach (entry := entry) hg hy).1, fun hl => ?_⟩, + fun y a ha => (entry_length_le_of_reach (entry := entry) hg ha.1).2.1 a ha, + fun v ⟨y, hy, hv⟩ => hv ▸ (entry_length_le_of_reach (entry := entry) hg hy).2.2, ?_, ?_⟩ + · exact hKL' y hy (by simpa [scheme] using hl) + · have h1 : H ≤ 1 * (n + 1) ^ K := by + have : n + 1 ≤ (n + 1) ^ K := Nat.le_self_pow (by omega) _ + omega + have h2 : 2 ^ 55 * (n + 1) ^ 24 ≤ 2 ^ 55 * (n + 1) ^ K := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_right hB1 (by omega)) + have h3 : KL * (n + 1) ^ KL ≤ KL * (n + 1) ^ K := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_right hB1 (by omega)) + calc H + 2 ^ 55 * (n + 1) ^ 24 + KL * (n + 1) ^ KL + ≤ 1 * (n + 1) ^ K + 2 ^ 55 * (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) + · exact Nat.mul_le_mul (Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right hB1 (by omega))) + (Nat.pow_le_pow_right (by norm_num) (Nat.div_le_div_right (Nat.mul_le_mul_right _ + (by omega)))) + +/-! ### The resources of the machine -/ + +private theorem mul_succ_le_sq (H F : ℕ) : (H + 1) * (F + 1) ≤ (H + F + 1) ^ 2 := by nlinarith + +private theorem mul_add_one_le {c x : ℕ} (hx : 1 ≤ x) : c * x + 1 ≤ (c + 1) * x := by nlinarith + +/-- The arithmetic of the time bound. -/ +private theorem time_assemble {gT runT cT rT fuel Z TL Wb n rest Q W c₁ k₁ c₃ ka R : ℕ} + (hrun : runT ≤ cT + rT + 2 * n + (fuel + 1) * (Z + TL + Wb)) + (hq : gT + cT + rT ≤ Q) (hQ : Q ≤ c₁ * W) + (hP1 : (fuel + 1) * Z ≤ 2 * k₁ * W) (hP2 : (fuel + 1) * TL ≤ 2 * ka * W) + (hP3 : (fuel + 1) * Wb ≤ 2 * c₃ * W) (hn : n + 1 ≤ W) (hR : rest ≤ R * W) : + gT + (2 * runT + n + rest) ≤ (2 * c₁ + 5 + 4 * k₁ + 4 * c₃ + 4 * ka + R) * W := by + have e : (fuel + 1) * (Z + TL + Wb) = (fuel + 1) * Z + (fuel + 1) * TL + (fuel + 1) * Wb := by + ring + rw [e] at hrun + nlinarith + +/-- The arithmetic of the space bound. -/ +private theorem space_assemble {gS runS cS rS fb Z SL n rest Q W c₁ k₁ ka R : ℕ} + (hrun : runS ≤ cS + rS + 2 * n + Z + SL + fb) + (hq : gS + cS + rS + fb ≤ Q) (hQ : Q ≤ c₁ * W) (hZ : Z ≤ k₁ * W) (hSL : SL ≤ ka * W) + (hn : n + 1 ≤ W) (hR : rest ≤ R * W) : + gS + (2 * runS + n + rest) ≤ (2 * c₁ + 5 + 2 * k₁ + 2 * ka + R) * W := by + nlinarith + +/-- **The machine within the interface's bounds.** For a native certificate `ce` of the entry +procedure and all constants `C` and `D` there is `K` such that on every input at the modulus +admissible at size `s ≥ 2` with constant `C` and with precision `1 ≤ P ≤ D s`, the machine +`EntryContraction.fastCore ce` takes time at most `K (n + 1) ^ K 2 ^ (K s / √⌊log₂ s⌋)` and space at +most `K (n + 1) ^ K`. Admissible inputs pass the guard; from some size on the clocked run returns +the root's value, and below it direct summation costs a constant factor. -/ +theorem exists_fastCore_le + (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)) (C D : ℕ) : + ∃ K : ℕ, ∀ (s P r : ℕ) (G : DescribedNetwork T), 2 ≤ s → 1 ≤ P → P ≤ D * s → + EntryAdmissible ce C s (r, G) → + (fastCore ce).time (P, modulus G.numEdges, r, G) ≤ + K * ((encInput encT (P, modulus G.numEdges, r, G)).length + 1) ^ K * + 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) ∧ + (fastCore ce).space (P, modulus G.numEdges, r, G) ≤ + K * ((encInput encT (P, modulus G.numEdges, r, G)).length + 1) ^ K := by + obtain ⟨Ka, s₀, hKa⟩ := exists_entryAnalysis ce C D + obtain ⟨K₁, hK₁⟩ := Scheme.certificate_le + (FastContraction.scheme_nativeMk_polyTime (encT := encT) entry) (leafCertificate ce nativeMk) + obtain ⟨K₂, hK₂⟩ := exists_directCore_le (entry := entry) ce C + have hgP := NativeCertificate.ofPolyTime_isPolynomial (guard_polyTime (encT := encT)) + have hcnP := NativeCertificate.ofPolyTime_isPolynomial (clock_polyTime (encT := encT)) + have hcrP := NativeCertificate.ofPolyTime_isPolynomial (rootCall_polyTime (encT := encT)) + have hfuelL := (clock_polyTime (encT := encT)).polyBounded_length + obtain ⟨c₁, d₁, h₁⟩ := ((((((hgP.1.add hgP.2).add hcnP.1).add hcnP.2).add hcrP.1).add + hcrP.2).add hfuelL).exists_le + have htP := NativeCertificate.ofPolyTime_isPolynomial (valueTag_polyTime (encT := encT)) + have hoP := NativeCertificate.ofPolyTime_isPolynomial (valueList_polyTime (encT := encT)) + have hfP := NativeCertificate.ofPolyTime_isPolynomial + (ComputableInPolyTime.fst (encInput encT) encValue) + obtain ⟨c₂, d₂, h₂⟩ := (((((htP.1.add htP.2).add hoP.1).add hoP.2).add hfP.1).add + hfP.2).exists_le + -- The constants. + set E := 2 * d₁ + 2 * Ka * K₁ + (Ka + 1) * d₂ + K₂ + Ka + 1 with hE + set Kc := 2 * c₁ + 5 + 4 * (K₁ * (Ka + 1) ^ (2 * K₁)) + 4 * (c₁ + 1) ^ 2 + 4 * Ka + + (c₂ * (Ka + 2) ^ d₂ + K₂ * 2 ^ (K₂ * s₀)) with hKc + refine ⟨Kc + E + fuelConst * (C + D) + Ka, fun s P r G hs hP hPD hA => ?_⟩ + obtain ⟨N, H, F, TL, SL, he, hN, hnode, hframe, hvalue, hHFS, hTL⟩ := + hKa s P r G hs hP hPD hA + have hg : EntryContraction.guard (P, modulus G.numEdges, r, G) = true := + guard_of_entryAdmissible hA + obtain ⟨hdT, hdS⟩ := hK₂ s P r G hA + have hsm : s ≤ G.numEdges := hA.2.1 + have hmC : G.numEdges ≤ C * s := hA.2.2.1 + set x := (P, modulus G.numEdges, r, G) with hx + set n := (encInput encT x).length with hn + set B := n + 1 with hB + have hB1 : 1 ≤ B := by omega + set S := Nat.sqrt (Nat.log 2 s) + set Xf := 2 ^ (fuelConst * (C + D) * s / S) + set Xa := 2 ^ (Ka * s / S) + set X := 2 ^ ((fuelConst * (C + D) + Ka) * s / S) + have hXfX : Xf ≤ X := Nat.pow_le_pow_right (by norm_num) + (Nat.div_le_div_right (Nat.mul_le_mul_right _ (by omega))) + have hXfXa : Xf * Xa ≤ X := by + rw [← pow_add] + refine Nat.pow_le_pow_right (by norm_num) (Nat.div_add_div_le_add_div.trans ?_) + rw [add_mul] + have hX1 : 1 ≤ X := Nat.one_le_two_pow + -- The run. + obtain ⟨hrT, hrS⟩ := hK₁ (NativeCertificate.ofPolyTime clock_polyTime) + (NativeCertificate.ofPolyTime rootCall_polyTime) _ F TL SL hnode hframe hvalue x _ N H he + have hclock : clock x ≤ Xf := clock_le hs hsm hmC hPD + have hq1 := h₁ x + have hrT' : (runCore ce).time x ≤ _ := hrT + have hrS' : (runCore ce).space x ≤ _ := hrS + -- Polynomial pieces. + set Q₁ := c₁ * B ^ d₁ with hQ₁ + have hBK (k : ℕ) : 1 ≤ B ^ k := Nat.one_le_pow _ _ (by omega) + have hHF : (H + 1) * (F + 1) ≤ ((Ka + 1) * B ^ Ka) ^ 2 := by + have h1 : H + F ≤ Ka * B ^ Ka := by have := hHFS; omega + have h2 := hBK Ka + calc (H + 1) * (F + 1) ≤ (H + F + 1) ^ 2 := mul_succ_le_sq H F + _ ≤ (Ka * B ^ Ka + B ^ Ka) ^ 2 := Nat.pow_le_pow_left (by omega) 2 + _ = ((Ka + 1) * B ^ Ka) ^ 2 := by ring + have hZ : K₁ * ((H + 1) * (F + 1)) ^ K₁ ≤ K₁ * (Ka + 1) ^ (2 * K₁) * B ^ (2 * Ka * K₁) := by + calc K₁ * ((H + 1) * (F + 1)) ^ K₁ ≤ K₁ * (((Ka + 1) * B ^ Ka) ^ 2) ^ K₁ := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hHF _) + _ = K₁ * (Ka + 1) ^ (2 * K₁) * B ^ (2 * Ka * K₁) := by + rw [mul_pow, ← pow_mul, mul_pow, ← pow_mul, ← pow_mul, + show Ka * 2 * K₁ = 2 * Ka * K₁ by ring] + ring + have hW : ((encNat (clock x)).length + 1) ^ 2 ≤ (c₁ + 1) ^ 2 * B ^ (2 * d₁) := by + have h1 : (encNat (clock x)).length ≤ Q₁ := by omega + have h2 := hBK d₁ + calc _ ≤ (Q₁ + 1) ^ 2 := Nat.pow_le_pow_left (by omega) 2 + _ ≤ ((c₁ + 1) * B ^ d₁) ^ 2 := Nat.pow_le_pow_left (mul_add_one_le h2) 2 + _ = (c₁ + 1) ^ 2 * B ^ (2 * d₁) := by ring + have hTL' : TL ≤ Ka * B ^ Ka * Xa := hTL + have hSL : SL ≤ Ka * B ^ Ka := by have := hHFS; omega + -- The output and direct summation. + set R₁ := c₂ * (Ka + 2) ^ d₂ * B ^ ((Ka + 1) * d₂) with hR₁ + set R₂ := K₂ * 2 ^ (K₂ * s₀) * B ^ K₂ with hR₂ + have hdec : ∀ v : ℕ × List ℕ, (reachInv entry nativeMk (rootCall x)).value v → + (NativeCertificate.ofPolyTime (valueTag_polyTime (encT := encT))).time (x, v) + + (NativeCertificate.ofPolyTime (valueTag_polyTime (encT := encT))).space (x, v) + + (NativeCertificate.ofPolyTime (valueList_polyTime (encT := encT))).time (x, v) + + (NativeCertificate.ofPolyTime (valueList_polyTime (encT := encT))).space (x, v) + + (NativeCertificate.ofPolyTime + (ComputableInPolyTime.fst (encInput encT) encValue)).time (x, v) + + (NativeCertificate.ofPolyTime + (ComputableInPolyTime.fst (encInput encT) encValue)).space (x, v) ≤ R₁ := by + intro v hv + have h := h₂ (x, v) + have hv' := hvalue v hv + have hF : F ≤ Ka * B ^ Ka := by have := hHFS; omega + have hk1 : B ≤ B ^ (Ka + 1) := by + calc B = B ^ 1 := (pow_one B).symm + _ ≤ B ^ (Ka + 1) := Nat.pow_le_pow_right hB1 (by omega) + have hk2 : B ^ Ka ≤ B ^ (Ka + 1) := Nat.pow_le_pow_right hB1 (by omega) + have hlen : (encPair (encInput encT) encValue (x, v)).length + 1 ≤ + (Ka + 2) * B ^ (Ka + 1) := by + have hl := length_encPair (enc₁ := encInput encT) (enc₂ := encValue) (x, v) + simp only at hl + rw [hl] + have : Ka * B ^ Ka ≤ Ka * B ^ (Ka + 1) := Nat.mul_le_mul_left _ hk2 + have e : (Ka + 2) * B ^ (Ka + 1) = Ka * B ^ (Ka + 1) + 2 * B ^ (Ka + 1) := by ring + omega + calc _ ≤ c₂ * ((encPair (encInput encT) encValue (x, v)).length + 1) ^ d₂ := h + _ ≤ c₂ * ((Ka + 2) * B ^ (Ka + 1)) ^ d₂ := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hlen _) + _ = R₁ := by rw [hR₁, mul_pow, ← pow_mul, Nat.mul_assoc] + have hdir (hs₀ : s < s₀) : (directCore entry ce).time x ≤ R₂ := by + refine hdT.trans ?_ + have h2 : 2 ^ (K₂ * s) ≤ 2 ^ (K₂ * s₀) := + Nat.pow_le_pow_right (by norm_num) (Nat.mul_le_mul_left _ hs₀.le) + calc K₂ * B ^ K₂ * 2 ^ (K₂ * s) ≤ K₂ * B ^ K₂ * 2 ^ (K₂ * s₀) := Nat.mul_le_mul_left _ h2 + _ = R₂ := by rw [hR₂]; ring + have hdirS : (directCore entry ce).space x ≤ R₂ := + hdS.trans (by + rw [hR₂] + calc K₂ * B ^ K₂ ≤ K₂ * B ^ K₂ * 2 ^ (K₂ * s₀) := + Nat.le_mul_of_pos_right _ Nat.one_le_two_pow + _ = K₂ * 2 ^ (K₂ * s₀) * B ^ K₂ := by ring) + have hbig : s₀ ≤ s → (scheme entry nativeMk).run clock rootCall x = + some (0, value entry nativeMk (rootCall x)) := + fun h => Scheme.run_eq_some he (hN h) + clear hKa hK₁ hK₂ h₁ h₂ + -- Everything against `W = B ^ E X`. + set W := B ^ E * X with hWdef + have lift {c d : ℕ} (hd : d ≤ E) : c * B ^ d ≤ c * W := by + rw [hWdef, ← Nat.mul_assoc] + exact (Nat.mul_le_mul_left c (Nat.pow_le_pow_right hB1 hd)).trans + (Nat.le_mul_of_pos_right _ hX1) + have lift' {c d : ℕ} (hd : d ≤ E) : c * B ^ d ≤ c * B ^ E := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_right hB1 hd) + have hQW : Q₁ ≤ c₁ * W := lift (by omega) + have hR₁W : R₁ ≤ c₂ * (Ka + 2) ^ d₂ * W := lift (by omega) + have hR₂W : R₂ ≤ K₂ * 2 ^ (K₂ * s₀) * W := lift (by omega) + have hnW : n + 1 ≤ W := by + have := lift (c := 1) (d := 1) (by omega); rw [pow_one] at this; omega + have hfuel1 : clock x + 1 ≤ 2 * Xf := by + have : 1 ≤ Xf := Nat.one_le_two_pow + omega + have hP1 : (clock x + 1) * (K₁ * ((H + 1) * (F + 1)) ^ K₁) ≤ + 2 * (K₁ * (Ka + 1) ^ (2 * K₁)) * W := by + calc _ ≤ (2 * Xf) * (K₁ * (Ka + 1) ^ (2 * K₁) * B ^ (2 * Ka * K₁)) := + Nat.mul_le_mul hfuel1 hZ + _ = 2 * (K₁ * (Ka + 1) ^ (2 * K₁)) * (B ^ (2 * Ka * K₁) * Xf) := by ring + _ ≤ 2 * (K₁ * (Ka + 1) ^ (2 * K₁)) * W := Nat.mul_le_mul_left _ + (Nat.mul_le_mul (Nat.pow_le_pow_right hB1 (by omega)) hXfX) + have hP2 : (clock x + 1) * TL ≤ 2 * Ka * W := by + calc _ ≤ (2 * Xf) * (Ka * B ^ Ka * Xa) := Nat.mul_le_mul hfuel1 hTL' + _ = 2 * Ka * (B ^ Ka * (Xf * Xa)) := by ring + _ ≤ 2 * Ka * W := Nat.mul_le_mul_left _ + (Nat.mul_le_mul (Nat.pow_le_pow_right hB1 (by omega)) hXfXa) + have hP3 : (clock x + 1) * ((encNat (clock x)).length + 1) ^ 2 ≤ 2 * (c₁ + 1) ^ 2 * W := by + calc _ ≤ (2 * Xf) * ((c₁ + 1) ^ 2 * B ^ (2 * d₁)) := Nat.mul_le_mul hfuel1 hW + _ = 2 * (c₁ + 1) ^ 2 * (B ^ (2 * d₁) * Xf) := by ring + _ ≤ 2 * (c₁ + 1) ^ 2 * W := Nat.mul_le_mul_left _ + (Nat.mul_le_mul (Nat.pow_le_pow_right hB1 (by omega)) hXfX) + have hZE : K₁ * ((H + 1) * (F + 1)) ^ K₁ ≤ K₁ * (Ka + 1) ^ (2 * K₁) * B ^ E := + hZ.trans (lift' (by omega)) + have hQE : Q₁ ≤ c₁ * B ^ E := lift' (by omega) + have hR₁E : R₁ ≤ c₂ * (Ka + 2) ^ d₂ * B ^ E := lift' (by omega) + have hR₂E : R₂ ≤ K₂ * 2 ^ (K₂ * s₀) * B ^ E := lift' (by omega) + have hSLE : SL ≤ Ka * B ^ E := hSL.trans (lift' (by omega)) + have hnE : n + 1 ≤ B ^ E := by + have := lift' (c := 1) (d := 1) (by omega); rw [pow_one] at this; omega + have hKK : Kc ≤ Kc + E + fuelConst * (C + D) + Ka := by omega + have hBE : B ^ E ≤ B ^ (Kc + E + fuelConst * (C + D) + Ka) := + Nat.pow_le_pow_right hB1 (by omega) + have hXK : X ≤ 2 ^ ((Kc + E + fuelConst * (C + D) + Ka) * s / S) := + Nat.pow_le_pow_right (by norm_num) (Nat.div_le_div_right (Nat.mul_le_mul_right _ (by omega))) + have hR : R₁ + R₂ ≤ (c₂ * (Ka + 2) ^ d₂ + K₂ * 2 ^ (K₂ * s₀)) * W := by + rw [Nat.add_mul]; exact Nat.add_le_add hR₁W hR₂W + have hRE : R₁ + R₂ ≤ (c₂ * (Ka + 2) ^ d₂ + K₂ * 2 ^ (K₂ * s₀)) * B ^ E := by + rw [Nat.add_mul]; exact Nat.add_le_add hR₁E hR₂E + refine ⟨?_, ?_⟩ + · rw [fastCore_time] + simp only [hg, ↓reduceIte] + have hrest : ((scheme entry nativeMk).run clock rootCall x).elim + ((directCore entry ce).time x) (fun (tag, coeffs) => + (NativeCertificate.ofPolyTime (valueTag_polyTime (encT := encT))).time + (x, (tag, coeffs)) + + if decide (tag = 0) = true then + (NativeCertificate.ofPolyTime (valueList_polyTime (encT := encT))).time + (x, (tag, coeffs)) + else (NativeCertificate.ofPolyTime + (ComputableInPolyTime.fst (encInput encT) encValue)).time (x, (tag, coeffs)) + + (directCore entry ce).time x) ≤ R₁ + R₂ := by + rcases hr : (scheme entry nativeMk).run clock rootCall x with _ | ⟨tag, coeffs⟩ + · by_cases hs₀ : s₀ ≤ s + · rw [hbig hs₀] at hr; cases hr + · simp only [Option.elim_none]; have := hdir (by omega); omega + · have hd := hdec (tag, coeffs) (Scheme.value_of_run_eq_some he hr) + simp only [Option.elim_some] + split_ifs with h0 + · omega + · by_cases hs₀ : s₀ ≤ s + · rw [hbig hs₀] at hr; cases hr; simp at h0 + · have := hdir (by omega); omega + have htot := time_assemble (gT := (NativeCertificate.ofPolyTime + (guard_polyTime (encT := encT))).time x) hrT' (by omega) hQW hP1 hP2 hP3 hnW + (hrest.trans hR) + calc _ ≤ Kc * W := by rw [hKc]; exact htot + _ ≤ _ := by + rw [hWdef, ← Nat.mul_assoc] + exact Nat.mul_le_mul (Nat.mul_le_mul hKK hBE) hXK + · rw [fastCore_space] + simp only [hg, ↓reduceIte] + have hrest : ((scheme entry nativeMk).run clock rootCall x).elim + ((directCore entry ce).space x) (fun (tag, coeffs) => + (NativeCertificate.ofPolyTime (valueTag_polyTime (encT := encT))).space + (x, (tag, coeffs)) + + if decide (tag = 0) = true then + (NativeCertificate.ofPolyTime (valueList_polyTime (encT := encT))).space + (x, (tag, coeffs)) + else (NativeCertificate.ofPolyTime + (ComputableInPolyTime.fst (encInput encT) encValue)).space (x, (tag, coeffs)) + + (directCore entry ce).space x) ≤ R₁ + R₂ := by + rcases hr : (scheme entry nativeMk).run clock rootCall x with _ | ⟨tag, coeffs⟩ + · simp only [Option.elim_none]; omega + · have hd := hdec (tag, coeffs) (Scheme.value_of_run_eq_some he hr) + simp only [Option.elim_some] + split_ifs <;> omega + have htot := space_assemble (gS := (NativeCertificate.ofPolyTime + (guard_polyTime (encT := encT))).space x) hrS' (by omega) hQE hZE hSLE hnE + (hrest.trans hRE) + calc _ ≤ (2 * c₁ + 5 + 2 * (K₁ * (Ka + 1) ^ (2 * K₁)) + 2 * Ka + + (c₂ * (Ka + 2) ^ d₂ + K₂ * 2 ^ (K₂ * s₀))) * B ^ E := htot + _ ≤ Kc * B ^ E := Nat.mul_le_mul_right _ (by rw [hKc]; omega) + _ ≤ _ := Nat.mul_le_mul hKK hBE + +/-! ### The contraction algorithm -/ + +/-- **Theorem D.1 for entry procedures** ([OpenAI2026ETH], p. 53, at truncation order `1`): for +every native certificate `ce` of an entry procedure, the guarded native recursion with direct +summation as the fallback (`EntryContraction.fastCore ce`) is a contraction algorithm for the +networks admissible for `ce`, in time `poly(n) 2 ^ O(s / √⌊log₂ s⌋)` and polynomial space. -/ +noncomputable def entryContractionAlgorithm + (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)) : + EntryContractionAlgorithm encT entry (EntryAdmissible ce) where + core := coreValue entry + certificate := fastCore ce + val_core := val_coreValue + bound C D := exists_fastCore_le ce C D + +end Cslib.Complexity.CountingSimulation diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAlgorithm.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAlgorithm.lean index 0348e3bde..229fd0594 100644 --- a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAlgorithm.lean +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAlgorithm.lean @@ -12,6 +12,7 @@ public import Complexity.Computability.Complexity.Classes.CountingSimulation.Adm public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionMachine public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionStep public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionPolyTime +import Complexity.Computability.Circuit.Frontier.TensorNetwork.RowsFirstPolyTime import Mathlib.Analysis.SpecificLimits.Normed import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat @@ -50,7 +51,8 @@ interface's bounds (`CountingSimulation.fastCertificate_le`), through `Cslib.GenericRAM.StackRecursion.Scheme.certificate_le`. Below the size threshold the run may not finish, and the machine falls back to direct summation, at a constant factor. -The guard is polynomial-time (`CountingSimulation.fastGuard_polyTime`). +The guard is polynomial-time (`CountingSimulation.fastGuard_polyTime`), with the rows-first test +`DescribedNetwork.rowsFirst_polyTime`. For the native child builder (`FastContraction.nativeMk`), the components of the scheme are polynomial-time (`FastContraction.scheme_nativeMk_polyTime`), and the step, the passage of @@ -151,87 +153,21 @@ open Turing.MultiTapeTM /-- The encoding of an explicit network with its number of rows. -/ local notation "encG" => encPair encNat ExplicitTensorNetwork.encExplicitNetwork -/-- The guard as a conjunction of list tests. -/ -private def guardTest (G : ℕ × ExplicitTensorNetwork ℕ) : Bool := - G.2.vertices.all (fun v => v.1.all fun i => decide (i < G.2.numEdges)) && - (List.range G.2.numEdges).all (fun i => - decide (((G.2.vertices.take G.1).flatMap Prod.fst).count i = 1) && - decide (((G.2.vertices.drop G.1).flatMap Prod.fst).count i = 1)) && - G.2.vertices.all (fun v => decide (v.2.length = 2 ^ v.1.length)) && - G.2.vertices.all (fun v => decide (v.1.length ≤ degreeBound G.2.numEdges)) - -private theorem fastGuard_eq_guardTest (G : ℕ × ExplicitTensorNetwork ℕ) : - fastGuard G = guardTest G := by - refine Bool.eq_iff_iff.mpr ?_ - simp only [fastGuard, guardTest, DescribedNetwork.IsRowsFirstBipartite, - ExplicitTensorNetwork.maxDegree_le_iff, decide_eq_true_eq, Bool.and_eq_true, - List.all_eq_true, List.mem_range, List.count_flatMap, Function.comp_def] - constructor - · rintro ⟨⟨h1, h2⟩, h3, h4⟩ - exact ⟨⟨⟨fun v hv i hi => h1 v hv i hi, fun i hi => h2 i hi⟩, h3⟩, h4⟩ - · rintro ⟨⟨⟨h1, h2⟩, h3⟩, h4⟩ - exact ⟨⟨fun v hv i hi => h1 v hv i hi, fun i hi => h2 i hi⟩, h3, h4⟩ - -/-- **The guard is polynomial-time.** -/ +/-- **The guard is polynomial-time**: the rows-first test (`DescribedNetwork.rowsFirst_polyTime`), +the lengths of the tables and the degrees of the vertices. -/ theorem fastGuard_polyTime : ComputableInPolyTime fastGuard encG encBool := by - have hpair : ComputableInPolyTime (DescribedNetwork.equivProd (T := List ℕ)) - ExplicitTensorNetwork.encExplicitNetwork - (encPair encUnary (encList (encPair (encList encNat) (encList encNat)))) := - ComputableInPolyTime.of_eq fun _ => rfl have hd := ComputableInPolyTime.snd encNat ExplicitTensorNetwork.encExplicitNetwork - have hr := ComputableInPolyTime.fst encNat ExplicitTensorNetwork.encExplicitNetwork have hm : ComputableInPolyTime (fun G : ℕ × ExplicitTensorNetwork ℕ => G.2.numEdges) encG - encUnary := (ComputableInPolyTime.fst _ _).comp (hpair.comp hd) + encUnary := DescribedNetwork.numEdges_polyTime.comp hd have hvs : ComputableInPolyTime (fun G : ℕ × ExplicitTensorNetwork ℕ => G.2.vertices) encG (encList (encPair (encList encNat) (encList encNat))) := - (ComputableInPolyTime.snd _ _).comp (hpair.comp hd) - -- Ports in range. - have h1 : ComputableInPolyTime (fun G : ℕ × ExplicitTensorNetwork ℕ => - G.2.vertices.all (fun v => v.1.all fun i => decide (i < G.2.numEdges))) encG encBool := by - refine ComputableInPolyTime.allWithInput hvs ?_ - refine ComputableInPolyTime.allWithInput - ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _)) ?_ - exact ComputableInPolyTime.binary_lt.comp ((ComputableInPolyTime.snd _ _).prod - (ComputableInPolyTime.unary_to_binary.comp (hm.comp ((ComputableInPolyTime.fst _ _).comp - (ComputableInPolyTime.fst _ _))))) - -- Each edge has one row port and one column port. - have hlen := (ComputableInPolyTime.length_list _).comp hvs - have hcap := ComputableInPolyTime.binary_min_unary' hlen hr - have htake : ComputableInPolyTime (fun G : ℕ × ExplicitTensorNetwork ℕ => - G.2.vertices.take (min G.2.vertices.length G.1)) encG - (encList (encPair (encList encNat) (encList encNat))) := - .of_tidy (ComputableTidilyInPolyTime.listTakeWithInput hvs.tidy hcap.tidy) - have hdrop : ComputableInPolyTime (fun G : ℕ × ExplicitTensorNetwork ℕ => - G.2.vertices.drop (min G.2.vertices.length G.1)) encG - (encList (encPair (encList encNat) (encList encNat))) := - .of_tidy (ComputableTidilyInPolyTime.listDropWithInput hvs.tidy hcap.tidy) - have hflat {l : ℕ × ExplicitTensorNetwork ℕ → List (List ℕ × List ℕ)} - (hl : ComputableInPolyTime l encG (encList (encPair (encList encNat) (encList encNat)))) : - ComputableInPolyTime (fun G => (l G).flatMap Prod.fst) encG (encList encNat) := - ComputableInPolyTime.flatMapWithInput (f := fun _ v => v.1) hl - ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _)) - have hcount {l : ℕ × ExplicitTensorNetwork ℕ → List ℕ} - (hl : ComputableInPolyTime l encG (encList encNat)) : - ComputableInPolyTime (fun p : (ℕ × ExplicitTensorNetwork ℕ) × ℕ => - decide ((l p.1).count p.2 = 1)) (encPair encG encUnary) encBool := by - have hc := ComputableInPolyTime.countPWithInput (test := fun p a => decide (a = p.2)) - (hl.comp (ComputableInPolyTime.fst encG encUnary)) - (ComputableInPolyTime.decide_eq' (ComputableInPolyTime.snd _ _) - (ComputableInPolyTime.unary_to_binary.comp ((ComputableInPolyTime.snd _ _).comp - (ComputableInPolyTime.fst _ _)))) - refine (ComputableInPolyTime.decide_eq' hc (ComputableInPolyTime.const 1)).of_enc_eq - fun p => ?_ - simp only [Function.comp_apply, List.count_eq_countP] - congr 3 - have h2 : ComputableInPolyTime (fun G : ℕ × ExplicitTensorNetwork ℕ => - (List.range G.2.numEdges).all (fun i => - decide (((G.2.vertices.take (min G.2.vertices.length G.1)).flatMap Prod.fst).count i = 1) && - decide (((G.2.vertices.drop (min G.2.vertices.length G.1)).flatMap Prod.fst).count i = - 1))) encG encBool := - ComputableInPolyTime.allWithInput (ComputableInPolyTime.range.comp hm) - (ComputableInPolyTime.bool_and.comp ((hcount (hflat htake)).prod (hcount (hflat hdrop)))) + DescribedNetwork.vertices_polyTime.comp hd + -- Rows first. + have hrows : ComputableInPolyTime (fun G : ℕ × ExplicitTensorNetwork ℕ => + decide (G.2.IsRowsFirstBipartite G.1)) encG encBool := + DescribedNetwork.rowsFirst_polyTime -- Full tables. - have h3 : ComputableInPolyTime (fun G : ℕ × ExplicitTensorNetwork ℕ => + have htab : ComputableInPolyTime (fun G : ℕ × ExplicitTensorNetwork ℕ => G.2.vertices.all (fun v => decide (v.2.length = 2 ^ v.1.length))) encG encBool := by refine ComputableInPolyTime.allWithInput hvs ?_ have hv := ComputableInPolyTime.snd encG (encPair (encList encNat) (encList encNat)) @@ -241,7 +177,7 @@ theorem fastGuard_polyTime : ComputableInPolyTime fastGuard encG encBool := by (ComputableInPolyTime.binary_two_pow.comp ((ComputableInPolyTime.length_list _).comp ((ComputableInPolyTime.fst _ _).comp hv))) -- The degree bound. - have h4 : ComputableInPolyTime (fun G : ℕ × ExplicitTensorNetwork ℕ => + have hdeg : ComputableInPolyTime (fun G : ℕ × ExplicitTensorNetwork ℕ => G.2.vertices.all (fun v => decide (v.1.length ≤ degreeBound G.2.numEdges))) encG encBool := by refine ComputableInPolyTime.allWithInput hvs ?_ @@ -249,18 +185,10 @@ theorem fastGuard_polyTime : ComputableInPolyTime fastGuard encG encBool := by (ComputableInPolyTime.unary_to_binary.comp ((ComputableInPolyTime.length_list _).comp ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _)))) (degreeBound_polyTime.comp (hm.comp (ComputableInPolyTime.fst _ _))) - refine (ComputableInPolyTime.bool_and.comp ((ComputableInPolyTime.bool_and.comp - ((ComputableInPolyTime.bool_and.comp (h1.prod h2)).prod h3)).prod h4)).of_enc_eq fun G => ?_ - have ht : G.2.vertices.take (min G.2.vertices.length G.1) = G.2.vertices.take G.1 := by - rcases le_total G.2.vertices.length G.1 with hle | hle - · rw [min_eq_left hle, List.take_length, List.take_of_length_le hle] - · rw [min_eq_right hle] - have hdr : G.2.vertices.drop (min G.2.vertices.length G.1) = G.2.vertices.drop G.1 := by - rcases le_total G.2.vertices.length G.1 with hle | hle - · rw [min_eq_left hle, List.drop_length, List.drop_of_length_le hle] - · rw [min_eq_right hle] - rw [fastGuard_eq_guardTest, guardTest] - simp only [Function.comp_apply, ht, hdr] + refine (ComputableInPolyTime.bool_and.comp (hrows.prod (ComputableInPolyTime.bool_and.comp + (htab.prod hdeg)))).of_enc_eq fun G => ?_ + simp only [fastGuard, ExplicitTensorNetwork.maxDegree_le_iff, Function.comp_apply, + Bool.decide_and, List.all_eq, decide_eq_true_eq] end GuardPolyTime diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastLeaves.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastLeaves.lean index 447d80216..8893e8b98 100644 --- a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastLeaves.lean +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastLeaves.lean @@ -49,9 +49,11 @@ public section namespace Cslib.Circuits.Frontier.FastContraction +variable {T : Type} + /-- **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 (List ℕ)} (h : Reach nativeMk x₀ x) (hw : WF x₀) +theorem Reach.wf_packetShape {x₀ x : Call T} (h : Reach nativeMk x₀ x) (hw : WF x₀) (hs : PacketShape x₀) : WF x ∧ PacketShape x := by induction h with | root => exact ⟨hw, hs⟩ @@ -61,7 +63,7 @@ theorem Reach.wf_packetShape {x₀ x : Call (List ℕ)} (h : Reach nativeMk x₀ /-- **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 (List ℕ)} (h₀s : x₀.scale = x₀.edges) +theorem Reach.edges_le_two_mul_scale {x₀ x : Call T} (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 diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkEntryAnalysis.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkEntryAnalysis.lean new file mode 100644 index 000000000..4afe8c6a2 --- /dev/null +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkEntryAnalysis.lean @@ -0,0 +1,124 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: local-only (test driver) + +public import Complexity.Computability.Complexity.Classes.CountingSimulation.EntryAnalysis + +/-! +# Tests for the contraction algorithm with entry procedures + +The guard of the entry machine on a network of two parallel edges between a row vertex and a +column vertex, at the modulus of its number of edges and at another modulus; the guarded root is +well-formed and has no packets; an admissible input passes the guard; and the contraction +algorithm for entry procedures, instantiated at the entry procedure of tables, is correct with no +remaining hypothesis. That instance is an `EntryContractionAlgorithm` whose `bound` applies to an +admissible input, the network of two parallel edges at size `2`, so the interface is not vacuous. +-/ + +@[expose] public section + +namespace ComplexityTests.TensorNetworkEntryAnalysis + +open Cslib Cslib.Circuits.Frontier Cslib.Circuits.Frontier.EntryContraction + Cslib.Complexity.CountingSimulation +open Turing.MultiTapeTM (encList encNat) + +/-- Two parallel edges between a row vertex with table `1, 2, 3, 4` and a column vertex of +ones. -/ +abbrev twoEdges : DescribedNetwork (List ℕ) := ⟨2, [([0, 1], [1, 2, 3, 4]), ([0, 1], [1, 1, 1, 1])]⟩ + +/-! ### The guard -/ + +-- The guard holds at the modulus of the number of edges. +example : EntryContraction.guard (3, FastContraction.modulus 2, 1, twoEdges) = true := by decide + +-- It fails at another modulus, and when the rows are not first. +example : EntryContraction.guard (3, [1, 1], 1, twoEdges) = false := by decide + +example : EntryContraction.guard (3, FastContraction.modulus 2, 0, twoEdges) = false := by decide + +-- The guarded root is well-formed and has no packets. +example : FastContraction.WF (rootCall (3, FastContraction.modulus 2, 1, twoEdges)) ∧ + FastContraction.PacketShape (rootCall (3, FastContraction.modulus 2, 1, twoEdges)) := + ⟨wf_rootCall (by decide), packetShape_rootCall _⟩ + +-- An admissible input passes the guard at the modulus, at every precision. +example (P : ℕ) {C s : ℕ} (hA : EntryAdmissible tableEntryCertificate C s (1, twoEdges)) : + EntryContraction.guard (P, FastContraction.modulus twoEdges.numEdges, 1, twoEdges) = true := + guard_of_entryAdmissible hA + +/-! ### Root descriptors along the recursion -/ + +-- Every root descriptor of a reached call comes from a vertex of the input with as many ports. +example (x : ℕ × List ℕ × ℕ × DescribedNetwork (List ℕ)) (y : FastContraction.Call (List ℕ)) + (hy : FastContraction.Reach FastContraction.nativeMk (rootCall x) y) + (v : List ℕ × VertexDesc (List ℕ)) (hv : v ∈ y.net.vertices) (t : List ℕ) + (ht : v.2 = .inl t) : ∃ w ∈ x.2.2.2.vertices, w.2 = t ∧ w.1.length = v.1.length := by + obtain ⟨w, hw, hwt, hlen⟩ := hy.exists_root_of_inl hv ht + change w ∈ List.map _ x.2.2.2.vertices at hw + obtain ⟨u, hu, rfl⟩ := List.mem_map.mp hw + exact ⟨u, hu, Sum.inl_injective hwt, hlen⟩ + +/-! ### The contraction algorithm -/ + +/-- The contraction algorithm for the entry procedure of tables, with no remaining hypothesis. -/ +noncomputable def tableAlgorithm : + EntryContractionAlgorithm (encList encNat) tableEntry (EntryAdmissible tableEntryCertificate) := + entryContractionAlgorithm tableEntryCertificate + +-- It is correct at the modulus of the number of edges. +example : GaloisRingArith.val 3 (FastContraction.modulus 2) + (tableAlgorithm.core (3, FastContraction.modulus 2, 1, twoEdges)) = + ((10 : ℕ) : GaloisRingArith.Ring 3 (FastContraction.modulus 2)) := by + have hval := val_directCore_tableEntry 3 (FastContraction.modulus 2) twoEdges + rw [val_directCore] at hval + refine (tableAlgorithm.val_core 3 1 twoEdges).trans (hval.trans ?_) + congr 1 + +-- Its bound holds for all constants. +example (C D : ℕ) : ∃ K : ℕ, ∀ (s P r : ℕ) (G : DescribedNetwork (List ℕ)), 2 ≤ s → 1 ≤ P → + P ≤ D * s → EntryAdmissible tableEntryCertificate C s (r, G) → + tableAlgorithm.certificate.time (P, FastContraction.modulus G.numEdges, r, G) ≤ + K * ((encInput (encList encNat) (P, FastContraction.modulus G.numEdges, r, G)).length + + 1) ^ K * 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) ∧ + tableAlgorithm.certificate.space (P, FastContraction.modulus G.numEdges, r, G) ≤ + K * ((encInput (encList encNat) (P, FastContraction.modulus G.numEdges, r, G)).length + + 1) ^ K := + tableAlgorithm.bound C D + +/-! ### The interface is not vacuous -/ + +/-- The network of two parallel edges is admissible at size `2` with the entry procedure of +tables, for some constant. -/ +theorem exists_entryAdmissible_twoEdges : + ∃ C, EntryAdmissible tableEntryCertificate C 2 (1, twoEdges) := by + obtain ⟨C₀, hC₀⟩ := exists_entryAdmissible_of_isPolynomial + tableEntryCertificate_isPolynomial + have h2 : ceilNineTenths 2 = 2 := + le_antisymm (ceilNineTenths_le (by norm_num)) ((le_ceilNineTenths_iff (by norm_num)).2 + (by norm_num)) + refine ⟨C₀ + 1, hC₀ (C₀ + 1) 2 1 twoEdges (by omega) (by decide) le_rfl (by simp) ?_⟩ + intro v hv + rw [h2] + simp only [List.mem_cons, List.not_mem_nil, or_false] at hv + rcases hv with rfl | rfl <;> rfl + +-- The bound of the instance applies to that admissible input: at size `2`, precision `1` and the +-- modulus of its two edges, the time and space of the certificate are within the bound. +example : ∃ C K : ℕ, EntryAdmissible tableEntryCertificate C 2 (1, twoEdges) ∧ + tableAlgorithm.certificate.time (1, FastContraction.modulus 2, 1, twoEdges) ≤ + K * ((encInput (encList encNat) (1, FastContraction.modulus 2, 1, twoEdges)).length + + 1) ^ K * 2 ^ (K * 2 / Nat.sqrt (Nat.log 2 2)) ∧ + tableAlgorithm.certificate.space (1, FastContraction.modulus 2, 1, twoEdges) ≤ + K * ((encInput (encList encNat) (1, FastContraction.modulus 2, 1, twoEdges)).length + + 1) ^ K := by + obtain ⟨C, hC⟩ := exists_entryAdmissible_twoEdges + obtain ⟨K, hK⟩ := tableAlgorithm.bound C 1 + exact ⟨C, K, hC, hK 2 1 1 twoEdges le_rfl le_rfl (by norm_num) hC⟩ + +end ComplexityTests.TensorNetworkEntryAnalysis diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkEntryContraction.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkEntryContraction.lean new file mode 100644 index 000000000..4e1969b60 --- /dev/null +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkEntryContraction.lean @@ -0,0 +1,81 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: local-only (test driver) + +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.EntryContraction + +/-! +# Tests for the contraction interface with entry procedures + +`⌈s ^ (9/10)⌉` at a few sizes. Direct summation with the entry procedure of tables, on a network +of two parallel edges between a row vertex and a column vertex, computes `1 + 2 + 3 + 4 = 10`, +which is `2` in `A_3 = (ℤ / 8)[U] / (U ^ 2 + U + 1)`. That network is admissible at size `2` with +the entry procedure of tables, for some constant (`EntryAdmissible` is not vacuous). An instance of +`EntryContractionAlgorithm` whose bound applies to that input is +`ComplexityTests.TensorNetworkEntryAnalysis.tableAlgorithm` (`TensorNetworkEntryAnalysis.lean`). +-/ + +@[expose] public section + +namespace ComplexityTests.TensorNetworkEntryContraction + +open Cslib Cslib.Circuits.Frontier Cslib.Circuits.Frontier.EntryContraction + +/-! ### The nine-tenths power -/ + +example : ceilNineTenths 1 = 1 := + le_antisymm (ceilNineTenths_le (by norm_num)) ((le_ceilNineTenths_iff le_rfl).2 (by norm_num)) + +example : ceilNineTenths 2 = 2 := + le_antisymm (ceilNineTenths_le (by norm_num)) ((le_ceilNineTenths_iff (by norm_num)).2 + (by norm_num)) + +-- `1024 ^ (9/10) = 512` exactly. +example : ceilNineTenths 1024 = 512 := + le_antisymm (ceilNineTenths_le (by norm_num)) ((le_ceilNineTenths_iff (by norm_num)).2 + (by norm_num)) + +-- `⌈s ^ (9/10)⌉` is at most the degree bound of the schedule. +example : ceilNineTenths 1024 ≤ ContractionSchedule.degreeBound 1024 := + ceilNineTenths_le_degreeBound 1024 + +/-! ### Direct summation -/ + +/-- Two parallel edges between a row vertex with table `1, 2, 3, 4` and a column vertex of +ones. -/ +abbrev twoEdges : DescribedNetwork (List ℕ) := ⟨2, [([0, 1], [1, 2, 3, 4]), ([0, 1], [1, 1, 1, 1])]⟩ + +-- Its contraction is `10`, which is `2` modulo `8`, a constant coefficient list over +-- `(ℤ / 8)[U] / (U ^ 2 + U + 1)`. +example : DescribedNetwork.sumValue SumOps.galois tableEntry (3, [1, 1]) twoEdges = [2, 0] := by + decide + +example : ExplicitTensorNetwork.contraction (R := ℕ) twoEdges = 10 := by decide + +-- Direct summation is the contraction in `A_3`. +example : GaloisRingArith.val 3 [1, 1] + (DescribedNetwork.sumValue SumOps.galois tableEntry (3, [1, 1]) twoEdges) = + ((10 : ℕ) : GaloisRingArith.Ring 3 [1, 1]) := by + rw [val_directCore_tableEntry] + congr 1 + +/-! ### Admissibility is not vacuous -/ + +example : ∃ C, EntryAdmissible tableEntryCertificate C 2 (1, twoEdges) := by + obtain ⟨C₀, hC₀⟩ := exists_entryAdmissible_of_isPolynomial + tableEntryCertificate_isPolynomial + have h2 : ceilNineTenths 2 = 2 := + le_antisymm (ceilNineTenths_le (by norm_num)) ((le_ceilNineTenths_iff (by norm_num)).2 + (by norm_num)) + refine ⟨C₀ + 1, hC₀ (C₀ + 1) 2 1 twoEdges (by omega) (by decide) le_rfl (by simp) ?_⟩ + intro v hv + rw [h2] + simp only [List.mem_cons, List.not_mem_nil, or_false] at hv + rcases hv with rfl | rfl <;> rfl + +end ComplexityTests.TensorNetworkEntryContraction