diff --git a/Complexity.lean b/Complexity.lean index 22abea106..5a811ed4b 100644 --- a/Complexity.lean +++ b/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 diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Truncated.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Truncated.lean new file mode 100644 index 000000000..f6c9515e4 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Truncated.lean @@ -0,0 +1,396 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContraction +public import Complexity.Computability.PolyTime.GaloisRingInterpolation +import Complexity.Computability.Circuit.Frontier.TensorNetwork.DescribedLift +import Complexity.Computability.Circuit.Frontier.TensorNetwork.NativeRecovery +import Complexity.Computability.PolyTime.GaloisRingSeries +import Complexity.Foundations.Data.Polynomial.RingLagrange +import Mathlib.Algebra.Polynomial.BigOperators +import Mathlib.Data.List.GetD +import Mathlib.RingTheory.Ideal.Quotient.Operations + +/-! +# Contraction at truncation order `ℓ`, by evaluation and interpolation + +Theorem D.1 of [OpenAI2026ETH] (p. 53) contracts Boolean tensor networks whose entries lie in +`B_{P,ℓ} = (ℤ / 2 ^ P)[V] / (V ^ ℓ)`. This file gives that contraction for described networks +(`DescribedNetwork T`) and reduces it to contractions over `A_P = (ℤ / 2 ^ P)[U] / (f)` of networks +with the same ports, by evaluating `V` at points of `A_P` and interpolating. + +**Entries and the contraction.** An entry is a list of natural numbers, its coefficients of +`1, V, V ^ 2, …` (`coeffPoly`). The contraction over `ℕ[V]` of the entries +(`DescribedNetwork.polyContraction`) has, below `V ^ ℓ` and modulo `2 ^ P`, the coefficients of +the contraction in `B_{P,ℓ}` (`DescribedNetwork.truncContraction`): they depend only on the images +of the entries in `B_{P,ℓ}`, their coefficients below `ℓ` modulo `2 ^ P` +(`DescribedNetwork.truncContraction_congr`). So `truncContraction` is the `B_{P,ℓ}` contraction of +the canonical lifts of the entries, as in §D.4.1 (p. 58). + +**Evaluation.** Cutting the entries to `ℓ` coefficients (`cutCoeffs`, +`DescribedNetwork.truncContraction_cutCoeffs`) +bounds the degree of the contraction over `ℕ[V]` by `(ℓ - 1) k` for `k` vertices +(`DescribedNetwork.natDegree_polyContraction_le`). The network specialized at a point `ζ` of +`A_P` (`DescribedNetwork.specNet`) has the same ports, and its entry at a vertex is the value at +`ζ` of the first `ℓ` coefficients of the original entry, by Horner's rule (`specEntry`). Its +contraction in `A_P` is the contraction over `ℕ[V]` evaluated at `ζ` +(`DescribedNetwork.val_contraction_specNet`). + +**Interpolation.** At `n` points of `A_P` with unit differences, the Lagrange interpolant of the +values (`GaloisRingArith.interp`) is a polynomial of degree below `n` agreeing with the contraction +at the points. When `(ℓ - 1) k < n` it is the contraction, so the constant coordinates of its first +`ℓ` coefficients, modulo `2 ^ P`, are the truncated contraction (`interpRecover`, +`DescribedNetwork.interpRecover_eq_truncContraction`). The binary digits of `0, …, n - 1` are such +points once `n ≤ 2 ^ deg f` and `f` is irreducible modulo `2` (`isUnit_val_sub_digits`). + +**The reduction** (`DescribedNetwork.interpContract`). Given a contraction `core` over `A_P` of the +specialized networks, contract the network specialized at each of the `(ℓ - 1) k + 1` digit +points and interpolate. If `core` is correct at those inputs, this is the truncated contraction +(`DescribedNetwork.interpContract_eq`). This route is not the manuscript's, which embeds the +entries into `A = O[V] / (V ^ ℓ)` and computes there throughout the recursion (§D.4.1, p. 57, and +the proof of Theorem D.1, §D.4.7, p. 64); it reduces truncation order `ℓ` to `ℓ = 1` over `A_P` +and leaves the recursion unchanged. + +This file proves correctness only. The native machine running the reduction, with the time and +space bounds of Theorem D.1, is not formalized here (#1538). + +## Main definitions + +* `Cslib.Circuits.Frontier.coeffPoly`: the polynomial of a list of coefficients. +* `Cslib.Circuits.Frontier.cutCoeffs`: the first `ℓ` coefficients. +* `Cslib.Circuits.Frontier.DescribedNetwork.polyContraction`: the contraction over `ℕ[V]`. +* `Cslib.Circuits.Frontier.DescribedNetwork.truncContraction`: the contraction in `B_{P,ℓ}`. +* `Cslib.Circuits.Frontier.specEntry`, `Cslib.Circuits.Frontier.DescribedNetwork.specNet`: the + network specialized at a point. +* `Cslib.Circuits.Frontier.interpRecover`: reading the truncated contraction off an interpolant. +* `Cslib.Circuits.Frontier.DescribedNetwork.interpContract`: the reduction to `ℓ = 1` over `A_P`. + +## Main results + +* `Cslib.Circuits.Frontier.DescribedNetwork.truncContraction_congr`: the contraction depends only + on the entries in `B_{P,ℓ}`. +* `Cslib.Circuits.Frontier.DescribedNetwork.natDegree_polyContraction_le`: the degree bound. +* `Cslib.Circuits.Frontier.DescribedNetwork.val_contraction_specNet`: specialization is + evaluation. +* `Cslib.Circuits.Frontier.interpRecover_eq`: recovery from values at points with unit + differences. +* `Cslib.Circuits.Frontier.DescribedNetwork.interpRecover_eq_truncContraction`: the truncated + contraction from the specialized contractions. +* `Cslib.Circuits.Frontier.DescribedNetwork.interpContract_eq`: the reduction is correct. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Theorem D.1 (p. 53), + §D.4.1 (pp. 57–58) and §D.4.7 (p. 64). +-/ + +public section + +namespace Cslib.Circuits.Frontier + +open Polynomial Finset GaloisRingArith + +/-! ### Entries as polynomials in `V` -/ + +/-- The polynomial `∑ i, c_i V ^ i` of a list of natural coefficients, constant first. -/ +@[expose] noncomputable def coeffPoly (c : List ℕ) : ℕ[X] := + ∑ i ∈ range c.length, C (c.getD i 0) * X ^ i + +/-- The coefficients of `coeffPoly c` are the entries of `c`, and zero past its end. -/ +@[simp] theorem coeff_coeffPoly (c : List ℕ) (j : ℕ) : (coeffPoly c).coeff j = c.getD j 0 := by + rw [coeffPoly, finsetSum_coeff] + simp only [coeff_C_mul, coeff_X_pow, mul_ite, mul_one, mul_zero, sum_ite_eq, mem_range] + split_ifs with h + · rfl + · rw [List.getD_eq_default _ _ (by omega)] + +/-- `coeffPoly c` has degree below the length of `c`. -/ +theorem natDegree_coeffPoly_le (c : List ℕ) : (coeffPoly c).natDegree ≤ c.length - 1 := + natDegree_le_iff_coeff_eq_zero.mpr fun N hN => by + rw [coeff_coeffPoly, List.getD_eq_default _ _ (by + have : c.length - 1 < N := by exact_mod_cast hN + omega)] + +/-- The first `ℓ` coefficients of a list, padded with zeros to length `ℓ`. -/ +@[expose] def cutCoeffs (ℓ : ℕ) (c : List ℕ) : List ℕ := (List.range ℓ).map fun i => c.getD i 0 + +@[simp] theorem length_cutCoeffs (ℓ : ℕ) (c : List ℕ) : (cutCoeffs ℓ c).length = ℓ := by + simp [cutCoeffs] + +/-- Below `ℓ`, the cut list has the coefficients of the list. -/ +theorem getD_cutCoeffs (c : List ℕ) {ℓ i : ℕ} (hi : i < ℓ) : + (cutCoeffs ℓ c).getD i 0 = c.getD i 0 := by + rw [cutCoeffs, List.getD_eq_getElem _ _ (by simpa using hi), List.getElem_map, + List.getElem_range] + +/-! ### The contraction in `B_{P,ℓ}` -/ + +/-- The map `ℕ[V] → (ℤ / 2 ^ P)[V] / (V ^ ℓ)` onto `B_{P,ℓ}`. -/ +noncomputable def truncHom (P ℓ : ℕ) : + ℕ[X] →+* (ZMod (2 ^ P))[X] ⧸ Ideal.span {(X ^ ℓ : (ZMod (2 ^ P))[X])} := + (Ideal.Quotient.mk _).comp (mapRingHom (Nat.castRingHom (ZMod (2 ^ P)))) + +/-- **Two polynomials have the same image in `B_{P,ℓ}`** exactly when their coefficients below +`ℓ` agree modulo `2 ^ P`. -/ +theorem truncHom_eq_iff {P ℓ : ℕ} {p q : ℕ[X]} : + truncHom P ℓ p = truncHom P ℓ q ↔ ∀ j < ℓ, p.coeff j % 2 ^ P = q.coeff j % 2 ^ P := by + rw [truncHom, RingHom.comp_apply, RingHom.comp_apply, Ideal.Quotient.eq, + Ideal.mem_span_singleton, X_pow_dvd_iff] + refine forall₂_congr fun j _ => ?_ + rw [coeff_sub, sub_eq_zero, coe_mapRingHom, coeff_map, coeff_map] + exact ZMod.natCast_eq_natCast_iff' _ _ _ + +namespace DescribedNetwork + +variable {T : Type*} + +/-- **The contraction over `ℕ[V]`** of a network whose entries are lists of coefficients of +`1, V, V ^ 2, …`. -/ +@[expose] noncomputable def polyContraction (entry : T → List Bool → List ℕ) + (G : DescribedNetwork T) : ℕ[X] := + G.contraction fun t bs => coeffPoly (entry t bs) + +/-- **The contraction in `B_{P,ℓ} = (ℤ / 2 ^ P)[V] / (V ^ ℓ)`**, as its `ℓ` coefficients in +`[0, 2 ^ P)`: the coefficients below `ℓ` of the contraction over `ℕ[V]`, modulo `2 ^ P`. -/ +@[expose] noncomputable def truncContraction (entry : T → List Bool → List ℕ) (P ℓ : ℕ) + (G : DescribedNetwork T) : List ℕ := + (List.range ℓ).map fun j => (G.polyContraction entry).coeff j % 2 ^ P + +/-- The image of the contraction over `ℕ[V]` in `B_{P,ℓ}` is the contraction of the images. -/ +theorem truncHom_polyContraction (entry : T → List Bool → List ℕ) (P ℓ : ℕ) + (G : DescribedNetwork T) : + truncHom P ℓ (G.polyContraction entry) = + G.contraction fun t bs => truncHom P ℓ (coeffPoly (entry t bs)) := + map_contraction _ _ G + +/-- **The contraction depends only on the entries in `B_{P,ℓ}`**: entries whose coefficients +below `ℓ` agree modulo `2 ^ P` have the same truncated contraction. -/ +theorem truncContraction_congr {entry entry' : T → List Bool → List ℕ} {P ℓ : ℕ} + (G : DescribedNetwork T) + (h : ∀ t bs, ∀ i < ℓ, (entry t bs).getD i 0 % 2 ^ P = (entry' t bs).getD i 0 % 2 ^ P) : + G.truncContraction entry P ℓ = G.truncContraction entry' P ℓ := by + have hG : truncHom P ℓ (G.polyContraction entry) = truncHom P ℓ (G.polyContraction entry') := by + rw [truncHom_polyContraction, truncHom_polyContraction] + congr 1 + funext t bs + exact truncHom_eq_iff.mpr fun j hj => by simpa only [coeff_coeffPoly] using h t bs j hj + refine List.map_congr_left fun j hj => truncHom_eq_iff.mp hG j (List.mem_range.mp hj) + +/-- Cutting the entries to their first `ℓ` coefficients does not change the truncated +contraction. -/ +theorem truncContraction_cutCoeffs (entry : T → List Bool → List ℕ) (P ℓ : ℕ) + (G : DescribedNetwork T) : + G.truncContraction (fun t bs => cutCoeffs ℓ (entry t bs)) P ℓ = G.truncContraction entry P ℓ := + truncContraction_congr G fun t bs i hi => by rw [getD_cutCoeffs _ hi] + +/-- **The degree bound**: if every entry has at most `ℓ` coefficients, the contraction over +`ℕ[V]` has degree at most `(ℓ - 1) k` for `k` vertices. -/ +theorem natDegree_polyContraction_le {entry : T → List Bool → List ℕ} {ℓ : ℕ} + (G : DescribedNetwork T) (h : ∀ t bs, (entry t bs).length ≤ ℓ) : + (G.polyContraction entry).natDegree ≤ (ℓ - 1) * G.vertices.length := by + refine natDegree_sum_le_of_forall_le _ _ fun x _ => (natDegree_list_prod_le _).trans ?_ + rw [List.map_map] + refine (List.sum_le_length_nsmul _ (ℓ - 1) fun d hd => ?_).trans (by simp [mul_comm]) + obtain ⟨v, -, rfl⟩ := List.mem_map.mp hd + exact (natDegree_coeffPoly_le _).trans (Nat.sub_le_sub_right (h _ _) 1) + +end DescribedNetwork + +/-! ### Specialization at a point of `A_P` -/ + +/-- The descriptor of a vertex of a network specialized at a point: the original descriptor with +the precision `P`, the truncation order `ℓ`, the coefficients `fl` of the modulus and the point +`ζ`, a coefficient list of `A_P = (ℤ / 2 ^ P)[U] / (f)`. -/ +abbrev SpecDesc (T : Type*) : Type _ := T × ℕ × ℕ × List ℕ × List ℕ + +/-- The first `ℓ` coefficients of a list, each as a constant coefficient list of `A_P`. -/ +@[expose] def constCoeffs (ℓ : ℕ) (c : List ℕ) : List (List ℕ) := + (List.range ℓ).map fun i => [c.getD i 0] + +variable {T : Type*} + +/-- **The entry of a specialized descriptor** `(t, P, ℓ, fl, ζ)`: the value at `ζ` in `A_P`, by +Horner's rule, of the first `ℓ` coefficients of the entry of `t`. -/ +@[expose] def specEntry (entry : T → List Bool → List ℕ) (d : SpecDesc T) (bs : List Bool) : + List ℕ := + peval d.2.1 d.2.2.2.1 (constCoeffs d.2.2.1 (entry d.1 bs)) d.2.2.2.2 + +/-- Constant coefficient lists represent the polynomial of the coefficients in `A_p`. -/ +theorem pval_constCoeffs (p ℓ : ℕ) (fl c : List ℕ) : + pval p fl (constCoeffs ℓ c) = + (coeffPoly (cutCoeffs ℓ c)).map (Nat.castRingHom (Ring p fl)) := by + rw [pval, coeffPoly, Polynomial.map_sum, constCoeffs, List.length_map, length_cutCoeffs, + List.length_range] + refine sum_congr rfl fun k hk => ?_ + rw [List.getD_eq_getElem _ _ (by simpa using hk), List.getElem_map, List.getElem_range, + val_singleton, getD_cutCoeffs _ (mem_range.mp hk)] + simp + +/-- **A specialized entry is the evaluation at the point** of the polynomial of the first `ℓ` +coefficients. -/ +theorem val_specEntry (entry : T → List Bool → List ℕ) (t : T) (P ℓ : ℕ) (fl ζ : List ℕ) + (bs : List Bool) : + val P fl (specEntry entry (t, P, ℓ, fl, ζ) bs) = + ((coeffPoly (cutCoeffs ℓ (entry t bs))).map (Nat.castRingHom (Ring P fl))).eval + (val P fl ζ) := by + rw [specEntry, peval_eq, pval_constCoeffs] + +namespace DescribedNetwork + +/-- **The network specialized at a point `ζ`**: the same ports, with each descriptor `t` +replaced by `(t, P, ℓ, fl, ζ)`. -/ +@[expose] def specNet (P ℓ : ℕ) (fl ζ : List ℕ) (G : DescribedNetwork T) : + DescribedNetwork (SpecDesc T) := + ⟨G.numEdges, G.vertices.map fun v => (v.1, (v.2, P, ℓ, fl, ζ))⟩ + +@[simp] theorem numEdges_specNet (P ℓ : ℕ) (fl ζ : List ℕ) (G : DescribedNetwork T) : + (specNet P ℓ fl ζ G).numEdges = G.numEdges := rfl + +@[simp] theorem vertices_specNet (P ℓ : ℕ) (fl ζ : List ℕ) (G : DescribedNetwork T) : + (specNet P ℓ fl ζ G).vertices = G.vertices.map fun v => (v.1, (v.2, P, ℓ, fl, ζ)) := rfl + +/-- The contraction of a specialized network, for any evaluator, is that of the original network +with the evaluator read at the specialized descriptors. -/ +theorem contraction_specNet {R : Type*} [CommSemiring R] (eval : SpecDesc T → List Bool → R) + (P ℓ : ℕ) (fl ζ : List ℕ) (G : DescribedNetwork T) : + (specNet P ℓ fl ζ G).contraction eval = G.contraction fun t bs => eval (t, P, ℓ, fl, ζ) bs := by + simp only [contraction, vertices_specNet, List.map_map, Function.comp_def] + rfl + +/-- **Specialization is evaluation**: the contraction in `A_P` of the network specialized at `ζ` +is the contraction over `ℕ[V]` of the entries cut to `ℓ` coefficients, evaluated at `ζ`. -/ +theorem val_contraction_specNet (entry : T → List Bool → List ℕ) (P ℓ : ℕ) (fl ζ : List ℕ) + (G : DescribedNetwork T) : + (specNet P ℓ fl ζ G).contraction (fun d bs => val P fl (specEntry entry d bs)) = + ((G.polyContraction fun t bs => cutCoeffs ℓ (entry t bs)).map + (Nat.castRingHom (Ring P fl))).eval (val P fl ζ) := by + rw [contraction_specNet] + have h := map_contraction ((evalRingHom (val P fl ζ)).comp + (mapRingHom (Nat.castRingHom (Ring P fl)))) (fun t bs => coeffPoly (cutCoeffs ℓ (entry t bs))) + G + simp only [RingHom.comp_apply, coe_evalRingHom, coe_mapRingHom] at h + rw [polyContraction, h] + simp only [val_specEntry] + +end DescribedNetwork + +/-! ### Recovery by interpolation -/ + +/-- **Reading the truncated contraction off an interpolant**: interpolate the values `ys` at the +points `pts` and take the constant coordinates, modulo `2 ^ P`, of the first `ℓ` coefficients. -/ +@[expose] def interpRecover (P ℓ : ℕ) (fl : List ℕ) (pts ys : List (List ℕ)) : List ℕ := + (List.range ℓ).map fun j => ((interp P fl pts ys).getD j []).getD 0 0 % 2 ^ P + +/-- An irreducible modulus has positive degree. -/ +theorem length_pos_of_irreducible {fl : List ℕ} + (hirr : Irreducible ((monicOf fl).map (Int.castRingHom (ZMod 2)))) : 0 < fl.length := by + refine Nat.pos_of_ne_zero fun h => hirr.not_isUnit ?_ + simp [monicOf, h] + +/-- **Recovery from values at points with unit differences.** If `Z` over `ℕ` has degree below the +number of points, the points have unit differences in `A_P`, and `ys` are the values of `Z` at +them, then reading off the interpolant gives the coefficients of `Z` below `ℓ` modulo `2 ^ P`. -/ +theorem interpRecover_eq {P ℓ : ℕ} {fl : List ℕ} + (hirr : Irreducible ((monicOf fl).map (Int.castRingHom (ZMod 2)))) {pts ys : List (List ℕ)} + (hunit : Pairwise fun i j : Fin pts.length => + IsUnit (val P fl (pts.getD i []) - val P fl (pts.getD j []))) + {Z : ℕ[X]} (hdeg : Z.natDegree < pts.length) + (hys : ∀ i < pts.length, val P fl (ys.getD i []) = + (Z.map (Nat.castRingHom (Ring P fl))).eval (val P fl (pts.getD i []))) : + interpRecover P ℓ fl pts ys = (List.range ℓ).map fun j => Z.coeff j % 2 ^ P := by + set Z' := Z.map (Nat.castRingHom (Ring P fl)) + set ζ : Fin pts.length → Ring P fl := fun i => val P fl (pts.getD i []) + -- The native interpolant is the interpolant of the values, which is `Z'`. + obtain ⟨g, hg⟩ := NativeRecovery.exists_pval_interp_eq_add hirr (RingHom.id _) ζ hunit pts rfl + (fun _ => rfl) (fun i => val P fl (ys.getD i [])) ys P fun _ => ⟨0, by simp⟩ + have h2 : (2 : Ring P fl) ^ P = 0 := by exact_mod_cast natCast_two_pow (p := P) (fl := fl) + rw [h2, C_0, zero_mul, add_zero, Polynomial.map_id] at hg + have hdeg' : Z'.degree < #(univ : Finset (Fin pts.length)) := by + rw [card_univ, Fintype.card_fin] + exact (degree_map_le.trans degree_le_natDegree).trans_lt (by exact_mod_cast hdeg) + have hZ : Z' = Lagrange.ringInterpolate univ ζ fun i => val P fl (ys.getD i []) := by + conv_lhs => rw [Lagrange.eq_ringInterpolate (fun i _ j _ hij => hunit hij) hdeg'] + congr 1 + funext i + exact (hys i i.2).symm + have hpval : pval P fl (interp P fl pts ys) = Z' := hg.trans hZ.symm + refine List.map_congr_left fun j _ => ?_ + have hval : val P fl ((interp P fl pts ys).getD j []) = val P fl [Z.coeff j] := by + rw [← NativeRecovery.coeff_pval, hpval, val_singleton, coeff_map, eq_natCast] + simpa using mod_eq_of_val_eq hval (length_pos_of_irreducible hirr) + +/-- **The binary digits are interpolation points of `A_P`.** The binary digits below +`e = fl.length` of `0, …, n - 1`, for `n ≤ 2 ^ e` and `f` irreducible modulo `2`, have unit +differences in `A_P`. -/ +theorem isUnit_val_sub_digits {P : ℕ} {fl : List ℕ} + (hirr : Irreducible ((monicOf fl).map (Int.castRingHom (ZMod 2)))) {n : ℕ} + (hn : n ≤ 2 ^ fl.length) : + Pairwise fun i j : Fin ((List.range n).map (FastContraction.digits fl.length)).length => + IsUnit (val P fl (((List.range n).map (FastContraction.digits fl.length)).getD i []) - + val P fl (((List.range n).map (FastContraction.digits fl.length)).getD j [])) := + fun i j hij => by + have h := (pairwise_isUnit_liftO_sub_digits hirr hn hij).map + (AdjoinRoot.reduction (monic_monicOf fl) hirr P) + rwa [map_sub, reduction_liftO, reduction_liftO] at h + +namespace DescribedNetwork + +/-- The number `(ℓ - 1) k + 1` of interpolation points for truncation order `ℓ` and `k` +vertices. -/ +@[expose] def pointCount (ℓ : ℕ) (G : DescribedNetwork T) : ℕ := (ℓ - 1) * G.vertices.length + 1 + +/-- **The truncated contraction from the specialized contractions.** At points with unit +differences in `A_P`, more than `(ℓ - 1) k` of them, if `ys` are the contractions in `A_P` of the +network specialized at the points, reading off the interpolant gives the truncated contraction. -/ +theorem interpRecover_eq_truncContraction {entry : T → List Bool → List ℕ} {P ℓ : ℕ} + {fl : List ℕ} (hirr : Irreducible ((monicOf fl).map (Int.castRingHom (ZMod 2)))) + (G : DescribedNetwork T) {pts ys : List (List ℕ)} + (hunit : Pairwise fun i j : Fin pts.length => + IsUnit (val P fl (pts.getD i []) - val P fl (pts.getD j []))) + (hlen : (ℓ - 1) * G.vertices.length < pts.length) + (hys : ∀ i < pts.length, val P fl (ys.getD i []) = + (specNet P ℓ fl (pts.getD i []) G).contraction fun d bs => val P fl (specEntry entry d bs)) : + interpRecover P ℓ fl pts ys = G.truncContraction entry P ℓ := by + rw [← truncContraction_cutCoeffs] + exact interpRecover_eq hirr hunit + ((natDegree_polyContraction_le G fun _ _ => (length_cutCoeffs _ _).le).trans_lt hlen) + fun i hi => (hys i hi).trans (val_contraction_specNet entry P ℓ fl _ G) + +/-- **The reduction to `ℓ = 1` over `A_P`**: contract, with `core`, the network specialized at +each of the `(ℓ - 1) k + 1` binary-digit points of `A_P` for the modulus `fl`, and read the +truncated contraction off the interpolant. The input of `core` is the precision, the modulus, the +number `r` of rows and the specialized network. -/ +@[expose] def interpContract (core : ℕ × List ℕ × ℕ × DescribedNetwork (SpecDesc T) → List ℕ) + (fl : List ℕ) (P ℓ r : ℕ) (G : DescribedNetwork T) : List ℕ := + interpRecover P ℓ fl ((List.range (pointCount ℓ G)).map (FastContraction.digits fl.length)) + (((List.range (pointCount ℓ G)).map (FastContraction.digits fl.length)).map fun ζ => + core (P, fl, r, specNet P ℓ fl ζ G)) + +/-- **The reduction is correct.** If `f` is irreducible modulo `2`, `A_P` has at least +`(ℓ - 1) k + 1` residues, and `core` computes the contraction in `A_P` of the network specialized +at each digit point, then `interpContract` is the truncated contraction. -/ +theorem interpContract_eq {entry : T → List Bool → List ℕ} + {core : ℕ × List ℕ × ℕ × DescribedNetwork (SpecDesc T) → List ℕ} {fl : List ℕ} {P ℓ r : ℕ} + (hirr : Irreducible ((monicOf fl).map (Int.castRingHom (ZMod 2)))) + (G : DescribedNetwork T) (hn : pointCount ℓ G ≤ 2 ^ fl.length) + (hcore : ∀ k < pointCount ℓ G, + val P fl (core (P, fl, r, specNet P ℓ fl (FastContraction.digits fl.length k) G)) = + (specNet P ℓ fl (FastContraction.digits fl.length k) G).contraction + fun d bs => val P fl (specEntry entry d bs)) : + interpContract core fl P ℓ r G = G.truncContraction entry P ℓ := by + refine interpRecover_eq_truncContraction hirr G (isUnit_val_sub_digits hirr hn) + (by simp [pointCount]) fun i hi => ?_ + have hi' : i < pointCount ℓ G := by simpa using hi + rw [List.getD_eq_getElem _ _ (by simpa using hi), List.getElem_map, List.getElem_map, + List.getD_eq_getElem _ _ (by simpa using hi), List.getElem_map, List.getElem_range] + exact hcore i hi' + +end DescribedNetwork + +end Cslib.Circuits.Frontier diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedAlgorithm.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedAlgorithm.lean new file mode 100644 index 000000000..756451d70 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedAlgorithm.lean @@ -0,0 +1,445 @@ +/- +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.TruncatedResources +import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionPolyTime +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeNatFrontends +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary + +/-! +# Theorem D.1 at truncation order `ℓ`, from a contraction over `A_P` + +Theorem D.1 of [OpenAI2026ETH] (p. 53) contracts networks whose entries lie in +`B_{P,ℓ} = (ℤ / 2 ^ P)[V] / (V ^ ℓ)`. This file states its interface for described networks +(`Cslib.Circuits.Frontier.TruncatedContractionAlgorithm`) and assembles it +(`Cslib.Circuits.Frontier.TruncatedContractionAlgorithm.ofCore`) from a native contraction over +`A_P = (ℤ / 2 ^ P)[U] / (f)` of the specialized networks, at the modulus +`f = FastContraction.modulus m` of a network with `m` edges. + +**The interface.** One native certificate computes the truncated contraction +(`DescribedNetwork.truncContraction`) from `(P, ℓ, r, G)`, with `P` and `ℓ` in unary. 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 `1 ≤ P, ℓ ≤ D s`, it takes time at most +`K (n + 1) ^ K 2 ^ (K s / √⌊log₂ s⌋)` and space at most `K (n + 1) ^ K`, for the encoded length `n` +of the input. This is the shape of `Cslib.Complexity.CountingSimulation.ContractionAlgorithm`. + +**The assembly** branches on whether the modulus has enough residues for the +`N = (ℓ - 1) k + 1` interpolation points (`Cslib.Circuits.Frontier.truncGuard`): +* if `N ≤ 2 ^ deg f`, it runs the reduction of truncation order `ℓ` to `A_P` + (`engineCertificate`) around the given contraction over `A_P` + (`Cslib.Circuits.Frontier.fastTruncCertificate`); +* otherwise it sums directly (`truncDirectCertificate`). + +On admissible inputs with `k ≤ C s` vertices, `s ≤ m` and `ℓ ≤ D s`, the first branch is taken once +`s ≥ 4 (C D + 1)` (`Cslib.Circuits.Frontier.truncGuard_of_le`), since `deg f ≥ 4 ⌊log₂ m⌋`. Below +that size, direct summation costs a constant factor. + +**The hypotheses on the contraction over `A_P`** are those of the interface planned in #1538 for +milestone E1: it is correct on every network at the modulus of its number of edges, and meets the +bound of the interface on the networks admissible for it. The assembly also asks that the +specialized networks of admissible networks be admissible for it, and that the entries be computed +within time `poly(L) 2 ^ O(s)` and polynomial space for the encoded length `L` of the network (for +the small sizes). The reduction itself is ours, not the manuscript's; see +`Complexity/Computability/Circuit/Frontier/TensorNetwork/Truncated.lean`. + +## Main definitions + +* `Cslib.Circuits.Frontier.TruncatedContractionAlgorithm`: the interface. +* `Cslib.Circuits.Frontier.truncGuard`: whether the modulus has enough residues. +* `Cslib.Circuits.Frontier.fastTruncCertificate`: the reduction at the modulus of the network. +* `Cslib.Circuits.Frontier.TruncatedContractionAlgorithm.ofCore`: the assembly. + +## Main results + +* `Cslib.Circuits.Frontier.truncGuard_polyTime`: the guard is polynomial-time. +* `Cslib.Circuits.Frontier.truncGuard_of_le`: admissible inputs pass the guard from some size on. +* `Cslib.Circuits.Frontier.fastTruncCertificate_correct`: the reduction is correct on guarded + inputs. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Theorem D.1 (p. 53). +-/ + +public section + +namespace Cslib.Circuits.Frontier + +open Turing.MultiTapeTM Cslib.GenericRAM GaloisRingArith + +variable {T : Type} {encT : T ↪ List Bool} + +/-- **The interface of Theorem D.1 at truncation order `ℓ`** for described networks. One native +certificate computes the truncated contraction from `(P, ℓ, r, G)`, with `P` and `ℓ` in unary. 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 `1 ≤ P, ℓ ≤ D s`, the certificate's time is at most +`K (n + 1) ^ K 2 ^ (K s / √⌊log₂ s⌋)` and its space at most `K (n + 1) ^ K`, where `n` is the +encoded length of the input. Outside admissible inputs the certificate need only be correct. -/ +structure TruncatedContractionAlgorithm (encT : T ↪ List Bool) (entry : T → List Bool → List ℕ) + (Admissible : ℕ → ℕ → ℕ × DescribedNetwork T → Prop) where + /-- The native truncated contraction. -/ + certificate : NativeCertificate + (fun x : ℕ × ℕ × ℕ × DescribedNetwork T => x.2.2.2.truncContraction entry x.1 x.2.1) + (encTrunc encT) (encList encNat) + /-- Its time and space on admissible inputs. -/ + bound : ∀ C D : ℕ, ∃ K : ℕ, ∀ (s P ℓ r : ℕ) (G : DescribedNetwork T), 2 ≤ s → 1 ≤ P → + P ≤ D * s → 1 ≤ ℓ → ℓ ≤ D * s → Admissible C s (r, G) → + certificate.time (P, ℓ, r, G) ≤ K * ((encTrunc encT (P, ℓ, r, G)).length + 1) ^ K * + 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) ∧ + certificate.space (P, ℓ, r, G) ≤ K * ((encTrunc encT (P, ℓ, r, G)).length + 1) ^ K + +/-- A polynomial bound composed with a polynomially bounded size. -/ +private theorem polyBounded_comp_poly {α : Type} {size u : α → ℕ} {p : ℕ → ℕ} + (hp : Cslib.PolynomiallyBounded p) (hu : PolyBounded size u) : + PolyBounded size fun a => p (u a) := + (PolyBounded.of_polynomiallyBounded id hp).comp hu + +/-! ### The guard -/ + +/-- **The guard**: the modulus `FastContraction.modulus m` of the network has at least as many +residues as the `(ℓ - 1) k + 1` interpolation points. -/ +@[expose] def truncGuard (x : ℕ × ℕ × ℕ × DescribedNetwork T) : Bool := + decide (DescribedNetwork.pointCount x.2.1 x.2.2.2 ≤ + 2 ^ (FastContraction.modulus x.2.2.2.numEdges).length) + +/-- The network of an input. -/ +private theorem network_polyTime : + ComputableInPolyTime (fun x : ℕ × ℕ × ℕ × DescribedNetwork T => x.2.2.2) (encTrunc encT) + (DescribedNetwork.encDescribed encT) := + (ComputableInPolyTime.snd _ _).comp ((ComputableInPolyTime.snd _ _).comp + (ComputableInPolyTime.snd _ _)) + +/-- **The guard is polynomial-time.** -/ +theorem truncGuard_polyTime : + ComputableInPolyTime (truncGuard (T := T)) (encTrunc encT) encBool := by + have hpc : ComputableInPolyTime + (fun x : ℕ × ℕ × ℕ × DescribedNetwork T => DescribedNetwork.pointCount x.2.1 x.2.2.2) + (encTrunc encT) encNat := + ComputableInPolyTime.unary_to_binary.comp (pointCount_polyTime (encT := encT).comp + ((ComputableInPolyTime.const ([] : List ℕ)).prod ComputableInPolyTime.id')) + have h2 : ComputableInPolyTime + (fun x : ℕ × ℕ × ℕ × DescribedNetwork T => + 2 ^ (FastContraction.modulus x.2.2.2.numEdges).length) (encTrunc encT) encNat := + ComputableInPolyTime.binary_two_pow.comp ((ComputableInPolyTime.length_list _).comp + (FastContraction.modulus_polyTime.comp + (DescribedNetwork.numEdges_polyTime.comp network_polyTime))) + refine (ComputableInPolyTime.bool_not.comp (ComputableInPolyTime.binary_lt' h2 hpc)).of_enc_eq + fun x => congrArg encBool ?_ + simp only [truncGuard, Function.comp_apply] + by_cases h : DescribedNetwork.pointCount x.2.1 x.2.2.2 ≤ + 2 ^ (FastContraction.modulus x.2.2.2.numEdges).length + · simp [h, Nat.not_lt.mpr h] + · simp [h, Nat.lt_of_not_le h] + +/-- **Admissible inputs pass the guard from some size on.** With at most `C s` vertices, at least +`s` edges and `ℓ ≤ D s`, the guard holds once `s ≥ 4 (C D + 1)`: the modulus has degree at least +`4 ⌊log₂ m⌋`, so more than `m ^ 4 / 16 ≥ C D s ^ 2 + 1` residues. -/ +theorem truncGuard_of_le {C D s P ℓ r : ℕ} {G : DescribedNetwork T} (hs : 4 * (C * D + 1) ≤ s) + (hℓ : ℓ ≤ D * s) (hk : G.vertices.length ≤ C * s) (hm : s ≤ G.numEdges) : + truncGuard (P, ℓ, r, G) = true := by + simp only [truncGuard, decide_eq_true_eq] + set m := G.numEdges + have hlog : m < 2 ^ (Nat.log 2 m + 1) := Nat.lt_pow_succ_log_self one_lt_two m + have h4 : m ^ 4 < 2 ^ (4 * Nat.log 2 m) * 16 := by + calc m ^ 4 < (2 ^ (Nat.log 2 m + 1)) ^ 4 := Nat.pow_lt_pow_left hlog (by norm_num) + _ = 2 ^ (4 * Nat.log 2 m) * 16 := by rw [← pow_mul]; ring + have h5 : 2 ^ (4 * Nat.log 2 m) ≤ 2 ^ (FastContraction.modulus m).length := + Nat.pow_le_pow_right (by norm_num) (FastContraction.four_mul_log_le_length_modulus m) + have hsm : s ^ 4 ≤ m ^ 4 := Nat.pow_le_pow_left hm 4 + have hpc : DescribedNetwork.pointCount ℓ G ≤ D * s * (C * s) + 1 := by + have : (ℓ - 1) * G.vertices.length ≤ D * s * (C * s) := + Nat.mul_le_mul (by omega) hk + simp only [DescribedNetwork.pointCount] + omega + have hss : 16 * (C * D + 1) ≤ s * s := by nlinarith + have hkey : 16 * (D * s * (C * s) + 1) ≤ s ^ 4 := by + have e : s ^ 4 = s * s * (s * s) := by ring + have e2 : D * s * (C * s) = C * D * (s * s) := by ring + rw [e, e2] + have h1 : 1 ≤ s * s := by nlinarith + nlinarith + omega + +/-! ### The fast branch -/ + +/-- The input of the reduction at the modulus of the network. -/ +theorem modulusEdges_polyTime : + ComputableInPolyTime + (fun x : ℕ × ℕ × ℕ × DescribedNetwork T => + (FastContraction.modulus x.2.2.2.numEdges, x)) + (encTrunc encT) (encEngine encT) := + (FastContraction.modulus_polyTime.comp + (DescribedNetwork.numEdges_polyTime.comp network_polyTime)).prod ComputableInPolyTime.id' + +variable {core : ℕ × List ℕ × ℕ × DescribedNetwork (SpecDesc T) → List ℕ} + +/-- **The reduction at the modulus of the network**: the native reduction of truncation order `ℓ` +to contractions over `A_P`, with the modulus `FastContraction.modulus m` for `m` edges. -/ +@[expose] noncomputable def fastTruncCertificate + (cc : NativeCertificate core (encCore encT) (encList encNat)) : + NativeCertificate + (fun x : ℕ × ℕ × ℕ × DescribedNetwork T => + DescribedNetwork.interpContract core (FastContraction.modulus x.2.2.2.numEdges) x.1 x.2.1 + x.2.2.1 x.2.2.2) + (encTrunc encT) (encList encNat) := + ((engineCertificate core cc).comp (NativeCertificate.ofPolyTime modulusEdges_polyTime)).congr + fun _ => by simp only [Function.comp_apply] + +/-- **The reduction is correct on guarded inputs**, for a contraction over `A_P` that is correct +at the modulus of the number of edges. -/ +theorem fastTruncCertificate_correct {entry : T → List Bool → List ℕ} + (hval : ∀ (P r : ℕ) (G' : DescribedNetwork (SpecDesc T)), + val P (FastContraction.modulus G'.numEdges) (core (P, FastContraction.modulus G'.numEdges, + r, G')) = + G'.contraction fun d bs => + val P (FastContraction.modulus G'.numEdges) (specEntry entry d bs)) + (x : ℕ × ℕ × ℕ × DescribedNetwork T) (hg : truncGuard x = true) : + DescribedNetwork.interpContract core (FastContraction.modulus x.2.2.2.numEdges) x.1 x.2.1 + x.2.2.1 x.2.2.2 = x.2.2.2.truncContraction entry x.1 x.2.1 := by + simp only [truncGuard, decide_eq_true_eq] at hg + refine DescribedNetwork.interpContract_eq (FastContraction.irreducible_modulus _) _ hg + fun k _ => ?_ + have h := hval x.1 x.2.2.1 (DescribedNetwork.specNet x.1 x.2.1 + (FastContraction.modulus x.2.2.2.numEdges) + (FastContraction.digits (FastContraction.modulus x.2.2.2.numEdges).length k) x.2.2.2) + rw [DescribedNetwork.numEdges_specNet] at h + exact h + +/-! ### The assembly -/ + +/-- **Theorem D.1 at truncation order `ℓ`, from a contraction over `A_P`.** Let `cc` be a native +contraction over `A_P` of specialized networks that is correct on every network at the modulus +`FastContraction.modulus m` of its number `m` of edges (`hval`) and meets the interface's bound on +the networks admissible for it (`hcore`, for an admissibility `CoreAdm`). Suppose that the networks +specialized at the digit points of admissible networks are admissible for it (`htransfer`), that +admissible networks have between `s` and `C s` edges and at most `C s` vertices (`hshape`), and +that the entries take time `K (L + 1) ^ K 2 ^ (K s)` and space `K (L + 1) ^ K` on admissible +networks of encoded length `L` (`hentry`). Then branching on `truncGuard` to the reduction around +`cc` or to direct summation is a truncated contraction algorithm. -/ +noncomputable def TruncatedContractionAlgorithm.ofCore {entry : T → List Bool → List ℕ} + {Adm : ℕ → ℕ → ℕ × DescribedNetwork T → Prop} + {CoreAdm : ℕ → ℕ → ℕ × DescribedNetwork (SpecDesc T) → Prop} + (cc : NativeCertificate core (encCore encT) (encList encNat)) + (hval : ∀ (P r : ℕ) (G' : DescribedNetwork (SpecDesc T)), + val P (FastContraction.modulus G'.numEdges) (core (P, FastContraction.modulus G'.numEdges, + r, G')) = + G'.contraction fun d bs => + val P (FastContraction.modulus G'.numEdges) (specEntry entry d bs)) + (hcore : ∀ C D : ℕ, ∃ K : ℕ, ∀ (s P r : ℕ) (G' : DescribedNetwork (SpecDesc T)), 2 ≤ s → + 1 ≤ P → P ≤ D * s → CoreAdm C s (r, G') → + cc.time (P, FastContraction.modulus G'.numEdges, r, G') ≤ + K * ((encCore encT (P, FastContraction.modulus G'.numEdges, r, G')).length + 1) ^ K * + 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) ∧ + cc.space (P, FastContraction.modulus G'.numEdges, r, G') ≤ + K * ((encCore encT (P, FastContraction.modulus G'.numEdges, r, G')).length + 1) ^ K) + (htransfer : ∀ C D : ℕ, ∃ C' : ℕ, ∀ (s P ℓ r k : ℕ) (G : DescribedNetwork T), 2 ≤ s → + 1 ≤ P → P ≤ D * s → 1 ≤ ℓ → ℓ ≤ D * s → Adm C s (r, G) → + CoreAdm C' s (r, DescribedNetwork.specNet P ℓ (FastContraction.modulus G.numEdges) + (FastContraction.digits (FastContraction.modulus G.numEdges).length k) G)) + (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)) + (hentry : ∀ C : ℕ, ∃ K : ℕ, ∀ (s r : ℕ) (G : DescribedNetwork T), Adm C s (r, G) → + ∀ v ∈ G.vertices, ∀ bs : List Bool, bs.length = v.1.length → + ce.time (v.2, bs) ≤ + K * ((DescribedNetwork.encDescribed encT G).length + 1) ^ K * 2 ^ (K * s) ∧ + ce.space (v.2, bs) ≤ K * ((DescribedNetwork.encDescribed encT G).length + 1) ^ K) + (hshape : ∀ C s r G, Adm C s (r, G) → + s ≤ G.numEdges ∧ G.numEdges ≤ C * s ∧ G.vertices.length ≤ C * s) : + TruncatedContractionAlgorithm encT entry Adm where + certificate := + (NativeCertificate.branch (NativeCertificate.ofPolyTime truncGuard_polyTime) + (fastTruncCertificate cc) (truncDirectCertificate entry ce)).congr fun x => by + split + · next h => exact fastTruncCertificate_correct hval x h + · rfl + bound C D := by + obtain ⟨C', hC'⟩ := htransfer C D + obtain ⟨K₀, hK₀⟩ := hcore C' D + obtain ⟨Ke, hKe⟩ := hentry C + obtain ⟨Kd, hKd⟩ := truncDirectCertificate_le entry ce + obtain ⟨KE, hKE⟩ := engineCertificate_le (encT := encT) core cc + obtain ⟨cO, -, hcO⟩ := cc.computes + obtain ⟨pg, hpg, mg, bg⟩ := exists_mono_poly_cert (truncGuard_polyTime (encT := encT)) + obtain ⟨pM, hpM, mM, bM⟩ := exists_mono_poly_cert (modulusEdges_polyTime (encT := encT)) + obtain ⟨cY, dY, hY⟩ := (modulusEdges_polyTime (encT := encT)).polyBounded_length.exists_le + set s₀ := 4 * (C * D + 1) with hs₀ + -- The overheads, as polynomials in the length `n` of the input. + let Yf : ℕ → ℕ := fun n => cY * (n + 1) ^ dY + let Qf : ℕ → ℕ := fun n => K₀ * (9 * (Yf n + 1) ^ 2 + 1) ^ K₀ + let F1 : ℕ → ℕ := fun n => pM n + (Yf n * Yf n + 2) * + (KE * (Yf n + cO * (Qf n + 1) + 1) ^ KE + Qf n) + let Ef : ℕ → ℕ := fun n => Ke * (n + 1) ^ Ke + let F2 : ℕ → ℕ := fun n => + Kd * (n + Ef n + 1) ^ Kd * 2 ^ (C * s₀) * (Ef n * 2 ^ (Ke * s₀) + 1) + let F : ℕ → ℕ := fun n => pg n + F1 n + F2 n + have hYp : PolyBounded id Yf := + (PolyBounded.const cY).mul ((PolyBounded.self.add (PolyBounded.const 1)).pow dY) + have hQp : PolyBounded id Qf := + (PolyBounded.const K₀).mul (((PolyBounded.const 9).mul ((hYp.add + (PolyBounded.const 1)).pow 2)).add (PolyBounded.const 1) |>.pow K₀) + have hEp : PolyBounded id Ef := + (PolyBounded.const Ke).mul ((PolyBounded.self.add (PolyBounded.const 1)).pow Ke) + have hFp : PolyBounded id F := + ((polyBounded_comp_poly hpg PolyBounded.self).add + ((polyBounded_comp_poly hpM PolyBounded.self).add (((hYp.mul hYp).add + (PolyBounded.const 2)).mul (((PolyBounded.const KE).mul (((hYp.add + ((PolyBounded.const cO).mul (hQp.add (PolyBounded.const 1)))).add + (PolyBounded.const 1)).pow KE)).add hQp)))).add + ((((PolyBounded.const Kd).mul (((PolyBounded.self.add hEp).add + (PolyBounded.const 1)).pow Kd)).mul (PolyBounded.const (2 ^ (C * s₀)))).mul + ((hEp.mul (PolyBounded.const (2 ^ (Ke * s₀)))).add (PolyBounded.const 1))) + obtain ⟨a, d, had⟩ := hFp.exists_le + refine ⟨a + d + K₀, fun s P ℓ r G hs hP hPD hℓ hℓD hA => ?_⟩ + obtain ⟨hsm, hmC, hkC⟩ := hshape C s r G hA + set n := (encTrunc encT (P, ℓ, r, G)).length with hn + set Xs := 2 ^ (K₀ * s / Nat.sqrt (Nat.log 2 s)) with hXs + have hXs1 : 1 ≤ Xs := Nat.one_le_two_pow + have hFn := had n + simp only [id] at hFn + have hK : a * (n + 1) ^ d * Xs ≤ (a + d + K₀) * (n + 1) ^ (a + d + K₀) * + 2 ^ ((a + d + K₀) * s / Nat.sqrt (Nat.log 2 s)) := + Nat.mul_le_mul (Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right (by omega) (by omega))) + (Nat.pow_le_pow_right (by norm_num) + (Nat.div_le_div_right (Nat.mul_le_mul_right _ (by omega)))) + have hKs : a * (n + 1) ^ d ≤ (a + d + K₀) * (n + 1) ^ (a + d + K₀) := + Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right (by omega) (by omega)) + have hgt : (NativeCertificate.ofPolyTime truncGuard_polyTime).time (P, ℓ, r, G) ≤ pg n := + (bg (P, ℓ, r, G)).1 + have hgs : (NativeCertificate.ofPolyTime truncGuard_polyTime).space (P, ℓ, r, G) ≤ pg n := + (bg (P, ℓ, r, G)).2 + -- The two branches. + have hfast : truncGuard (P, ℓ, r, G) = true → + (fastTruncCertificate cc).time (P, ℓ, r, G) ≤ Xs * F1 n ∧ + (fastTruncCertificate cc).space (P, ℓ, r, G) ≤ F1 n := by + intro _ + set fl := FastContraction.modulus G.numEdges with hfl + have hLy : (encEngine encT (fl, P, ℓ, r, G)).length ≤ Yf n := hY (P, ℓ, r, G) + have hNy : DescribedNetwork.pointCount ℓ G + 1 ≤ Yf n * Yf n + 2 := by + have h1 := pointCount_le (encT := encT) (fl, P, ℓ, r, G) + have h2 := Nat.mul_le_mul hLy hLy + dsimp only at h1 + omega + have hcall (k : ℕ) : + cc.time (coreInput (fl, P, ℓ, r, G) k) ≤ Qf n * Xs ∧ + cc.space (coreInput (fl, P, ℓ, r, G) k) ≤ Qf n ∧ + (encList encNat (core (coreInput (fl, P, ℓ, r, G) k))).length ≤ + cO * (Qf n + 1) := by + have hc := length_encCore_coreInput_le (encT := encT) (fl, P, ℓ, r, G) k + have hci : coreInput (fl, P, ℓ, r, G) k = (P, FastContraction.modulus + (DescribedNetwork.specNet P ℓ fl (FastContraction.digits fl.length k) G).numEdges, + r, DescribedNetwork.specNet P ℓ fl (FastContraction.digits fl.length k) G) := rfl + rw [hci] at hc ⊢ + obtain ⟨hT, hS⟩ := hK₀ s P r _ hs hP hPD (hC' s P ℓ r k G hs hP hPD hℓ hℓD hA) + have hQ : K₀ * ((encCore encT (P, FastContraction.modulus + (DescribedNetwork.specNet P ℓ fl (FastContraction.digits fl.length k) G).numEdges, + r, DescribedNetwork.specNet P ℓ fl (FastContraction.digits fl.length k) G)).length + + 1) ^ K₀ ≤ Qf n := by + refine Nat.mul_le_mul_left _ (Nat.pow_le_pow_left ?_ _) + have : 9 * ((encEngine encT (fl, P, ℓ, r, G)).length + 1) ^ 2 ≤ 9 * (Yf n + 1) ^ 2 := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) _) + omega + have hS' := hS.trans hQ + refine ⟨hT.trans (Nat.mul_le_mul_right _ hQ), hS', ?_⟩ + have hout := hcO (P, FastContraction.modulus + (DescribedNetwork.specNet P ℓ fl (FastContraction.digits fl.length k) G).numEdges, + r, DescribedNetwork.specNet P ℓ fl (FastContraction.digits fl.length k) G) + exact hout.trans (Nat.mul_le_mul_left _ (Nat.add_le_add_right hS' 1)) + obtain ⟨hTe, hSe⟩ := hKE (fl, P, ℓ, r, G) _ _ _ fun k _ => hcall k + dsimp only at hTe hSe + have hEng : KE * ((encEngine encT (fl, P, ℓ, r, G)).length + cO * (Qf n + 1) + 1) ^ KE ≤ + KE * (Yf n + cO * (Qf n + 1) + 1) ^ KE := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) _) + have hMt : (NativeCertificate.ofPolyTime modulusEdges_polyTime).time (P, ℓ, r, G) ≤ pM n := + (bM (P, ℓ, r, G)).1 + have hMs : (NativeCertificate.ofPolyTime modulusEdges_polyTime).space (P, ℓ, r, G) ≤ + pM n := (bM (P, ℓ, r, G)).2 + refine ⟨?_, ?_⟩ + · simp only [fastTruncCertificate, NativeCertificate.congr, NativeCertificate.comp_time] + change (NativeCertificate.ofPolyTime modulusEdges_polyTime).time (P, ℓ, r, G) + + (engineCertificate core cc).time (fl, P, ℓ, r, G) ≤ _ + have hTe' := hTe.trans (Nat.mul_le_mul hNy (Nat.add_le_add_right hEng _)) + have e1 : (Yf n * Yf n + 2) * (KE * (Yf n + cO * (Qf n + 1) + 1) ^ KE + Qf n * Xs) ≤ + Xs * ((Yf n * Yf n + 2) * (KE * (Yf n + cO * (Qf n + 1) + 1) ^ KE + Qf n)) := by + have h1 : KE * (Yf n + cO * (Qf n + 1) + 1) ^ KE ≤ + Xs * (KE * (Yf n + cO * (Qf n + 1) + 1) ^ KE) := Nat.le_mul_of_pos_left _ hXs1 + calc (Yf n * Yf n + 2) * (KE * (Yf n + cO * (Qf n + 1) + 1) ^ KE + Qf n * Xs) + ≤ (Yf n * Yf n + 2) * (Xs * (KE * (Yf n + cO * (Qf n + 1) + 1) ^ KE) + + Qf n * Xs) := Nat.mul_le_mul_left _ (by omega) + _ = Xs * ((Yf n * Yf n + 2) * (KE * (Yf n + cO * (Qf n + 1) + 1) ^ KE + Qf n)) := by + ring + have e2 : pM n ≤ Xs * pM n := Nat.le_mul_of_pos_left _ hXs1 + have e3 : Xs * F1 n = Xs * pM n + + Xs * ((Yf n * Yf n + 2) * (KE * (Yf n + cO * (Qf n + 1) + 1) ^ KE + Qf n)) := by + simp only [F1]; ring + omega + · simp only [fastTruncCertificate, NativeCertificate.congr, NativeCertificate.comp_space] + change (NativeCertificate.ofPolyTime modulusEdges_polyTime).space (P, ℓ, r, G) + + (engineCertificate core cc).space (fl, P, ℓ, r, G) ≤ _ + have h1 : KE * (Yf n + cO * (Qf n + 1) + 1) ^ KE + Qf n ≤ + (Yf n * Yf n + 2) * (KE * (Yf n + cO * (Qf n + 1) + 1) ^ KE + Qf n) := + Nat.le_mul_of_pos_left _ (by omega) + simp only [F1] + omega + have hdirect : truncGuard (P, ℓ, r, G) = false → + (truncDirectCertificate entry ce).time (P, ℓ, r, G) ≤ F2 n ∧ + (truncDirectCertificate entry ce).space (P, ℓ, r, G) ≤ F2 n := by + intro hg + have hss : s < s₀ := by + by_contra h + have := truncGuard_of_le (P := P) (r := r) (show 4 * (C * D + 1) ≤ s by omega) hℓD hkC hsm + rw [this] at hg + exact Bool.noConfusion hg + have hL : (DescribedNetwork.encDescribed encT G).length ≤ n := by + simp only [hn, encTrunc, length_encPair] + omega + have hEf : Ke * ((DescribedNetwork.encDescribed encT G).length + 1) ^ Ke ≤ Ef n := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) _) + have h2s : 2 ^ (Ke * s) ≤ 2 ^ (Ke * s₀) := + Nat.pow_le_pow_right (by norm_num) (Nat.mul_le_mul_left _ hss.le) + obtain ⟨hT, hS⟩ := hKd (P, ℓ, r, G) (Ef n * 2 ^ (Ke * s₀)) (Ef n) fun v hv bs hbs => by + obtain ⟨h1, h2⟩ := hKe s r G hA v hv bs hbs + exact ⟨h1.trans (Nat.mul_le_mul hEf h2s), h2.trans hEf⟩ + have h2m : 2 ^ G.numEdges ≤ 2 ^ (C * s₀) := + Nat.pow_le_pow_right (by norm_num) (hmC.trans (Nat.mul_le_mul_left _ hss.le)) + refine ⟨hT.trans (Nat.mul_le_mul_right _ (Nat.mul_le_mul_left _ h2m)), hS.trans ?_⟩ + simp only [F2] + have h1 : 1 ≤ 2 ^ (C * s₀) * (Ef n * 2 ^ (Ke * s₀) + 1) := + Nat.one_le_iff_ne_zero.mpr (by positivity) + calc Kd * (n + Ef n + 1) ^ Kd ≤ Kd * (n + Ef n + 1) ^ Kd * + (2 ^ (C * s₀) * (Ef n * 2 ^ (Ke * s₀) + 1)) := Nat.le_mul_of_pos_right _ h1 + _ = _ := by ring + refine ⟨?_, ?_⟩ + · simp only [NativeCertificate.congr, NativeCertificate.branch_time] + have hF : pg n + Xs * F1 n + F2 n ≤ Xs * F n := by + have h1 : pg n ≤ Xs * pg n := Nat.le_mul_of_pos_left _ hXs1 + have h2 : F2 n ≤ Xs * F2 n := Nat.le_mul_of_pos_left _ hXs1 + have e : Xs * F n = Xs * pg n + Xs * F1 n + Xs * F2 n := by simp only [F]; ring + omega + have hFX : Xs * F n ≤ a * (n + 1) ^ d * Xs := by + calc Xs * F n ≤ Xs * (a * (n + 1) ^ d) := Nat.mul_le_mul_left _ hFn + _ = a * (n + 1) ^ d * Xs := by ring + split + · next hg => + have := (hfast hg).1 + omega + · next hg => + have := (hdirect (by simpa using hg)).1 + omega + · simp only [NativeCertificate.congr, NativeCertificate.branch_space] + have hF : pg n + F1 n + F2 n ≤ F n := le_rfl + split + · next hg => + have := (hfast hg).2 + omega + · next hg => + have := (hdirect (by simpa using hg)).2 + omega + +end Cslib.Circuits.Frontier diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedEntry.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedEntry.lean new file mode 100644 index 000000000..a45969f7f --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedEntry.lean @@ -0,0 +1,287 @@ +/- +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.TruncatedAlgorithm +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.EntryContraction +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length + +/-! +# Theorem D.1 at truncation order `ℓ` for entry procedures + +Theorem D.1 of [OpenAI2026ETH] (p. 53) contracts networks whose entries lie in +`B_{P,ℓ} = (ℤ / 2 ^ P)[V] / (V ^ ℓ)` and are computed by procedures. This file reduces it to the +case `ℓ = 1` with entries in `A_P = (ℤ / 2 ^ P)[U] / (f)`: from a contraction algorithm for entry +procedures (`Cslib.Circuits.Frontier.EntryContractionAlgorithm`) for the specialized entries, +`Cslib.Circuits.Frontier.TruncatedContractionAlgorithm.ofEntry` builds a truncated contraction +algorithm for the original entries. It instantiates the assembly +`Cslib.Circuits.Frontier.TruncatedContractionAlgorithm.ofCore` and discharges its hypotheses. + +**Admissible networks** (`Cslib.Circuits.Frontier.TruncEntryAdmissible`). The hypotheses of +Theorem D.1 as in `Cslib.Circuits.Frontier.EntryAdmissible`, plus **at most `C s` vertices**. The +precision and the truncation order are bounded by `P, ℓ ≤ D s` in the interface itself. + +*Narrowing against Theorem D.1.* The theorem asks only that the number of vertices be bounded by +a fixed polynomial in `s`. The bound `k ≤ C s` is what the assembly needs: the reduction of +truncation order `ℓ` to `A_P` interpolates at `(ℓ - 1) k + 1` points, which must fit in the +residues of the modulus `FastContraction.modulus m`, more than `m ^ 4 / 16` of them for `m` edges. +With `k ≤ C s` and `ℓ ≤ D s` they fit once `s ≥ 4 (C D + 1)` +(`Cslib.Circuits.Frontier.truncGuard_of_le`), and below that size direct summation costs a constant +factor. The applications satisfy the narrower bound: the network of Lemma D.2 (p. 56) has +`2 J = 2 ⌈n ^ (1/4)⌉` vertices at size `s = n ν`, and that of the fixed-density bound (§D.2, +p. 54) has `O_k(n + m)` vertices at size `s = n + m`. + +**The hypotheses of the assembly.** +* *Specialization keeps networks admissible* (`EntryContraction.exists_entryAdmissible_specNet`): + the specialized network has the same ports, and evaluating a specialized entry costs the original + entry plus a polynomial in the lengths of its input and of the original entry + (`Cslib.Circuits.Frontier.specEntryCertificate_le`). The original entry is at most linear in its + space, and specialization does not shorten the encoded network + (`DescribedNetwork.length_encDescribed_le_specNet`). +* *Entries within `poly(L) 2 ^ O(s)`* (`EntryContraction.exists_entry_le_of_entryAdmissible`): the + number of edges is in unary in the encoding, so `s ≤ L`, and `⌈s ^ (9/10)⌉ ≤ s`. +* *The shape*: between `s` and `C s` edges by `EntryAdmissible`, and at most `C s` vertices. + +## Main definitions + +* `Cslib.Circuits.Frontier.TruncEntryAdmissible`: the admissible networks. +* `Cslib.Circuits.Frontier.TruncatedContractionAlgorithm.ofEntry`: the truncated contraction + algorithm from a contraction algorithm for the specialized entries. + +## Main results + +* `Cslib.Circuits.Frontier.DescribedNetwork.isRowsFirstBipartite_specNet_iff`: specialization + keeps a network rows-first. +* `Cslib.Circuits.Frontier.DescribedNetwork.length_encDescribed_le_specNet`: specialization does + not shorten the encoded network. +* `Cslib.Circuits.Frontier.EntryContraction.exists_entryAdmissible_specNet`: specialization keeps + networks admissible. +* `Cslib.Circuits.Frontier.EntryContraction.exists_entry_le_of_entryAdmissible`: entries within + `poly(L) 2 ^ O(s)` on admissible networks. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Theorem D.1 (p. 53), the + fixed-density bound (§D.2, p. 54) and Lemma D.2 (pp. 54–56). +-/ + +public section + +namespace Cslib.Circuits.Frontier + +open Turing.MultiTapeTM Cslib.GenericRAM + +variable {T : Type} {encT : T ↪ List Bool} {entry : T → List Bool → List ℕ} + +namespace DescribedNetwork + +/-- **Specialization keeps a network rows-first**: it keeps the ports. -/ +theorem isRowsFirstBipartite_specNet_iff (P ℓ : ℕ) (fl ζ : List ℕ) (G : DescribedNetwork T) + (r : ℕ) : (specNet P ℓ fl ζ G).IsRowsFirstBipartite r ↔ G.IsRowsFirstBipartite r := by + simp only [IsRowsFirstBipartite, numEdges_specNet, vertices_specNet, List.forall_mem_map, + ← List.map_take, ← List.map_drop, List.map_map, Function.comp_def] + +/-- **Specialization does not shorten the encoded network**: each descriptor `t` becomes +`(t, P, ℓ, fl, ζ)`. -/ +theorem length_encDescribed_le_specNet (P ℓ : ℕ) (fl ζ : List ℕ) (G : DescribedNetwork T) : + (encDescribed encT G).length ≤ + (encDescribed (encSpecDesc encT) (specNet P ℓ fl ζ G)).length := by + change (encPair encUnary (encList (encPair (encList encNat) encT)) + (G.numEdges, G.vertices)).length ≤ + (encPair encUnary (encList (encPair (encList encNat) (encSpecDesc encT))) + (G.numEdges, G.vertices.map fun v => (v.1, (v.2, P, ℓ, fl, ζ)))).length + simp only [length_encPair, length_encList, List.map_map] + refine Nat.add_le_add_left (List.sum_le_sum fun v _ => ?_) _ + simp only [Function.comp_apply] + omega + +end DescribedNetwork + +/-- **Admissible networks for Theorem D.1 at truncation order `ℓ`**, with an entry procedure, at +size `s` with constant `C`: the network `G` with `r` row vertices is admissible for `ce` +(`EntryAdmissible`: rows-first bipartite, between `s` and `C s` edges, degree at most +`⌈s ^ (9/10)⌉`, entries within `C (s + L + 1) ^ C 2 ^ (C ⌈s ^ (9/10)⌉)` time and +`C (s + L + 1) ^ C` space) and has **at most `C s` vertices**. + +The vertex bound narrows Theorem D.1 of [OpenAI2026ETH] (p. 53), which asks only for a polynomial +bound in `s`. The networks of Lemma D.2 (p. 56) and of the fixed-density bound (§D.2, p. 54) +satisfy it. -/ +@[expose] def TruncEntryAdmissible + (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)) (C s : ℕ) (G : ℕ × DescribedNetwork T) : Prop := + EntryAdmissible ce C s G ∧ G.2.vertices.length ≤ C * s + +namespace EntryContraction + +variable (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)) + +/-- **Specialization keeps networks admissible.** For every entry certificate `ce` and constant +`C` there is `C'` such that, for every network `G` admissible for `ce` at size `s` with constant +`C`, every network specialized from it, at any precision `P`, truncation order `ℓ`, modulus `fl` +and point `ζ`, is admissible for the specialized entries (`specEntryCertificate entry ce`) at +size `s` with constant `C'`. -/ +theorem exists_entryAdmissible_specNet (C : ℕ) : + ∃ C' : ℕ, ∀ (s P ℓ r : ℕ) (fl ζ : List ℕ) (G : DescribedNetwork T), + EntryAdmissible ce C s (r, G) → + EntryAdmissible (specEntryCertificate entry ce) C' s + (r, DescribedNetwork.specNet P ℓ fl ζ G) := by + obtain ⟨K₁, hK₁⟩ := specEntryCertificate_le (encT := encT) + obtain ⟨cO, -, hcO⟩ := ce.computes + -- The overhead of specialization, as a polynomial in `s + L'`. + let f : ℕ → ℕ := fun n => K₁ * (3 * n + 3 + cO * (C * (n + 1) ^ C + 1) + 1) ^ K₁ + have hf : PolyBounded id f := + (PolyBounded.const K₁).mul (((((PolyBounded.const 3).mul PolyBounded.self).add + (PolyBounded.const 3)).add ((PolyBounded.const cO).mul (((PolyBounded.const C).mul + ((PolyBounded.self.add (PolyBounded.const 1)).pow C)).add (PolyBounded.const 1)))).add + (PolyBounded.const 1) |>.pow K₁) + obtain ⟨a, d, had⟩ := hf.exists_le + refine ⟨C + a + d, fun s P ℓ r fl ζ G hA => ?_⟩ + obtain ⟨hrows, hsm, hmC, hdeg, hent⟩ := hA + refine ⟨(DescribedNetwork.isRowsFirstBipartite_specNet_iff P ℓ fl ζ G r).2 hrows, hsm, + hmC.trans (Nat.mul_le_mul_right _ (by omega)), ?_, ?_⟩ + · intro v hv + change v ∈ G.vertices.map _ at hv + obtain ⟨u, hu, rfl⟩ := List.mem_map.mp hv + exact hdeg u hu + · intro v hv bs hbs + have hv' := hv + change v ∈ G.vertices.map _ at hv' + obtain ⟨u, hu, rfl⟩ := List.mem_map.mp hv' + change bs.length = u.1.length at hbs + set L' := (DescribedNetwork.encDescribed (encSpecDesc encT) + (DescribedNetwork.specNet P ℓ fl ζ G)).length with hL' + have hLL : (DescribedNetwork.encDescribed encT G).length ≤ L' := + DescribedNetwork.length_encDescribed_le_specNet P ℓ fl ζ G + set n := s + L' with hn + have hn1 : 1 ≤ n + 1 := by omega + obtain ⟨hT, hS⟩ := hent u hu bs hbs + have hbase : C * (s + (DescribedNetwork.encDescribed encT G).length + 1) ^ C ≤ + C * (n + 1) ^ C := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) _) + -- The input of the specialized entry is at most `3 n + 3` bits. + have hq : (encPair (encSpecDesc encT) encBits ((u.2, P, ℓ, fl, ζ), bs)).length ≤ 3 * n + 3 := by + have h1 := length_le_encList_of_mem (encPair (encList encNat) (encSpecDesc encT)) hv + have h2 : (encList (encPair (encList encNat) (encSpecDesc encT)) + (DescribedNetwork.specNet P ℓ fl ζ G).vertices).length ≤ L' := by + rw [hL'] + change _ ≤ (encPair encUnary (encList (encPair (encList encNat) (encSpecDesc encT))) + ((DescribedNetwork.specNet P ℓ fl ζ G).numEdges, + (DescribedNetwork.specNet P ℓ fl ζ G).vertices)).length + rw [length_encPair] + dsimp only + omega + have h3 := length_le_length_encList encNat u.1 + rw [length_encPair] at h1 ⊢ + change 2 * (encSpecDesc encT (u.2, P, ℓ, fl, ζ)).length + 1 + bs.length ≤ 3 * n + 3 + dsimp only at h1 + omega + -- The original entry is at most `cO (C (n + 1) ^ C + 1)` bits. + have hout : (encList encNat (entry u.2 bs)).length ≤ cO * (C * (n + 1) ^ C + 1) := + (hcO (u.2, bs)).trans (Nat.mul_le_mul_left _ (Nat.add_le_add_right (hS.trans hbase) 1)) + obtain ⟨hT', hS'⟩ := hK₁ entry ce ((u.2, P, ℓ, fl, ζ), bs) + have hover : K₁ * ((encPair (encSpecDesc encT) encBits ((u.2, P, ℓ, fl, ζ), bs)).length + + (encList encNat (entry u.2 bs)).length + 1) ^ K₁ ≤ a * (n + 1) ^ d := by + refine le_trans ?_ (had n) + exact Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) _) + have hpow {c e : ℕ} (hc : c ≤ C + a + d) (he : e ≤ C + a + d) : + c * (n + 1) ^ e ≤ (C + a + d) * (n + 1) ^ (C + a + d) := + Nat.mul_le_mul hc (Nat.pow_le_pow_right hn1 he) + have h2 : 2 ^ (C * ceilNineTenths s) ≤ 2 ^ ((C + a + d) * ceilNineTenths s) := + Nat.pow_le_pow_right (by norm_num) (Nat.mul_le_mul_right _ (by omega)) + have hX1 : 1 ≤ 2 ^ ((C + a + d) * ceilNineTenths s) := Nat.one_le_two_pow + have hsplit : C * (n + 1) ^ C + a * (n + 1) ^ d ≤ + (C + a + d) * (n + 1) ^ (C + a + d) := by + have e1 := hpow (c := C) (e := C) (by omega) (by omega) + have e2 := hpow (c := a) (e := d) (by omega) (by omega) + have e3 : C * (n + 1) ^ (C + a + d) + a * (n + 1) ^ (C + a + d) ≤ + (C + a + d) * (n + 1) ^ (C + a + d) := by + rw [← Nat.add_mul] + exact Nat.mul_le_mul_right _ (by omega) + have e1' : C * (n + 1) ^ C ≤ C * (n + 1) ^ (C + a + d) := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_right hn1 (by omega)) + have e2' : a * (n + 1) ^ d ≤ a * (n + 1) ^ (C + a + d) := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_right hn1 (by omega)) + omega + refine ⟨?_, ?_⟩ + · change (specEntryCertificate entry ce).time ((u.2, P, ℓ, fl, ζ), bs) ≤ + (C + a + d) * (n + 1) ^ (C + a + d) * 2 ^ ((C + a + d) * ceilNineTenths s) + have hT2 : ce.time (u.2, bs) ≤ C * (n + 1) ^ C * 2 ^ ((C + a + d) * ceilNineTenths s) := + hT.trans (Nat.mul_le_mul (hbase) h2) + have hA2 : a * (n + 1) ^ d ≤ a * (n + 1) ^ d * 2 ^ ((C + a + d) * ceilNineTenths s) := + Nat.le_mul_of_pos_right _ hX1 + calc (specEntryCertificate entry ce).time ((u.2, P, ℓ, fl, ζ), bs) + ≤ C * (n + 1) ^ C * 2 ^ ((C + a + d) * ceilNineTenths s) + + a * (n + 1) ^ d * 2 ^ ((C + a + d) * ceilNineTenths s) := by + dsimp only at hT' + omega + _ = (C * (n + 1) ^ C + a * (n + 1) ^ d) * 2 ^ ((C + a + d) * ceilNineTenths s) := by + ring + _ ≤ (C + a + d) * (n + 1) ^ (C + a + d) * 2 ^ ((C + a + d) * ceilNineTenths s) := + Nat.mul_le_mul_right _ hsplit + · change (specEntryCertificate entry ce).space ((u.2, P, ℓ, fl, ζ), bs) ≤ + (C + a + d) * (n + 1) ^ (C + a + d) + dsimp only at hS' + have := hS.trans hbase + omega + +/-- **Entries within `poly(L) 2 ^ O(s)` on admissible networks.** For every constant `C` there is +`K` such that on every network admissible for `ce` at size `s` with constant `C`, of encoded length +`L`, every entry takes time at most `K (L + 1) ^ K 2 ^ (K s)` and space at most `K (L + 1) ^ K`: +the number of edges is in unary in the encoding, so `s ≤ L`, and `⌈s ^ (9/10)⌉ ≤ s`. -/ +theorem exists_entry_le_of_entryAdmissible (C : ℕ) : + ∃ K : ℕ, ∀ (s r : ℕ) (G : DescribedNetwork T), EntryAdmissible ce C s (r, G) → + ∀ v ∈ G.vertices, ∀ bs : List Bool, bs.length = v.1.length → + ce.time (v.2, bs) ≤ + K * ((DescribedNetwork.encDescribed encT G).length + 1) ^ K * 2 ^ (K * s) ∧ + ce.space (v.2, bs) ≤ K * ((DescribedNetwork.encDescribed encT G).length + 1) ^ K := by + refine ⟨C * 2 ^ C + C, fun s r G hA v hv bs hbs => ?_⟩ + obtain ⟨-, hsm, -, -, hent⟩ := hA + change s ≤ G.numEdges at hsm + obtain ⟨hT, hS⟩ := hent v hv bs hbs + set L := (DescribedNetwork.encDescribed encT G).length with hL + have hmL := DescribedNetwork.length_numEdges_vertices_le (encT := encT) G + have hL1 : 1 ≤ L + 1 := by omega + -- `C (s + L + 1) ^ C ≤ C 2 ^ C (L + 1) ^ C ≤ K (L + 1) ^ K`. + have hbase : C * (s + L + 1) ^ C ≤ (C * 2 ^ C + C) * (L + 1) ^ (C * 2 ^ C + C) := by + calc C * (s + L + 1) ^ C ≤ C * (2 * (L + 1)) ^ C := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) _) + _ = C * 2 ^ C * (L + 1) ^ C := by rw [Nat.mul_pow, Nat.mul_assoc] + _ ≤ (C * 2 ^ C + C) * (L + 1) ^ (C * 2 ^ C + C) := + Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right hL1 (by omega)) + have h2 : 2 ^ (C * ceilNineTenths s) ≤ 2 ^ ((C * 2 ^ C + C) * s) := + Nat.pow_le_pow_right (by norm_num) + (Nat.mul_le_mul (by omega) (ceilNineTenths_le_self s)) + exact ⟨hT.trans (Nat.mul_le_mul hbase h2), hS.trans hbase⟩ + +end EntryContraction + +/-- **Theorem D.1 at truncation order `ℓ` for entry procedures, from the case `ℓ = 1`.** Let `ce` +be a native certificate of an entry procedure, and `A` a contraction algorithm for the specialized +entries (`specEntry entry`, with the certificate `specEntryCertificate entry ce`) on the networks +admissible for them. Then the assembly `TruncatedContractionAlgorithm.ofCore` around `A` is a +truncated contraction algorithm for the networks admissible for `ce` with at most `C s` vertices +(`TruncEntryAdmissible ce`): it computes the contraction in `B_{P,ℓ}` in time +`poly(n) 2 ^ O(s / √⌊log₂ s⌋)` and polynomial space, for `1 ≤ P, ℓ ≤ D s`. -/ +noncomputable def TruncatedContractionAlgorithm.ofEntry + (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)) + (A : EntryContractionAlgorithm (encSpecDesc encT) (specEntry entry) + (EntryAdmissible (specEntryCertificate entry ce))) : + TruncatedContractionAlgorithm encT entry (TruncEntryAdmissible ce) := + ofCore (core := A.core) A.certificate A.val_core A.bound + (fun C _ => by + obtain ⟨C', hC'⟩ := EntryContraction.exists_entryAdmissible_specNet ce C + exact ⟨C', fun s P ℓ r _ G _ _ _ _ _ hA => hC' s P ℓ r _ _ G hA.1⟩) + ce + (fun C => by + obtain ⟨K, hK⟩ := EntryContraction.exists_entry_le_of_entryAdmissible ce C + exact ⟨K, fun s r G hA => hK s r G hA.1⟩) + (fun _ _ _ _ hA => ⟨hA.1.2.1, hA.1.2.2.1, hA.2⟩) + +end Cslib.Circuits.Frontier diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedPolyTime.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedPolyTime.lean new file mode 100644 index 000000000..e2f976d41 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedPolyTime.lean @@ -0,0 +1,468 @@ +/- +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.Truncated +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DescribedContraction +public import Complexity.Computability.GenericRAM.Native.IndexFold +import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionPolyTime +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionSchedule +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListMap +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeNatFrontends +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat + +/-! +# The reduction of truncation order `ℓ` as a native machine + +The reduction of `Complexity/Computability/Circuit/Frontier/TensorNetwork/Truncated.lean` +(`Cslib.Circuits.Frontier.DescribedNetwork.interpContract`) contracts specialized networks over +`A_P = (ℤ / 2 ^ P)[U] / (f)` and interpolates. This file runs it as one native machine around any +native certificate of the contraction over `A_P` (`engineCertificate`), with the precision `P` and +the truncation order `ℓ` in unary. + +**Polynomial-time steps.** Specializing a network at a point (`DescribedNetwork.specNet_polyTime`), +the binary-digit points (`DescribedNetwork.digitPoints_polyTime`), the inputs of the contractions +(`coreInput_polyTime`) and reading the truncated contraction off the interpolant +(`interpRecover_polyTime`, `engineRecover_polyTime`) are polynomial-time. + +**The loop.** The machine visits the digit points with the binary-index fold +`Cslib.GenericRAM.IndexFold`, keeping the index, the input and the values so far; each round +calls the given certificate once (`engineStep`, `engineStepCertificate`, `run_engineStep`). Then it +interpolates. + +**Direct summation.** A native certificate of the entries gives one of the specialized entries +(`specEntryCertificate`: the entry, then Horner's rule), hence direct summation over `A_P` of a +specialized network (`directCoreCertificate`). Through the reduction at the modulus +`FastContraction.modulus n` for `n = (ℓ - 1) k + 1` points, which has enough residues +(`le_two_pow_length_modulus`), this computes the truncated contraction on every input +(`truncDirectCertificate`). Its cost is that of direct summation. + +The time and space of the loop are bounded in +`Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedResources.lean`. With the +contraction of Theorem D.1 at `ℓ = 1` over `A_P` in place of direct summation, that bound gives +Theorem D.1 at truncation order `ℓ` (#1538). + +## Main definitions + +* `Cslib.Circuits.Frontier.encSpecDesc`, `Cslib.Circuits.Frontier.encTrunc`, + `Cslib.Circuits.Frontier.encCore`, `Cslib.Circuits.Frontier.encEngine`: encodings. +* `Cslib.Circuits.Frontier.specEntryCertificate`: the native evaluator of specialized entries. +* `Cslib.Circuits.Frontier.engineCertificate`: the reduction around a contraction over `A_P`. +* `Cslib.Circuits.Frontier.directCoreCertificate`: direct summation over `A_P`. +* `Cslib.Circuits.Frontier.truncDirectCertificate`: the truncated contraction by direct summation. + +## Main results + +* `Cslib.Circuits.Frontier.DescribedNetwork.specNet_polyTime`, + `Cslib.Circuits.Frontier.interpRecover_polyTime`: polynomial-time steps. +* `Cslib.Circuits.Frontier.run_engineStep`, `Cslib.Circuits.Frontier.interpContract_eq_run`: the + loop computes the reduction. +* `Cslib.Circuits.Frontier.interpContract_direct_eq`: direct summation through the reduction is + the truncated contraction. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Theorem D.1 (p. 53). +-/ + +public section + +namespace Cslib.Circuits.Frontier + +open Turing.MultiTapeTM Cslib.GenericRAM GaloisRingArith + +variable {T : Type} (encT : T ↪ List Bool) + +/-- The encoding of the data `(P, ℓ, fl, ζ)` of a specialization: `P` and `ℓ` in unary, the +coefficients of the modulus and the point in binary. -/ +abbrev encSpecData : ℕ × ℕ × List ℕ × List ℕ ↪ List Bool := + encPair encUnary (encPair encUnary (encPair (encList encNat) (encList encNat))) + +/-- The encoding of a specialized descriptor: the original descriptor, then the data of the +specialization. -/ +abbrev encSpecDesc : SpecDesc T ↪ List Bool := encPair encT encSpecData + +variable {encT} + +/-- The first `ℓ` coefficients as constant coefficient lists, from `ℓ` in unary. -/ +theorem constCoeffs_polyTime : + ComputableInPolyTime (fun q : ℕ × List ℕ => constCoeffs q.1 q.2) + (encPair encUnary (encList encNat)) (encList (encList encNat)) := by + have hc : ComputableInPolyTime (fun q : (ℕ × List ℕ) × ℕ => q.1.2) + (encPair (encPair encUnary (encList encNat)) encUnary) (encList encNat) := + (ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.fst _ _) + have hget := computableInPolyTime_getD hc (ComputableInPolyTime.snd _ _) + exact ComputableInPolyTime.mapWithInput + (ComputableInPolyTime.range.comp (ComputableInPolyTime.fst _ _)) + (ComputableInPolyTime.cons' hget (ComputableInPolyTime.const [])) + +/-- **Horner's rule on the first `ℓ` coefficients**, from the data of a specialization and a +coefficient list, with `P` and `ℓ` in unary. -/ +theorem horner_polyTime : + ComputableInPolyTime + (fun q : (ℕ × ℕ × List ℕ × List ℕ) × List ℕ => + peval q.1.1 q.1.2.2.1 (constCoeffs q.1.2.1 q.2) q.1.2.2.2) + (encPair encSpecData (encList encNat)) (encList encNat) := by + have hd := ComputableInPolyTime.fst encSpecData (encList encNat) + have hc := ComputableInPolyTime.snd encSpecData (encList encNat) + have hP := (ComputableInPolyTime.fst _ _).comp hd + have hrest := (ComputableInPolyTime.snd _ _).comp hd + have hℓ := (ComputableInPolyTime.fst _ _).comp hrest + have hfz := (ComputableInPolyTime.snd _ _).comp hrest + have hfl := (ComputableInPolyTime.fst _ _).comp hfz + have hz := (ComputableInPolyTime.snd _ _).comp hfz + exact computableInPolyTime_peval hP hfl (constCoeffs_polyTime.comp (hℓ.prod hc)) hz + +variable (entry : T → List Bool → List ℕ) + +/-- **The native evaluator of specialized entries**, from a native certificate of the entries: +evaluate the original entry, then apply Horner's rule in `A_P`. -/ +@[expose] noncomputable def specEntryCertificate + (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)) : + NativeCertificate (fun q : SpecDesc T × List Bool => specEntry entry q.1 q.2) + (encPair (encSpecDesc encT) encBits) (encList encNat) := + ((NativeCertificate.ofPolyTime horner_polyTime).comp + ((NativeCertificate.ofPolyTime + ((ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.fst _ _))).prod + (ce.comp (NativeCertificate.ofPolyTime + ((((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.fst _ _))).prod + (ComputableInPolyTime.snd _ _)))))).congr fun _ => rfl + +namespace DescribedNetwork + +/-- **Specializing is polynomial-time**: from the data `(P, ℓ, fl, ζ)` and the network to the +specialized network. -/ +theorem specNet_polyTime : + ComputableInPolyTime + (fun q : (ℕ × ℕ × List ℕ × List ℕ) × DescribedNetwork T => + specNet q.1.1 q.1.2.1 q.1.2.2.1 q.1.2.2.2 q.2) + (encPair encSpecData (encDescribed encT)) (encDescribed (encSpecDesc encT)) := by + have hG := ComputableInPolyTime.snd encSpecData (encDescribed encT) + have hd := ComputableInPolyTime.fst encSpecData (encDescribed encT) + have hv : ComputableInPolyTime + (fun q : ((ℕ × ℕ × List ℕ × List ℕ) × DescribedNetwork T) × (List ℕ × T) => + (q.2.1, (q.2.2, q.1.1))) + (encPair (encPair encSpecData (encDescribed encT)) (encPair (encList encNat) encT)) + (encPair (encList encNat) (encSpecDesc encT)) := + ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _)).prod + (((ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.snd _ _)).prod + ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.fst _ _))) + have hpair : ComputableInPolyTime + (fun q : (ℕ × ℕ × List ℕ × List ℕ) × DescribedNetwork T => + (q.2.numEdges, q.2.vertices.map fun v => (v.1, (v.2, q.1)))) + (encPair encSpecData (encDescribed encT)) + (encPair encUnary (encList (encPair (encList encNat) (encSpecDesc encT)))) := + (numEdges_polyTime.comp hG).prod + (ComputableInPolyTime.mapWithInput (vertices_polyTime.comp hG) hv) + exact (ComputableInPolyTime.of_eq (encIn := encPair encUnary + (encList (encPair (encList encNat) (encSpecDesc encT)))) + (f := fun p : ℕ × List (List ℕ × SpecDesc T) => (⟨p.1, p.2⟩ : DescribedNetwork (SpecDesc T))) + fun _ => rfl).comp hpair + +/-- **The binary-digit points are polynomial-time**, from the number of coordinates and the +number of points in unary. -/ +theorem digitPoints_polyTime : + ComputableInPolyTime + (fun q : ℕ × ℕ => (List.range q.2).map (FastContraction.digits q.1)) + (encPair encUnary encUnary) (encList (encList encNat)) := + ComputableInPolyTime.mapWithInput + (ComputableInPolyTime.range.comp (ComputableInPolyTime.snd _ _)) + (FastContraction.digits_polyTime.comp + (((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.fst _ _)).prod + (ComputableInPolyTime.snd _ _))) + +end DescribedNetwork + +/-- **Reading off the interpolant is polynomial-time**, with `P` and `ℓ` in unary. -/ +theorem interpRecover_polyTime : + ComputableInPolyTime + (fun q : ℕ × ℕ × List ℕ × List (List ℕ) × List (List ℕ) => + interpRecover q.1 q.2.1 q.2.2.1 q.2.2.2.1 q.2.2.2.2) + (encPair encUnary (encPair encUnary (encPair (encList encNat) + (encPair (encList (encList encNat)) (encList (encList encNat)))))) + (encList encNat) := by + let encQ := encPair encUnary (encPair encUnary (encPair (encList encNat) + (encPair (encList (encList encNat)) (encList (encList encNat))))) + have hP := ComputableInPolyTime.fst encUnary (encPair encUnary (encPair (encList encNat) + (encPair (encList (encList encNat)) (encList (encList encNat))))) + have hr := ComputableInPolyTime.snd encUnary (encPair encUnary (encPair (encList encNat) + (encPair (encList (encList encNat)) (encList (encList encNat))))) + have hℓ := (ComputableInPolyTime.fst _ _).comp hr + have hr' := (ComputableInPolyTime.snd _ _).comp hr + have hfl := (ComputableInPolyTime.fst _ _).comp hr' + have hr'' := (ComputableInPolyTime.snd _ _).comp hr' + have hpts := (ComputableInPolyTime.fst _ _).comp hr'' + have hys := (ComputableInPolyTime.snd _ _).comp hr'' + have hI := computableInPolyTime_interp hP hfl hpts hys + have hq : ComputableInPolyTime + (fun q : (ℕ × ℕ × List ℕ × List (List ℕ) × List (List ℕ)) × ℕ => + ((interp q.1.1 q.1.2.2.1 q.1.2.2.2.1 q.1.2.2.2.2).getD q.2 []).getD 0 0 % 2 ^ q.1.1) + (encPair encQ encUnary) encNat := by + have h1 := ComputableInPolyTime.fst encQ encUnary + have hrow := (ComputableInPolyTime.listGetD (encA := encList encNat) []).comp + ((hI.comp h1).prod (ComputableInPolyTime.snd encQ encUnary)) + exact computableInPolyTime_mod_two_pow + (computableInPolyTime_getD hrow (ComputableInPolyTime.const 0)) (hP.comp h1) + exact ComputableInPolyTime.mapWithInput (ComputableInPolyTime.range.comp hℓ) hq + +/-! ### The reduction as a streaming loop -/ + +/-- The encoding of an input `(P, ℓ, r, G)` of the truncated contraction: `P` and `ℓ` in unary, +`r` in binary, then the network. -/ +abbrev encTrunc (encT : T ↪ List Bool) : ℕ × ℕ × ℕ × DescribedNetwork T ↪ List Bool := + encPair encUnary (encPair encUnary (encPair encNat (DescribedNetwork.encDescribed encT))) + +/-- The encoding of an input `(P, fl, r, G')` of a contraction over `A_P` of specialized +networks: `P` in unary, the modulus, `r` in binary, then the specialized network. -/ +abbrev encCore (encT : T ↪ List Bool) : + ℕ × List ℕ × ℕ × DescribedNetwork (SpecDesc T) ↪ List Bool := + encPair encUnary (encPair (encList encNat) + (encPair encNat (DescribedNetwork.encDescribed (encSpecDesc encT)))) + +/-- The input of the reduction: the modulus and the input `(P, ℓ, r, G)`. -/ +abbrev encEngine (encT : T ↪ List Bool) : List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T ↪ List Bool := + encPair (encList encNat) (encTrunc encT) + +/-- The input of the contraction at the `k`-th digit point, for a modulus `y.1` and an input +`y.2 = (P, ℓ, r, G)`. -/ +@[expose] def coreInput (y : List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T) (k : ℕ) : + ℕ × List ℕ × ℕ × DescribedNetwork (SpecDesc T) := + (y.2.1, y.1, y.2.2.2.1, + DescribedNetwork.specNet y.2.1 y.2.2.1 y.1 (FastContraction.digits y.1.length k) y.2.2.2.2) + +variable (core : ℕ × List ℕ × ℕ × DescribedNetwork (SpecDesc T) → List ℕ) + +/-- **One round of the reduction** at the index `p.1`: append the contraction at the `p.1`-th digit +point to the values so far. -/ +@[expose] def engineStep + (p : ℕ × ((List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T) × List (List ℕ))) : + (List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T) × List (List ℕ) := + (p.2.1, p.2.2 ++ [core (coreInput p.2.1 p.1)]) + +/-- After `j` rounds, the values are the contractions at the first `j` digit points. -/ +theorem run_engineStep (y : List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T) (j : ℕ) : + IndexFold.run (engineStep core) j (y, []) = + (j, (y, (List.range j).map fun k => core (coreInput y k))) := by + induction j with + | zero => rfl + | succ j ih => + rw [IndexFold.run_succ, ih] + simp only [IndexFold.step, engineStep, List.range_succ, List.map_append, List.map_cons, + List.map_nil] + +/-- **The reduction is the streaming loop followed by recovery.** -/ +theorem interpContract_eq_run (y : List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T) : + DescribedNetwork.interpContract core y.1 y.2.1 y.2.2.1 y.2.2.2.1 y.2.2.2.2 = + interpRecover y.2.1 y.2.2.1 y.1 + ((List.range (DescribedNetwork.pointCount y.2.2.1 y.2.2.2.2)).map + (FastContraction.digits y.1.length)) + (IndexFold.run (engineStep core) (DescribedNetwork.pointCount y.2.2.1 y.2.2.2.2) + (y, [])).2.2 := by + rw [run_engineStep, DescribedNetwork.interpContract, List.map_map] + rfl + +/-- The binary digits are polynomial-time from the number in binary. -/ +theorem digits_polyTime_binary : + ComputableInPolyTime (fun q : ℕ × ℕ => FastContraction.digits q.1 q.2) + (encPair encUnary encNat) (encList encNat) := + ComputableInPolyTime.mapWithInput + (ComputableInPolyTime.range.comp (ComputableInPolyTime.fst _ _)) + (ComputableInPolyTime.ite (encMid := encNat) + (ComputableInPolyTime.binary_testBit + ((ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.fst _ _)) + (ComputableInPolyTime.snd _ _)) + (ComputableInPolyTime.const 1) (ComputableInPolyTime.const 0)) + +/-- The number of points is polynomial-time, in unary. -/ +theorem pointCount_polyTime : + ComputableInPolyTime (fun y : List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T => + DescribedNetwork.pointCount y.2.2.1 y.2.2.2.2) (encEngine encT) encUnary := by + have hx := ComputableInPolyTime.snd (encList encNat) (encTrunc encT) + have hℓ := (ComputableInPolyTime.fst _ _).comp ((ComputableInPolyTime.snd _ _).comp hx) + have hG := (ComputableInPolyTime.snd _ _).comp ((ComputableInPolyTime.snd _ _).comp + ((ComputableInPolyTime.snd _ _).comp hx)) + have hk := (ComputableInPolyTime.length_list _).comp + (DescribedNetwork.vertices_polyTime.comp hG) + exact ComputableInPolyTime.unary_add' + (ComputableInPolyTime.unary_mul' (ComputableInPolyTime.unary_sub' hℓ + (ComputableInPolyTime.const 1)) hk) (ComputableInPolyTime.const 1) + +/-- The input of the contraction at a binary index is polynomial-time. -/ +theorem coreInput_polyTime : + ComputableInPolyTime + (fun p : ℕ × ((List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T) × List (List ℕ)) => + coreInput p.2.1 p.1) + (encPair encNat (encPair (encEngine encT) (encList (encList encNat)))) (encCore encT) := by + have hy := (ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd encNat + (encPair (encEngine encT) (encList (encList encNat)))) + have hk := ComputableInPolyTime.fst encNat (encPair (encEngine encT) (encList (encList encNat))) + have hfl := (ComputableInPolyTime.fst _ _).comp hy + have hx := (ComputableInPolyTime.snd _ _).comp hy + have hP := (ComputableInPolyTime.fst _ _).comp hx + have hx' := (ComputableInPolyTime.snd _ _).comp hx + have hℓ := (ComputableInPolyTime.fst _ _).comp hx' + have hx'' := (ComputableInPolyTime.snd _ _).comp hx' + have hr := (ComputableInPolyTime.fst _ _).comp hx'' + have hG := (ComputableInPolyTime.snd _ _).comp hx'' + have hζ := digits_polyTime_binary.comp + (((ComputableInPolyTime.length_list _).comp hfl).prod hk) + exact hP.prod (hfl.prod (hr.prod (DescribedNetwork.specNet_polyTime.comp + ((hP.prod (hℓ.prod (hfl.prod hζ))).prod hG)))) + +/-- The certificate of one round, from a certificate of the contraction over `A_P`. -/ +@[expose] noncomputable def engineStepCertificate + (cc : NativeCertificate core (encCore encT) (encList encNat)) : + NativeCertificate (engineStep core) + (encPair encNat (encPair (encEngine encT) (encList (encList encNat)))) + (encPair (encEngine encT) (encList (encList encNat))) := + (NativeCertificate.ofPolyTime + ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _))).prod + ((NativeCertificate.ofPolyTime (ComputableInPolyTime.snoc (encList encNat))).comp + ((NativeCertificate.ofPolyTime + ((ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.snd _ _))).prod + (cc.comp (NativeCertificate.ofPolyTime coreInput_polyTime)))) + +/-- Recovery from the final state of the loop is polynomial-time. -/ +theorem engineRecover_polyTime : + ComputableInPolyTime + (fun p : ℕ × ((List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T) × List (List ℕ)) => + interpRecover p.2.1.2.1 p.2.1.2.2.1 p.2.1.1 + ((List.range (DescribedNetwork.pointCount p.2.1.2.2.1 p.2.1.2.2.2.2)).map + (FastContraction.digits p.2.1.1.length)) p.2.2) + (encPair encNat (encPair (encEngine encT) (encList (encList encNat)))) (encList encNat) := by + let encS := encPair encNat (encPair (encEngine encT) (encList (encList encNat))) + have hy : ComputableInPolyTime + (fun p : ℕ × ((List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T) × List (List ℕ)) => p.2.1) + encS (encEngine encT) := + (ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _) + have hys : ComputableInPolyTime + (fun p : ℕ × ((List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T) × List (List ℕ)) => p.2.2) + encS (encList (encList encNat)) := + (ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.snd _ _) + have hfl : ComputableInPolyTime + (fun p : ℕ × ((List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T) × List (List ℕ)) => p.2.1.1) + encS (encList encNat) := (ComputableInPolyTime.fst _ _).comp hy + have hP : ComputableInPolyTime + (fun p : ℕ × ((List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T) × List (List ℕ)) => p.2.1.2.1) + encS encUnary := + (ComputableInPolyTime.fst _ _).comp ((ComputableInPolyTime.snd _ _).comp hy) + have hℓ : ComputableInPolyTime + (fun p : ℕ × ((List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T) × List (List ℕ)) => p.2.1.2.2.1) + encS encUnary := + (ComputableInPolyTime.fst _ _).comp ((ComputableInPolyTime.snd _ _).comp + ((ComputableInPolyTime.snd _ _).comp hy)) + have hpts : ComputableInPolyTime + (fun p : ℕ × ((List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T) × List (List ℕ)) => + (List.range (DescribedNetwork.pointCount p.2.1.2.2.1 p.2.1.2.2.2.2)).map + (FastContraction.digits p.2.1.1.length)) + encS (encList (encList encNat)) := + DescribedNetwork.digitPoints_polyTime.comp + (((ComputableInPolyTime.length_list _).comp hfl).prod (pointCount_polyTime.comp hy)) + have h := interpRecover_polyTime.comp (hP.prod (hℓ.prod (hfl.prod (hpts.prod hys)))) + exact h + +/-- **The reduction as one native machine**, from a native certificate of the contraction over +`A_P` of specialized networks: the streaming loop over the digit points, keeping only the binary +index, the input and the values so far, then recovery. On input `(fl, (P, ℓ, r, G))` it computes +`interpContract core fl P ℓ r G`. -/ +@[expose] noncomputable def engineCertificate + (cc : NativeCertificate core (encCore encT) (encList encNat)) : + NativeCertificate (fun y : List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T => + DescribedNetwork.interpContract core y.1 y.2.1 y.2.2.1 y.2.2.2.1 y.2.2.2.2) + (encEngine encT) (encList encNat) := + ((NativeCertificate.ofPolyTime engineRecover_polyTime).comp + (IndexFold.certificate + (NativeCertificate.ofPolyTime (ComputableInPolyTime.unary_to_binary.comp pointCount_polyTime)) + (NativeCertificate.ofPolyTime + (ComputableInPolyTime.id'.prod (ComputableInPolyTime.const []))) + (engineStepCertificate core cc))).congr fun y => by + simp only [Function.comp_apply] + rw [interpContract_eq_run, run_engineStep] + +/-! ### Direct summation as the contraction over `A_P` -/ + +/-- **Direct summation over a specialized network**, as a contraction over `A_P` with the input +`(P, fl, r, G')`, from a native certificate of the entries. -/ +@[expose] noncomputable def directCoreCertificate + (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)) : + NativeCertificate + (fun x : ℕ × List ℕ × ℕ × DescribedNetwork (SpecDesc T) => + DescribedNetwork.sumValue SumOps.galois (specEntry entry) (x.1, x.2.1) x.2.2.2) + (encCore encT) (encList encNat) := + ((DescribedNetwork.contractionCertificate (specEntry entry) SumOps.galois_polyTime + (specEntryCertificate entry ce)).comp + (NativeCertificate.ofPolyTime + ((((ComputableInPolyTime.fst _ _).prod + ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _))).prod + ((ComputableInPolyTime.snd _ _).comp ((ComputableInPolyTime.snd _ _).comp + (ComputableInPolyTime.snd _ _)))) : + ComputableInPolyTime + (fun x : ℕ × List ℕ × ℕ × DescribedNetwork (SpecDesc T) => ((x.1, x.2.1), x.2.2.2)) + (encCore encT) + (DescribedNetwork.encInput (encPair encUnary (encList encNat)) + (encSpecDesc encT))))).congr fun _ => rfl + +/-- `n ≤ 2 ^ deg f` for the modulus `FastContraction.modulus n`: it has enough residues for `n` +points. -/ +theorem le_two_pow_length_modulus (n : ℕ) : n ≤ 2 ^ (FastContraction.modulus n).length := by + have h4 := FastContraction.four_mul_log_le_length_modulus n + have hlt := Nat.lt_pow_succ_log_self (b := 2) one_lt_two n + rcases Nat.eq_zero_or_pos (Nat.log 2 n) with h0 | hpos + · have h2 : n < 2 := by simpa [h0] using hlt + exact (show n ≤ 1 by omega).trans Nat.one_le_two_pow + · exact hlt.le.trans (Nat.pow_le_pow_right (by norm_num) (by omega)) + +/-- Choosing the modulus `FastContraction.modulus n` for `n = (ℓ - 1) k + 1` points is +polynomial-time. -/ +theorem modulusChoice_polyTime : + ComputableInPolyTime + (fun x : ℕ × ℕ × ℕ × DescribedNetwork T => + (FastContraction.modulus (DescribedNetwork.pointCount x.2.1 x.2.2.2), x)) + (encTrunc encT) (encEngine encT) := by + have hpc : ComputableInPolyTime + (fun x : ℕ × ℕ × ℕ × DescribedNetwork T => DescribedNetwork.pointCount x.2.1 x.2.2.2) + (encTrunc encT) encUnary := by + have h := pointCount_polyTime (encT := encT).comp + ((ComputableInPolyTime.const ([] : List ℕ)).prod ComputableInPolyTime.id') + exact h + have h := (FastContraction.modulus_polyTime.comp hpc).prod ComputableInPolyTime.id' + exact h + +/-- **Direct summation through the reduction computes the truncated contraction**, at the modulus +`FastContraction.modulus n` for `n = (ℓ - 1) k + 1` points. -/ +theorem interpContract_direct_eq (P ℓ r : ℕ) (G : DescribedNetwork T) : + DescribedNetwork.interpContract + (fun x : ℕ × List ℕ × ℕ × DescribedNetwork (SpecDesc T) => + DescribedNetwork.sumValue SumOps.galois (specEntry entry) (x.1, x.2.1) x.2.2.2) + (FastContraction.modulus (DescribedNetwork.pointCount ℓ G)) P ℓ r G = + G.truncContraction entry P ℓ := by + refine DescribedNetwork.interpContract_eq (entry := entry) + (FastContraction.irreducible_modulus (DescribedNetwork.pointCount ℓ G)) G + (le_two_pow_length_modulus _) fun k _ => ?_ + exact DescribedNetwork.val_sumValue_galois (specEntry entry) + (P, FastContraction.modulus (DescribedNetwork.pointCount ℓ G)) _ + +/-- **The truncated contraction by direct summation**, as one native machine on every input +`(P, ℓ, r, G)`: the reduction with direct summation over `A_P` at the modulus +`FastContraction.modulus n`, for `n = (ℓ - 1) k + 1` points. It is correct everywhere; its cost is +that of direct summation, exponential in the number of edges. -/ +@[expose] noncomputable def truncDirectCertificate + (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)) : + NativeCertificate + (fun x : ℕ × ℕ × ℕ × DescribedNetwork T => x.2.2.2.truncContraction entry x.1 x.2.1) + (encTrunc encT) (encList encNat) := + ((engineCertificate _ (directCoreCertificate entry ce)).comp + (NativeCertificate.ofPolyTime modulusChoice_polyTime)).congr fun x => + interpContract_direct_eq entry x.1 x.2.1 x.2.2.1 x.2.2.2 + +end Cslib.Circuits.Frontier diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedResources.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedResources.lean new file mode 100644 index 000000000..364360abc --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedResources.lean @@ -0,0 +1,731 @@ +/- +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.TruncatedPolyTime +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LinearSpaceArith +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeNatFrontends + +/-! +# Resources of the truncation-order reduction + +The native machine `Cslib.Circuits.Frontier.engineCertificate` of +`Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedPolyTime.lean` runs the reduction +of truncation order `ℓ` to contractions over `A_P = (ℤ / 2 ^ P)[U] / (f)`: it streams over the +`N = (ℓ - 1) k + 1` digit points, calling a given certificate of the contraction over `A_P` once per +point, and then interpolates. This file bounds its time and space by those of the calls. + +**The loop** (`Cslib.Circuits.Frontier.engineCertificate_le`). If at every point the call takes +time at most `R`, space at most `Q`, and outputs at most `Yb` bits, then the machine takes time at +most `(N + 1) (K (n + Yb + 1) ^ K + R)` and space at most `K (n + Yb + 1) ^ K + Q`, for a constant +`K` and the encoded length `n` of the input. The live state is the binary index, the input and the +values so far (`Cslib.Circuits.Frontier.length_run_engineStep_le`), and `N ≤ n ^ 2 + 1` +(`Cslib.Circuits.Frontier.pointCount_le`). + +**The calls.** The input of a call has length at most `9 (n + 1) ^ 2` +(`Cslib.Circuits.Frontier.length_encCore_coreInput_le`): the specialized network copies the +precision, the truncation order, the modulus and the point into every vertex. + +**Specialized entries** (`Cslib.Circuits.Frontier.specEntryCertificate_le`). Evaluating a +specialized entry costs the original entry plus a polynomial in the lengths of the input and of the +original entry. + +**Direct summation** (`Cslib.Circuits.Frontier.directCoreCertificate_le`, +`Cslib.Circuits.Frontier.truncDirectCertificate_le`). If the entry certificate takes time at most +`E` and space at most `ES` on the vertices of a network with `m` edges, direct summation over a +specialized network, and the truncated contraction by direct summation, take time +`K (n + ES + 1) ^ K 2 ^ m (E + 1)` and space `K (n + ES + 1) ^ K`. + +## Main results + +* `Cslib.Circuits.Frontier.engineCertificate_le`: time and space of the reduction. +* `Cslib.Circuits.Frontier.length_encCore_coreInput_le`: the size of a call. +* `Cslib.Circuits.Frontier.specEntryCertificate_le`: time and space of specialized entries. +* `Cslib.Circuits.Frontier.directCoreCertificate_le`, + `Cslib.Circuits.Frontier.truncDirectCertificate_le`: time and space of direct summation. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Theorem D.1 (p. 53). +-/ + +public section + +namespace Cslib.Circuits.Frontier + +open Turing.MultiTapeTM Cslib.GenericRAM GaloisRingArith + +variable {T : Type} {encT : T ↪ List Bool} + +/-! ### Sizes -/ + +/-- A polynomial bound composed with a polynomially bounded size. -/ +private theorem polyBounded_comp_poly {α : Type} {size u : α → ℕ} {p : ℕ → ℕ} + (hp : Cslib.PolynomiallyBounded p) (hu : PolyBounded size u) : + PolyBounded size fun a => p (u a) := + (PolyBounded.of_polynomiallyBounded id hp).comp hu + +/-- A list of values, each at most `Yb` bits, is at most `(2 Yb + 1)` bits per value. -/ +private theorem length_encList_le_of_forall {vals : List (List ℕ)} {Yb : ℕ} + (h : ∀ v ∈ vals, (encList encNat v).length ≤ Yb) : + (encList (encList encNat) vals).length ≤ vals.length * (2 * Yb + 1) := by + rw [length_encList] + have h' := List.sum_le_length_nsmul (vals.map fun a => 2 * (encList encNat a).length + 1) + (2 * Yb + 1) fun x hx => by + obtain ⟨v, hv, rfl⟩ := List.mem_map.mp hx + have := h v hv + omega + rwa [List.length_map, smul_eq_mul] at h' + +/-- The length of an input of the reduction, by components. -/ +theorem length_encEngine (y : List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T) : + (encEngine encT y).length = 2 * (encList encNat y.1).length + 1 + + (2 * y.2.1 + 1 + (2 * y.2.2.1 + 1 + + (2 * (encNat y.2.2.2.1).length + 1 + + (DescribedNetwork.encDescribed encT y.2.2.2.2).length))) := by + simp [encEngine, encTrunc] + +/-- **The number of points is at most `n ^ 2 + 1`** for an input of length `n`: the truncation +order is in unary, and there are at most `n` vertices. -/ +theorem pointCount_le (y : List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T) : + DescribedNetwork.pointCount y.2.2.1 y.2.2.2.2 ≤ + (encEngine encT y).length * (encEngine encT y).length + 1 := by + have hk := DescribedNetwork.length_numEdges_vertices_le (encT := encT) y.2.2.2.2 + have hlen := length_encEngine (encT := encT) y + have hℓ : y.2.2.1 - 1 ≤ (encEngine encT y).length := by omega + have hv : y.2.2.2.2.vertices.length ≤ (encEngine encT y).length := by omega + exact Nat.add_le_add_right (Nat.mul_le_mul hℓ hv) 1 + +/-- The length of an encoded described network, by components. -/ +private theorem length_encDescribed {T' : Type} (encT' : T' ↪ List Bool) + (G : DescribedNetwork T') : + (DescribedNetwork.encDescribed encT' G).length = + 2 * G.numEdges + 1 + (encList (encPair (encList encNat) encT') G.vertices).length := by + simp [DescribedNetwork.encDescribed, DescribedNetwork.equivProd] + +/-- A binary-digit point has at most three bits per coordinate. -/ +private theorem length_encList_digits_le (e k : ℕ) : + (encList encNat (FastContraction.digits e k)).length ≤ 3 * e := by + rw [length_encList] + have h := List.sum_le_length_nsmul + ((FastContraction.digits e k).map fun a => 2 * (encNat a).length + 1) 3 fun x hx => by + obtain ⟨b, hb, rfl⟩ := List.mem_map.mp hx + obtain ⟨i, -, rfl⟩ := List.mem_map.mp hb + have := length_encNat_le_self (if k.testBit i then 1 else 0) + split_ifs at this ⊢ <;> omega + simpa [FastContraction.digits, mul_comm] using h + +/-- Copying the data `d` of a specialization into every vertex adds `2 |d|` bits per vertex, and +at most doubles the rest. -/ +private theorem length_encList_spec_le (vs : List (List ℕ × T)) (d : ℕ × ℕ × List ℕ × List ℕ) : + (encList (encPair (encList encNat) (encSpecDesc encT)) + (vs.map fun v => (v.1, (v.2, d)))).length ≤ + 2 * (encList (encPair (encList encNat) encT) vs).length + + vs.length * (2 * (encSpecData d).length) := by + induction vs with + | nil => simp + | cons v vs ih => + simp only [length_encList, List.map_cons, List.map_map, List.sum_cons, List.length_cons, + Function.comp_def, length_encPair, add_one_mul] at ih ⊢ + omega + +/-- **The size of a call.** The input of the contraction at a digit point is at most +`9 (n + 1) ^ 2` bits for an input of the reduction of length `n`: the specialized network copies +the precision, the truncation order, the modulus and the point, at most `3 n` bits, into each of +at most `n` vertices. -/ +theorem length_encCore_coreInput_le (y : List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T) (k : ℕ) : + (encCore encT (coreInput y k)).length ≤ 9 * ((encEngine encT y).length + 1) ^ 2 := by + obtain ⟨fl, P, ℓ, r, G⟩ := y + have hlen := length_encEngine (encT := encT) (fl, P, ℓ, r, G) + have hG := length_encDescribed encT G + have hk := DescribedNetwork.length_numEdges_vertices_le (encT := encT) G + have hζ := length_encList_digits_le fl.length k + have hfl := length_le_length_encList encNat fl + have hspec := length_encList_spec_le (encT := encT) G.vertices + (P, ℓ, fl, FastContraction.digits fl.length k) + set L := (encEngine encT (fl, P, ℓ, r, G)).length + have hd : (encSpecData (P, ℓ, fl, FastContraction.digits fl.length k)).length ≤ 3 * L := by + simp only [length_encPair, encUnary_apply, List.length_replicate] at hlen ⊢ + omega + have hkL : G.vertices.length ≤ L := by simp only at hlen; omega + have hmul : G.vertices.length * + (2 * (encSpecData (P, ℓ, fl, FastContraction.digits fl.length k)).length) ≤ L * (6 * L) := + Nat.mul_le_mul hkL (by omega) + simp only [coreInput, encCore, length_encPair, encUnary_apply, List.length_replicate, + length_encDescribed, DescribedNetwork.numEdges_specNet, DescribedNetwork.vertices_specNet] + at hspec ⊢ + simp only at hlen hG hk + nlinarith + +variable (core : ℕ × List ℕ × ℕ × DescribedNetwork (SpecDesc T) → List ℕ) + +/-- The encoding of the state of the loop: the binary index, the input and the values so far. -/ +local notation "encS" => encPair encNat (encPair (encEngine encT) (encList (encList encNat))) + +/-- **The live state of the loop.** After `j` rounds, if each of the first `j` values is at most +`Yb` bits, the state is at most `2 |j| + 2 n + 2 + j (2 Yb + 1)` bits, for the binary length `|j|` +of `j` and the length `n` of the input. -/ +theorem length_run_engineStep_le (y : List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T) {j Yb : ℕ} + (hY : ∀ k < j, (encList encNat (core (coreInput y k))).length ≤ Yb) : + (encS (IndexFold.run (engineStep core) j (y, []))).length ≤ + 2 * (encNat j).length + 2 * (encEngine encT y).length + 2 + j * (2 * Yb + 1) := by + rw [run_engineStep] + have h := length_encList_le_of_forall (vals := (List.range j).map fun k => core (coreInput y k)) + (Yb := Yb) fun v hv => by + obtain ⟨k, hk, rfl⟩ := List.mem_map.mp hv + exact hY k (List.mem_range.mp hk) + simp only [List.length_map, List.length_range] at h + simp only [length_encPair] + omega + +/-! ### The loop -/ + +/-- **Time and space of the reduction.** There is `K` such that, on an input `y` of length `n` with +`N = (ℓ - 1) k + 1` points, if at each of the indices `0, …, N` the call takes time at most `R` +and space at most `Q` and outputs at most `Yb` bits, the reduction takes time at most +`(N + 1) (K (n + Yb + 1) ^ K + R)` and space at most `K (n + Yb + 1) ^ K + Q`. (The loop charges +one more round than it runs, at the index `N`.) -/ +theorem engineCertificate_le (cc : NativeCertificate core (encCore encT) (encList encNat)) : + ∃ K : ℕ, ∀ (y : List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T) (R Q Yb : ℕ), + (∀ k ≤ DescribedNetwork.pointCount y.2.2.1 y.2.2.2.2, + cc.time (coreInput y k) ≤ R ∧ cc.space (coreInput y k) ≤ Q ∧ + (encList encNat (core (coreInput y k))).length ≤ Yb) → + (engineCertificate core cc).time y ≤ + (DescribedNetwork.pointCount y.2.2.1 y.2.2.2.2 + 1) * + (K * ((encEngine encT y).length + Yb + 1) ^ K + R) ∧ + (engineCertificate core cc).space y ≤ + K * ((encEngine encT y).length + Yb + 1) ^ K + Q := by + -- The polynomial-time pieces. + have hcN : ComputableInPolyTime + (fun y : List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T => + DescribedNetwork.pointCount y.2.2.1 y.2.2.2.2) (encEngine encT) encNat := + ComputableInPolyTime.unary_to_binary.comp pointCount_polyTime + have hcI : ComputableInPolyTime + (fun y : List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T => (y, ([] : List (List ℕ)))) + (encEngine encT) (encPair (encEngine encT) (encList (encList encNat))) := + ComputableInPolyTime.id'.prod (ComputableInPolyTime.const []) + have hcA : ComputableInPolyTime + (fun p : ℕ × ((List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T) × List (List ℕ)) => p.2.1) + encS (encEngine encT) := + (ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _) + have hcC : ComputableInPolyTime + (fun p : ℕ × ((List ℕ × ℕ × ℕ × ℕ × DescribedNetwork T) × List (List ℕ)) => p.2.2) + encS (encList (encList encNat)) := + (ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.snd _ _) + have hcB := ComputableInPolyTime.snoc (encList encNat) + obtain ⟨pN, hpN, mN, bN⟩ := exists_mono_poly_cert hcN + obtain ⟨pI, hpI, mI, bI⟩ := exists_mono_poly_cert hcI + obtain ⟨pA, hpA, mA, bA⟩ := exists_mono_poly_cert hcA + obtain ⟨pC, hpC, mC, bC⟩ := exists_mono_poly_cert hcC + obtain ⟨pB, hpB, mB, bB⟩ := exists_mono_poly_cert hcB + obtain ⟨pD, hpD, mD, bD⟩ := exists_mono_poly_cert (coreInput_polyTime (encT := encT)) + obtain ⟨pR, hpR, mR, bR⟩ := exists_mono_poly_cert (engineRecover_polyTime (encT := encT)) + -- The overhead, as a polynomial in `X = n + Yb`. + let Sh : ℕ → ℕ := fun X => 7 * (X + 1) ^ 3 + let U : ℕ → ℕ := fun X => pN X + X + pI X + 3 * Sh X + 3 * ((X + 1) ^ 2 + 1) ^ 2 + + pA (Sh X) + pC (Sh X) + pD (Sh X) + pB (2 * Sh X + 1 + X) + pR (Sh X) + have hSh : PolyBounded id Sh := + (PolyBounded.const 7).mul ((PolyBounded.self.add (PolyBounded.const 1)).pow 3) + have hU : PolyBounded id U := + (((((((((polyBounded_comp_poly hpN PolyBounded.self).add PolyBounded.self).add + (polyBounded_comp_poly hpI PolyBounded.self)).add ((PolyBounded.const 3).mul hSh)).add + ((PolyBounded.const 3).mul ((((PolyBounded.self.add (PolyBounded.const 1)).pow 2).add + (PolyBounded.const 1)).pow 2))).add (polyBounded_comp_poly hpA hSh)).add + (polyBounded_comp_poly hpC hSh)).add (polyBounded_comp_poly hpD hSh)).add + (polyBounded_comp_poly hpB ((((PolyBounded.const 2).mul hSh).add (PolyBounded.const 1)).add + PolyBounded.self))).add (polyBounded_comp_poly hpR hSh) + obtain ⟨a, d, hUad⟩ := hU.exists_le + refine ⟨a + d, fun y R Q Yb hcore => ?_⟩ + set L := (encEngine encT y).length with hL + set N := DescribedNetwork.pointCount y.2.2.1 y.2.2.2.2 with hN + set X := L + Yb with hX + have hUX : U X ≤ (a + d) * (X + 1) ^ (a + d) := by + have h1 := hUad X + have h2 : (X + 1) ^ d ≤ (X + 1) ^ (a + d) := Nat.pow_le_pow_right (by omega) (by omega) + simp only [id] at h1 + calc U X ≤ a * (X + 1) ^ d := h1 + _ ≤ (a + d) * (X + 1) ^ (a + d) := Nat.mul_le_mul (by omega) h2 + -- Sizes of the states. + have hNL : N ≤ L * L + 1 := pointCount_le y + have hNX : N ≤ (X + 1) ^ 2 := by + have : L * L ≤ X * X := Nat.mul_le_mul (by omega) (by omega) + nlinarith + let S := 2 * N + 2 * L + 2 + N * (2 * Yb + 1) + have hSSh : S ≤ Sh X := by + have h1 : N * (2 * Yb + 1) ≤ (X + 1) ^ 2 * (2 * X + 2) := Nat.mul_le_mul hNX (by omega) + have h2 : (X + 1) ^ 2 ≤ (X + 1) ^ 3 := Nat.pow_le_pow_right (by omega) (by omega) + have h3 : X + 1 ≤ (X + 1) ^ 3 := by + calc X + 1 = (X + 1) ^ 1 := (pow_one _).symm + _ ≤ (X + 1) ^ 3 := Nat.pow_le_pow_right (by omega) (by omega) + have h4 : (X + 1) ^ 2 * (2 * X + 2) = 2 * (X + 1) ^ 3 := by ring + simp only [Sh, S] + omega + have hstate (j : ℕ) (hj : j ≤ N) : + (encS (IndexFold.run (engineStep core) j (y, []))).length ≤ S := by + have h := length_run_engineStep_le (encT := encT) core y (j := j) (Yb := Yb) + fun k hk => (hcore k (by omega)).2.2 + have hj' : (encNat j).length ≤ N := (length_encNat_mono hj).trans (length_encNat_le_self N) + have hjN : j * (2 * Yb + 1) ≤ N * (2 * Yb + 1) := Nat.mul_le_mul_right _ hj + omega + -- The values so far, then the snoc input, are bounded by the state. + have hsnoc (j : ℕ) (hj : j ≤ N) : + (encPair (encList (encList encNat)) (encList encNat) + ((IndexFold.run (engineStep core) j (y, [])).2.2, + core (coreInput (IndexFold.run (engineStep core) j (y, [])).2.1 + (IndexFold.run (engineStep core) j (y, [])).1))).length ≤ 2 * S + 1 + Yb := by + have hs := hstate j hj + have hY := (hcore j hj).2.2 + rw [run_engineStep] at hs ⊢ + simp only [length_encPair] at hs ⊢ + omega + have hround_time (j : ℕ) (hj : j ≤ N) : + (IndexFold.roundCertificate (engineStepCertificate core cc)).time + (IndexFold.run (engineStep core) j (y, [])) ≤ + S + (N + 1) ^ 2 + pA (Sh X) + pC (Sh X) + pD (Sh X) + pB (2 * Sh X + 1 + X) + R := by + have hs := hstate j hj + have hsn := hsnoc j hj + simp only [IndexFold.roundCertificate, engineStepCertificate, NativeCertificate.comp_time, + NativeCertificate.prod_time] + have h1 := (bA (IndexFold.run (engineStep core) j (y, []))).1.trans (mA (hs.trans hSSh)) + have h2 := (bC (IndexFold.run (engineStep core) j (y, []))).1.trans (mC (hs.trans hSSh)) + have h3 := (bD (IndexFold.run (engineStep core) j (y, []))).1.trans (mD (hs.trans hSSh)) + have h4 := (bB _).1.trans (mB (hsn.trans (by omega : 2 * S + 1 + Yb ≤ 2 * Sh X + 1 + X))) + have hidx : (encNat (IndexFold.run (engineStep core) j (y, [])).1).length + 1 ≤ N + 1 := by + rw [IndexFold.run_index] + exact Nat.add_le_add_right ((length_encNat_mono hj).trans (length_encNat_le_self N)) 1 + have hsq := Nat.pow_le_pow_left hidx 2 + have hR := (hcore j hj).1 + rw [run_engineStep] at h1 h2 h3 h4 hs hsq ⊢ + simp only [Function.comp_apply] at h1 h2 h3 h4 hs hsq ⊢ + omega + have hround_space (j : ℕ) (hj : j ≤ N) : + (IndexFold.roundCertificate (engineStepCertificate core cc)).space + (IndexFold.run (engineStep core) j (y, [])) ≤ + S + (N + 1) + pA (Sh X) + pC (Sh X) + pD (Sh X) + pB (2 * Sh X + 1 + X) + Q := by + have hs := hstate j hj + have hsn := hsnoc j hj + simp only [IndexFold.roundCertificate, engineStepCertificate, NativeCertificate.comp_space, + NativeCertificate.prod_space] + have h1 := (bA (IndexFold.run (engineStep core) j (y, []))).2.trans (mA (hs.trans hSSh)) + have h2 := (bC (IndexFold.run (engineStep core) j (y, []))).2.trans (mC (hs.trans hSSh)) + have h3 := (bD (IndexFold.run (engineStep core) j (y, []))).2.trans (mD (hs.trans hSSh)) + have h4 := (bB _).2.trans (mB (hsn.trans (by omega : 2 * S + 1 + Yb ≤ 2 * Sh X + 1 + X))) + have hidx : (encNat (IndexFold.run (engineStep core) j (y, [])).1).length ≤ N := by + rw [IndexFold.run_index] + exact (length_encNat_mono hj).trans (length_encNat_le_self N) + have hQ := (hcore j hj).2.1 + rw [run_engineStep] at h1 h2 h3 h4 hs hidx ⊢ + simp only [Function.comp_apply] at h1 h2 h3 h4 hs hidx ⊢ + omega + -- The trajectory maxima. + have hmaxT : NativeCertificate.maxRoundTime + (IndexFold.roundCertificate (engineStepCertificate core cc)) N (0, y, []) ≤ + S + (N + 1) ^ 2 + pA (Sh X) + pC (Sh X) + pD (Sh X) + pB (2 * Sh X + 1 + X) + R := + NativeCertificate.maxRoundTime_le _ _ _ fun j hj => hround_time j hj + have hmaxS : NativeCertificate.maxRoundSpace + (IndexFold.roundCertificate (engineStepCertificate core cc)) N (0, y, []) ≤ + S + (N + 1) + pA (Sh X) + pC (Sh X) + pD (Sh X) + pB (2 * Sh X + 1 + X) + Q := + NativeCertificate.maxRoundSpace_le _ _ _ fun j hj => hround_space j hj + have hmaxL : NativeCertificate.maxStateLength encS (IndexFold.step (engineStep core)) N + (0, y, []) ≤ S := + NativeCertificate.maxStateLength_le _ _ _ _ fun j hj => hstate j hj + -- The pieces outside the loop. + have hLX : L ≤ X := by omega + have hNt := (bN y).1.trans (mN hLX) + have hNs := (bN y).2.trans (mN hLX) + have hIt := (bI y).1.trans (mI hLX) + have hIs := (bI y).2.trans (mI hLX) + have hRt := (bR (IndexFold.run (engineStep core) N (y, []))).1.trans + (mR ((hstate N le_rfl).trans hSSh)) + have hRs := (bR (IndexFold.run (engineStep core) N (y, []))).2.trans + (mR ((hstate N le_rfl).trans hSSh)) + have hNlen : (encNat N).length ≤ N := length_encNat_le_self N + have hsq : ((encNat N).length + 1) ^ 2 ≤ (N + 1) ^ 2 := Nat.pow_le_pow_left (by omega) 2 + have hNsq : (N + 1) ^ 2 ≤ ((X + 1) ^ 2 + 1) ^ 2 := Nat.pow_le_pow_left (by omega) 2 + have hN1 : N ≤ (N + 1) ^ 2 := by nlinarith + refine ⟨?_, ?_⟩ + · rw [engineCertificate, NativeCertificate.congr_time, NativeCertificate.comp_time, + IndexFold.certificate, NativeCertificate.iterate_time] + simp only [NativeCertificate.prod_time, NativeCertificate.const_time, Function.comp_apply] + rw [← hN, ← hL] + set P4 := pA (Sh X) + pC (Sh X) + pD (Sh X) + pB (2 * Sh X + 1 + X) + set A := pN X + X + pI X + pR (Sh X) + have hA : A ≤ (N + 1) * A := Nat.le_mul_of_pos_left _ (by omega) + have hB := Nat.mul_le_mul_left (N + 1) (show + NativeCertificate.maxRoundTime (IndexFold.roundCertificate (engineStepCertificate core cc)) + N (0, y, []) + + NativeCertificate.maxStateLength encS (IndexFold.step (engineStep core)) N (0, y, []) + + ((encNat N).length + 1) ^ 2 ≤ 2 * S + 2 * (N + 1) ^ 2 + P4 + R by omega) + have hsum : (N + 1) * A + (N + 1) * (2 * S + 2 * (N + 1) ^ 2 + P4 + R) = + (N + 1) * (A + 2 * S + 2 * (N + 1) ^ 2 + P4 + R) := by ring + have hC := Nat.mul_le_mul_left (N + 1) + (show A + 2 * S + 2 * (N + 1) ^ 2 + P4 + R ≤ (a + d) * (X + 1) ^ (a + d) + R by + simp only [U] at hUX + omega) + omega + · rw [engineCertificate, NativeCertificate.congr_space, NativeCertificate.comp_space, + IndexFold.certificate, NativeCertificate.iterate_space] + simp only [NativeCertificate.prod_space, NativeCertificate.const_space, Function.comp_apply] + rw [← hN, ← hL] + simp only [U] at hUX + omega + +/-! ### Specialized entries -/ + +/-- **Time and space of specialized entries.** There is `K` such that, for every entry +certificate `ce`, evaluating the specialized entry at `q = ((t, P, ℓ, fl, ζ), bs)` costs the +original entry at `(t, bs)` plus `K (n + e + 1) ^ K`, in time and in space, for the length `n` of +`q` and the length `e` of the original entry. -/ +theorem specEntryCertificate_le : + ∃ K : ℕ, ∀ (entry : T → List Bool → List ℕ) + (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)) (q : SpecDesc T × List Bool), + (specEntryCertificate entry ce).time q ≤ ce.time (q.1.1, q.2) + + K * ((encPair (encSpecDesc encT) encBits q).length + + (encList encNat (entry q.1.1 q.2)).length + 1) ^ K ∧ + (specEntryCertificate entry ce).space q ≤ ce.space (q.1.1, q.2) + + K * ((encPair (encSpecDesc encT) encBits q).length + + (encList encNat (entry q.1.1 q.2)).length + 1) ^ K := by + have hcD : ComputableInPolyTime (fun q : SpecDesc T × List Bool => q.1.2) + (encPair (encSpecDesc encT) encBits) encSpecData := + (ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.fst _ _) + have hcE : ComputableInPolyTime (fun q : SpecDesc T × List Bool => (q.1.1, q.2)) + (encPair (encSpecDesc encT) encBits) (encPair encT encBits) := + ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.fst _ _)).prod + (ComputableInPolyTime.snd _ _) + obtain ⟨pD, hpD, mD, bD⟩ := exists_mono_poly_cert hcD + obtain ⟨pE, hpE, mE, bE⟩ := exists_mono_poly_cert hcE + obtain ⟨pH, hpH, mH, bH⟩ := exists_mono_poly_cert horner_polyTime + let U : ℕ → ℕ := fun Z => pD Z + pE Z + pH (2 * Z + 1) + have hU : PolyBounded id U := + ((polyBounded_comp_poly hpD PolyBounded.self).add + (polyBounded_comp_poly hpE PolyBounded.self)).add + (polyBounded_comp_poly hpH (((PolyBounded.const 2).mul PolyBounded.self).add + (PolyBounded.const 1))) + obtain ⟨a, d, hUad⟩ := hU.exists_le + refine ⟨a + d, fun entry ce q => ?_⟩ + set n := (encPair (encSpecDesc encT) encBits q).length with hn + set Z := n + (encList encNat (entry q.1.1 q.2)).length with hZ + have hUZ : U Z ≤ (a + d) * (Z + 1) ^ (a + d) := by + have h1 := hUad Z + simp only [id] at h1 + exact h1.trans (Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right (by omega) (by omega))) + have hnZ : n ≤ Z := by omega + have hH : (encPair encSpecData (encList encNat) (q.1.2, entry q.1.1 q.2)).length ≤ 2 * Z + 1 := by + have : (encSpecData q.1.2).length ≤ n := by + simp only [hn, length_encPair] + omega + simp only [length_encPair] at this ⊢ + omega + simp only [U] at hUZ + have h1 := (bD q).1.trans (mD hnZ) + have h2 := (bE q).1.trans (mE hnZ) + have h3 := (bH (q.1.2, entry q.1.1 q.2)).1.trans (mH hH) + have h1' := (bD q).2.trans (mD hnZ) + have h2' := (bE q).2.trans (mE hnZ) + have h3' := (bH (q.1.2, entry q.1.1 q.2)).2.trans (mH hH) + refine ⟨?_, ?_⟩ + · simp only [specEntryCertificate, NativeCertificate.congr, NativeCertificate.comp_time, + NativeCertificate.prod_time, Function.comp_apply] + omega + · simp only [specEntryCertificate, NativeCertificate.congr, NativeCertificate.comp_space, + NativeCertificate.prod_space, Function.comp_apply] + omega + +/-! ### Direct summation -/ + +/-- A vertex is no longer than its network. -/ +private theorem length_vertex_le {T' : Type} (encT' : T' ↪ List Bool) (G : DescribedNetwork T') + {v : List ℕ × T'} (hv : v ∈ G.vertices) : + (encPair (encList encNat) encT' v).length ≤ (DescribedNetwork.encDescribed encT' G).length := by + have h1 := List.le_sum_of_mem + (List.mem_map_of_mem (f := fun a => (encPair (encList encNat) encT' a).length) hv) + have h2 := sum_length_le_length_encList (encPair (encList encNat) encT') G.vertices + rw [length_encDescribed] + omega + +/-- **Time and space of direct summation over a specialized network.** There is `K` such that, +at the input `x = (P, fl, r, G')` for the network `G'` specialized at a point, of length `n`, if +the entry certificate takes time at most `E` and space at most `ES` at every vertex of the original +network `G` with `m` edges and every list of bits on its ports, then direct summation takes time +at most `K (n + ES + 1) ^ K 2 ^ m (E + 1)` and space at most `K (n + ES + 1) ^ K`. -/ +theorem directCoreCertificate_le (entry : T → List Bool → List ℕ) + (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)) : + ∃ K : ℕ, ∀ (P ℓ r : ℕ) (fl ζ : List ℕ) (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) → + (directCoreCertificate entry ce).time (P, fl, r, DescribedNetwork.specNet P ℓ fl ζ G) ≤ + K * ((encCore encT (P, fl, r, DescribedNetwork.specNet P ℓ fl ζ G)).length + ES + 1) ^ K * + 2 ^ G.numEdges * (E + 1) ∧ + (directCoreCertificate entry ce).space (P, fl, r, DescribedNetwork.specNet P ℓ fl ζ G) ≤ + K * ((encCore encT (P, fl, r, DescribedNetwork.specNet P ℓ fl ζ G)).length + ES + 1) ^ + K := by + obtain ⟨cE, -, hcE⟩ := ce.computes + obtain ⟨K₃, hK₃⟩ := specEntryCertificate_le (encT := encT) + obtain ⟨cS, -, hcS⟩ := (specEntryCertificate entry ce).computes + obtain ⟨K₂, hK₂⟩ := DescribedNetwork.contractionCertificate_le (eval := specEntry entry) + SumOps.galois_polyTime (specEntryCertificate entry ce) + have hcR : ComputableInPolyTime + (fun x : ℕ × List ℕ × ℕ × DescribedNetwork (SpecDesc T) => ((x.1, x.2.1), x.2.2.2)) + (encCore encT) + (DescribedNetwork.encInput (encPair encUnary (encList encNat)) (encSpecDesc encT)) := + ((ComputableInPolyTime.fst _ _).prod + ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _))).prod + ((ComputableInPolyTime.snd _ _).comp ((ComputableInPolyTime.snd _ _).comp + (ComputableInPolyTime.snd _ _))) + obtain ⟨pS, hpS, mS, bS⟩ := exists_mono_poly_cert hcR + -- The overheads, as polynomials in `Z = n + ES`. + let Af : ℕ → ℕ := fun Z => 3 * Z + 1 + cE * (Z + 1) + 1 + let Uf : ℕ → ℕ := fun Z => K₃ * Af Z ^ K₃ + let Bf : ℕ → ℕ := fun Z => + K₂ * (2 * Z + 1 + cS * (Z + Uf Z + 1) + Z * (2 * Z + 3) + 1) ^ K₂ + let Tf : ℕ → ℕ := fun Z => pS Z + (Z + 2) * (Bf Z + 2 * Uf Z) + (Z + 2) * 2 + let Sf : ℕ → ℕ := fun Z => pS Z + Bf Z + (Z + Uf Z) + have hAp : PolyBounded id Af := + ((((PolyBounded.const 3).mul PolyBounded.self).add (PolyBounded.const 1)).add + ((PolyBounded.const cE).mul (PolyBounded.self.add (PolyBounded.const 1)))).add + (PolyBounded.const 1) + have hUp : PolyBounded id Uf := (PolyBounded.const K₃).mul (hAp.pow K₃) + have hBp : PolyBounded id Bf := + (PolyBounded.const K₂).mul ((((((PolyBounded.const 2).mul PolyBounded.self).add + (PolyBounded.const 1)).add ((PolyBounded.const cS).mul ((PolyBounded.self.add hUp).add + (PolyBounded.const 1)))).add (PolyBounded.self.mul (((PolyBounded.const 2).mul + PolyBounded.self).add (PolyBounded.const 3)))).add (PolyBounded.const 1) |>.pow K₂) + have hTSp : PolyBounded id fun Z => Tf Z + Sf Z := + ((((polyBounded_comp_poly hpS PolyBounded.self).add + ((PolyBounded.self.add (PolyBounded.const 2)).mul + (hBp.add ((PolyBounded.const 2).mul hUp)))).add + ((PolyBounded.self.add (PolyBounded.const 2)).mul (PolyBounded.const 2)))).add + (((polyBounded_comp_poly hpS PolyBounded.self).add hBp).add (PolyBounded.self.add hUp)) + obtain ⟨a, d, had⟩ := hTSp.exists_le + refine ⟨a + d, fun P ℓ r fl ζ G E ES hE => ?_⟩ + set G' := DescribedNetwork.specNet P ℓ fl ζ G with hG' + set n := (encCore encT (P, fl, r, G')).length with hn + set Z := n + ES with hZ + set X := 2 ^ G.numEdges with hX + have hX1 : 1 ≤ X := Nat.one_le_two_pow + have hG'n : (DescribedNetwork.encDescribed (encSpecDesc encT) G').length ≤ n := by + simp only [hn, encCore, length_encPair] + omega + -- The specialized entries. + have hv : ∀ v' ∈ G'.vertices, ∀ bs : List Bool, bs.length = v'.1.length → + (specEntryCertificate entry ce).time (v'.2, bs) ≤ E + Uf Z ∧ + (specEntryCertificate entry ce).space (v'.2, bs) ≤ ES + Uf Z ∧ + (encList encNat (specEntry entry v'.2 bs)).length ≤ cS * (Z + Uf Z + 1) := by + intro v' hv' bs hbs + have hvl := length_vertex_le (encSpecDesc encT) G' hv' + rw [hG', DescribedNetwork.vertices_specNet, List.mem_map] at hv' + obtain ⟨v, hvG, rfl⟩ := hv' + simp only at hbs ⊢ + obtain ⟨hEt, hEs⟩ := hE v hvG bs hbs + have hent : (encList encNat (entry v.2 bs)).length ≤ cE * (ES + 1) := + (hcE (v.2, bs)).trans (Nat.mul_le_mul_left _ (by omega)) + obtain ⟨h1, h2⟩ := hK₃ entry ce ((v.2, P, ℓ, fl, ζ), bs) + simp only at h1 h2 + have hq : (encPair (encSpecDesc encT) encBits ((v.2, P, ℓ, fl, ζ), bs)).length + + (encList encNat (entry v.2 bs)).length + 1 ≤ Af Z := by + have hports := length_le_length_encList encNat v.1 + have hcE' : cE * (ES + 1) ≤ cE * (Z + 1) := Nat.mul_le_mul_left _ (by omega) + simp only [length_encPair, encBits_apply] at hvl ⊢ + simp only [Af] + omega + have hpow : K₃ * ((encPair (encSpecDesc encT) encBits ((v.2, P, ℓ, fl, ζ), bs)).length + + (encList encNat (entry v.2 bs)).length + 1) ^ K₃ ≤ Uf Z := + Nat.mul_le_mul_left K₃ (Nat.pow_le_pow_left hq K₃) + have ht : (specEntryCertificate entry ce).time ((v.2, P, ℓ, fl, ζ), bs) ≤ E + Uf Z := + h1.trans (Nat.add_le_add hEt hpow) + have hs : (specEntryCertificate entry ce).space ((v.2, P, ℓ, fl, ζ), bs) ≤ ES + Uf Z := + h2.trans (Nat.add_le_add hEs hpow) + have hout := hcS ((v.2, P, ℓ, fl, ζ), bs) + have hZ' : ES ≤ Z := by omega + refine ⟨ht, hs, hout.trans (Nat.mul_le_mul_left _ ?_)⟩ + exact Nat.add_le_add_right (hs.trans (Nat.add_le_add_right hZ' _)) 1 + have hr : ∀ z, SumOps.galois.Reduced (P, fl) z → (encList encNat z).length ≤ Z * (2 * Z + 3) := + fun z hz => (SumOps.length_encList_le_of_galois_reduced hz).trans (by + have hfl := length_le_length_encList encNat fl + have hlen : (encList encNat fl).length + P ≤ n := by + simp only [hn, encCore, length_encPair, encUnary_apply, List.length_replicate] + omega + dsimp only + exact Nat.mul_le_mul (by omega) (by omega)) + obtain ⟨hT, hS⟩ := hK₂ ((P, fl), G') (E + Uf Z) (ES + Uf Z) (cS * (Z + Uf Z + 1)) + (Z * (2 * Z + 3)) hv hr + have hin : (DescribedNetwork.encInput (encPair encUnary (encList encNat)) (encSpecDesc encT) + ((P, fl), G')).length ≤ 2 * Z + 1 := by + have : (DescribedNetwork.encInput (encPair encUnary (encList encNat)) (encSpecDesc encT) + ((P, fl), G')).length ≤ 2 * n + 1 := by + simp only [hn, DescribedNetwork.encInput, encCore, length_encPair] + omega + omega + have hB : K₂ * ((DescribedNetwork.encInput (encPair encUnary (encList encNat)) + (encSpecDesc encT) ((P, fl), G')).length + cS * (Z + Uf Z + 1) + Z * (2 * Z + 3) + 1) ^ K₂ ≤ + Bf Z := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) _) + have hk : G'.vertices.length ≤ Z := by + have := DescribedNetwork.length_numEdges_vertices_le (encT := encSpecDesc encT) G' + omega + have hedges : G'.numEdges = G.numEdges := rfl + rw [hedges] at hT + have hfac : X * (G'.vertices.length + 1) + 1 ≤ X * (Z + 2) := by + have := Nat.mul_le_mul_left X (show G'.vertices.length + 1 ≤ Z + 1 by omega) + have e : X * (Z + 2) = X * (Z + 1) + X := by ring + omega + have hT' := hT.trans (Nat.mul_le_mul hfac (Nat.add_le_add_right hB _)) + have hRt := (bS (P, fl, r, G')).1.trans (mS (show n ≤ Z by omega)) + have hRs := (bS (P, fl, r, G')).2.trans (mS (show n ≤ Z by omega)) + have h1 := had Z + simp only [id] at h1 + have hK : a * (Z + 1) ^ d ≤ (a + d) * (Z + 1) ^ (a + d) := + Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right (by omega) (by omega)) + refine ⟨?_, ?_⟩ + · simp only [directCoreCertificate, NativeCertificate.congr, NativeCertificate.comp_time, + Function.comp_apply] + -- `pS Z + X (Z + 2) (B + 2 (E + U)) ≤ X (E + 1) T`. + have hsplit : pS Z + X * (Z + 2) * (Bf Z + 2 * (E + Uf Z)) ≤ X * (Tf Z * (E + 1)) := by + have e : X * (Z + 2) * (Bf Z + 2 * (E + Uf Z)) = + X * ((Z + 2) * (Bf Z + 2 * Uf Z)) + X * ((Z + 2) * 2 * E) := by ring + have e2 : X * (Tf Z * (E + 1)) = X * (Tf Z * E) + X * Tf Z := by ring + have h3 : pS Z + X * ((Z + 2) * (Bf Z + 2 * Uf Z)) ≤ X * Tf Z := by + have := Nat.le_mul_of_pos_left (pS Z) hX1 + have e3 : X * Tf Z = X * pS Z + X * ((Z + 2) * (Bf Z + 2 * Uf Z)) + X * ((Z + 2) * 2) := + by simp only [Tf]; ring + omega + have hT2 : (Z + 2) * 2 ≤ Tf Z := by simp only [Tf]; omega + have h4 : X * ((Z + 2) * 2 * E) ≤ X * (Tf Z * E) := + Nat.mul_le_mul_left _ (Nat.mul_le_mul_right _ hT2) + omega + have hfin : X * (Tf Z * (E + 1)) ≤ (a + d) * (Z + 1) ^ (a + d) * X * (E + 1) := by + calc X * (Tf Z * (E + 1)) ≤ X * (a * (Z + 1) ^ d * (E + 1)) := + Nat.mul_le_mul_left _ (Nat.mul_le_mul_right _ (by omega)) + _ = a * (Z + 1) ^ d * X * (E + 1) := by ring + _ ≤ _ := Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ hK) + have hpS : (NativeCertificate.ofPolyTime hcR).time (P, fl, r, G') ≤ pS Z := hRt + omega + · simp only [directCoreCertificate, NativeCertificate.congr, NativeCertificate.comp_space, + Function.comp_apply] + have : Sf Z ≤ a * (Z + 1) ^ d := by omega + simp only [Sf] at this + omega + +/-- **Time and space of the truncated contraction by direct summation.** There is `K` such that, +on an input `x = (P, ℓ, r, G)` of length `n` with `m` edges, if the entry certificate takes time at +most `E` and space at most `ES` at every vertex and every list of bits on its ports, then +`truncDirectCertificate` takes time at most `K (n + ES + 1) ^ K 2 ^ m (E + 1)` and space at most +`K (n + ES + 1) ^ K`. -/ +theorem truncDirectCertificate_le (entry : T → List Bool → List ℕ) + (ce : NativeCertificate (fun q : T × List Bool => entry q.1 q.2) (encPair encT encBits) + (encList encNat)) : + ∃ K : ℕ, ∀ (x : ℕ × ℕ × ℕ × DescribedNetwork T) (E ES : ℕ), + (∀ v ∈ x.2.2.2.vertices, ∀ bs : List Bool, bs.length = v.1.length → + ce.time (v.2, bs) ≤ E ∧ ce.space (v.2, bs) ≤ ES) → + (truncDirectCertificate entry ce).time x ≤ + K * ((encTrunc encT x).length + ES + 1) ^ K * 2 ^ x.2.2.2.numEdges * (E + 1) ∧ + (truncDirectCertificate entry ce).space x ≤ + K * ((encTrunc encT x).length + ES + 1) ^ K := by + obtain ⟨KA, hKA⟩ := directCoreCertificate_le entry ce + obtain ⟨cD, -, hcD⟩ := (directCoreCertificate entry ce).computes + obtain ⟨K₁, hK₁⟩ := engineCertificate_le (encT := encT) _ (directCoreCertificate entry ce) + obtain ⟨pM, hpM, mM, bM⟩ := exists_mono_poly_cert (modulusChoice_polyTime (encT := encT)) + obtain ⟨cY, dY, hY⟩ := (modulusChoice_polyTime (encT := encT)).polyBounded_length.exists_le + -- The overheads, as polynomials in `W = n + ES`. + let Yf : ℕ → ℕ := fun W => cY * (W + 1) ^ dY + let Rf : ℕ → ℕ := fun W => KA * (9 * (Yf W + 1) ^ 2 + W + 1) ^ KA + let Engf : ℕ → ℕ := fun W => K₁ * (Yf W + cD * (Rf W + 1) + 1) ^ K₁ + let Tf : ℕ → ℕ := fun W => pM W + (Yf W * Yf W + 2) * (Engf W + Rf W) + let Sf : ℕ → ℕ := fun W => pM W + (Engf W + Rf W) + have hYp : PolyBounded id Yf := + (PolyBounded.const cY).mul ((PolyBounded.self.add (PolyBounded.const 1)).pow dY) + have hRp : PolyBounded id Rf := + (PolyBounded.const KA).mul (((((PolyBounded.const 9).mul ((hYp.add + (PolyBounded.const 1)).pow 2)).add PolyBounded.self).add (PolyBounded.const 1)).pow KA) + have hEngp : PolyBounded id Engf := + (PolyBounded.const K₁).mul (((hYp.add ((PolyBounded.const cD).mul + (hRp.add (PolyBounded.const 1)))).add (PolyBounded.const 1)).pow K₁) + have hTSp : PolyBounded id fun W => Tf W + Sf W := + ((polyBounded_comp_poly hpM PolyBounded.self).add + (((hYp.mul hYp).add (PolyBounded.const 2)).mul (hEngp.add hRp))).add + ((polyBounded_comp_poly hpM PolyBounded.self).add (hEngp.add hRp)) + obtain ⟨a, d, had⟩ := hTSp.exists_le + refine ⟨a + d, fun x E ES hE => ?_⟩ + obtain ⟨P, ℓ, r, G⟩ := x + set n := (encTrunc encT (P, ℓ, r, G)).length with hn + set W := n + ES with hW + set X := 2 ^ G.numEdges with hX + have hX1 : 1 ≤ X := Nat.one_le_two_pow + set fl := FastContraction.modulus (DescribedNetwork.pointCount ℓ G) with hfl + have hLy : (encEngine encT (fl, P, ℓ, r, G)).length ≤ Yf W := (hY (P, ℓ, r, G)).trans + (Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) _)) + have hNy : DescribedNetwork.pointCount ℓ G + 1 ≤ Yf W * Yf W + 2 := by + have h1 := pointCount_le (encT := encT) (fl, P, ℓ, r, G) + have h2 := Nat.mul_le_mul hLy hLy + dsimp only at h1 + omega + -- The calls of the loop. + have hcall (k : ℕ) : + (directCoreCertificate entry ce).time (coreInput (fl, P, ℓ, r, G) k) ≤ Rf W * X * (E + 1) ∧ + (directCoreCertificate entry ce).space (coreInput (fl, P, ℓ, r, G) k) ≤ Rf W ∧ + (encList encNat (DescribedNetwork.sumValue SumOps.galois (specEntry entry) + ((coreInput (fl, P, ℓ, r, G) k).1, (coreInput (fl, P, ℓ, r, G) k).2.1) + (coreInput (fl, P, ℓ, r, G) k).2.2.2)).length ≤ cD * (Rf W + 1) := by + have hc := length_encCore_coreInput_le (encT := encT) (fl, P, ℓ, r, G) k + have hci : coreInput (fl, P, ℓ, r, G) k = + (P, fl, r, DescribedNetwork.specNet P ℓ fl (FastContraction.digits fl.length k) G) := rfl + rw [hci] at hc ⊢ + obtain ⟨hT, hS⟩ := hKA P ℓ r fl (FastContraction.digits fl.length k) G E ES hE + have hR : KA * ((encCore encT (P, fl, r, DescribedNetwork.specNet P ℓ fl + (FastContraction.digits fl.length k) G)).length + ES + 1) ^ KA ≤ Rf W := by + refine Nat.mul_le_mul_left _ (Nat.pow_le_pow_left ?_ _) + have : 9 * ((encEngine encT (fl, P, ℓ, r, G)).length + 1) ^ 2 ≤ 9 * (Yf W + 1) ^ 2 := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) _) + omega + have hS' := hS.trans hR + refine ⟨hT.trans (Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ hR)), hS', ?_⟩ + have hout := hcD + (P, fl, r, DescribedNetwork.specNet P ℓ fl (FastContraction.digits fl.length k) G) + exact hout.trans (Nat.mul_le_mul_left _ (Nat.add_le_add_right hS' 1)) + obtain ⟨hTe, hSe⟩ := hK₁ (fl, P, ℓ, r, G) _ _ _ fun k _ => hcall k + dsimp only at hTe hSe + have hEng : K₁ * ((encEngine encT (fl, P, ℓ, r, G)).length + cD * (Rf W + 1) + 1) ^ K₁ ≤ + Engf W := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) _) + have hMt := (bM (P, ℓ, r, G)).1.trans (mM (show n ≤ W by omega)) + have hMs := (bM (P, ℓ, r, G)).2.trans (mM (show n ≤ W by omega)) + have h1 := had W + simp only [id] at h1 + have hK : a * (W + 1) ^ d ≤ (a + d) * (W + 1) ^ (a + d) := + Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right (by omega) (by omega)) + refine ⟨?_, ?_⟩ + · simp only [truncDirectCertificate, NativeCertificate.congr, NativeCertificate.comp_time] + have hTe' := hTe.trans (Nat.mul_le_mul hNy (Nat.add_le_add_right hEng _)) + have hsum : pM W + (Yf W * Yf W + 2) * (Engf W + Rf W * X * (E + 1)) ≤ + X * (E + 1) * Tf W := by + have hXE : 1 ≤ X * (E + 1) := Nat.one_le_iff_ne_zero.mpr (by positivity) + have h2 : pM W + (Yf W * Yf W + 2) * Engf W ≤ + X * (E + 1) * (pM W + (Yf W * Yf W + 2) * Engf W) := Nat.le_mul_of_pos_left _ hXE + have e1 : (Yf W * Yf W + 2) * (Engf W + Rf W * X * (E + 1)) = + (Yf W * Yf W + 2) * Engf W + X * (E + 1) * ((Yf W * Yf W + 2) * Rf W) := by ring + have e2 : X * (E + 1) * Tf W = X * (E + 1) * (pM W + (Yf W * Yf W + 2) * Engf W) + + X * (E + 1) * ((Yf W * Yf W + 2) * Rf W) := by simp only [Tf]; ring + omega + have hfin : X * (E + 1) * Tf W ≤ (a + d) * (W + 1) ^ (a + d) * X * (E + 1) := by + calc X * (E + 1) * Tf W ≤ X * (E + 1) * (a * (W + 1) ^ d) := + Nat.mul_le_mul_left _ (by omega) + _ ≤ X * (E + 1) * ((a + d) * (W + 1) ^ (a + d)) := Nat.mul_le_mul_left _ hK + _ = (a + d) * (W + 1) ^ (a + d) * X * (E + 1) := by ring + change (NativeCertificate.ofPolyTime modulusChoice_polyTime).time (P, ℓ, r, G) + + (engineCertificate _ (directCoreCertificate entry ce)).time (fl, P, ℓ, r, G) ≤ _ + omega + · simp only [truncDirectCertificate, NativeCertificate.congr, NativeCertificate.comp_space] + change (NativeCertificate.ofPolyTime modulusChoice_polyTime).space (P, ℓ, r, G) + + (engineCertificate _ (directCoreCertificate entry ce)).space (fl, P, ℓ, r, G) ≤ _ + have : Sf W ≤ a * (W + 1) ^ d := by omega + simp only [Sf] at this + omega + +end Cslib.Circuits.Frontier diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/TruncatedEntry.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/TruncatedEntry.lean new file mode 100644 index 000000000..6a849014b --- /dev/null +++ b/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 diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkTruncated.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkTruncated.lean new file mode 100644 index 000000000..dea650606 --- /dev/null +++ b/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 diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkTruncatedAlgorithm.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkTruncatedAlgorithm.lean new file mode 100644 index 000000000..cf09fa820 --- /dev/null +++ b/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 diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkTruncatedEntry.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkTruncatedEntry.lean new file mode 100644 index 000000000..b9ccd07f6 --- /dev/null +++ b/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 diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkTruncatedPolyTime.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkTruncatedPolyTime.lean new file mode 100644 index 000000000..4b8bdc3ef --- /dev/null +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkTruncatedPolyTime.lean @@ -0,0 +1,56 @@ +/- +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.TruncatedPolyTime + +/-! +# Tests for the native machine of truncation order `ℓ` + +Descriptors that are their own entry (a constant list of `V`-coefficients) have a polynomial-time +entry certificate, so direct summation through the reduction is a native machine for their +truncated contraction on every input. The loop's values after `j` rounds are the contractions at +the first `j` digit points. +-/ + +@[expose] public section + +namespace ComplexityTests.TensorNetworkTruncatedPolyTime + +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 _ _) + +/-- **A native machine for the truncated contraction** of constant-entry networks, on every +input `(P, ℓ, r, G)` with `P` and `ℓ` in unary. -/ +noncomputable def truncConstCert : + NativeCertificate + (fun x : ℕ × ℕ × ℕ × DescribedNetwork (List ℕ) => + x.2.2.2.truncContraction constEntry x.1 x.2.1) + (encTrunc (encList encNat)) (encList encNat) := + truncDirectCertificate constEntry constCert + +-- The loop's values are the contractions at the digit points, in order. +example (core : ℕ × List ℕ × ℕ × DescribedNetwork (SpecDesc (List ℕ)) → List ℕ) + (y : List ℕ × ℕ × ℕ × ℕ × DescribedNetwork (List ℕ)) : + (IndexFold.run (engineStep core) 2 (y, [])).2.2 = + [core (coreInput y 0), core (coreInput y 1)] := by + rw [run_engineStep] + rfl + +-- `FastContraction.modulus n` has at least `n` residues. +example : 100 ≤ 2 ^ (FastContraction.modulus 100).length := le_two_pow_length_modulus 100 + +end ComplexityTests.TensorNetworkTruncatedPolyTime diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkTruncatedResources.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkTruncatedResources.lean new file mode 100644 index 000000000..ad0338ef5 --- /dev/null +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkTruncatedResources.lean @@ -0,0 +1,78 @@ +/- +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.TruncatedResources + +/-! +# Tests for the resources of the truncation-order reduction + +Around a polynomial-time contraction over `A_P`, the reduction is polynomial-time: the calls are +polynomially long (`length_encCore_coreInput_le`), so the loop bound (`engineCertificate_le`) is a +polynomial. Specialized entries of a polynomial-time entry certificate are polynomial-time in the +input and the entry (`specEntryCertificate_le`). +-/ + +@[expose] public section + +namespace ComplexityTests.TensorNetworkTruncatedResources + +open Cslib Cslib.GenericRAM Cslib.Circuits.Frontier Turing.MultiTapeTM + +/-- A contraction over `A_P` that returns the zero coefficient list. -/ +def zeroCore (_ : ℕ × List ℕ × ℕ × DescribedNetwork (SpecDesc (List ℕ))) : List ℕ := [] + +/-- Its polynomial-time certificate. -/ +noncomputable def zeroCoreCert : + NativeCertificate zeroCore (encCore (encList encNat)) (encList encNat) := + NativeCertificate.ofPolyTime (ComputableInPolyTime.const []) + +/-- **A polynomial-time core gives a polynomial-time reduction.** -/ +example : ∃ c d : ℕ, ∀ y : List ℕ × ℕ × ℕ × ℕ × DescribedNetwork (List ℕ), + (engineCertificate zeroCore zeroCoreCert).time y ≤ + c * ((encEngine (encList encNat) y).length + 1) ^ d := by + obtain ⟨p, hp, hm, hb⟩ := exists_mono_poly_cert + (ComputableInPolyTime.const (encIn := encCore (encList encNat)) (encOut := encList encNat) + ([] : List ℕ)) + obtain ⟨K, hK⟩ := engineCertificate_le zeroCore zeroCoreCert + let L := fun y : List ℕ × ℕ × ℕ × ℕ × DescribedNetwork (List ℕ) => + (encEngine (encList encNat) y).length + have hpoly : PolyBounded L fun y => (L y * L y + 2) * + (K * (L y + 0 + 1) ^ K + p (9 * (L y + 1) ^ 2)) := + ((PolyBounded.self.mul PolyBounded.self).add (PolyBounded.const 2)).mul + (((PolyBounded.const K).mul ((PolyBounded.self.add (PolyBounded.const 0)).add + (PolyBounded.const 1) |>.pow K)).add + ((PolyBounded.of_polynomiallyBounded id hp).comp + ((PolyBounded.const 9).mul ((PolyBounded.self.add (PolyBounded.const 1)).pow 2)))) + obtain ⟨c, d, hcd⟩ := hpoly.exists_le + refine ⟨c, d, fun y => ?_⟩ + have h := (hK y (p (9 * (L y + 1) ^ 2)) (p (9 * (L y + 1) ^ 2)) 0 fun k _ => + ⟨(hb _).1.trans (hm (length_encCore_coreInput_le y k)), + (hb _).2.trans (hm (length_encCore_coreInput_le y k)), by simp [zeroCore]⟩).1 + have hN := pointCount_le (encT := encList encNat) y + have hmul := Nat.mul_le_mul_right (K * (L y + 0 + 1) ^ K + p (9 * (L y + 1) ^ 2)) + (show DescribedNetwork.pointCount y.2.2.1 y.2.2.2.2 + 1 ≤ L y * L y + 2 by + simp only [L] + omega) + exact h.trans (hmul.trans (hcd y)) + +/-- The entry certificate of descriptors that are their own entry. -/ +noncomputable def constCert : + NativeCertificate (fun q : List ℕ × List Bool => q.1) (encPair (encList encNat) encBits) + (encList encNat) := + NativeCertificate.ofPolyTime (ComputableInPolyTime.fst _ _) + +-- Specialized entries cost the original entry plus a polynomial in the input and the entry. +example : ∃ K : ℕ, ∀ q : SpecDesc (List ℕ) × List Bool, + (specEntryCertificate (fun t _ => t) constCert).time q ≤ constCert.time (q.1.1, q.2) + + K * ((encPair (encSpecDesc (encList encNat)) encBits q).length + + (encList encNat q.1.1).length + 1) ^ K := by + obtain ⟨K, hK⟩ := specEntryCertificate_le (encT := encList encNat) + exact ⟨K, fun q => (hK (fun t _ => t) constCert q).1⟩ + +end ComplexityTests.TensorNetworkTruncatedResources