From c33195005eae3e6da0e33ad648b13d3cefaf9b42 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 17:41:28 -0400 Subject: [PATCH 1/5] feat(circuit/frontier): Boolean tensor networks and their contraction Tensor networks over a commutative semiring as the weighted form of the frontier constraint networks (shared Multigraph and locality), with the contraction Z, subdivision by equality tensors (preserves Z, bipartite, keeps degree bounds), explicit tables with ordered ports and size measures, the write-out theorem, and the 0-1 bridge from constraint networks. Tracking: #1833 (T1), #1538. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 3 + .../Circuit/Frontier/TensorNetwork.lean | 251 ++++++++++++++++++ .../Frontier/TensorNetwork/Constraint.lean | 81 ++++++ .../Frontier/TensorNetwork/Explicit.lean | 210 +++++++++++++++ .../Circuit/Frontier/TensorNetwork.lean | 116 ++++++++ 5 files changed, 661 insertions(+) create mode 100644 Complexity/Computability/Circuit/Frontier/TensorNetwork.lean create mode 100644 Complexity/Computability/Circuit/Frontier/TensorNetwork/Constraint.lean create mode 100644 Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean create mode 100644 ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean diff --git a/Complexity.lean b/Complexity.lean index 3942e2e28..3e53d5172 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -857,6 +857,9 @@ public import Complexity.Computability.Circuit.Frontier.Projection public import Complexity.Computability.Circuit.Frontier.Rectangle public import Complexity.Computability.Circuit.Frontier.Reduction 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.Explicit public import Complexity.Computability.Circuit.Frontier.TwoSidedWitness public import Complexity.Computability.Circuit.Frontier.Unconditional public import Complexity.Computability.Circuit.Frontier.Witness diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork.lean new file mode 100644 index 000000000..cf45df7f8 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork.lean @@ -0,0 +1,251 @@ +/- +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.Multigraph +public import Mathlib.Algebra.BigOperators.Group.Finset.Basic +public import Mathlib.Combinatorics.SimpleGraph.Bipartite +public import Mathlib.Basic.Finite.Sum +public import Mathlib.Data.Fintype.Pi +import Mathlib.Algebra.BigOperators.GroupWithZero.Finset +import Mathlib.Algebra.BigOperators.Ring.Finset + +/-! +# Tensor networks and their contraction + +A *tensor network* over a commutative semiring `R` and an alphabet `U` is a multigraph whose +edges carry values in `U`, with a *tensor* at each vertex `v`: a value `N.tensor v x ∈ R` for each +assignment `x : E → U` of values to the edges, which depends only on the values on the edges at +`v`. Its *contraction* sums, over all assignments, the product of the tensors: + + `Z(N) = ∑ x : E → U, ∏ v, N.tensor v x`. + +A *Boolean* tensor network has `U = Bool`, one bit per edge. The usual presentation gives the +tensor at `v` as a function `F_v` of the bits on the ordered list `δ(v)` of edges at `v`, with +`Z = ∑ x ∏ v F_v (x|δ(v))`. Here the tensor is a function of the whole assignment, constrained to +read only the edges at `v` (`TensorNetwork.tensor_congr`); the ordered presentation, with +explicit tables, is `Cslib.Circuits.Frontier.ExplicitTensorNetwork`, and +`Cslib.Circuits.Frontier.TensorNetwork.contraction_toExplicit` shows that the two contractions +agree. Parallel edges are distinct elements of `E` and so give distinct ports. + +A tensor network is the weighted form of a constraint network +(`Cslib.Circuits.Frontier.Network`) on a fixed input: the two share the multigraph and the +locality condition, and a constraint becomes its `0`–`1` indicator tensor, whose contraction +counts the satisfying assignments +(`Cslib.Circuits.Frontier.Network.contraction_toTensorNetwork`). + +**Subdivision** (`TensorNetwork.subdivide`). Splitting every edge `e` into two edges joined at a +new vertex that carries the *equality tensor* `[y₁ = y₂]` preserves the contraction +(`TensorNetwork.contraction_subdivide`): each assignment of the old network extends in exactly one +way to an assignment of the new one with nonzero weight. The subdivided network is bipartite +(`TensorNetwork.isBipartite_subdivide`), with the old vertices on one side and the new ones on the +other, and it keeps the degree bound of a loopless network (`TensorNetwork.maxDegreeLE_subdivide`). +It has twice as many edges and one new vertex per old edge. + +## Main definitions + +* `Cslib.Circuits.Frontier.Multigraph.IsBipartite`: the vertices split into two sides and every + edge joins the two sides. +* `Cslib.Circuits.Frontier.TensorNetwork`: a tensor network. +* `Cslib.Circuits.Frontier.TensorNetwork.contraction`: its contraction `Z`. +* `Cslib.Circuits.Frontier.TensorNetwork.subdivide`: subdivision of every edge by an equality + tensor. + +## Main results + +* `Cslib.Circuits.Frontier.Multigraph.isBipartite_iff`: a multigraph is bipartite iff it has no + loops and its underlying simple graph is bipartite (`SimpleGraph.IsBipartite`). +* `Cslib.Circuits.Frontier.TensorNetwork.contraction_subdivide`: subdivision preserves the + contraction. +* `Cslib.Circuits.Frontier.TensorNetwork.isBipartite_subdivide`: a subdivided network is + bipartite. +* `Cslib.Circuits.Frontier.TensorNetwork.maxDegreeLE_subdivide`: subdividing a loopless network of + maximum degree at most `d ≥ 2` gives maximum degree at most `d`. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Appendix D.1 (p. 53) and + the subdivision step of Appendix D.2 (p. 54). +-/ + +@[expose] public section + +namespace Cslib.Circuits.Frontier + +open Set + +/-! ### Bipartite multigraphs -/ + +namespace Multigraph + +variable {V E : Type*} (G : Multigraph V E) + +/-- A multigraph is *bipartite* when its vertices split into two sides, `side v = true` and +`side v = false`, and every edge joins the two sides. A bipartite multigraph has no loops +(`Multigraph.IsBipartite.loopless`). -/ +def IsBipartite : Prop := + ∃ side : V → Bool, ∀ e, side (G.src e) ≠ side (G.tgt e) + +variable {G} + +/-- A bipartite multigraph has no loops. -/ +theorem IsBipartite.loopless (h : G.IsBipartite) : G.Loopless := by + obtain ⟨side, hside⟩ := h + exact fun e he => hside e (congrArg side he) + +/-- A multigraph is bipartite exactly when it has no loops and its underlying simple graph is +bipartite in the sense of Mathlib (`SimpleGraph.IsBipartite`, a `2`-colouring). -/ +theorem isBipartite_iff : G.IsBipartite ↔ G.Loopless ∧ G.toSimpleGraph.IsBipartite := by + constructor + · intro h + refine ⟨h.loopless, ?_⟩ + obtain ⟨side, hside⟩ := h + have hcol : G.toSimpleGraph.Coloring Bool := SimpleGraph.Coloring.mk side fun {u v} huv => by + obtain ⟨-, e, he⟩ := toSimpleGraph_adj.mp huv + rcases Sym2.eq_iff.mp he with ⟨hu, hv⟩ | ⟨hu, hv⟩ + · exact hu ▸ hv ▸ hside e + · exact hu ▸ hv ▸ (hside e).symm + simpa using hcol.colorable + · rintro ⟨hloop, ⟨c⟩⟩ + refine ⟨fun v => decide (c v = 0), fun e he => ?_⟩ + have hadj : G.toSimpleGraph.Adj (G.src e) (G.tgt e) := toSimpleGraph_adj.mpr ⟨hloop e, e, rfl⟩ + have key : ∀ a b : Fin 2, a ≠ b → decide (a = 0) ≠ decide (b = 0) := by decide + exact key _ _ (c.valid hadj) he + +end Multigraph + +/-! ### Tensor networks -/ + +/-- A *tensor network* over the commutative semiring `R` with alphabet `U`: a multigraph on the +vertices `V` and edges `E`, whose edges carry values in `U`, and at each vertex a *tensor*, a value +in `R` for each assignment of values to the edges, that sees only the values on the edges at that +vertex. A *Boolean* tensor network has `U = Bool`. -/ +structure TensorNetwork (R U V E : Type*) extends Multigraph V E where + /-- The tensor at a vertex: its value on an assignment of values to the edges. -/ + tensor : V → (E → U) → R + /-- Tensors are local: the tensor at `v` sees only the values on the edges incident to `v`. -/ + tensor_congr : ∀ v x y, (∀ e, src e = v ∨ tgt e = v → x e = y e) → tensor v x = tensor v y + +namespace TensorNetwork + +variable {R U V E : Type*} + +section Contraction + +variable [CommSemiring R] [Fintype U] [Fintype V] [Fintype E] [DecidableEq E] + +/-- The *contraction* of a tensor network: the sum over all assignments of values to the edges of +the product of the tensors at all vertices. -/ +def contraction (N : TensorNetwork R U V E) : R := + ∑ x : E → U, ∏ v, N.tensor v x + +end Contraction + +/-! ### Subdivision by equality tensors -/ + +section Subdivide + +variable [DecidableEq U] [DecidableEq V] [Zero R] [One R] (N : TensorNetwork R U V E) + +/-- The *subdivision* of a tensor network by equality tensors. Each edge `e` becomes a new vertex +`Sum.inr e` and two edges: `Sum.inl e`, from the source of `e`, and `Sum.inr e`, from its target, +both ending at `Sum.inr e`. The new vertex carries the *equality tensor*, one when its two edges +carry the same value and zero otherwise. An old vertex reads the value of `e` on the half of `e` +at its end. -/ +def subdivide : TensorNetwork R U (V ⊕ E) (E ⊕ E) where + src := Sum.elim (fun e => .inl (N.src e)) (fun e => .inl (N.tgt e)) + tgt := Sum.elim .inr .inr + tensor + | .inl v, y => N.tensor v fun e => if N.src e = v then y (.inl e) else y (.inr e) + | .inr e, y => if y (.inl e) = y (.inr e) then 1 else 0 + tensor_congr := by + rintro (v | e) y y' h + · refine N.tensor_congr v _ _ fun e he => ?_ + by_cases hs : N.src e = v + · simp only [hs, ite_true] + exact h (.inl e) (Or.inl (by simp [hs])) + · simp only [hs, ite_false] + exact h (.inr e) (Or.inl (by simp [he.resolve_left hs])) + · simp only + rw [h (.inl e) (Or.inr rfl), h (.inr e) (Or.inr rfl)] + +@[simp] theorem subdivide_src_inl (e : E) : N.subdivide.src (.inl e) = .inl (N.src e) := rfl + +@[simp] theorem subdivide_src_inr (e : E) : N.subdivide.src (.inr e) = .inl (N.tgt e) := rfl + +@[simp] theorem subdivide_tgt_inl (e : E) : N.subdivide.tgt (.inl e) = .inr e := rfl + +@[simp] theorem subdivide_tgt_inr (e : E) : N.subdivide.tgt (.inr e) = .inr e := rfl + +/-- The tensor at an old vertex of the subdivision. -/ +theorem subdivide_tensor_inl (v : V) (y : E ⊕ E → U) : + N.subdivide.tensor (.inl v) y = + N.tensor v fun e => if N.src e = v then y (.inl e) else y (.inr e) := rfl + +/-- The equality tensor at a new vertex of the subdivision. -/ +theorem subdivide_tensor_inr (e : E) (y : E ⊕ E → U) : + N.subdivide.tensor (.inr e) y = if y (.inl e) = y (.inr e) then 1 else 0 := rfl + +/-- **Subdivision is bipartite.** Every edge of the subdivision joins an old vertex to a new one. -/ +theorem isBipartite_subdivide : N.subdivide.IsBipartite := + ⟨Sum.isLeft, fun e => by cases e <;> simp⟩ + +/-- **Subdivision preserves the contraction.** An assignment of the subdivision has nonzero +weight only when the two halves of every edge carry the same value, and such assignments are +exactly the assignments of the original network. -/ +theorem contraction_subdivide {R : Type*} [CommSemiring R] [Fintype U] [Fintype V] [Fintype E] + [DecidableEq E] (N : TensorNetwork R U V E) : N.subdivide.contraction = N.contraction := by + classical + -- Split an assignment of the subdivision into its values `a` on the source halves and `b` on + -- the target halves. + rw [contraction, contraction, ← (Equiv.sumArrowEquivProdArrow E E U).symm.sum_comp, + Fintype.sum_prod_type] + refine Finset.sum_congr rfl fun a _ => ?_ + simp only [Fintype.prod_sum_type, subdivide_tensor_inl, subdivide_tensor_inr, + Equiv.sumArrowEquivProdArrow_symm_apply_inl, Equiv.sumArrowEquivProdArrow_symm_apply_inr] + rw [Finset.sum_eq_single a] + · -- Equal halves: every equality tensor is one, and the old vertices read `a`. + simp only [ite_self, ite_true, Finset.prod_const_one, mul_one] + · -- Unequal halves on some edge `e`: the equality tensor at `e` vanishes. + intro b _ hb + obtain ⟨e, he⟩ := Function.ne_iff.mp hb + exact mul_eq_zero_of_right _ + (Finset.prod_eq_zero (Finset.mem_univ e) (ite_eq_right fun h => he h.symm)) + · exact fun h => absurd (Finset.mem_univ a) h + +/-- The edges at an old vertex of the subdivision are the halves of its old edges at it. -/ +theorem incidenceSet_subdivide_inl (v : V) : + N.subdivide.incidenceSet (.inl v) = + Sum.inl '' {e | N.src e = v} ∪ Sum.inr '' {e | N.tgt e = v} := by + ext (e | e) <;> simp [Multigraph.mem_incidenceSet] + +/-- The edges at a new vertex of the subdivision are the two halves of its edge. -/ +theorem incidenceSet_subdivide_inr (e : E) : + N.subdivide.incidenceSet (.inr e) = {.inl e, .inr e} := by + ext (e' | e') <;> simp [Multigraph.mem_incidenceSet, eq_comm] + +/-- **Subdivision keeps the degree bound.** In a loopless network, the edges at a vertex are those +with it as source and those with it as target, and they are the halves at its old vertex in the +subdivision; a new vertex has degree two. -/ +theorem maxDegreeLE_subdivide [Finite E] {d : ℕ} (hloop : N.Loopless) + (hd : N.MaxDegreeLE d) (h2 : 2 ≤ d) : N.subdivide.MaxDegreeLE d := by + rintro (v | e) + · rw [incidenceSet_subdivide_inl, ncard_union_eq _ (toFinite _) (toFinite _), + ncard_image_of_injective _ Sum.inl_injective, ncard_image_of_injective _ Sum.inr_injective, + ← ncard_union_eq _ (toFinite _) (toFinite _)] + · exact hd v + · exact disjoint_left.mpr fun e hs ht => hloop e (hs.trans ht.symm) + · exact disjoint_left.mpr fun _ ⟨_, _, h⟩ ⟨_, _, h'⟩ => Sum.inl_ne_inr (h.trans h'.symm) + · rw [incidenceSet_subdivide_inr, ncard_pair Sum.inl_ne_inr] + exact h2 + +end Subdivide + +end TensorNetwork + +end Cslib.Circuits.Frontier diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Constraint.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Constraint.lean new file mode 100644 index 000000000..08c80a664 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Constraint.lean @@ -0,0 +1,81 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Frontier.Network +public import Complexity.Computability.Circuit.Frontier.TensorNetwork +import Mathlib.Algebra.BigOperators.GroupWithZero.Finset +import Mathlib.Algebra.BigOperators.Ring.Finset + +/-! +# Constraint networks as `0`–`1` tensor networks + +A constraint network (`Cslib.Circuits.Frontier.Network`) on a fixed input is a tensor network +whose tensors take only the values zero and one: the tensor at `v` is the indicator of the +constraint at `v` (`Network.toTensorNetwork`). The two share the multigraph, and the locality of +the constraints is the locality of the tensors. The contraction of this tensor network is the +number of satisfying assignments (`Network.contraction_toTensorNetwork`), so over `ℕ` it is +nonzero exactly at the accepted inputs (`Network.mem_accepted_iff_contraction_ne_zero`). + +A general tensor network is thus the weighted form of a constraint network, and the frontier +constraint networks of circuits (`Cslib.Circuits.Frontier.Compiler.network`) are special cases. + +## Main definitions + +* `Cslib.Circuits.Frontier.Network.toTensorNetwork`: the indicator tensor network of a constraint + network on an input. + +## Main results + +* `Cslib.Circuits.Frontier.Network.contraction_toTensorNetwork`: its contraction counts the + satisfying assignments. +* `Cslib.Circuits.Frontier.Network.mem_accepted_iff_contraction_ne_zero`: an input is accepted iff + the contraction over `ℕ` is nonzero. +-/ + +@[expose] public section + +namespace Cslib.Circuits.Frontier.Network + +variable {U ι V E : Type*} (R : Type*) (N : Network U ι V E) + +open Classical in +/-- The `0`–`1` tensor network of a constraint network on the input `x`: the same multigraph, with +the tensor at `v` equal to one where the constraint at `v` holds and to zero elsewhere. -/ +noncomputable def toTensorNetwork [Zero R] [One R] (x : ι → U) : TensorNetwork R U V E where + toMultigraph := N.toMultigraph + tensor v α := if N.Constraint v x α then 1 else 0 + tensor_congr v α β h := by + have hiff : N.Constraint v x α ↔ N.Constraint v x β := + ⟨N.constraint_congr v x x α β (fun _ _ => rfl) h, + N.constraint_congr v x x β α (fun _ _ => rfl) fun e he => (h e he).symm⟩ + simp only [hiff] + +/-- The tensor network of a constraint network has the same multigraph. -/ +@[simp] theorem toMultigraph_toTensorNetwork [Zero R] [One R] (x : ι → U) : + (N.toTensorNetwork R x).toMultigraph = N.toMultigraph := + rfl + +/-- **The contraction counts satisfying assignments.** The contraction of the `0`–`1` tensor +network of a constraint network on the input `x` is the number of assignments of values to the +edges that satisfy every constraint on `x`. -/ +theorem contraction_toTensorNetwork [CommSemiring R] [Fintype U] [Fintype V] [Fintype E] + [DecidableEq E] (x : ι → U) : + (N.toTensorNetwork R x).contraction = ({α | N.Satisfies x α} : Set (E → U)).ncard := by + classical + simp only [TensorNetwork.contraction, toTensorNetwork, Fintype.prod_boole, Finset.sum_boole, + Set.ncard_eq_toFinset_card', Set.toFinset_ofPred, Satisfies] + +/-- Over `ℕ`, the contraction is nonzero exactly at the accepted inputs. -/ +theorem mem_accepted_iff_contraction_ne_zero [Fintype U] [Fintype V] [Fintype E] [DecidableEq E] + (x : ι → U) : x ∈ N.accepted ↔ (N.toTensorNetwork ℕ x).contraction ≠ 0 := by + rw [contraction_toTensorNetwork, Nat.cast_id, Ne, Set.ncard_eq_zero (Set.toFinite _), + ← Ne, ← Set.nonempty_iff_ne_empty] + rfl + +end Cslib.Circuits.Frontier.Network diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean new file mode 100644 index 000000000..28f5dd3f5 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean @@ -0,0 +1,210 @@ +/- +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 +import Mathlib.Algebra.BigOperators.Fin +import Mathlib.Data.List.GetD + +/-! +# Explicit Boolean tensor networks + +An *explicit* Boolean tensor network (`ExplicitTensorNetwork R`) is the data an algorithm reads: +the number of edges, numbered `0, 1, …`, and a list of vertices, each given by + +* its ordered list of *ports*, the numbers of the edges at the vertex, and +* its *table*: the value of its tensor when port `i` carries the bit `bs[i]` is the entry at + position `tableIndex bs`, the number whose binary digit `i` is `bs[i]`. + +So a vertex with `k` ports has a table of `2 ^ k` entries. The contraction of an explicit network +(`ExplicitTensorNetwork.contraction`) sums, over all assignments of bits to the edges, the product +of the table entries at the bits on the ports. It needs no well-formedness: a port naming no edge +reads `false`, and a position past the end of a table has entry zero. + +Its size measures are the number of edges, the number of vertices, the maximum number of ports of +a vertex (`ExplicitTensorNetwork.maxDegree`) and the total length of the tables +(`ExplicitTensorNetwork.tableLength`). + +**Writing a network out** (`TensorNetwork.toExplicit`). Given numberings of the vertices and the +edges of a Boolean tensor network on finite types, list the edges at each vertex in increasing +order and tabulate its tensor on them. The contraction is unchanged +(`TensorNetwork.contraction_toExplicit`). + +## Main definitions + +* `Cslib.Circuits.Frontier.tableIndex`: the position of a list of bits in a table. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork`: an explicit Boolean tensor network. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.entry`, + `Cslib.Circuits.Frontier.ExplicitTensorNetwork.portBits`: table lookup and the bits on a list + of ports. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.contraction`: the contraction. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.maxDegree`, + `Cslib.Circuits.Frontier.ExplicitTensorNetwork.tableLength`: size measures. +* `Cslib.Circuits.Frontier.TensorNetwork.explicitPorts`, + `Cslib.Circuits.Frontier.TensorNetwork.explicitTable`, + `Cslib.Circuits.Frontier.TensorNetwork.toExplicit`: writing a Boolean tensor network out. + +## Main results + +* `Cslib.Circuits.Frontier.testBit_tableIndex`, `Cslib.Circuits.Frontier.tableIndex_lt`: the + digits and range of a table position. +* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.maxDegree_le_iff`: the degree bound. +* `Cslib.Circuits.Frontier.TensorNetwork.entry_explicitTable`: a written-out table evaluates the + tensor. +* `Cslib.Circuits.Frontier.TensorNetwork.contraction_toExplicit`: writing a network out preserves + its contraction. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Appendix D.1 (p. 53). +-/ + +@[expose] public section + +namespace Cslib.Circuits.Frontier + +/-- The position of a list of bits in a table: the number whose binary digit `i` is `bs[i]`, so +that the bits are read little-endian. -/ +def tableIndex (bs : List Bool) : ℕ := + (BitVec.ofBoolListLE bs).toNat + +/-- Binary digit `i` of the position of `bs` is `bs[i]`, or `false` past the end of `bs`. -/ +@[simp] theorem testBit_tableIndex (bs : List Bool) (i : ℕ) : + (tableIndex bs).testBit i = bs.getD i false := by + rw [tableIndex, BitVec.testBit_toNat, BitVec.getLsbD_ofBoolListLE] + +/-- A list of `k` bits has a position below `2 ^ k`. -/ +theorem tableIndex_lt (bs : List Bool) : tableIndex bs < 2 ^ bs.length := + BitVec.isLt _ + +/-- An *explicit Boolean tensor network* over `R`: the number of edges, numbered from zero, and a +list of vertices. A vertex is given by its ordered list of *ports*, the numbers of its edges, and +its *table*, whose entry at position `tableIndex bs` is the value of its tensor when port `i` +carries the bit `bs[i]`. -/ +structure ExplicitTensorNetwork (R : Type*) where + /-- The number of edges; the edges are numbered `0, …, numEdges - 1`. -/ + numEdges : ℕ + /-- The vertices, each given by its ports and its table. -/ + vertices : List (List ℕ × List R) + +namespace ExplicitTensorNetwork + +variable {R : Type*} (d : ExplicitTensorNetwork R) + +/-- The entry of a table at a list of bits. A position past the end of the table has entry +zero. -/ +def entry [Zero R] (table : List R) (bs : List Bool) : R := + table.getD (tableIndex bs) 0 + +/-- The bits on a list of ports under an assignment of bits to the edges. A port naming no edge +reads `false`. -/ +def portBits (x : Fin d.numEdges → Bool) (ports : List ℕ) : List Bool := + ports.map fun i => if h : i < d.numEdges then x ⟨i, h⟩ else false + +/-- The *contraction* of an explicit network: the sum over all assignments of bits to the edges of +the product, over the vertices, of the table entries at the bits on their ports. -/ +def contraction [CommSemiring R] : R := + ∑ x : Fin d.numEdges → Bool, (d.vertices.map fun v => entry v.2 (d.portBits x v.1)).prod + +/-- The *maximum degree*: the largest number of ports of a vertex, or zero without vertices. -/ +def maxDegree : ℕ := + (d.vertices.map fun v => v.1.length).foldr max 0 + +/-- The total length of the tables. -/ +def tableLength : ℕ := + (d.vertices.map fun v => v.2.length).sum + +private theorem foldr_max_le_iff (l : List ℕ) (k : ℕ) : l.foldr max 0 ≤ k ↔ ∀ n ∈ l, n ≤ k := by + induction l with + | nil => simp + | cons a l ih => simp [ih] + +/-- The maximum degree is at most `k` exactly when every vertex has at most `k` ports. -/ +theorem maxDegree_le_iff {k : ℕ} : d.maxDegree ≤ k ↔ ∀ v ∈ d.vertices, v.1.length ≤ k := by + rw [maxDegree, foldr_max_le_iff] + constructor + · exact fun h v hv => h _ (List.mem_map_of_mem hv) + · rintro h _ hn + obtain ⟨v, hv, rfl⟩ := List.mem_map.mp hn + exact h v hv + +/-- Every vertex has at most `maxDegree` ports. -/ +theorem length_le_maxDegree {v : List ℕ × List R} (hv : v ∈ d.vertices) : + v.1.length ≤ d.maxDegree := + d.maxDegree_le_iff.mp le_rfl v hv + +end ExplicitTensorNetwork + +/-! ### Writing a tensor network out -/ + +namespace TensorNetwork + +variable {R V E : Type*} [DecidableEq V] {n m : ℕ} (N : TensorNetwork R Bool V E) (ev : V ≃ Fin n) + (ee : E ≃ Fin m) + +/-- The ports of a vertex when the edges are numbered by `ee`: the numbers of the edges at the +vertex, in increasing order. -/ +def explicitPorts (v : V) : List (Fin m) := + (List.finRange m).filter fun j => N.src (ee.symm j) = v ∨ N.tgt (ee.symm j) = v + +/-- An edge is a port of `v` exactly when it is incident to `v`. -/ +@[simp] theorem mem_explicitPorts {v : V} {j : Fin m} : + j ∈ N.explicitPorts ee v ↔ N.src (ee.symm j) = v ∨ N.tgt (ee.symm j) = v := by + simp [explicitPorts] + +/-- The table of a vertex: its tensor at each list of bits on its ports, by position. -/ +def explicitTable (v : V) : List R := + (List.range (2 ^ (N.explicitPorts ee v).length)).map fun j => + N.tensor v fun e => j.testBit ((N.explicitPorts ee v).idxOf (ee e)) + +/-- **A written-out table evaluates the tensor.** At the bits that an assignment puts on the ports +of `v`, the table of `v` has the value of the tensor at that assignment. -/ +theorem entry_explicitTable [Zero R] (v : V) (x : Fin m → Bool) : + ExplicitTensorNetwork.entry (N.explicitTable ee v) ((N.explicitPorts ee v).map x) = + N.tensor v (x ∘ ee) := by + set ps := N.explicitPorts ee v + have hlt : tableIndex (ps.map x) < (N.explicitTable ee v).length := by + simpa [explicitTable, ps] using tableIndex_lt (ps.map x) + rw [ExplicitTensorNetwork.entry, List.getD_eq_getElem _ _ hlt] + simp only [explicitTable, List.getElem_map, List.getElem_range] + refine N.tensor_congr v _ _ fun e he => ?_ + have hmem : ee e ∈ ps := (N.mem_explicitPorts ee).mpr (by simpa using he) + have hidx := List.idxOf_lt_length_of_mem hmem + rw [testBit_tableIndex, List.getD_eq_getElem _ _ (by simpa using hidx), List.getElem_map, + List.getElem_idxOf hidx, Function.comp_apply] + +/-- A Boolean tensor network on finite types written out as an explicit network, numbering the +vertices by `ev` and the edges by `ee`: vertex `i` is `ev.symm i`, with its ports in increasing +order and its table. -/ +def toExplicit : ExplicitTensorNetwork R where + numEdges := m + vertices := List.ofFn fun i => + ((N.explicitPorts ee (ev.symm i)).map Fin.val, N.explicitTable ee (ev.symm i)) + +/-- **Writing a network out preserves its contraction.** -/ +theorem contraction_toExplicit [CommSemiring R] [Fintype V] [Fintype E] [DecidableEq E] : + (N.toExplicit ev ee).contraction = N.contraction := by + rw [ExplicitTensorNetwork.contraction, contraction] + refine Fintype.sum_equiv (ee.symm.arrowCongr (Equiv.refl Bool)) _ _ fun x => ?_ + have hv : (N.toExplicit ev ee).vertices = List.ofFn fun i => + ((N.explicitPorts ee (ev.symm i)).map Fin.val, N.explicitTable ee (ev.symm i)) := rfl + rw [hv, List.map_ofFn, List.prod_ofFn, ← ev.symm.prod_comp] + refine Finset.prod_congr rfl fun i _ => ?_ + -- Every port names an edge, so the bits on the ports are those of the assignment. + have hbits : (N.toExplicit ev ee).portBits x ((N.explicitPorts ee (ev.symm i)).map Fin.val) = + (N.explicitPorts ee (ev.symm i)).map x := by + unfold ExplicitTensorNetwork.portBits + rw [List.map_map] + exact List.map_congr_left fun j _ => dite_eq_left j.isLt + simp only [Function.comp_apply] + rw [hbits, entry_explicitTable] + rfl + +end TensorNetwork + +end Cslib.Circuits.Frontier diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean new file mode 100644 index 000000000..5be31a11e --- /dev/null +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean @@ -0,0 +1,116 @@ +/- +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.Constraint +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit +public import Mathlib.Data.ZMod.Defs + +/-! +# Tests for tensor networks + +Hand-checked contractions of small explicit Boolean tensor networks (two parallel edges, and +four-cycles of equality and negation tensors over `ZMod 8`), a tensor network on finite types +written out and subdivided, and a constraint network counted by its indicator tensor network. +-/ + +@[expose] public section + +namespace ComplexityTests.Computability.Circuit.Frontier.TensorNetwork + +open Cslib.Circuits.Frontier + +/-! ### Explicit networks -/ + +/-- Two vertices joined by two parallel edges `0` and `1`, with the tables `A = (1, 2, 3, 4)` and +`B = (5, 6, 7, 8)`, read at positions `x₀ + 2 x₁`. -/ +def parallel : ExplicitTensorNetwork ℤ := + ⟨2, [([0, 1], [1, 2, 3, 4]), ([0, 1], [5, 6, 7, 8])]⟩ + +/-- By hand: `Z = ∑ᵢ Aᵢ Bᵢ = 1·5 + 2·6 + 3·7 + 4·8 = 70`. -/ +example : parallel.contraction = 70 := by decide + +example : parallel.maxDegree = 2 ∧ parallel.tableLength = 8 := by decide + +/-- The equality tensor on two ports. -/ +def eqTable : List (ZMod 8) := [1, 0, 0, 1] + +/-- The negation tensor on two ports: its two bits differ. -/ +def neTable : List (ZMod 8) := [0, 1, 1, 0] + +/-- A bipartite four-cycle `r₀ - c₀ - r₁ - c₁ - r₀` on the edges `0, 1, 2, 3`, with the table `t` +at `c₁` and equality tensors elsewhere. -/ +def cycle (t : List (ZMod 8)) : ExplicitTensorNetwork (ZMod 8) := + ⟨4, [([3, 0], eqTable), ([0, 1], eqTable), ([1, 2], eqTable), ([2, 3], t)]⟩ + +/-- With equality tensors all around, an assignment contributes exactly when all four bits are +equal: `Z = 2`. -/ +example : (cycle eqTable).contraction = 2 := by decide + +/-- One negation on a cycle forces an odd number of bit changes around it, which is impossible: +`Z = 0`. -/ +example : (cycle neTable).contraction = 0 := by decide + +/-! ### A network on finite types, written out and subdivided -/ + +/-- The table `A` or `B` of `parallel` as a tensor on assignments to `Fin 2`. -/ +def table (v : Fin 2) (x : Fin 2 → Bool) : ℤ := + [[1, 2, 3, 4], [5, 6, 7, 8]][v]!.getD (tableIndex [x 0, x 1]) 0 + +/-- The network `parallel` on `Fin 2` vertices and `Fin 2` edges, both edges from `0` to `1`. +Every edge is at both vertices, so the tensors are trivially local. -/ +def parallelNetwork : TensorNetwork ℤ Bool (Fin 2) (Fin 2) where + src _ := 0 + tgt _ := 1 + tensor := table + tensor_congr v x y h := by + have hxy : x = y := funext fun e => h e (by fin_cases v <;> simp) + rw [hxy] + +/-- Writing the network out gives `parallel` up to the order of its data, and the same +contraction. -/ +example : parallelNetwork.contraction = 70 := by + rw [← parallelNetwork.contraction_toExplicit (Equiv.refl _) (Equiv.refl _)] + decide + +/-- Subdividing both edges by equality tensors gives a bipartite network with the same +contraction and degree bound. -/ +example : parallelNetwork.subdivide.contraction = 70 ∧ parallelNetwork.subdivide.IsBipartite ∧ + parallelNetwork.subdivide.MaxDegreeLE 2 := by + refine ⟨?_, parallelNetwork.isBipartite_subdivide, + parallelNetwork.maxDegreeLE_subdivide (fun e => by simp [parallelNetwork]) (fun v => ?_) + le_rfl⟩ + · rw [TensorNetwork.contraction_subdivide, + ← parallelNetwork.contraction_toExplicit (Equiv.refl _) (Equiv.refl _)] + decide + · exact (Set.ncard_le_card _).trans (by simp) + +/-! ### Constraint networks -/ + +/-- Two vertices joined by two parallel edges, each requiring its two edges to agree. -/ +def agree : Network Bool Empty (Fin 2) (Fin 2) where + src _ := 0 + tgt _ := 1 + site := Empty.elim + Constraint _ _ α := α 0 = α 1 + constraint_congr v _ _ α β _ h hα := by + have h' : ∀ e, α e = β e := fun e => h e (by fin_cases v <;> simp) + rw [← h' 0, ← h' 1] + exact hα + +/-- The indicator tensor network of `agree` counts its two satisfying assignments. -/ +example : (agree.toTensorNetwork ℕ Empty.elim).contraction = 2 := by + rw [Network.contraction_toTensorNetwork, Nat.cast_id] + have hsat : {α | agree.Satisfies Empty.elim α} = {fun _ => false, fun _ => true} := by + ext α + simp only [Network.Satisfies, agree, Set.mem_ofPred_eq, forall_const, Set.mem_insert_iff, + Set.mem_singleton_iff, funext_iff, Fin.forall_fin_two] + cases α 0 <;> cases α 1 <;> simp + rw [hsat, Set.ncard_pair (fun h => Bool.false_ne_true (congrFun h 0))] + +end ComplexityTests.Computability.Circuit.Frontier.TensorNetwork From b06c2112f2badd9381e157200e2880137e5a13db Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:19:33 -0400 Subject: [PATCH 2/5] refactor(circuit/frontier): index explicit tables by BitString.lsbValue Address the #1844 review: replace the duplicate public `tableIndex` encoding and its lemmas by the existing `Cslib.BitString.lsbValue` and `lsbValue_lt`. Add the missing digit lemma `BitString.testBit_lsbValue` next to `lsbValue` in `BitString/Counter.lean`, and update the table lookup, its proof and the tests. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Frontier/TensorNetwork/Explicit.lean | 37 ++++++------------- .../Foundations/Data/BitString/Counter.lean | 11 ++++++ .../Circuit/Frontier/TensorNetwork.lean | 2 +- 3 files changed, 23 insertions(+), 27 deletions(-) diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean index 28f5dd3f5..051a95b90 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Computability.Circuit.Frontier.TensorNetwork +public import Complexity.Foundations.Data.BitString.Counter import Mathlib.Algebra.BigOperators.Fin import Mathlib.Data.List.GetD @@ -19,7 +20,8 @@ the number of edges, numbered `0, 1, …`, and a list of vertices, each given by * its ordered list of *ports*, the numbers of the edges at the vertex, and * its *table*: the value of its tensor when port `i` carries the bit `bs[i]` is the entry at - position `tableIndex bs`, the number whose binary digit `i` is `bs[i]`. + position `BitString.lsbValue bs`, the number whose binary digit `i` is `bs[i]` + (`BitString.testBit_lsbValue`). So a vertex with `k` ports has a table of `2 ^ k` entries. The contraction of an explicit network (`ExplicitTensorNetwork.contraction`) sums, over all assignments of bits to the edges, the product @@ -37,7 +39,6 @@ order and tabulate its tensor on them. The contraction is unchanged ## Main definitions -* `Cslib.Circuits.Frontier.tableIndex`: the position of a list of bits in a table. * `Cslib.Circuits.Frontier.ExplicitTensorNetwork`: an explicit Boolean tensor network. * `Cslib.Circuits.Frontier.ExplicitTensorNetwork.entry`, `Cslib.Circuits.Frontier.ExplicitTensorNetwork.portBits`: table lookup and the bits on a list @@ -51,8 +52,6 @@ order and tabulate its tensor on them. The contraction is unchanged ## Main results -* `Cslib.Circuits.Frontier.testBit_tableIndex`, `Cslib.Circuits.Frontier.tableIndex_lt`: the - digits and range of a table position. * `Cslib.Circuits.Frontier.ExplicitTensorNetwork.maxDegree_le_iff`: the degree bound. * `Cslib.Circuits.Frontier.TensorNetwork.entry_explicitTable`: a written-out table evaluates the tensor. @@ -68,24 +67,10 @@ order and tabulate its tensor on them. The contraction is unchanged namespace Cslib.Circuits.Frontier -/-- The position of a list of bits in a table: the number whose binary digit `i` is `bs[i]`, so -that the bits are read little-endian. -/ -def tableIndex (bs : List Bool) : ℕ := - (BitVec.ofBoolListLE bs).toNat - -/-- Binary digit `i` of the position of `bs` is `bs[i]`, or `false` past the end of `bs`. -/ -@[simp] theorem testBit_tableIndex (bs : List Bool) (i : ℕ) : - (tableIndex bs).testBit i = bs.getD i false := by - rw [tableIndex, BitVec.testBit_toNat, BitVec.getLsbD_ofBoolListLE] - -/-- A list of `k` bits has a position below `2 ^ k`. -/ -theorem tableIndex_lt (bs : List Bool) : tableIndex bs < 2 ^ bs.length := - BitVec.isLt _ - /-- An *explicit Boolean tensor network* over `R`: the number of edges, numbered from zero, and a list of vertices. A vertex is given by its ordered list of *ports*, the numbers of its edges, and -its *table*, whose entry at position `tableIndex bs` is the value of its tensor when port `i` -carries the bit `bs[i]`. -/ +its *table*, whose entry at position `BitString.lsbValue bs` is the value of its tensor when +port `i` carries the bit `bs[i]`. -/ structure ExplicitTensorNetwork (R : Type*) where /-- The number of edges; the edges are numbered `0, …, numEdges - 1`. -/ numEdges : ℕ @@ -96,10 +81,10 @@ namespace ExplicitTensorNetwork variable {R : Type*} (d : ExplicitTensorNetwork R) -/-- The entry of a table at a list of bits. A position past the end of the table has entry -zero. -/ +/-- The entry of a table at a list of bits, read little-endian (`BitString.lsbValue`). A position +past the end of the table has entry zero. -/ def entry [Zero R] (table : List R) (bs : List Bool) : R := - table.getD (tableIndex bs) 0 + table.getD (BitString.lsbValue bs) 0 /-- The bits on a list of ports under an assignment of bits to the edges. A port naming no edge reads `false`. -/ @@ -168,14 +153,14 @@ theorem entry_explicitTable [Zero R] (v : V) (x : Fin m → Bool) : ExplicitTensorNetwork.entry (N.explicitTable ee v) ((N.explicitPorts ee v).map x) = N.tensor v (x ∘ ee) := by set ps := N.explicitPorts ee v - have hlt : tableIndex (ps.map x) < (N.explicitTable ee v).length := by - simpa [explicitTable, ps] using tableIndex_lt (ps.map x) + have hlt : BitString.lsbValue (ps.map x) < (N.explicitTable ee v).length := by + simpa [explicitTable, ps] using BitString.lsbValue_lt (ps.map x) rw [ExplicitTensorNetwork.entry, List.getD_eq_getElem _ _ hlt] simp only [explicitTable, List.getElem_map, List.getElem_range] refine N.tensor_congr v _ _ fun e he => ?_ have hmem : ee e ∈ ps := (N.mem_explicitPorts ee).mpr (by simpa using he) have hidx := List.idxOf_lt_length_of_mem hmem - rw [testBit_tableIndex, List.getD_eq_getElem _ _ (by simpa using hidx), List.getElem_map, + rw [BitString.testBit_lsbValue, List.getD_eq_getElem _ _ (by simpa using hidx), List.getElem_map, List.getElem_idxOf hidx, Function.comp_apply] /-- A Boolean tensor network on finite types written out as an explicit network, numbering the diff --git a/Complexity/Foundations/Data/BitString/Counter.lean b/Complexity/Foundations/Data/BitString/Counter.lean index d13e8137f..40319f05b 100644 --- a/Complexity/Foundations/Data/BitString/Counter.lean +++ b/Complexity/Foundations/Data/BitString/Counter.lean @@ -35,6 +35,7 @@ their candidates in this way, storing only the current one. * `Cslib.BitString.iterate_increment`, `Cslib.BitString.iterate_increment_lsbValue`: counting from zero enumerates the words of a length. * `Cslib.BitString.lsbValue_eq_foldr_bit`: `lsbValue` is a right fold of `Nat.bit`. +* `Cslib.BitString.testBit_lsbValue`: binary digit `i` of `lsbValue w` is the bit `w[i]`. -/ @[expose] public section @@ -154,4 +155,14 @@ theorem lsbValue_eq_foldr_bit (w : List Bool) : lsbValue w = w.foldr Nat.bit 0 : | nil => rfl | cons b w ih => rw [lsbValue, List.foldr_cons, ← ih, Nat.bit_val, Nat.add_comm] +/-- Binary digit `i` of the value of a word is its bit `i`, or `false` past its end. -/ +@[simp] theorem testBit_lsbValue : ∀ (w : List Bool) (i : ℕ), + (lsbValue w).testBit i = w.getD i false + | [], _ => by simp [lsbValue] + | b :: w, i => by + rw [lsbValue_eq_foldr_bit, List.foldr_cons, ← lsbValue_eq_foldr_bit] + cases i with + | zero => simp + | succ i => simp [Nat.testBit_bit_succ, testBit_lsbValue w i] + end Cslib.BitString diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean index 5be31a11e..27d867afd 100644 --- a/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean @@ -60,7 +60,7 @@ example : (cycle neTable).contraction = 0 := by decide /-- The table `A` or `B` of `parallel` as a tensor on assignments to `Fin 2`. -/ def table (v : Fin 2) (x : Fin 2 → Bool) : ℤ := - [[1, 2, 3, 4], [5, 6, 7, 8]][v]!.getD (tableIndex [x 0, x 1]) 0 + [[1, 2, 3, 4], [5, 6, 7, 8]][v]!.getD (Cslib.BitString.lsbValue [x 0, x 1]) 0 /-- The network `parallel` on `Fin 2` vertices and `Fin 2` edges, both edges from `0` to `1`. Every edge is at both vertices, so the tensors are trivially local. -/ From 120ab9a15e167825a46fb1359ae718c47e29fdf3 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:33:16 -0400 Subject: [PATCH 3/5] feat(circuit/frontier): direct-summation contraction modulo 2^P Contract an explicit Boolean tensor network over the naturals modulo 2^P by streaming over all 2^m edge assignments with BooleanFold: the leaf and small-size case of Theorem D.1 of the ETH manuscript (D.4.2 p. 58, D.4.7 p. 64) and the fallback of the contraction contract. Fix the rows-first input encoding (P unary, r binary, network with its edge count in unary), prove directContraction (P, r, d) = d.contraction % 2^P on every input, give plain polynomial-time certificates for the weight and one loop step, and build the native certificate. Explicit 2^m * poly time and polynomial space bounds remain to be extracted. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../TensorNetwork/DirectContraction.lean | 328 ++++++++++++++++++ .../Foundations/Data/BitString/Binary.lean | 11 + .../Circuit/Frontier/DirectContraction.lean | 61 ++++ 4 files changed, 401 insertions(+) create mode 100644 Complexity/Computability/Circuit/Frontier/TensorNetwork/DirectContraction.lean create mode 100644 ComplexityTests/Computability/Circuit/Frontier/DirectContraction.lean diff --git a/Complexity.lean b/Complexity.lean index 3e53d5172..d49a760db 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -859,6 +859,7 @@ public import Complexity.Computability.Circuit.Frontier.Reduction 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.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..e47c1d6f8 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DirectContraction.lean @@ -0,0 +1,328 @@ +/- +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.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.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. + +## 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`. + +## 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. + +**Status.** `directContractionCertificate` is a native certificate, but its explicit bounds, +`2 ^ m` times a polynomial in time and a polynomial in space on every input, are not yet extracted +(`IndexFold.computableInO`, with `runPrefix_sumStep` bounding the live state). + +## 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 resource +bounds are those of `BooleanFold.certificate`; the explicit `2 ^ m · poly` time and polynomial +space bounds are not yet extracted here. -/ +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)))) + +end Cslib.Circuits.Frontier.ExplicitTensorNetwork 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..d0a659ecf --- /dev/null +++ b/ComplexityTests/Computability/Circuit/Frontier/DirectContraction.lean @@ -0,0 +1,61 @@ +/- +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. +-/ + +@[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 + +end ComplexityTests.Computability.Circuit.Frontier.DirectContraction From 4d59135117561d64df2e314cdd6f4a3cc1af76fd Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:50:18 -0400 Subject: [PATCH 4/5] feat(circuit/frontier): explicit bounds of direct-summation contraction On every input (P, r, d), direct summation runs in polynomial workspace and in time (2^m + 1) times a polynomial in the input length, where m is the number of edges: `directContractionCertificate_bounds`, the one-constant form `exists_directContractionCertificate_le` (time K (n+1)^K 2^m, space K (n+1)^K), and the plain `exists_computableInO_contraction_mod`. The bound proof is shared: `BooleanFold.certificate_bounds` extracts the bounds of any BooleanFold loop from polynomial component certificates and a polynomial bound on the live accumulator. It generalizes the counting-only core of `ExhaustiveCountFallback.countPredicateCertificate_bounds`, which is now a short corollary. `IndexFold.roundCertificate_isPolynomial` moves out of that file, and `BooleanFold.clock_isPolynomial` is new. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../TensorNetwork/DirectContraction.lean | 98 +++++++++++- .../GenericRAM/Native/BooleanFold.lean | 101 +++++++++++- .../Native/ExhaustiveCountFallback.lean | 147 ++---------------- .../GenericRAM/Native/IndexFold.lean | 17 ++ .../Circuit/Frontier/DirectContraction.lean | 14 +- 5 files changed, 234 insertions(+), 143 deletions(-) diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/DirectContraction.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DirectContraction.lean index e47c1d6f8..24befb44a 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/DirectContraction.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DirectContraction.lean @@ -69,10 +69,19 @@ modulo `2 ^ P` and the streamed assignments polynomial in the input length. `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. - -**Status.** `directContractionCertificate` is a native certificate, but its explicit bounds, -`2 ^ m` times a polynomial in time and a polynomial in space on every input, are not yet extracted -(`IndexFold.computableInO`, with `runPrefix_sumStep` bounding the live state). +* `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. + +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`). ## References @@ -315,9 +324,8 @@ theorem initial_polyTime : (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 resource -bounds are those of `BooleanFold.certificate`; the explicit `2 ^ m · poly` time and polynomial -space bounds are not yet extracted here. -/ +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 @@ -325,4 +333,80 @@ noncomputable def directContractionCertificate : (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 + +/-- **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 := by + obtain ⟨hspace, T, hT, htime⟩ := directContractionCertificate_bounds + 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 : ((encContractionInput x).length + 1) ^ dt ≤ + ((encContractionInput x).length + 1) ^ (2 * ct + cs + dt + ds) := + Nat.pow_le_pow_right (Nat.succ_pos _) (by omega) + calc directContractionCertificate.time x + ≤ (2 * 2 ^ x.2.2.numEdges) * (ct * ((encContractionInput x).length + 1) ^ dt) := + (htime x).trans (Nat.mul_le_mul h1 (hct x)) + _ = 2 * ct * ((encContractionInput 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))) + +/-- **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] + 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/ComplexityTests/Computability/Circuit/Frontier/DirectContraction.lean b/ComplexityTests/Computability/Circuit/Frontier/DirectContraction.lean index d0a659ecf..b8d4f6542 100644 --- a/ComplexityTests/Computability/Circuit/Frontier/DirectContraction.lean +++ b/ComplexityTests/Computability/Circuit/Frontier/DirectContraction.lean @@ -14,7 +14,7 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DirectCont 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. +a network without edges. The last test derives the unconditional contract form of the bounds. -/ @[expose] public section @@ -58,4 +58,16 @@ def noEdges : ExplicitTensorNetwork ℕ := 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)) + end ComplexityTests.Computability.Circuit.Frontier.DirectContraction From a96527eae4fb802da1723ca1437937180de85403 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:58:36 -0400 Subject: [PATCH 5/5] feat(circuit/frontier): direct summation with the precision in binary MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The contraction interface of the counting simulation takes the precision P in binary (`encPair encNat encN`). A binary P can be exponentially larger than the input, so it is capped first: the contraction is below 2^|d| for |d| the encoded length of the network (`contraction_lt_two_pow_length`), so reducing modulo 2^(min |d| P) keeps the residue (`contraction_mod_two_pow_min`). `capPrecision` computes the unary capped precision in polynomial time. `directContractionBinaryCertificate` computes `d.contraction % 2 ^ P` on `encPair encNat (encPair encNat encExplicitNetwork)`, with the same bounds on every input: `directContractionBinaryCertificate_bounds` and `exists_directContractionBinaryCertificate_le`. A test checks that its type is the interface's certificate type for `N = ℕ × ExplicitTensorNetwork ℕ`. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../TensorNetwork/DirectContraction.lean | 214 ++++++++++++++++-- .../Circuit/Frontier/DirectContraction.lean | 15 +- 2 files changed, 210 insertions(+), 19 deletions(-) diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/DirectContraction.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DirectContraction.lean index 24befb44a..954c85cb0 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/DirectContraction.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DirectContraction.lean @@ -12,6 +12,9 @@ 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 @@ -20,6 +23,8 @@ import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListP 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 @@ -45,6 +50,11 @@ of its number of edges, in unary, and its list of vertices. Each vertex is the p 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 @@ -56,6 +66,9 @@ modulo `2 ^ P` and the streamed assignments polynomial in the input length. `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 @@ -79,9 +92,17 @@ modulo `2 ^ P` and the streamed assignments polynomial in the input length. 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`). +`Cslib.GenericRAM.BooleanFold.certificate_bounds`) or capped at the input length. ## References @@ -361,35 +382,44 @@ theorem directContractionCertificate_bounds : (NativeCertificate.ofPolyTime_isPolynomial sumStep_polyTime) ((PolyBounded.const 3).mul .self) fun x j _ => length_runPrefix_sumStep_le x j -/-- **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 := by - obtain ⟨hspace, T, hT, htime⟩ := directContractionCertificate_bounds +/-- 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 : ((encContractionInput x).length + 1) ^ dt ≤ - ((encContractionInput x).length + 1) ^ (2 * ct + cs + dt + ds) := + 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 directContractionCertificate.time x - ≤ (2 * 2 ^ x.2.2.numEdges) * (ct * ((encContractionInput x).length + 1) ^ dt) := + 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 * ((encContractionInput x).length + 1) ^ dt * 2 ^ x.2.2.numEdges := by - ac_rfl + _ = 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. -/ @@ -409,4 +439,152 @@ theorem exists_computableInO_contraction_mod : · 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/ComplexityTests/Computability/Circuit/Frontier/DirectContraction.lean b/ComplexityTests/Computability/Circuit/Frontier/DirectContraction.lean index b8d4f6542..e662ad97f 100644 --- a/ComplexityTests/Computability/Circuit/Frontier/DirectContraction.lean +++ b/ComplexityTests/Computability/Circuit/Frontier/DirectContraction.lean @@ -14,7 +14,8 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DirectCont 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 test derives the unconditional contract form of the bounds. +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 @@ -70,4 +71,16 @@ example : ∃ K : ℕ, ∀ x : ℕ × ℕ × ExplicitTensorNetwork ℕ, (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