From 4ab09bde32be97eab30757ba3ba94bd610124bc6 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 23:26:08 -0400 Subject: [PATCH] feat(Classes/CountingSimulation): a contraction algorithm from a guarded fast algorithm Branch on a polynomial-time guard to a fast machine or to direct summation; admissible networks failing the guard have bounded size, so direct summation there costs a constant factor. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Classes/CountingSimulation/Guarded.lean | 168 ++++++++++++++++++ ComplexityTests/GuardedContraction.lean | 30 ++++ 3 files changed, 199 insertions(+) create mode 100644 Complexity/Computability/Complexity/Classes/CountingSimulation/Guarded.lean create mode 100644 ComplexityTests/GuardedContraction.lean diff --git a/Complexity.lean b/Complexity.lean index e6f116c6e2..f92420e7b7 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1054,6 +1054,7 @@ public import Complexity.Computability.Complexity.Classes.Counting.Space public import Complexity.Computability.Complexity.Classes.CountingSimulation.Accumulate public import Complexity.Computability.Complexity.Classes.CountingSimulation.Assembly public import Complexity.Computability.Complexity.Classes.CountingSimulation.Containments +public import Complexity.Computability.Complexity.Classes.CountingSimulation.Guarded public import Complexity.Computability.Complexity.Classes.CountingSimulation.Interfaces public import Complexity.Computability.Complexity.Classes.DP public import Complexity.Computability.Complexity.Classes.EXP diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/Guarded.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/Guarded.lean new file mode 100644 index 0000000000..8e6857f83f --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/Guarded.lean @@ -0,0 +1,168 @@ +/- +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.Interfaces +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DirectContraction +public import Complexity.Computability.GenericRAM.Native.Combinators + +/-! +# A contraction algorithm from a guarded fast algorithm + +The contraction interface (`Cslib.Complexity.CountingSimulation.ContractionAlgorithm`) quantifies +its admissibility constants `C` and `D` after the machine, so a machine cannot test them. For +explicit networks, a contraction algorithm is assembled from a fast machine that is correct and +within the interface's bounds on the inputs passing a polynomial-time guard that does not mention +`C` and `D`, and from direct summation (`ExplicitTensorNetwork.directContractionBinaryCertificate`) +elsewhere (`ContractionAlgorithm.ofGuarded`). This needs only that admissible networks have at most +`C s` edges and that, for each `C`, the admissible networks failing the guard have bounded size `s`: +there direct summation costs `2 ^ (C s₀)` times a polynomial, a constant factor. + +In the contraction theorem of [OpenAI2026ETH] (Theorem D.1, with the proof of Appendix D.4), the +guard is the degree bound `⌈m ^ (9/10)⌉` in the number `m` of edges, and a network of degree at +most `C ⌊log₂ s⌋` fails it only for `s` below a threshold depending on `C`. The recursion of +Appendix D.4 then needs to be fast only on networks passing the guard. + +## Main definitions + +* `Cslib.Complexity.CountingSimulation.ContractionAlgorithm.ofGuarded`: the assembled algorithm. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Theorem D.1 (p. 53). +-/ + +public section + +namespace Cslib.Complexity.CountingSimulation + +open Cslib.Circuits.Frontier Cslib.Circuits.Frontier.ExplicitTensorNetwork Cslib.GenericRAM + Turing.MultiTapeTM + +/-- The encoding of an explicit network with its number of rows. -/ +local notation "encG" => encPair encNat encExplicitNetwork + +/-- Absorb a constant factor and a smaller exponent: `c₁ (n + 1) ^ e₁ + c₂ (n + 1) ^ e₂ 2 ^ x ≤ +K (n + 1) ^ K 2 ^ x` for `c₁ + c₂ ≤ K` and `e₁, e₂ ≤ K`. -/ +private theorem absorb_le {n c₁ c₂ e₁ e₂ K x : ℕ} (hc : c₁ + c₂ ≤ K) (he₁ : e₁ ≤ K) + (he₂ : e₂ ≤ K) : + c₁ * (n + 1) ^ e₁ + c₂ * (n + 1) ^ e₂ * 2 ^ x ≤ K * (n + 1) ^ K * 2 ^ x := by + have h1 : (n + 1) ^ e₁ ≤ (n + 1) ^ K := Nat.pow_le_pow_right (Nat.succ_pos _) he₁ + have h2 : (n + 1) ^ e₂ ≤ (n + 1) ^ K := Nat.pow_le_pow_right (Nat.succ_pos _) he₂ + have h3 : 1 ≤ 2 ^ x := Nat.one_le_two_pow + calc c₁ * (n + 1) ^ e₁ + c₂ * (n + 1) ^ e₂ * 2 ^ x + ≤ c₁ * ((n + 1) ^ K * 2 ^ x) + c₂ * ((n + 1) ^ K * 2 ^ x) := by + refine Nat.add_le_add (Nat.mul_le_mul_left _ (h1.trans (Nat.le_mul_of_pos_right _ h3))) + ?_ + rw [Nat.mul_assoc] + exact Nat.mul_le_mul_left _ (Nat.mul_le_mul_right _ h2) + _ = (c₁ + c₂) * ((n + 1) ^ K * 2 ^ x) := by ring + _ ≤ K * ((n + 1) ^ K * 2 ^ x) := Nat.mul_le_mul_right _ hc + _ = K * (n + 1) ^ K * 2 ^ x := by ring + +/-- **A contraction algorithm from a guarded fast algorithm.** Let `fast` compute the contraction +modulo `2 ^ P` on the networks passing a polynomial-time `guard`, within the interface's bounds on +the admissible ones. If admissible networks have at most `C s` edges, and for each `C` the +admissible networks failing the guard have bounded size `s`, then branching on the guard to `fast` +or to direct summation is a contraction algorithm. -/ +noncomputable def ContractionAlgorithm.ofGuarded + {Adm : ℕ → ℕ → ℕ × ExplicitTensorNetwork ℕ → Prop} + {guard : ℕ × ExplicitTensorNetwork ℕ → Bool} + (hguard : ComputableInPolyTime guard encG encBool) + {f : ℕ × (ℕ × ExplicitTensorNetwork ℕ) → ℕ} + (fast : NativeCertificate f (encPair encNat encG) encNat) + (hcorrect : ∀ P G, guard G = true → f (P, G) = G.2.contraction % 2 ^ P) + (hbound : ∀ C D : ℕ, ∃ K : ℕ, ∀ (s P : ℕ) (G : ℕ × ExplicitTensorNetwork ℕ), 2 ≤ s → + 1 ≤ P → P ≤ D * s → Adm C s G → guard G = true → + fast.time (P, G) ≤ K * ((encPair encNat encG (P, G)).length + 1) ^ K * + 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) ∧ + fast.space (P, G) ≤ K * ((encPair encNat encG (P, G)).length + 1) ^ K) + (hedges : ∀ C s G, Adm C s G → G.2.numEdges ≤ C * s) + (hsmall : ∀ C, ∃ s₀, ∀ s G, Adm C s G → guard G = false → s ≤ s₀) : + ContractionAlgorithm encG (fun G => G.2.contraction) Adm where + certificate := + (NativeCertificate.branch + (NativeCertificate.ofPolyTime (hguard.comp (ComputableInPolyTime.snd encNat encG))) + fast directContractionBinaryCertificate).congr fun p => by + split + · next h => exact hcorrect p.1 p.2 h + · rfl + bound C D := by + have ht := NativeCertificate.ofPolyTime_isPolynomial + (hguard.comp (ComputableInPolyTime.snd encNat encG)) + obtain ⟨ct, dt, hct⟩ := ht.1.exists_le + obtain ⟨cs, ds, hcs⟩ := ht.2.exists_le + obtain ⟨K₁, hK₁⟩ := hbound C D + obtain ⟨K₂, hK₂⟩ := exists_directContractionBinaryCertificate_le + obtain ⟨s₀, hs₀⟩ := hsmall C + refine ⟨ct + cs + dt + ds + K₁ + K₂ * 2 ^ (C * s₀) + K₂, fun s P G hs hP hPD hA => ?_⟩ + set K := ct + cs + dt + ds + K₁ + K₂ * 2 ^ (C * s₀) + K₂ + have hct' := hct (P, G) + have hcs' := hcs (P, G) + obtain ⟨hdt, hds⟩ := hK₂ (P, G) + have hfast : guard G = true → + fast.time (P, G) ≤ K₁ * ((encPair encNat encG (P, G)).length + 1) ^ K₁ * + 2 ^ (K₁ * s / Nat.sqrt (Nat.log 2 s)) ∧ + fast.space (P, G) ≤ K₁ * ((encPair encNat encG (P, G)).length + 1) ^ K₁ := + hK₁ s P G hs hP hPD hA + set n := (encPair encNat encG (P, G)).length + change (NativeCertificate.ofPolyTime (hguard.comp (ComputableInPolyTime.snd encNat encG))).time + (P, G) + (if guard G = true then fast.time (P, G) + else directContractionBinaryCertificate.time (P, G)) ≤ _ ∧ + (NativeCertificate.ofPolyTime (hguard.comp (ComputableInPolyTime.snd encNat encG))).space + (P, G) + (if guard G = true then fast.space (P, G) + else directContractionBinaryCertificate.space (P, G)) ≤ _ + have hpowK {e : ℕ} (he : e ≤ K) : (n + 1) ^ e ≤ (n + 1) ^ K := + Nat.pow_le_pow_right (Nat.succ_pos _) he + cases hg : guard G + · -- The guard fails: `s ≤ s₀`, so direct summation costs a constant factor. + have hsm := hs₀ s G hA hg + have hm : G.2.numEdges ≤ C * s₀ := + (hedges C s G hA).trans (Nat.mul_le_mul_left _ hsm) + simp only [Bool.false_eq_true, ite_false] + have h2m : 2 ^ G.2.numEdges ≤ 2 ^ (C * s₀) := Nat.pow_le_pow_right (by norm_num) hm + have hdt' : directContractionBinaryCertificate.time (P, G) ≤ + K₂ * 2 ^ (C * s₀) * (n + 1) ^ K₂ * 2 ^ 0 := by + refine hdt.trans ?_ + rw [pow_zero, Nat.mul_one] + calc K₂ * (n + 1) ^ K₂ * 2 ^ G.2.numEdges + ≤ K₂ * (n + 1) ^ K₂ * 2 ^ (C * s₀) := Nat.mul_le_mul_left _ h2m + _ = K₂ * 2 ^ (C * s₀) * (n + 1) ^ K₂ := by ring + constructor + · have habs := absorb_le (n := n) (c₁ := ct) (c₂ := K₂ * 2 ^ (C * s₀)) (e₁ := dt) + (e₂ := K₂) (K := K) (x := 0) (by omega) (by omega) (by omega) + have hexp : K * (n + 1) ^ K * 2 ^ 0 ≤ + K * (n + 1) ^ K * 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (by norm_num) (Nat.zero_le _)) + have := hdt' + omega + · have h1 := Nat.mul_le_mul_left cs (hpowK (show ds ≤ K by omega)) + have h2 := Nat.mul_le_mul_left K₂ (hpowK (show K₂ ≤ K by omega)) + have h3 : (cs + K₂) * (n + 1) ^ K ≤ K * (n + 1) ^ K := + Nat.mul_le_mul_right _ (by omega) + have e : (cs + K₂) * (n + 1) ^ K = cs * (n + 1) ^ K + K₂ * (n + 1) ^ K := by ring + omega + · -- The guard holds: the fast bound. + obtain ⟨hft, hfs⟩ := hfast hg + simp only [ite_true] + constructor + · have hx : K₁ * s / Nat.sqrt (Nat.log 2 s) ≤ K * s / Nat.sqrt (Nat.log 2 s) := + Nat.div_le_div_right (Nat.mul_le_mul_right _ (by omega)) + have hft' : fast.time (P, G) ≤ K₁ * (n + 1) ^ K₁ * 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) := + hft.trans (Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (by norm_num) hx)) + have habs := absorb_le (n := n) (c₁ := ct) (c₂ := K₁) (e₁ := dt) (e₂ := K₁) (K := K) + (x := K * s / Nat.sqrt (Nat.log 2 s)) (by omega) (by omega) (by omega) + omega + · have h1 := Nat.mul_le_mul_left cs (hpowK (show ds ≤ K by omega)) + have h2 := Nat.mul_le_mul_left K₁ (hpowK (show K₁ ≤ K by omega)) + have h3 : (cs + K₁) * (n + 1) ^ K ≤ K * (n + 1) ^ K := + Nat.mul_le_mul_right _ (by omega) + have e : (cs + K₁) * (n + 1) ^ K = cs * (n + 1) ^ K + K₁ * (n + 1) ^ K := by ring + omega + +end Cslib.Complexity.CountingSimulation diff --git a/ComplexityTests/GuardedContraction.lean b/ComplexityTests/GuardedContraction.lean new file mode 100644 index 0000000000..55c3004a12 --- /dev/null +++ b/ComplexityTests/GuardedContraction.lean @@ -0,0 +1,30 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Complexity.Classes.CountingSimulation.Guarded + +/-! # A contraction algorithm from a guarded fast algorithm + +The hypotheses of `ContractionAlgorithm.ofGuarded` are satisfiable: with a guard that always +fails, direct summation alone is a contraction algorithm for networks of bounded size `s`. -/ + +namespace ComplexityTests.GuardedContraction + +open Cslib.Complexity.CountingSimulation Cslib.Circuits.Frontier + Cslib.Circuits.Frontier.ExplicitTensorNetwork Turing.MultiTapeTM + +/-- Networks with at most `C s` edges and size at most `C`. -/ +def Bounded (C s : ℕ) (G : ℕ × ExplicitTensorNetwork ℕ) : Prop := G.2.numEdges ≤ C * s ∧ s ≤ C + +/-- Direct summation alone, behind a guard that always fails. -/ +noncomputable example : + ContractionAlgorithm (encPair encNat encExplicitNetwork) (fun G => G.2.contraction) Bounded := + ContractionAlgorithm.ofGuarded (guard := fun _ => false) (ComputableInPolyTime.const false) + directContractionBinaryCertificate (fun _ _ h => absurd h (by simp)) + (fun _ _ => ⟨0, fun _ _ _ _ _ _ _ h => absurd h (by simp)⟩) + (fun _ _ _ h => h.1) (fun C => ⟨C, fun _ _ h _ => h.2⟩) + +end ComplexityTests.GuardedContraction