diff --git a/Complexity.lean b/Complexity.lean index aa9a09e9b..ca4dbea74 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -868,6 +868,7 @@ public import Complexity.Computability.Circuit.Frontier.Sweep public import Complexity.Computability.Circuit.Frontier.TensorNetwork public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Constraint public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Deformation +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DirectContraction public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit public import Complexity.Computability.Circuit.Frontier.TwoSidedWitness public import Complexity.Computability.Circuit.Frontier.Unconditional diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/DirectContraction.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DirectContraction.lean new file mode 100644 index 000000000..954c85cb0 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DirectContraction.lean @@ -0,0 +1,590 @@ +/- +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.Explicit +public import Complexity.Computability.GenericRAM.Native.BooleanFold +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Words +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryDivision +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListBinaryLookup +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListMap +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListToBits +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeLoops +import Mathlib.Algebra.BigOperators.Group.Finset.Basic +import Mathlib.Algebra.Order.BigOperators.Group.Finset +import Mathlib.Algebra.Order.BigOperators.Group.List +import Mathlib.Data.List.GetD +import Mathlib.Data.Nat.Size + +/-! +# Contracting an explicit tensor network by direct summation + +The leaf and small-size case of the contraction theorem, Theorem D.1 of [OpenAI2026ETH] +(Appendix D.4.7, p. 64), where a leaf sums directly over all Boolean edge assignments, and the +fallback for small sizes (Appendix D.4.2, p. 58). On input `(P, r, d)`, with `d` an explicit network +whose row vertices are the first `r` (the bipartition the fast algorithm uses), direct summation +computes the contraction of `d` modulo `2 ^ P`. It ignores `r`. + +`directContraction` streams over the `2 ^ m` assignments of bits to the `m` edges with +`Cslib.GenericRAM.BooleanFold`, in their binary order, keeping only the current index, the input +and an accumulator below `2 ^ P`. For each assignment it multiplies the table entries at the bits +on the ports, reducing modulo `2 ^ P` after each factor (`weightMod`), and adds the product to the +accumulator modulo `2 ^ P` (`sumStep`). `directContraction_eq` proves that the result is +`d.contraction % 2 ^ P`. + +**Input encoding** (`encContractionInput`). The triple `(P, r, d)` is encoded as a pair: `P` in +unary, then the pair of `r` in binary and `d`. The network `d` (`encExplicitNetwork`) is the pair +of its number of edges, in unary, and its list of vertices. Each vertex is the pair of its list +of ports and its table, both lists of binary numbers. The unary fields keep the arithmetic +modulo `2 ^ P` and the streamed assignments polynomial in the input length. + +**Precision in binary** (`directContractionBinaryCertificate`). The same triple with `P` in binary +(`encPair encNat (encPair encNat encExplicitNetwork)`) is handled by capping first: the +contraction is below `2 ^ |d|` for `|d|` the encoded length of `d`, so `P` can be replaced by the +unary `min |d| P` (`capPrecision`) without changing the residue. The bounds carry over. + +## Main definitions + +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.weightMod`: the weight of an assignment modulo + `2 ^ P`. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.sumStep`: one step of direct summation. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.directContraction`: direct summation on + `(P, r, d)`. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.encExplicitNetwork`, + `Cslib.Circuits.Frontier.ExplicitTensorNetwork.encContractionInput`: the input encodings. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.directContractionCertificate`: one native + machine for direct summation, streaming with `BooleanFold`. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.capPrecision`, + `Cslib.Circuits.Frontier.ExplicitTensorNetwork.directContractionBinaryCertificate`: capping a + binary precision, and direct summation with the precision in binary. + +## Main results + +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.weightMod_ofFn`: the weight of an assignment. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.directContraction_eq`: direct summation computes + the contraction modulo `2 ^ P`. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.runPrefix_sumStep`: every prefix of the loop + retains the input and keeps its accumulator below `2 ^ P`. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.weightMod_polyTime`, + `Cslib.Circuits.Frontier.ExplicitTensorNetwork.sumStep_polyTime`, + `Cslib.Circuits.Frontier.ExplicitTensorNetwork.numEdges_polyTime`, + `Cslib.Circuits.Frontier.ExplicitTensorNetwork.initial_polyTime`: the weight, one step, the + width and the initial state in polynomial time. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.directContractionCertificate_bounds`: on every + input, polynomial workspace and time `2 ^ m + 1` times a polynomial in the input length, where + `m` is the number of edges. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.exists_directContractionCertificate_le`: the same + with one constant, time `K (n + 1) ^ K 2 ^ m` and workspace `K (n + 1) ^ K` for input length + `n`. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.exists_computableInO_contraction_mod`: the + contraction modulo `2 ^ P` is computable within time `(n + 1) ^ K 2 ^ m` and space + `(n + 1) ^ K`, up to constants, on every input. + +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.contraction_lt_two_pow_length`, + `Cslib.Circuits.Frontier.ExplicitTensorNetwork.contraction_mod_two_pow_min`, + `Cslib.Circuits.Frontier.ExplicitTensorNetwork.capPrecision_polyTime`: the contraction is below + `2 ^ |d|`, so capping the precision at `|d|` keeps the residue, in polynomial time. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.directContractionBinaryCertificate_bounds`, + `Cslib.Circuits.Frontier.ExplicitTensorNetwork.exists_directContractionBinaryCertificate_le`: + the same bounds with the precision in binary. + +These bounds hold on every input because the live state keeps only the binary index, the input +and an accumulator below `2 ^ P`, and `P` is unary (`runPrefix_sumStep`, with +`Cslib.GenericRAM.BooleanFold.certificate_bounds`) or capped at the input length. + +## References + +* [OpenAI2026ETH], Theorem D.1 (Appendix D.1, p. 53) and its proof (Appendix D.4.7, p. 64). +-/ + +@[expose] public section + +namespace Cslib.Circuits.Frontier.ExplicitTensorNetwork + +open Cslib.BitString Cslib.GenericRAM Turing.MultiTapeTM + +/-- The weight modulo `2 ^ P` of an assignment of bits to the edges, given as a word: port `i` +reads bit `i` of the word, and `false` past its end. It is the product of the table entries at +the bits on the ports, reduced modulo `2 ^ P` after each factor. -/ +def weightMod (P : ℕ) (d : ExplicitTensorNetwork ℕ) (word : List Bool) : ℕ := + d.vertices.foldl (fun acc v => acc * entry v.2 (v.1.map fun i => word.getD i false) % 2 ^ P) + (1 % 2 ^ P) + +/-- One step of direct summation, as a `BooleanFold` body: add the weight of the current word to +the accumulator modulo `2 ^ P`, retaining the precision `P` and the network. -/ +def sumStep (s : (ℕ × List Bool) × ((ℕ × ExplicitTensorNetwork ℕ) × ℕ)) : + (ℕ × ExplicitTensorNetwork ℕ) × ℕ := + (s.2.1, (s.2.2 + weightMod s.2.1.1 s.2.1.2 s.1.2) % 2 ^ s.2.1.1) + +/-- **Direct summation** on the input `(P, r, d)`: stream over the `2 ^ m` assignments to the `m` +edges of `d`, accumulating their weights modulo `2 ^ P`. The number `r` of row vertices is not +used. -/ +def directContraction (x : ℕ × ℕ × ExplicitTensorNetwork ℕ) : ℕ := + (BooleanFold.run sumStep x.2.2.numEdges ((x.1, x.2.2), 0)).2.2.2 + +/-! ### Input encoding -/ + +/-- An explicit network over `ℕ` is its number of edges and its list of vertices. -/ +def equivProd : ExplicitTensorNetwork ℕ ≃ ℕ × List (List ℕ × List ℕ) where + toFun d := (d.numEdges, d.vertices) + invFun p := ⟨p.1, p.2⟩ + left_inv _ := rfl + right_inv _ := rfl + +/-- **The encoding of an explicit network**: its number of edges in unary, then its list of +vertices, each the pair of its list of ports and its table, as lists of binary numbers. -/ +def encExplicitNetwork : ExplicitTensorNetwork ℕ ↪ List Bool := + encOfEquiv equivProd (encPair encUnary (encList (encPair (encList encNat) (encList encNat)))) + +/-- **The encoding of a contraction input `(P, r, d)`**: the precision `P` in unary, then the +number `r` of row vertices in binary and the network (`encExplicitNetwork`). -/ +def encContractionInput : ℕ × ℕ × ExplicitTensorNetwork ℕ ↪ List Bool := + encPair encUnary (encPair encNat encExplicitNetwork) + +/-! ### Correctness -/ + +private theorem foldl_mul_mod {α : Type*} (f : α → ℕ) (m : ℕ) (l : List α) (a : ℕ) : + l.foldl (fun acc v => acc * f v % m) (a % m) = a * (l.map f).prod % m := by + induction l generalizing a with + | nil => simp + | cons v l ih => + rw [List.foldl_cons, Nat.mod_mul_mod, ih, List.map_cons, List.prod_cons, Nat.mul_assoc] + +private theorem getD_ofFn {n : ℕ} (x : Fin n → Bool) (i : ℕ) : + (List.ofFn x).getD i false = if h : i < n then x ⟨i, h⟩ else false := by + by_cases h : i < n + · rw [dite_eq_left h, List.getD_eq_getElem _ _ (by simpa using h), List.getElem_ofFn] + · rw [dite_eq_right h, List.getD_eq_default _ _ (by simp only [List.length_ofFn]; omega)] + +/-- **The weight of an assignment.** On the word of an assignment `x` to the edges, `weightMod` is +the product of the table entries at the bits on the ports, modulo `2 ^ P`. -/ +theorem weightMod_ofFn (P : ℕ) (d : ExplicitTensorNetwork ℕ) (x : Fin d.numEdges → Bool) : + weightMod P d (List.ofFn x) = + (d.vertices.map fun v => entry v.2 (d.portBits x v.1)).prod % 2 ^ P := by + rw [weightMod, foldl_mul_mod, Nat.one_mul] + simp only [portBits, getD_ofFn] + +private theorem foldl_sumStep (P n : ℕ) (d : ExplicitTensorNetwork ℕ) (words : List (List Bool)) + (a : ℕ) : + words.foldl (fun acc word => sumStep ((n, word), acc)) ((P, d), a % 2 ^ P) = + ((P, d), (a + (words.map (weightMod P d)).sum) % 2 ^ P) := by + induction words generalizing a with + | nil => simp + | cons w ws ih => + rw [List.foldl_cons] + change ws.foldl (fun acc word => sumStep ((n, word), acc)) + ((P, d), (a % 2 ^ P + weightMod P d w) % 2 ^ P) = _ + rw [Nat.mod_add_mod, ih, List.map_cons, List.sum_cons, Nat.add_assoc] + +private theorem sum_enumList (n : ℕ) (g : List Bool → ℕ) : + ((enumList n).map g).sum = ∑ σ : BitString n, g (List.ofFn σ) := by + have hall : (enum n).toFinset = Finset.univ := by ext; simp + rw [enumList, List.map_map, ← List.sum_toFinset _ (nodup_enum n), hall] + rfl + +/-- **Direct summation computes the contraction modulo `2 ^ P`**, on every input. -/ +theorem directContraction_eq (P r : ℕ) (d : ExplicitTensorNetwork ℕ) : + directContraction (P, r, d) = d.contraction % 2 ^ P := by + have h := foldl_sumStep P d.numEdges d (enumList d.numEdges) 0 + rw [Nat.zero_mod] at h + rw [directContraction, BooleanFold.run_accumulator, h, Nat.zero_add, sum_enumList, + contraction] + simp only [weightMod_ofFn] + exact (Finset.sum_nat_mod _ _ _).symm + +/-! ### One step in polynomial time -/ + +local notation "encVertices" => encList (encPair (encList encNat) (encList encNat)) + +/-- The encoding of the precision, the network and the current word. -/ +local notation "encWeightInput" => encPair (encPair encUnary encExplicitNetwork) encBits + +/-- The vertices of a network, read from its encoding. -/ +private theorem vertices_polyTime : + ComputableInPolyTime (fun d : ExplicitTensorNetwork ℕ => d.vertices) encExplicitNetwork + encVertices := + (ComputableInPolyTime.snd encUnary encVertices).comp + (ComputableInPolyTime.of_eq (f := equivProd) fun _ => rfl) + +/-- `2 ^ P` in binary from `P` in unary. -/ +private theorem twoPow_polyTime : + ComputableInPolyTime (fun P : ℕ => 2 ^ P) encUnary encNat := + BooleanFold.clock.polyTime ⟨PolyBounded.self, PolyBounded.self⟩ + +/-- A number below `2 ^ P` has at most `P` binary digits. -/ +private theorem length_encNat_le {x P : ℕ} (hx : x < 2 ^ P) : (encNat x).length ≤ P := by + change x.bits.length ≤ P + rw [Nat.size_eq_bits_len] + exact Nat.size_le.mpr hx + +/-- The weight of the current word modulo `2 ^ P` is computable in polynomial time. -/ +theorem weightMod_polyTime : + ComputableInPolyTime (fun q : (ℕ × ExplicitTensorNetwork ℕ) × List Bool => + weightMod q.1.1 q.1.2 q.2) encWeightInput encNat := by + -- The modulus `2 ^ P`, the vertices and the word. + have hP := (ComputableInPolyTime.fst encUnary encExplicitNetwork).comp + (ComputableInPolyTime.fst (encPair encUnary encExplicitNetwork) encBits) + have hmod := twoPow_polyTime.comp hP + have hverts := vertices_polyTime.comp ((ComputableInPolyTime.snd encUnary encExplicitNetwork).comp + (ComputableInPolyTime.fst (encPair encUnary encExplicitNetwork) encBits)) + have hinit : ComputableInPolyTime (fun q : (ℕ × ExplicitTensorNetwork ℕ) × List Bool => + 1 % 2 ^ q.1.1) encWeightInput encNat := + (ComputableInPolyTime.snd encNat encNat).comp + (ComputableInPolyTime.binary_divMod.comp ((ComputableInPolyTime.const 1).prod hmod)) + -- One step of the product: multiply by the entry at the bits on the ports, modulo `2 ^ P`. + let encStep := encPair (encPair encWeightInput encNat) (encPair (encList encNat) (encList encNat)) + have hq : ComputableInPolyTime + (fun p : (((ℕ × ExplicitTensorNetwork ℕ) × List Bool) × ℕ) × (List ℕ × List ℕ) => p.1.1) + encStep encWeightInput := + (ComputableInPolyTime.fst encWeightInput encNat).comp + (ComputableInPolyTime.fst (encPair encWeightInput encNat) _) + have hacc : ComputableInPolyTime + (fun p : (((ℕ × ExplicitTensorNetwork ℕ) × List Bool) × ℕ) × (List ℕ × List ℕ) => p.1.2) + encStep encNat := + (ComputableInPolyTime.snd encWeightInput encNat).comp + (ComputableInPolyTime.fst (encPair encWeightInput encNat) _) + have hv := ComputableInPolyTime.snd (encPair encWeightInput encNat) + (encPair (encList encNat) (encList encNat)) + have hports := (ComputableInPolyTime.fst (encList encNat) (encList encNat)).comp hv + have htable := (ComputableInPolyTime.snd (encList encNat) (encList encNat)).comp hv + have hbit : ComputableInPolyTime + (fun z : ((((ℕ × ExplicitTensorNetwork ℕ) × List Bool) × ℕ) × (List ℕ × List ℕ)) × ℕ => + z.1.1.1.2.getD z.2 false) (encPair encStep encNat) encBool := + ComputableInPolyTime.listGetD_binary (encA := encBool) (encL := encBits) false + ((ComputableInPolyTime.snd (encPair encUnary encExplicitNetwork) encBits).comp + (hq.comp (ComputableInPolyTime.fst encStep encNat))) + (ComputableInPolyTime.snd encStep encNat) + have hbits := ComputableInPolyTime.listToBits.comp + (ComputableInPolyTime.mapWithInput (f := fun p i => p.1.1.2.getD i false) hports hbit) + have hindex := ComputableInPolyTime.bitsBinaryValue.comp + (ComputableInPolyTime.bitsReverse.comp hbits) + have hentry := ComputableInPolyTime.listGetD_binary (encA := encNat) (encL := encList encNat) 0 + htable hindex + have hstepMod := twoPow_polyTime.comp ((ComputableInPolyTime.fst encUnary encExplicitNetwork).comp + ((ComputableInPolyTime.fst (encPair encUnary encExplicitNetwork) encBits).comp hq)) + have hstep : ComputableInPolyTime + (fun p : (((ℕ × ExplicitTensorNetwork ℕ) × List Bool) × ℕ) × (List ℕ × List ℕ) => + p.1.2 * entry p.2.2 (p.2.1.map fun i => p.1.1.2.getD i false) % 2 ^ p.1.1.1.1) + encStep encNat := by + have h := (ComputableInPolyTime.snd encNat encNat).comp + (ComputableInPolyTime.binary_divMod.comp + ((ComputableInPolyTime.binary_mul' hacc hentry).prod hstepMod)) + refine ComputableInPolyTime.of_enc_eq h fun p => ?_ + simp only [Function.comp_def, entry, lsbValue_eq_binaryValue_reverse] + have hfold := ComputableInPolyTime.foldlWithInput_of_bounded_growth + (encA := encPair (encList encNat) (encList encNat)) (encL := encVertices) + (step := fun q acc v => acc * entry v.2 (v.1.map fun i => q.2.getD i false) % 2 ^ q.1.1) + hinit ⟨hverts, hstep, inferInstance, inferInstance⟩ + (growth := fun q => q.1.1) + ⟨PolyBounded.of_forall_le 1 1 fun q => by + simp only [length_encPair, encUnary_apply, List.length_replicate, pow_one, one_mul]; omega, + fun q acc v _ => (length_encNat_le (Nat.mod_lt _ (Nat.two_pow_pos _))).trans + (Nat.le_add_left _ _)⟩ + exact hfold + +/-- The live state of direct summation: the precision, the network and the accumulator. -/ +local notation "encSumState" => encPair (encPair encUnary encExplicitNetwork) encNat + +/-- **One step of direct summation is computable in polynomial time**, in the encoding of the +`BooleanFold` callback input: the width and the current word, and the live state. -/ +theorem sumStep_polyTime : + ComputableInPolyTime sumStep (encPair (encPair encUnary encBits) encSumState) encSumState := by + have hstate := ComputableInPolyTime.snd (encPair encUnary encBits) encSumState + have hpd := (ComputableInPolyTime.fst (encPair encUnary encExplicitNetwork) encNat).comp hstate + have hacc := (ComputableInPolyTime.snd (encPair encUnary encExplicitNetwork) encNat).comp hstate + have hword := (ComputableInPolyTime.snd encUnary encBits).comp + (ComputableInPolyTime.fst (encPair encUnary encBits) encSumState) + have hweight := weightMod_polyTime.comp (hpd.prod hword) + have hmod := twoPow_polyTime.comp + ((ComputableInPolyTime.fst encUnary encExplicitNetwork).comp hpd) + have hsum := (ComputableInPolyTime.snd encNat encNat).comp + (ComputableInPolyTime.binary_divMod.comp + ((ComputableInPolyTime.binary_add.comp (hacc.prod hweight)).prod hmod)) + exact hpd.prod hsum + +/-! ### The streaming loop -/ + +/-- **The live state of every prefix** of the loop: the precision and the network are retained, +and the accumulator is the sum of the weights of the visited words modulo `2 ^ P`, so it stays +below `2 ^ P`. -/ +theorem runPrefix_sumStep (P : ℕ) (d : ExplicitTensorNetwork ℕ) (j : ℕ) : + (BooleanFold.runPrefix sumStep d.numEdges j ((P, d), 0)).2.2 = + ((P, d), (((List.range j).map (lowBits d.numEdges)).map (weightMod P d)).sum % 2 ^ P) := by + have h := foldl_sumStep P d.numEdges d ((List.range j).map (lowBits d.numEdges)) 0 + rw [Nat.zero_mod, Nat.zero_add] at h + rw [BooleanFold.prefix_accumulator, ← h, List.foldl_map] + +/-- The width of the loop: the number of edges, in unary. -/ +theorem numEdges_polyTime : + ComputableInPolyTime (fun x : ℕ × ℕ × ExplicitTensorNetwork ℕ => x.2.2.numEdges) + encContractionInput encUnary := + (ComputableInPolyTime.fst encUnary encVertices).comp + ((ComputableInPolyTime.of_eq (f := equivProd) fun _ => rfl).comp + ((ComputableInPolyTime.snd encNat encExplicitNetwork).comp + (ComputableInPolyTime.snd encUnary (encPair encNat encExplicitNetwork)))) + +/-- The initial live state: the precision, the network and a zero accumulator. -/ +theorem initial_polyTime : + ComputableInPolyTime (fun x : ℕ × ℕ × ExplicitTensorNetwork ℕ => ((x.1, x.2.2), (0 : ℕ))) + encContractionInput encSumState := + ((ComputableInPolyTime.fst encUnary (encPair encNat encExplicitNetwork)).prod + ((ComputableInPolyTime.snd encNat encExplicitNetwork).comp + (ComputableInPolyTime.snd encUnary (encPair encNat encExplicitNetwork)))).prod + (ComputableInPolyTime.const 0) + +/-- **A native certificate for direct summation**: one finite machine streams the `2 ^ m` +assignments with `BooleanFold`, running the polynomial-time step `sumStep` on each. Its explicit +bounds are `directContractionCertificate_bounds` and `exists_directContractionCertificate_le`. -/ +noncomputable def directContractionCertificate : + NativeCertificate directContraction encContractionInput encNat := + NativeCertificate.snd (NativeCertificate.snd (NativeCertificate.snd + (BooleanFold.certificate (NativeCertificate.ofPolyTime numEdges_polyTime) + (NativeCertificate.ofPolyTime initial_polyTime) + (NativeCertificate.ofPolyTime sumStep_polyTime)))) + +/-! ### Explicit bounds -/ + +/-- The live state of every prefix is at most three times as long as the input: it retains the +precision and the network, and its accumulator is below `2 ^ P`. -/ +private theorem length_runPrefix_sumStep_le (x : ℕ × ℕ × ExplicitTensorNetwork ℕ) (j : ℕ) : + (encSumState (BooleanFold.runPrefix sumStep x.2.2.numEdges j ((x.1, x.2.2), 0)).2.2).length ≤ + 3 * (encContractionInput x).length := by + obtain ⟨P, r, d⟩ := x + rw [runPrefix_sumStep] + have h := length_encNat_le + (Nat.mod_lt (((List.range j).map (lowBits d.numEdges)).map (weightMod P d)).sum + (Nat.two_pow_pos P)) + simp only [encContractionInput, length_encPair, encUnary_apply, List.length_replicate] + omega + +/-- **The bounds of direct summation**, on every input `(P, r, d)`: polynomial workspace in the +input length, and time `2 ^ m + 1` times a polynomial in the input length, where `m` is the number +of edges of `d`. -/ +theorem directContractionCertificate_bounds : + PolyBounded (fun x => (encContractionInput x).length) directContractionCertificate.space ∧ + ∃ T : ℕ × ℕ × ExplicitTensorNetwork ℕ → ℕ, + PolyBounded (fun x => (encContractionInput x).length) T ∧ + ∀ x, directContractionCertificate.time x ≤ (2 ^ x.2.2.numEdges + 1) * T x := + BooleanFold.certificate_bounds (NativeCertificate.ofPolyTime_isPolynomial numEdges_polyTime) + (NativeCertificate.ofPolyTime_isPolynomial initial_polyTime) + (NativeCertificate.ofPolyTime_isPolynomial sumStep_polyTime) + ((PolyBounded.const 3).mul .self) fun x j _ => length_runPrefix_sumStep_le x j + +/-- One constant for bounds of the form `(2 ^ m + 1)` times a polynomial in time and a polynomial in +space. -/ +private theorem exists_le_of_bounds {enc : ℕ × ℕ × ExplicitTensorNetwork ℕ ↪ List Bool} + {time space T : ℕ × ℕ × ExplicitTensorNetwork ℕ → ℕ} + (hspace : PolyBounded (fun x => (enc x).length) space) + (hT : PolyBounded (fun x => (enc x).length) T) + (htime : ∀ x, time x ≤ (2 ^ x.2.2.numEdges + 1) * T x) : + ∃ K : ℕ, ∀ x, time x ≤ K * ((enc x).length + 1) ^ K * 2 ^ x.2.2.numEdges ∧ + space x ≤ K * ((enc x).length + 1) ^ K := by + obtain ⟨ct, dt, hct⟩ := hT.exists_le + obtain ⟨cs, ds, hcs⟩ := hspace.exists_le + refine ⟨2 * ct + cs + dt + ds, fun x => ⟨?_, ?_⟩⟩ + · have h1 : 2 ^ x.2.2.numEdges + 1 ≤ 2 * 2 ^ x.2.2.numEdges := by + have := Nat.one_le_two_pow (n := x.2.2.numEdges) + omega + have h2 : ((enc x).length + 1) ^ dt ≤ ((enc x).length + 1) ^ (2 * ct + cs + dt + ds) := + Nat.pow_le_pow_right (Nat.succ_pos _) (by omega) + calc time x + ≤ (2 * 2 ^ x.2.2.numEdges) * (ct * ((enc x).length + 1) ^ dt) := + (htime x).trans (Nat.mul_le_mul h1 (hct x)) + _ = 2 * ct * ((enc x).length + 1) ^ dt * 2 ^ x.2.2.numEdges := by ac_rfl + _ ≤ _ := Nat.mul_le_mul_right _ (Nat.mul_le_mul (by omega) h2) + · exact (hcs x).trans (Nat.mul_le_mul (by omega) + (Nat.pow_le_pow_right (Nat.succ_pos _) (by omega))) + +/-- **The bounds of direct summation in one constant**: there is `K` such that on every input +`x = (P, r, d)` the time is at most `K (n + 1) ^ K 2 ^ m` and the workspace at most +`K (n + 1) ^ K`, where `n` is the input length and `m` the number of edges of `d`. Since +`2 ^ m ≤ 2 ^ (K m)`, this gives the unconditional `K (n + 1) ^ K 2 ^ (K m)` form of the +contraction contract. -/ +theorem exists_directContractionCertificate_le : + ∃ K : ℕ, ∀ x : ℕ × ℕ × ExplicitTensorNetwork ℕ, + directContractionCertificate.time x ≤ + K * ((encContractionInput x).length + 1) ^ K * 2 ^ x.2.2.numEdges ∧ + directContractionCertificate.space x ≤ K * ((encContractionInput x).length + 1) ^ K := + let ⟨hspace, _, hT, htime⟩ := directContractionCertificate_bounds + exists_le_of_bounds hspace hT htime + +/-- **Direct summation is computable within time `(n + 1) ^ K 2 ^ m` and space `(n + 1) ^ K`**, +up to constants, on every input `x = (P, r, d)`, where `n` is the input length and `m` the number +of edges of `d`. The output is the contraction of `d` modulo `2 ^ P`, in binary. -/ +theorem exists_computableInO_contraction_mod : + ∃ K : ℕ, ComputableInO + (fun x : ℕ × ℕ × ExplicitTensorNetwork ℕ => x.2.2.contraction % 2 ^ x.1) + encContractionInput encNat + (fun x => ((encContractionInput x).length + 1) ^ K * 2 ^ x.2.2.numEdges) + (fun x => ((encContractionInput x).length + 1) ^ K) := by + obtain ⟨K, hK⟩ := exists_directContractionCertificate_le + refine ⟨K, (directContractionCertificate.computes.mono K (fun x => ?_) (fun x => ?_)).of_enc_eq + fun x => ?_⟩ + · refine (hK x).1.trans ?_ + rw [Nat.mul_assoc] + exact Nat.mul_le_mul_left K (Nat.le_succ _) + · exact (hK x).2.trans (Nat.mul_le_mul_left K (Nat.le_succ _)) + · obtain ⟨P, r, d⟩ := x + rw [directContraction_eq] + +/-! ### The precision in binary + +A precision given in binary can be exponentially larger than the input. It can be capped: the +contraction is below `2 ^ |d|`, for `|d|` the encoded length of the network, so reducing modulo +`2 ^ min |d| P` gives the same residue. The capped precision is unary and at most `|d|`, so direct +summation keeps its bounds. -/ + +/-- The encoding of a contraction input with the precision in binary. -/ +local notation "encBinaryInput" => encPair encNat (encPair encNat encExplicitNetwork) + +private theorem sum_lt_two_pow_length (t : List ℕ) : t.sum < 2 ^ (encList encNat t).length := by + induction t with + | nil => simp + | cons e t ih => + have he : e < 2 ^ (encNat e).length := by + change e < 2 ^ e.bits.length + rw [Nat.size_eq_bits_len] + exact Nat.lt_size_self e + have h1 : 2 ^ (encNat e).length ≤ 2 ^ (2 * (encNat e).length + (encList encNat t).length) := + Nat.pow_le_pow_right two_pos (by omega) + have h2 : 2 ^ (encList encNat t).length ≤ + 2 ^ (2 * (encNat e).length + (encList encNat t).length) := + Nat.pow_le_pow_right two_pos (by omega) + have hlen : (encList encNat (e :: t)).length = + 2 * (encNat e).length + (encList encNat t).length + 1 := by + rw [length_encList, List.map_cons, List.sum_cons, ← length_encList] + omega + rw [List.sum_cons, hlen, pow_succ] + omega + +private theorem entry_le_sum (t : List ℕ) (bs : List Bool) : entry t bs ≤ t.sum := by + unfold entry + rcases lt_or_ge (lsbValue bs) t.length with h | h + · rw [List.getD_eq_getElem _ _ h] + exact List.le_sum_of_mem (List.getElem_mem h) + · rw [List.getD_eq_default _ _ h] + exact Nat.zero_le _ + +private theorem prod_le_two_pow_length (vs : List (List ℕ × List ℕ)) (f : List ℕ × List ℕ → ℕ) + (hf : ∀ v ∈ vs, f v ≤ v.2.sum) : + (vs.map f).prod ≤ 2 ^ (encVertices vs).length := by + induction vs with + | nil => simp + | cons v vs ih => + have hv : f v ≤ 2 ^ (encList encNat v.2).length := + (hf v List.mem_cons_self).trans (sum_lt_two_pow_length v.2).le + have hvs := ih fun w hw => hf w (List.mem_cons_of_mem _ hw) + have hlen : (encVertices (v :: vs)).length = + 2 * (2 * (encList encNat v.1).length + 1 + (encList encNat v.2).length) + 1 + + (encVertices vs).length := by + rw [length_encList, List.map_cons, List.sum_cons, ← length_encList, length_encPair] + rw [List.map_cons, List.prod_cons, hlen] + calc f v * (vs.map f).prod + ≤ 2 ^ (encList encNat v.2).length * 2 ^ (encVertices vs).length := Nat.mul_le_mul hv hvs + _ = 2 ^ ((encList encNat v.2).length + (encVertices vs).length) := (pow_add _ _ _).symm + _ ≤ _ := Nat.pow_le_pow_right two_pos (by omega) + +/-- **The contraction is below `2 ^ |d|`**, for `|d|` the encoded length of the network: each +table entry is at most the sum of its table, and there are `2 ^ m` assignments. -/ +theorem contraction_lt_two_pow_length (d : ExplicitTensorNetwork ℕ) : + d.contraction < 2 ^ (encExplicitNetwork d).length := by + have hw (x : Fin d.numEdges → Bool) : + (d.vertices.map fun v => entry v.2 (d.portBits x v.1)).prod ≤ + 2 ^ (encVertices d.vertices).length := + prod_le_two_pow_length _ _ fun v _ => entry_le_sum _ _ + have hlen : (encExplicitNetwork d).length = + 2 * d.numEdges + 1 + (encVertices d.vertices).length := by + change (encPair encUnary encVertices (d.numEdges, d.vertices)).length = _ + rw [length_encPair, encUnary_apply, List.length_replicate] + calc d.contraction + ≤ ∑ _x : Fin d.numEdges → Bool, 2 ^ (encVertices d.vertices).length := + Finset.sum_le_sum fun x _ => hw x + _ = 2 ^ (d.numEdges + (encVertices d.vertices).length) := by + rw [Finset.sum_const, Finset.card_univ, Fintype.card_fun, Fintype.card_bool, + Fintype.card_fin, smul_eq_mul, pow_add] + _ < 2 ^ (encExplicitNetwork d).length := Nat.pow_lt_pow_right one_lt_two (by omega) + +/-- Capping the precision at the encoded length of the network does not change the residue. -/ +theorem contraction_mod_two_pow_min (P : ℕ) (d : ExplicitTensorNetwork ℕ) : + d.contraction % 2 ^ min (encExplicitNetwork d).length P = d.contraction % 2 ^ P := by + rcases le_total (encExplicitNetwork d).length P with h | h + · rw [min_eq_left h, Nat.mod_eq_of_lt (contraction_lt_two_pow_length d), + Nat.mod_eq_of_lt ((contraction_lt_two_pow_length d).trans_le + (Nat.pow_le_pow_right two_pos h))] + · rw [min_eq_right h] + +/-- Cap the precision at the encoded length of the network. -/ +def capPrecision (x : ℕ × ℕ × ExplicitTensorNetwork ℕ) : ℕ × ℕ × ExplicitTensorNetwork ℕ := + (min (encExplicitNetwork x.2.2).length x.1, x.2) + +/-- **Capping is computable in polynomial time**, from the precision in binary to the capped +precision in unary. -/ +theorem capPrecision_polyTime : + ComputableInPolyTime capPrecision encBinaryInput encContractionInput := by + have hrd := ComputableInPolyTime.snd encNat (encPair encNat encExplicitNetwork) + have hd := (ComputableInPolyTime.snd encNat encExplicitNetwork).comp hrd + have hbits : ComputableInPolyTime (fun d : ExplicitTensorNetwork ℕ => encExplicitNetwork d) + encExplicitNetwork encBits := ComputableInPolyTime.of_eq fun _ => rfl + have hlen := ComputableInPolyTime.length_bits_comp (hbits.comp hd) + exact (ComputableInPolyTime.binary_min_unary' hlen + (ComputableInPolyTime.fst encNat (encPair encNat encExplicitNetwork))).prod hrd + +/-- **Direct summation with the precision in binary**: cap the precision, then sum directly. The +input `(P, r, d)` is encoded as `P` in binary, then `r` in binary and the network, and the output is +`d.contraction % 2 ^ P` in binary. -/ +noncomputable def directContractionBinaryCertificate : + NativeCertificate (fun x : ℕ × ℕ × ExplicitTensorNetwork ℕ => x.2.2.contraction % 2 ^ x.1) + encBinaryInput encNat := + (directContractionCertificate.comp (NativeCertificate.ofPolyTime capPrecision_polyTime)).congr + fun x => (directContraction_eq _ x.2.1 x.2.2).trans (contraction_mod_two_pow_min x.1 x.2.2) + +/-- **The bounds of direct summation with the precision in binary**, on every input `(P, r, d)`: +polynomial workspace in the input length, and time `2 ^ m + 1` times a polynomial in the input +length, where `m` is the number of edges of `d`. -/ +theorem directContractionBinaryCertificate_bounds : + PolyBounded (fun x => (encBinaryInput x).length) directContractionBinaryCertificate.space ∧ + ∃ T : ℕ × ℕ × ExplicitTensorNetwork ℕ → ℕ, + PolyBounded (fun x => (encBinaryInput x).length) T ∧ + ∀ x, directContractionBinaryCertificate.time x ≤ (2 ^ x.2.2.numEdges + 1) * T x := by + obtain ⟨hspace, T, hT, htime⟩ := directContractionCertificate_bounds + have hcap := NativeCertificate.ofPolyTime_isPolynomial capPrecision_polyTime + have hlen : PolyBounded (fun x => (encBinaryInput x).length) + fun x => (encContractionInput (capPrecision x)).length := + PolyBounded.of_forall_le 3 1 fun x => by + have := min_le_left (encExplicitNetwork x.2.2).length x.1 + simp only [capPrecision, encContractionInput, length_encPair, encUnary_apply, + List.length_replicate, pow_one] + omega + refine ⟨hcap.2.add (hspace.comp hlen), fun x => + (NativeCertificate.ofPolyTime capPrecision_polyTime).time x + T (capPrecision x), + hcap.1.add (hT.comp hlen), fun x => ?_⟩ + have h := htime (capPrecision x) + change (NativeCertificate.ofPolyTime capPrecision_polyTime).time x + + directContractionCertificate.time (capPrecision x) ≤ _ + rw [Nat.mul_add] + exact Nat.add_le_add (Nat.le_mul_of_pos_left _ (Nat.succ_pos _)) h + +/-- **The bounds of direct summation with the precision in binary, in one constant**: there is `K` +such that on every input the time is at most `K (n + 1) ^ K 2 ^ m` and the workspace at most +`K (n + 1) ^ K`, where `n` is the input length and `m` the number of edges. -/ +theorem exists_directContractionBinaryCertificate_le : + ∃ K : ℕ, ∀ x : ℕ × ℕ × ExplicitTensorNetwork ℕ, + directContractionBinaryCertificate.time x ≤ + K * ((encBinaryInput x).length + 1) ^ K * 2 ^ x.2.2.numEdges ∧ + directContractionBinaryCertificate.space x ≤ K * ((encBinaryInput x).length + 1) ^ K := + let ⟨hspace, _, hT, htime⟩ := directContractionBinaryCertificate_bounds + exists_le_of_bounds hspace hT htime + +end Cslib.Circuits.Frontier.ExplicitTensorNetwork diff --git a/Complexity/Computability/GenericRAM/Native/BooleanFold.lean b/Complexity/Computability/GenericRAM/Native/BooleanFold.lean index 45b9f3ef1..4d6c0f85e 100644 --- a/Complexity/Computability/GenericRAM/Native/BooleanFold.lean +++ b/Complexity/Computability/GenericRAM/Native/BooleanFold.lean @@ -26,7 +26,10 @@ The assignment list in the correctness specification is not constructed by the s This is the local Boolean-vector component of the enumeration in [OpenAI2026ETH], Lemma 3.2 and Proposition 3.4, pp. 22–26. It is not a mixed-radix or subset-pair enumerator, and gives no -polynomial-time bound for a whole loop with exponentially many rounds. +polynomial-time bound for a whole loop with exponentially many rounds. `certificate_bounds` gives +the loop's explicit bounds instead: when the components are polynomial and every prefix keeps its +accumulator polynomially bounded, the workspace is polynomial and the time is `2 ^ n + 1` times a +polynomial. -/ @[expose] public section @@ -256,4 +259,100 @@ noncomputable def certificate {α : Type} {encIn : α ↪ List Bool} encIn (encPair encNat (encPair encUnary encB)) := IndexFold.certificate (clock.comp cn) (cn.prod ci) (visitCertificate cb) +/-- The clock is linear in the unary dimension. -/ +theorem clock_isPolynomial : clock.IsPolynomial := ⟨.self, .self⟩ + +private theorem add_mul_le_mul_add {N X Y Y' : ℕ} (h : Y ≤ Y') : + X + (N + 1) * Y ≤ (N + 1) * (X + Y') := by + rw [Nat.mul_add] + exact Nat.add_le_add (Nat.le_mul_of_pos_left X (Nat.succ_pos N)) (Nat.mul_le_mul_left _ h) + +/-- **Explicit bounds of a streaming traversal.** Suppose the dimension, the initial state and +the body have polynomial certificates, and every prefix keeps its accumulator within a polynomial +bound `B` in the encoded input length. Then the traversal of all `2 ^ n` words, for `n` the +dimension, uses polynomial workspace, and its time is `2 ^ n + 1` times a polynomial. The +traversal count enters only the time. -/ +theorem certificate_bounds {α : Type} {encIn : α ↪ List Bool} + {dimension : α → ℕ} {initial : α → β} {body : (ℕ × List Bool) × β → β} + {cn : NativeCertificate dimension encIn encUnary} + {ci : NativeCertificate initial encIn encB} + {cb : NativeCertificate body (encPair (encPair encUnary encBits) encB) encB} + (hcn : cn.IsPolynomial) (hci : ci.IsPolynomial) (hcb : cb.IsPolynomial) + {B : α → ℕ} (hB : PolyBounded (fun a => (encIn a).length) B) + (hstate : ∀ a j, j ≤ 2 ^ dimension a → + (encB (runPrefix body (dimension a) j (initial a)).2.2).length ≤ B a) : + PolyBounded (fun a => (encIn a).length) (certificate cn ci cb).space ∧ + ∃ T : α → ℕ, PolyBounded (fun a => (encIn a).length) T ∧ + ∀ a, (certificate cn ci cb).time a ≤ (2 ^ dimension a + 1) * T a := by + let cstep := IndexFold.roundCertificate (visitCertificate cb) + have hcstep : cstep.IsPolynomial := + IndexFold.roundCertificate_isPolynomial _ (visitCertificate_isPolynomial cb hcb) + obtain ⟨ct, dt, hct⟩ := hcstep.1.exists_le + obtain ⟨cs, ds, hcs⟩ := hcstep.2.exists_le + have hdim : PolyBounded (fun a => (encIn a).length) dimension := by + simpa only [encUnary_apply, List.length_replicate] using + (cn.polyTime hcn).polyBounded_length + -- Every live state: the binary index, the unary width and the accumulator. + let S := fun a => 4 * dimension a + 4 + B a + have hS : PolyBounded (fun a => (encIn a).length) S := + (((PolyBounded.const 4).mul hdim).add (.const 4)).add hB + have hstateS (a : α) (j : ℕ) (hj : j ≤ 2 ^ dimension a) : + (encPair encNat (encPair encUnary encB) + ((IndexFold.step (visit body))^[j] (0, (dimension a, initial a)))).length ≤ S a := + length_prefix_le body _ j _ _ hj (hstate a j hj) + have hmaxS (a : α) : + NativeCertificate.maxStateLength (encPair encNat (encPair encUnary encB)) + (IndexFold.step (visit body)) (2 ^ dimension a) (0, (dimension a, initial a)) ≤ S a := + NativeCertificate.maxStateLength_le _ _ _ _ (hstateS a) + have hmaxRT (a : α) : + NativeCertificate.maxRoundTime cstep (2 ^ dimension a) (0, (dimension a, initial a)) ≤ + ct * (S a + 1) ^ dt := + NativeCertificate.maxRoundTime_le cstep _ _ fun j hj => (hct _).trans + (Nat.mul_le_mul_left ct (Nat.pow_le_pow_left (by have := hstateS a j hj; omega) dt)) + have hmaxRS (a : α) : + NativeCertificate.maxRoundSpace cstep (2 ^ dimension a) (0, (dimension a, initial a)) ≤ + cs * (S a + 1) ^ ds := + NativeCertificate.maxRoundSpace_le cstep _ _ fun j hj => (hcs _).trans + (Nat.mul_le_mul_left cs (Nat.pow_le_pow_left (by have := hstateS a j hj; omega) ds)) + have htime (a : α) : (certificate cn ci cb).time a = + (cn.time a + (encUnary (dimension a)).length) + + ((encIn a).length + (cn.time a + ci.time a)) + + (2 ^ dimension a + 1) * + (NativeCertificate.maxRoundTime cstep (2 ^ dimension a) (0, (dimension a, initial a)) + + NativeCertificate.maxStateLength (encPair encNat (encPair encUnary encB)) + (IndexFold.step (visit body)) (2 ^ dimension a) (0, (dimension a, initial a)) + + ((encNat (2 ^ dimension a)).length + 1) ^ 2) := rfl + have hspace (a : α) : (certificate cn ci cb).space a = + (cn.space a + (encUnary (dimension a)).length) + + ((encIn a).length + (cn.space a + ci.space a)) + + NativeCertificate.maxRoundSpace cstep (2 ^ dimension a) (0, (dimension a, initial a)) + + NativeCertificate.maxStateLength (encPair encNat (encPair encUnary encB)) + (IndexFold.step (visit body)) (2 ^ dimension a) (0, (dimension a, initial a)) + + (encNat (2 ^ dimension a)).length := rfl + refine ⟨?_, fun a => 2 * cn.time a + dimension a + (encIn a).length + ci.time a + + (ct * (S a + 1) ^ dt + S a + (dimension a + 1 + 1) ^ 2), ?_, fun a => ?_⟩ + · refine (((((((PolyBounded.const 2).mul hcn.2).add hdim).add .self).add hci.2).add + (NativeCertificate.polyBounded_pow_of_polyBounded hS cs ds)).add + (hS.add (hdim.add (.const 1)))).mono fun a => ?_ + rw [hspace a] + simp only [encUnary_apply, List.length_replicate, length_clock] + have := hmaxRS a + have := hmaxS a + omega + · exact ((((((PolyBounded.const 2).mul hcn.1).add hdim).add .self).add hci.1).add + (((NativeCertificate.polyBounded_pow_of_polyBounded hS ct dt).add hS).add + (((hdim.add (.const 1)).add (.const 1)).pow 2))) + · have hY : NativeCertificate.maxRoundTime cstep (2 ^ dimension a) + (0, (dimension a, initial a)) + + NativeCertificate.maxStateLength (encPair encNat (encPair encUnary encB)) + (IndexFold.step (visit body)) (2 ^ dimension a) (0, (dimension a, initial a)) + + ((encNat (2 ^ dimension a)).length + 1) ^ 2 ≤ + ct * (S a + 1) ^ dt + S a + (dimension a + 1 + 1) ^ 2 := by + rw [length_clock] + exact Nat.add_le_add (Nat.add_le_add (hmaxRT a) (hmaxS a)) le_rfl + refine le_trans (le_of_eq ?_) (add_mul_le_mul_add (N := 2 ^ dimension a) + (X := 2 * cn.time a + dimension a + (encIn a).length + ci.time a) hY) + rw [htime a, encUnary_apply, List.length_replicate] + omega + end Cslib.GenericRAM.BooleanFold diff --git a/Complexity/Computability/GenericRAM/Native/ExhaustiveCountFallback.lean b/Complexity/Computability/GenericRAM/Native/ExhaustiveCountFallback.lean index 8fb86b2c8..f94306a75 100644 --- a/Complexity/Computability/GenericRAM/Native/ExhaustiveCountFallback.lean +++ b/Complexity/Computability/GenericRAM/Native/ExhaustiveCountFallback.lean @@ -207,11 +207,11 @@ noncomputable def countPredicateCertificate {pred : P → List Bool → Bool} ((NativeCertificate.linear (.of_eq fun _ => rfl)).prod (NativeCertificate.const 0)) (NativeCertificate.ofPolyTime (computableInPolyTime_countStep hpred))))) -private theorem length_prefix_state_le (pred : P → List Bool → Bool) (x : ℕ × P) {j : ℕ} +private theorem length_prefix_accumulator_le (pred : P → List Bool → Bool) (x : ℕ × P) {j : ℕ} (hj : j ≤ 2 ^ x.1) : - (encPair encNat (encPair encUnary (encPair (encPair encUnary encP) encNat)) - (BooleanFold.runPrefix (countStep pred) x.1 j (x, 0))).length ≤ - 7 * (encPair encUnary encP x).length + 6 := by + (encPair (encPair encUnary encP) encNat + (BooleanFold.runPrefix (countStep pred) x.1 j (x, 0)).2.2).length ≤ + 3 * (encPair encUnary encP x).length + 2 := by have hx_le : x.1 ≤ (encPair encUnary encP x).length := by simp only [length_encPair, encUnary_apply, List.length_replicate] omega @@ -224,32 +224,9 @@ private theorem length_prefix_state_le (pred : P → List Bool → Bool) (x : simpa [Nat.size_eq_bits_len] using Nat.size_le_size hz_le rw [BooleanFold.length_clock] at hm exact hm - have hacc_le : - (encPair (encPair encUnary encP) encNat - (BooleanFold.runPrefix (countStep pred) x.1 j (x, 0)).2.2).length ≤ - 3 * (encPair encUnary encP x).length + 2 := by - rw [length_encPair, prefix_payload_eq] - omega - have hpref := BooleanFold.length_prefix_le (countStep pred) x.1 j - (3 * (encPair encUnary encP x).length + 2) (x, 0) hj hacc_le + rw [length_encPair, prefix_payload_eq] omega -private theorem roundCertificate_isPolynomial {β : Type} {encB : β ↪ List Bool} - {body : ℕ × β → β} (cb : NativeCertificate body (encPair encNat encB) encB) - (hcb : cb.IsPolynomial) : - (IndexFold.roundCertificate cb).IsPolynomial := by - have hsq : PolyBounded (fun p : ℕ × β => (encPair encNat encB p).length) - (fun p => ((encNat p.1).length + 1) ^ 2) := - PolyBounded.of_forall_le 1 2 fun p => by - have hp1 : (encNat p.1).length ≤ (encPair encNat encB p).length := by - simp only [length_encPair]; omega - simpa only [one_mul] using Nat.pow_le_pow_left (Nat.add_le_add_right hp1 1) 2 - have hlin : PolyBounded (fun p : ℕ × β => (encPair encNat encB p).length) - (fun p => (encNat p.1).length + 1) := - PolyBounded.of_forall_le 1 1 fun p => by - simp only [length_encPair, pow_one, one_mul]; omega - exact ⟨(PolyBounded.self.add hsq).add hcb.1, (PolyBounded.self.add hlin).add hcb.2⟩ - private theorem countPredicateCertificate_bounds {pred : P → List Bool → Bool} (hpred : ComputableInPolyTime (fun q : P × List Bool => pred q.1 q.2) (encPair encP encBits) encBool) : @@ -259,112 +236,14 @@ private theorem countPredicateCertificate_bounds {pred : P → List Bool → Boo PolyBounded (fun x : ℕ × P => (encPair encUnary encP x).length) P_ex ∧ PolyBounded (fun x : ℕ × P => (encPair encUnary encP x).length) Q_ex ∧ ∀ x : ℕ × P, (countPredicateCertificate hpred).time x ≤ (2 ^ x.1 + 1) * P_ex x + Q_ex x := by - let cb : NativeCertificate (countStep pred) - (encPair (encPair encUnary encBits) (encPair (encPair encUnary encP) encNat)) - (encPair (encPair encUnary encP) encNat) := - NativeCertificate.ofPolyTime (computableInPolyTime_countStep hpred) - have hcb : cb.IsPolynomial := - NativeCertificate.ofPolyTime_isPolynomial (computableInPolyTime_countStep hpred) - let cstep := IndexFold.roundCertificate (BooleanFold.visitCertificate cb) - have hcstep : cstep.IsPolynomial := - roundCertificate_isPolynomial (BooleanFold.visitCertificate cb) - (BooleanFold.visitCertificate_isPolynomial cb hcb) - obtain ⟨ct, dt, hct⟩ := hcstep.1.exists_le - obtain ⟨cs, ds, hcs⟩ := hcstep.2.exists_le - have hstate (x : ℕ × P) (j : ℕ) (hj : j ≤ 2 ^ x.1) : - (encPair encNat (encPair encUnary (encPair (encPair encUnary encP) encNat)) - ((IndexFold.step (BooleanFold.visit (countStep pred)))^[j] (0, (x.1, (x, 0))))).length ≤ - 7 * (encPair encUnary encP x).length + 6 := - length_prefix_state_le pred x hj - have hmaxS (x : ℕ × P) : - NativeCertificate.maxStateLength - (encPair encNat (encPair encUnary (encPair (encPair encUnary encP) encNat))) - (IndexFold.step (BooleanFold.visit (countStep pred))) - (2 ^ x.1) (0, (x.1, (x, 0))) ≤ 7 * (encPair encUnary encP x).length + 6 := - NativeCertificate.maxStateLength_le _ _ (2 ^ x.1) _ (hstate x) - have hmaxRT (x : ℕ × P) : - NativeCertificate.maxRoundTime cstep (2 ^ x.1) (0, (x.1, (x, 0))) ≤ - ct * (7 * (encPair encUnary encP x).length + 7) ^ dt := - NativeCertificate.maxRoundTime_le cstep (2 ^ x.1) _ fun j hj => - (hct _).trans (Nat.mul_le_mul_left ct - (Nat.pow_le_pow_left (by have := hstate x j hj; omega) dt)) - have hmaxRS (x : ℕ × P) : - NativeCertificate.maxRoundSpace cstep (2 ^ x.1) (0, (x.1, (x, 0))) ≤ - cs * (7 * (encPair encUnary encP x).length + 7) ^ ds := - NativeCertificate.maxRoundSpace_le cstep (2 ^ x.1) _ fun j hj => - (hcs _).trans (Nat.mul_le_mul_left cs - (Nat.pow_le_pow_left (by have := hstate x j hj; omega) ds)) - have hx_le (x : ℕ × P) : x.1 ≤ (encPair encUnary encP x).length := by - simp only [length_encPair, encUnary_apply, List.length_replicate]; omega - have hB7 : PolyBounded (fun x : ℕ × P => (encPair encUnary encP x).length) - (fun x => 7 * (encPair encUnary encP x).length + 6) := - ((PolyBounded.const 7).mul .self).add (.const 6) - have hSpace : PolyBounded (fun x : ℕ × P => (encPair encUnary encP x).length) - (countPredicateCertificate hpred).space := by - have hupper : PolyBounded (fun x : ℕ × P => (encPair encUnary encP x).length) - (fun x => 6 * (encPair encUnary encP x).length + - cs * (7 * (encPair encUnary encP x).length + 7) ^ ds + - (7 * (encPair encUnary encP x).length + 6) + - ((encPair encUnary encP x).length + 1)) := - (((((PolyBounded.const 6).mul .self).add - (NativeCertificate.polyBounded_pow_of_polyBounded hB7 cs ds)).add hB7).add - (PolyBounded.self.add (.const 1))) - refine hupper.mono fun x => ?_ - change (BooleanFold.clock.comp - (NativeCertificate.linear (ComputableInO.fst encUnary encP))).space x + - ((NativeCertificate.const 0).prod - ((NativeCertificate.linear (ComputableInO.fst encUnary encP)).prod - ((NativeCertificate.linear (.of_eq fun _ => rfl)).prod - (NativeCertificate.const 0)))).space x + - NativeCertificate.maxRoundSpace cstep (2 ^ x.1) (0, (x.1, (x, 0))) + - NativeCertificate.maxStateLength - (encPair encNat (encPair encUnary (encPair (encPair encUnary encP) encNat))) - (IndexFold.step (BooleanFold.visit (countStep pred))) (2 ^ x.1) (0, (x.1, (x, 0))) + - (encNat (2 ^ x.1)).length ≤ _ - simp only [NativeCertificate.comp_space, NativeCertificate.linear_space, - NativeCertificate.prod_space, NativeCertificate.const_space, BooleanFold.clock, - encUnary_apply, List.length_replicate, BooleanFold.length_clock] - have h1 := hmaxRS x - have h2 := hmaxS x - have h3 := hx_le x - omega - refine ⟨hSpace, fun x => ct * (7 * (encPair encUnary encP x).length + 7) ^ dt + - (7 * (encPair encUnary encP x).length + 6) + - ((encPair encUnary encP x).length + 2) ^ 2, - fun x => 6 * (encPair encUnary encP x).length, ?_, (PolyBounded.const 6).mul .self, fun x => ?_⟩ - · exact ((NativeCertificate.polyBounded_pow_of_polyBounded hB7 ct dt).add hB7).add - (NativeCertificate.polyBounded_pow_of_polyBounded (PolyBounded.self.add (.const 1)) 1 2 - |>.mono fun x => by simp only [one_mul]; exact le_of_eq (by ring)) - · change (BooleanFold.clock.comp - (NativeCertificate.linear (ComputableInO.fst encUnary encP))).time x + - ((NativeCertificate.const 0).prod - ((NativeCertificate.linear (ComputableInO.fst encUnary encP)).prod - ((NativeCertificate.linear (.of_eq fun _ => rfl)).prod - (NativeCertificate.const 0)))).time x + - (2 ^ x.1 + 1) * (NativeCertificate.maxRoundTime cstep (2 ^ x.1) (0, (x.1, (x, 0))) + - NativeCertificate.maxStateLength - (encPair encNat (encPair encUnary (encPair (encPair encUnary encP) encNat))) - (IndexFold.step (BooleanFold.visit (countStep pred))) (2 ^ x.1) (0, (x.1, (x, 0))) + - ((encNat (2 ^ x.1)).length + 1) ^ 2) ≤ _ - simp only [NativeCertificate.comp_time, NativeCertificate.linear_time, - NativeCertificate.prod_time, NativeCertificate.const_time, BooleanFold.clock, - encUnary_apply, List.length_replicate, BooleanFold.length_clock] - have h1 := hmaxRT x - have h2 := hmaxS x - have h3 := hx_le x - have h4 : (x.1 + 1 + 1) ^ 2 ≤ ((encPair encUnary encP x).length + 2) ^ 2 := - Nat.pow_le_pow_left (by omega) 2 - have hmul : - (2 ^ x.1 + 1) * (NativeCertificate.maxRoundTime cstep (2 ^ x.1) (0, (x.1, (x, 0))) + - NativeCertificate.maxStateLength - (encPair encNat (encPair encUnary (encPair (encPair encUnary encP) encNat))) - (IndexFold.step (BooleanFold.visit (countStep pred))) - (2 ^ x.1) (0, (x.1, (x, 0))) + (x.1 + 1 + 1) ^ 2) ≤ - (2 ^ x.1 + 1) * (ct * (7 * (encPair encUnary encP x).length + 7) ^ dt + - (7 * (encPair encUnary encP x).length + 6) + - ((encPair encUnary encP x).length + 2) ^ 2) := - Nat.mul_le_mul_left _ (by omega) - omega + obtain ⟨hspace, T, hT, htime⟩ := BooleanFold.certificate_bounds + (NativeCertificate.linear_isPolynomial _) + (NativeCertificate.prod_isPolynomial _ _ (NativeCertificate.linear_isPolynomial _) + (NativeCertificate.const_isPolynomial _)) + (NativeCertificate.ofPolyTime_isPolynomial (computableInPolyTime_countStep hpred)) + (((PolyBounded.const 3).mul .self).add (.const 2)) + fun x j hj => length_prefix_accumulator_le pred x hj + exact ⟨hspace, T, fun _ => 0, hT, .const 0, fun x => htime x⟩ end StreamingCore diff --git a/Complexity/Computability/GenericRAM/Native/IndexFold.lean b/Complexity/Computability/GenericRAM/Native/IndexFold.lean index be1c86cf8..9b3c66844 100644 --- a/Complexity/Computability/GenericRAM/Native/IndexFold.lean +++ b/Complexity/Computability/GenericRAM/Native/IndexFold.lean @@ -107,6 +107,23 @@ def roundCertificate {body : ℕ × β → β} space p := (encPair encNat encB p).length + ((encNat p.1).length + 1) + cb.space p computes := (ComputableInO.natSucc.comp (ComputableInO.fst encNat encB)).prod cb.computes +/-- A polynomial callback gives a polynomial round: advancing the binary index costs a polynomial +in its length. -/ +theorem roundCertificate_isPolynomial {body : ℕ × β → β} + (cb : NativeCertificate body (encPair encNat encB) encB) (hcb : cb.IsPolynomial) : + (roundCertificate cb).IsPolynomial := by + have hsq : PolyBounded (fun p : ℕ × β => (encPair encNat encB p).length) + (fun p => ((encNat p.1).length + 1) ^ 2) := + PolyBounded.of_forall_le 1 2 fun p => by + have hp1 : (encNat p.1).length ≤ (encPair encNat encB p).length := by + simp only [length_encPair]; omega + simpa only [one_mul] using Nat.pow_le_pow_left (Nat.add_le_add_right hp1 1) 2 + have hlin : PolyBounded (fun p : ℕ × β => (encPair encNat encB p).length) + (fun p => (encNat p.1).length + 1) := + PolyBounded.of_forall_le 1 1 fun p => by + simp only [length_encPair, pow_one, one_mul]; omega + exact ⟨(PolyBounded.self.add hsq).add hcb.1, (PolyBounded.self.add hlin).add hcb.2⟩ + /-- One fixed native machine streams a runtime binary number of indices. Its bound is the existing iterator's trajectory-max bound; neither a finite state type nor a machine is selected separately for each runtime `n`. -/ diff --git a/Complexity/Foundations/Data/BitString/Binary.lean b/Complexity/Foundations/Data/BitString/Binary.lean index 38abbff5e..f85245c37 100644 --- a/Complexity/Foundations/Data/BitString/Binary.lean +++ b/Complexity/Foundations/Data/BitString/Binary.lean @@ -29,6 +29,8 @@ significant bit first), as well as `Nat.ofBits` and `Nat.testBit`, without addin * `Cslib.BitString.val_equivFin_eq_ofBits`: `equivFin` agrees with `Nat.ofBits`. * `Cslib.BitString.equivFin_symm_apply`: the `i`-th bit of `(equivFin n).symm k` is `(k : ℕ).testBit i`. +* `Cslib.BitString.lsbValue_eq_binaryValue_reverse`: little-endian digits are the reversed + big-endian ones. * `Cslib.BitString.lsbValue_ofFn`: reading the bits of an `n`-bit word in order gives its number in `equivFin n`. * `Cslib.BitString.binaryValue_reverse_ofFn`: reading the reversed list of bits of an `n`-bit word @@ -84,6 +86,15 @@ theorem binaryValue_reverse_ofFn {n : ℕ} (y : BitString n) : rw [h, Nat.add_comm] rfl +/-- Reading little-endian digits (`lsbValue`) is reading the reversed digits most significant +first (`binaryValue`). -/ +theorem lsbValue_eq_binaryValue_reverse (w : List Bool) : lsbValue w = binaryValue w.reverse := by + induction w with + | nil => rfl + | cons b w ih => + rw [lsbValue, List.reverse_cons, binaryValue_snoc, ih] + omega + /-- The fixed-width word `lowBits n k` equals the bits of `(equivFin n).symm k`. -/ theorem lowBits_eq_ofFn_equivFin_symm (n : ℕ) (k : Fin (2 ^ n)) : lowBits n (k : ℕ) = List.ofFn ((equivFin n).symm k) := by diff --git a/ComplexityTests/Computability/Circuit/Frontier/DirectContraction.lean b/ComplexityTests/Computability/Circuit/Frontier/DirectContraction.lean new file mode 100644 index 000000000..e662ad97f --- /dev/null +++ b/ComplexityTests/Computability/Circuit/Frontier/DirectContraction.lean @@ -0,0 +1,86 @@ +/- +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.DirectContraction + +/-! +# Tests for direct summation + +Hand-checked direct summations of small explicit networks modulo `2 ^ P`, including a precision +that reduces the result, a precision zero, a port naming no edge, a table that is too short, and +a network without edges. The last tests derive the unconditional contract form of the bounds +and check the shape of the binary-precision certificate. +-/ + +@[expose] public section + +namespace ComplexityTests.Computability.Circuit.Frontier.DirectContraction + +open Cslib.Circuits.Frontier ExplicitTensorNetwork + +/-- Edges `0` and `1`; vertex `A` reads both, with table `(1, 2, 3, 4)` at positions `x₀ + 2 x₁`, +and vertex `B` reads edge `0`, with table `(5, 7)`. By hand, +`Z = (A₀₀ + A₀₁) B₀ + (A₁₀ + A₁₁) B₁ = (1 + 3)·5 + (2 + 4)·7 = 62`. -/ +def path : ExplicitTensorNetwork ℕ := + ⟨2, [([0, 1], [1, 2, 3, 4]), ([0], [5, 7])]⟩ + +example : path.contraction = 62 := by decide + +/-- `62 = 3·16 + 14`, `62 < 2 ^ 6`, and every number is `0` modulo `2 ^ 0 = 1`. -/ +example : directContraction (4, 1, path) = 14 ∧ directContraction (6, 1, path) = 62 ∧ + directContraction (0, 1, path) = 0 := by + decide + +/-- The number `r` of row vertices does not change direct summation. -/ +example : directContraction (4, 0, path) = directContraction (4, 2, path) := by decide + +/-- The correctness theorem on this instance. -/ +example : directContraction (4, 1, path) = 62 % 2 ^ 4 := by + rw [directContraction_eq] + decide + +/-- Port `5` names no edge and reads `false`; the table `(3)` of the last vertex has no entry at +position `1`, which reads `0`. So only `x₀ = 0` contributes: `Z = 3 · 3 = 9`. -/ +def ragged : ExplicitTensorNetwork ℕ := + ⟨1, [([5], [3, 4]), ([0], [3])]⟩ + +example : ragged.contraction = 9 ∧ directContraction (10, 0, ragged) = 9 := by decide + +/-- A network without edges has one assignment, the empty one, and its contraction is the product +of the entries at position `0`. -/ +def noEdges : ExplicitTensorNetwork ℕ := + ⟨0, [([], [6]), ([], [7])]⟩ + +example : directContraction (5, 0, noEdges) = 42 % 32 := by decide + +/-- The bounds give the unconditional contract form `K (n + 1) ^ K 2 ^ (K m)` on every input. -/ +example : ∃ K : ℕ, ∀ x : ℕ × ℕ × ExplicitTensorNetwork ℕ, + directContractionCertificate.time x ≤ + K * ((encContractionInput x).length + 1) ^ K * 2 ^ (K * x.2.2.numEdges) ∧ + directContractionCertificate.space x ≤ K * ((encContractionInput x).length + 1) ^ K := by + obtain ⟨K, hK⟩ := exists_directContractionCertificate_le + refine ⟨K + 1, fun x => ⟨(hK x).1.trans ?_, (hK x).2.trans ?_⟩⟩ + · exact Nat.mul_le_mul (Nat.mul_le_mul (Nat.le_succ K) + (Nat.pow_le_pow_right (Nat.succ_pos _) (Nat.le_succ K))) + (Nat.pow_le_pow_right two_pos (Nat.le_mul_of_pos_left _ (Nat.succ_pos K))) + · exact Nat.mul_le_mul (Nat.le_succ K) (Nat.pow_le_pow_right (Nat.succ_pos _) (Nat.le_succ K)) + +/-- With the precision in binary, the certificate has the shape the counting simulation's +contraction interface asks for: `(P, G) ↦ value G % 2 ^ P` on `encPair encNat encN`, with `G` +the row count and the network, `value G` its contraction and +`encN = encPair encNat encExplicitNetwork`. -/ +noncomputable example : Cslib.GenericRAM.NativeCertificate + (fun p : ℕ × (ℕ × ExplicitTensorNetwork ℕ) => + (fun G : ℕ × ExplicitTensorNetwork ℕ => G.2.contraction) p.2 % 2 ^ p.1) + (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat + (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat encExplicitNetwork)) + Turing.MultiTapeTM.encNat := + directContractionBinaryCertificate + +end ComplexityTests.Computability.Circuit.Frontier.DirectContraction