feat(CountingSimulation): Theorem D.1 at truncation order ℓ for entry procedures

Complexity.lean

@@ -970,6 +970,11 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Schedule
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ScheduleCount
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ScheduledRecursion
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.TaperedRecovery
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Truncated
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.TruncatedAlgorithm
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.TruncatedEntry
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.TruncatedPolyTime
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.TruncatedResources
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.VertexDesc
 public import Complexity.Computability.Circuit.Frontier.TwoSidedWitness
 public import Complexity.Computability.Circuit.Frontier.Unconditional
@@ -1179,6 +1184,7 @@ public import Complexity.Computability.Complexity.Classes.CountingSimulation.Fas
 public import Complexity.Computability.Complexity.Classes.CountingSimulation.Guarded
 public import Complexity.Computability.Complexity.Classes.CountingSimulation.Interfaces
 public import Complexity.Computability.Complexity.Classes.CountingSimulation.Separation
+public import Complexity.Computability.Complexity.Classes.CountingSimulation.TruncatedEntry
 public import Complexity.Computability.Complexity.Classes.DP
 public import Complexity.Computability.Complexity.Classes.EXP
 public import Complexity.Computability.Complexity.Classes.FewP

Complexity/Computability/Complexity/Classes/CountingSimulation/TruncatedEntry.lean

@@ -0,0 +1,67 @@
+/-
+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.EntryAnalysis
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.TruncatedEntry
+
+/-!
+# Theorem D.1 at truncation order `ℓ` for entry procedures
+
+The instance of the interface of Theorem D.1 at truncation order `ℓ`
+(`Cslib.Circuits.Frontier.TruncatedContractionAlgorithm`) for networks whose entries are
+computed by procedures: for every native certificate `ce` of an entry procedure,
+`CountingSimulation.truncEntryContractionAlgorithm ce` computes the contraction in
+`B_{P,ℓ} = (ℤ / 2 ^ P)[V] / (V ^ ℓ)` of the networks admissible for `ce` with at most `C s` vertices
+(`Cslib.Circuits.Frontier.TruncEntryAdmissible`), for `1 ≤ P, ℓ ≤ D s`, in time
+`poly(n) 2 ^ O(s / √⌊log₂ s⌋)` and polynomial space.
+
+It combines the reduction of truncation order `ℓ` to `A_P = (ℤ / 2 ^ P)[U] / (f)`
+(`Cslib.Circuits.Frontier.TruncatedContractionAlgorithm.ofEntry`) with the contraction algorithm
+for entry procedures (`CountingSimulation.entryContractionAlgorithm`), applied to the specialized
+entries.
+
+This is Theorem D.1 of [OpenAI2026ETH] (p. 53) with one narrowing: the theorem asks for at most
+polynomially many vertices in `s`, and admissibility here asks for at most `C s`. The networks of
+Lemma D.2 (p. 56) and of the fixed-density bound (§D.2, p. 54) have that many. As for all the
+interfaces of this development, admissibility also asks for at least `s` edges, which a caller
+gets by padding (see `Cslib.Circuits.Frontier.EntryAdmissible`).
+
+## Main definitions
+
+* `Cslib.Complexity.CountingSimulation.truncEntryContractionAlgorithm`: Theorem D.1 at truncation
+  order `ℓ` for entry procedures.
+
+## 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.GenericRAM Turing.MultiTapeTM
+
+variable {T : Type} {encT : T ↪ List Bool} {entry : T → List Bool → List ℕ}
+
+/-- **Theorem D.1 at truncation order `ℓ` for entry procedures** ([OpenAI2026ETH], p. 53, for
+networks with at most `C s` vertices): for every native certificate `ce` of an entry procedure,
+the reduction of truncation order `ℓ` to `A_P` around the contraction algorithm for the
+specialized entries is a truncated contraction algorithm for the networks admissible for `ce` with
+at most `C s` vertices. It computes the contraction in `B_{P,ℓ}` from `(P, ℓ, r, G)` on every
+input, and on admissible inputs with `1 ≤ P, ℓ ≤ D s` in time `poly(n) 2 ^ O(s / √⌊log₂ s⌋)` and
+polynomial space. -/
+noncomputable def truncEntryContractionAlgorithm
+    (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits)
+      (encList encNat)) :
+    TruncatedContractionAlgorithm encT entry (TruncEntryAdmissible ce) :=
+  TruncatedContractionAlgorithm.ofEntry ce
+    (entryContractionAlgorithm (specEntryCertificate entry ce))
+
+end Cslib.Complexity.CountingSimulation

ComplexityTests/Computability/Circuit/Frontier/TensorNetworkTruncated.lean

@@ -0,0 +1,101 @@
+/-
+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.Truncated
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionMachine
+
+/-!
+# Tests for contraction at truncation order `ℓ`
+
+The networks have one edge between a row and a column, with tables of `V`-coefficient lists.
+With row entries `1, V` and column entries `1 + V, 2`, the contraction is `1 + 3 V`; with row
+entries `1 + V, 0` and column entries `1 + V, 5`, it is `(1 + V) ^ 2 = 1 + 2 V + V ^ 2`. The
+reduction contracts the networks specialized at digit points of `A_3` by direct summation and
+interpolates. At a modulus with enough residues it returns the truncated contraction; through
+`DescribedNetwork.interpContract_eq` at the irreducible `FastContraction.modulus 1` this computes
+`truncContraction`, which is not computable by itself.
+-/
+
+@[expose] public section
+
+namespace ComplexityTests.TensorNetworkTruncated
+
+open Cslib Cslib.Circuits.Frontier Cslib.Circuits.Frontier.DescribedNetwork
+
+/-- Tables of `V`-coefficient lists, read little-endian. -/
+def entry (table : List (List ℕ)) (bs : List Bool) : List ℕ :=
+  table.getD (BitString.lsbValue bs) []
+
+/-- Direct summation in `A_P` of a specialized network. -/
+def direct (x : ℕ × List ℕ × ℕ × DescribedNetwork (SpecDesc (List (List ℕ)))) : List ℕ :=
+  sumValue SumOps.galois (specEntry entry) (x.1, x.2.1) x.2.2.2
+
+/-- Row entries `1, V` and column entries `1 + V, 2`: the contraction `1 + 3 V`. -/
+def G₁ : DescribedNetwork (List (List ℕ)) := ⟨1, [([0], [[1], [0, 1]]), ([0], [[1, 1], [2]])]⟩
+
+/-- Row entries `1 + V, 0` and column entries `1 + V, 5`: the contraction `1 + 2 V + V ^ 2`. -/
+def G₂ : DescribedNetwork (List (List ℕ)) := ⟨1, [([0], [[1, 1], [0]]), ([0], [[1, 1], [5]])]⟩
+
+/-! ### Coefficients -/
+
+example : (coeffPoly [3, 5]).coeff 1 = 5 := by simp
+
+example : (coeffPoly [3, 5]).coeff 7 = 0 := by simp
+
+example : (coeffPoly [3, 5, 2]).natDegree ≤ 2 := natDegree_coeffPoly_le _
+
+/-! ### The reduction, computed -/
+
+-- Three points of `A_3 = (ℤ / 8)[U] / (U ^ 2 + U + 1)` recover `1 + 3 V` at `ℓ = 2`.
+example : pointCount 2 G₁ = 3 := rfl
+
+example : interpContract direct [1, 1] 3 2 1 G₁ = [1, 3] := by decide
+
+-- At `ℓ = 1` only the constant coefficient is kept.
+example : interpContract direct [1, 1] 3 1 1 G₁ = [1] := by decide
+
+-- Five points of `(ℤ / 8)[U] / (U ^ 3 + U + 1)` recover `1 + 2 V + V ^ 2` at `ℓ = 3`, and the
+-- entries are cut to `ℓ` coefficients at `ℓ = 2`.
+example : interpContract direct [1, 1, 0] 3 3 1 G₂ = [1, 2, 1] := by decide
+
+example : interpContract direct [1, 1, 0] 3 2 1 G₂ = [1, 2] := by decide
+
+-- Modulo `2 ^ 1` the coefficients are reduced.
+example : interpContract direct [1, 1, 0] 1 3 1 G₂ = [1, 0, 1] := by decide
+
+/-! ### The truncated contraction, through correctness -/
+
+/-- Direct summation in `A_P` is correct on every specialized network. -/
+theorem direct_correct (P : ℕ) (fl : List ℕ) (r : ℕ)
+    (G : DescribedNetwork (SpecDesc (List (List ℕ)))) :
+    GaloisRingArith.val P fl (direct (P, fl, r, G)) =
+      G.contraction fun d bs => GaloisRingArith.val P fl (specEntry entry d bs) :=
+  val_sumValue_galois _ (P, fl) G
+
+/-- The truncated contraction of `G₁` at `ℓ = 2` modulo `8` is `1 + 3 V`. -/
+example : G₁.truncContraction entry 3 2 = [1, 3] := by
+  rw [← interpContract_eq (core := direct) (r := 1) (FastContraction.irreducible_modulus 1) G₁
+    (by decide) fun k _ => direct_correct _ _ _ _]
+  decide +kernel
+
+/-- The truncated contraction of `G₂` at `ℓ = 3` modulo `8` is `1 + 2 V + V ^ 2`. -/
+example : G₂.truncContraction entry 3 3 = [1, 2, 1] := by
+  rw [← interpContract_eq (core := direct) (r := 1) (FastContraction.irreducible_modulus 1) G₂
+    (by decide) fun k _ => direct_correct _ _ _ _]
+  decide +kernel
+
+/-- The truncated contraction depends only on the entries in `B_{P,ℓ}`: changing the entries by
+multiples of `2 ^ P` and past `V ^ ℓ` does not change it. -/
+example : G₁.truncContraction entry 1 1 =
+    G₁.truncContraction (fun t bs => (entry t bs).map (· + 2)) 1 1 :=
+  truncContraction_congr G₁ fun t bs i hi => by
+    obtain rfl : i = 0 := by omega
+    cases entry t bs <;> simp
+
+end ComplexityTests.TensorNetworkTruncated

ComplexityTests/Computability/Circuit/Frontier/TensorNetworkTruncatedAlgorithm.lean

@@ -0,0 +1,108 @@
+/-
+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.TruncatedAlgorithm
+import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length
+
+/-!
+# Tests for the interface of Theorem D.1 at truncation order `ℓ`
+
+The interface is not vacuous: for networks with at most `C` edges and descriptors that are their
+own entries, direct summation meets its bound (`boundedAlgorithm`). The guard holds on a small
+network, and on admissible inputs from the size `4 (C D + 1)` on.
+-/
+
+@[expose] public section
+
+namespace ComplexityTests.TensorNetworkTruncatedAlgorithm
+
+open Cslib Cslib.GenericRAM Cslib.Circuits.Frontier Turing.MultiTapeTM
+
+/-- A descriptor is its own entry, whatever the bits. -/
+def constEntry (t : List ℕ) (_ : List Bool) : List ℕ := t
+
+/-- The entry certificate of constant descriptors. -/
+noncomputable def constCert :
+    NativeCertificate (fun q : List ℕ × List Bool => constEntry q.1 q.2)
+      (encPair (encList encNat) encBits) (encList encNat) :=
+  NativeCertificate.ofPolyTime (ComputableInPolyTime.fst _ _)
+
+/-- Networks with at most `C` edges. -/
+def BoundedEdges (C _s : ℕ) (G : ℕ × DescribedNetwork (List ℕ)) : Prop := G.2.numEdges ≤ C
+
+/-- **The interface is not vacuous**: direct summation is a truncated contraction algorithm for
+networks with boundedly many edges. -/
+noncomputable def boundedAlgorithm :
+    TruncatedContractionAlgorithm (encList encNat) constEntry BoundedEdges where
+  certificate := truncDirectCertificate constEntry constCert
+  bound C _ := by
+    obtain ⟨K, hK⟩ := truncDirectCertificate_le (encT := encList encNat) constEntry constCert
+    obtain ⟨p, hp, hm, hb⟩ := exists_mono_poly_cert
+      (ComputableInPolyTime.fst (encList encNat) encBits)
+    let F : ℕ → ℕ := fun n => K * (n + p (3 * n + 1) + 1) ^ K * 2 ^ C * (p (3 * n + 1) + 1)
+    have hF : PolyBounded id F :=
+      ((((PolyBounded.const K).mul (((PolyBounded.self.add
+        ((PolyBounded.of_polynomiallyBounded id hp).comp (((PolyBounded.const 3).mul
+          PolyBounded.self).add (PolyBounded.const 1)))).add (PolyBounded.const 1)).pow K)).mul
+        (PolyBounded.const (2 ^ C))).mul
+        (((PolyBounded.of_polynomiallyBounded id hp).comp (((PolyBounded.const 3).mul
+          PolyBounded.self).add (PolyBounded.const 1))).add (PolyBounded.const 1)))
+    obtain ⟨a, d, had⟩ := hF.exists_le
+    refine ⟨a + d, fun s P ℓ r G _ _ _ _ _ hA => ?_⟩
+    set n := (encTrunc (encList encNat) (P, ℓ, r, G)).length with hn
+    have hv : ∀ v ∈ G.vertices, ∀ bs : List Bool, bs.length = v.1.length →
+        constCert.time (v.2, bs) ≤ p (3 * n + 1) ∧ constCert.space (v.2, bs) ≤ p (3 * n + 1) := by
+      intro v hv bs hbs
+      have h1 := List.le_sum_of_mem
+        (List.mem_map_of_mem (f := fun a => (encPair (encList encNat) (encList encNat) a).length)
+          hv)
+      have h2 := sum_length_le_length_encList (encPair (encList encNat) (encList encNat))
+        G.vertices
+      have h3 := length_le_length_encList encNat v.1
+      have hG : (encList (encPair (encList encNat) (encList encNat)) G.vertices).length ≤ n := by
+        simp only [hn, encTrunc, DescribedNetwork.encDescribed, DescribedNetwork.equivProd,
+          encOfEquiv_apply, length_encPair]
+        simp
+        omega
+      have hvl : (encPair (encList encNat) (encList encNat) v).length ≤ n := by
+        omega
+      have hlen : (encPair (encList encNat) encBits (v.2, bs)).length ≤ 3 * n + 1 := by
+        simp only [length_encPair, encBits_apply] at hvl ⊢
+        omega
+      exact ⟨(hb _).1.trans (hm hlen), (hb _).2.trans (hm hlen)⟩
+    obtain ⟨hT, hS⟩ := hK (P, ℓ, r, G) _ _ hv
+    have h2 : 2 ^ G.numEdges ≤ 2 ^ C := Nat.pow_le_pow_right (by norm_num) hA
+    have hFn := had n
+    simp only [id] at hFn
+    have hK' : a * (n + 1) ^ d ≤ (a + d) * (n + 1) ^ (a + d) :=
+      Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right (by omega) (by omega))
+    have hX : (a + d) * (n + 1) ^ (a + d) ≤ (a + d) * (n + 1) ^ (a + d) *
+        2 ^ ((a + d) * s / Nat.sqrt (Nat.log 2 s)) :=
+      Nat.le_mul_of_pos_right _ Nat.one_le_two_pow
+    have hT' : (truncDirectCertificate constEntry constCert).time (P, ℓ, r, G) ≤ F n :=
+      hT.trans (Nat.mul_le_mul_right _ (Nat.mul_le_mul_left _ h2))
+    have hS' : (truncDirectCertificate constEntry constCert).space (P, ℓ, r, G) ≤ F n := by
+      refine hS.trans ?_
+      have h1 : 1 ≤ 2 ^ C * (p (3 * n + 1) + 1) := Nat.one_le_iff_ne_zero.mpr (by positivity)
+      calc K * (n + p (3 * n + 1) + 1) ^ K ≤ K * (n + p (3 * n + 1) + 1) ^ K *
+            (2 ^ C * (p (3 * n + 1) + 1)) := Nat.le_mul_of_pos_right _ h1
+        _ = F n := by simp only [F]; ring
+    exact ⟨by omega, by omega⟩
+
+-- The guard holds on a network with one edge and one vertex at truncation order `2`.
+example : truncGuard (1, 2, 0, (⟨1, [([0], [1, 1])]⟩ : DescribedNetwork (List ℕ))) = true := by
+  decide
+
+-- Admissible inputs pass the guard from the size `4 (C D + 1)` on.
+example {C D s P ℓ r : ℕ} {G : DescribedNetwork (List ℕ)} (hs : 4 * (C * D + 1) ≤ s)
+    (hℓ : ℓ ≤ D * s) (hk : G.vertices.length ≤ C * s) (hm : s ≤ G.numEdges) :
+    truncGuard (P, ℓ, r, G) = true :=
+  truncGuard_of_le hs hℓ hk hm
+
+end ComplexityTests.TensorNetworkTruncatedAlgorithm

ComplexityTests/Computability/Circuit/Frontier/TensorNetworkTruncatedEntry.lean

@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: local-only (test driver)
+
+public import Complexity.Computability.Complexity.Classes.CountingSimulation.TruncatedEntry
+
+/-!
+# Tests for Theorem D.1 at truncation order `ℓ` for entry procedures
+
+A network of two parallel edges between a row vertex and a column vertex is admissible at size `2`
+with the entry procedure of tables, with its two vertices (`TruncEntryAdmissible` is not vacuous);
+its specialization at a point is rows-first and admissible for the specialized entries; and the
+truncated contraction algorithm for entry procedures, instantiated at the entry procedure of
+tables, has no remaining hypothesis.
+-/
+
+@[expose] public section
+
+namespace ComplexityTests.TensorNetworkTruncatedEntry
+
+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])]⟩
+
+/-- `⌈2 ^ (9/10)⌉ = 2`. -/
+theorem ceilNineTenths_two : ceilNineTenths 2 = 2 :=
+  le_antisymm (ceilNineTenths_le (by norm_num)) ((le_ceilNineTenths_iff (by norm_num)).2
+    (by norm_num))
+
+/-- The network is admissible at size `2` with the entry procedure of tables, for some constant. -/
+theorem exists_entryAdmissible_twoEdges :
+    ∃ C, 1 ≤ C ∧ EntryAdmissible tableEntryCertificate C 2 (1, twoEdges) := by
+  obtain ⟨C₀, hC₀⟩ := exists_entryAdmissible_of_isPolynomial
+    tableEntryCertificate_isPolynomial
+  refine ⟨C₀ + 1, by omega, hC₀ (C₀ + 1) 2 1 twoEdges (by omega) (by decide) le_rfl (by simp) ?_⟩
+  intro v hv
+  rw [ceilNineTenths_two]
+  simp only [List.mem_cons, List.not_mem_nil, or_false] at hv
+  rcases hv with rfl | rfl <;> rfl
+
+/-! ### Admissibility is not vacuous -/
+
+-- With its two vertices, the network is admissible for Theorem D.1 at truncation order `ℓ`.
+example : ∃ C, TruncEntryAdmissible tableEntryCertificate C 2 (1, twoEdges) := by
+  obtain ⟨C, hC1, hC⟩ := exists_entryAdmissible_twoEdges
+  exact ⟨C, hC, by simp only [List.length_cons, List.length_nil]; omega⟩
+
+/-! ### Specialization -/
+
+-- Specializing at the point `U` of `A_3 = (ℤ / 8)[U] / (U ^ 2 + U + 1)` keeps the network
+-- rows-first.
+example : (DescribedNetwork.specNet 3 2 [1, 1] [0, 1] twoEdges).IsRowsFirstBipartite 1 := by
+  decide
+
+-- Specialization keeps the network admissible, for the specialized entries.
+example : ∃ C', EntryAdmissible (specEntryCertificate tableEntry tableEntryCertificate) C' 2
+    (1, DescribedNetwork.specNet 3 2 [1, 1] [0, 1] twoEdges) := by
+  obtain ⟨C, -, hC⟩ := exists_entryAdmissible_twoEdges
+  obtain ⟨C', hC'⟩ := exists_entryAdmissible_specNet tableEntryCertificate C
+  exact ⟨C', hC' 2 3 2 1 [1, 1] [0, 1] twoEdges hC⟩
+
+/-! ### The truncated contraction algorithm -/
+
+/-- The truncated contraction algorithm for the entry procedure of tables, with no remaining
+hypothesis. Its certificate computes the contraction in `B_{P,ℓ}` on every input, by its type. -/
+noncomputable def tableTruncAlgorithm :
+    TruncatedContractionAlgorithm (encList encNat) tableEntry
+      (TruncEntryAdmissible tableEntryCertificate) :=
+  truncEntryContractionAlgorithm tableEntryCertificate
+
+-- Its bound holds for all constants.
+example (C D : ℕ) : ∃ K : ℕ, ∀ (s P ℓ r : ℕ) (G : DescribedNetwork (List ℕ)), 2 ≤ s → 1 ≤ P →
+    P ≤ D * s → 1 ≤ ℓ → ℓ ≤ D * s → TruncEntryAdmissible tableEntryCertificate C s (r, G) →
+      tableTruncAlgorithm.certificate.time (P, ℓ, r, G) ≤
+          K * ((encTrunc (encList encNat) (P, ℓ, r, G)).length + 1) ^ K *
+            2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) ∧
+        tableTruncAlgorithm.certificate.space (P, ℓ, r, G) ≤
+          K * ((encTrunc (encList encNat) (P, ℓ, r, G)).length + 1) ^ K :=
+  tableTruncAlgorithm.bound C D
+
+end ComplexityTests.TensorNetworkTruncatedEntry