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/3] 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/3] 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 13a6daeafef1e752435505e47f5329da96b392e6 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:24:25 -0400 Subject: [PATCH 3/3] feat(circuit/frontier): binarize a tensor network by an injective code MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit An injective code `U → (Fin m → Bool)` turns a tensor network over a finite alphabet into a Boolean one on `m` parallel copies of every edge. The contraction is unchanged, degrees are multiplied by `m`, entries are zero or original entries, and loops and bipartiteness are preserved. Used by the HPV block-counting networks of #1833 (H3). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Frontier/TensorNetwork/Binarize.lean | 165 ++++++++++++++++++ .../Frontier/TensorNetworkBinarize.lean | 78 +++++++++ 3 files changed, 244 insertions(+) create mode 100644 Complexity/Computability/Circuit/Frontier/TensorNetwork/Binarize.lean create mode 100644 ComplexityTests/Computability/Circuit/Frontier/TensorNetworkBinarize.lean diff --git a/Complexity.lean b/Complexity.lean index 3e53d5172..d6cce81ba 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -858,6 +858,7 @@ 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.Binarize public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Constraint public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit public import Complexity.Computability.Circuit.Frontier.TwoSidedWitness diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Binarize.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Binarize.lean new file mode 100644 index 000000000..caaca2155 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Binarize.lean @@ -0,0 +1,165 @@ +/- +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 +public import Mathlib.Logic.Function.Basic +import Mathlib.Data.Set.Card + +/-! +# Binarizing a tensor network + +A tensor network whose edges carry letters of a finite alphabet `U` becomes a Boolean tensor +network once every letter is written in `m` bits. Fix an injective *code* +`code : U → (Fin m → Bool)`. The *binarization* `TensorNetwork.binarize` replaces every edge `e` +by the `m` parallel Boolean edges `(e, 0), …, (e, m - 1)` between the same two vertices. A vertex +decodes the `m` bits on each of its edges and evaluates its old tensor on the decoded letters; if +the bits on one of its edges are not the code of any letter, its tensor is zero. + +The contraction is unchanged (`TensorNetwork.contraction_binarize`): assignments of bits in which +every edge carries a code word correspond exactly to assignments of letters, and every other +assignment of bits has an edge with an invalid code word, whose source tensor vanishes. Every edge +becomes `m` edges, so vertex degrees are multiplied by `m` +(`TensorNetwork.maxDegreeLE_binarize`). Every tensor entry of the binarization is zero or an entry +of the original network (`TensorNetwork.tensor_binarize_eq_zero_or`). Loops and bipartiteness are +preserved. + +This lets a construction use a structured alphabet, such as words over a machine's tape alphabet, +and then pass to the Boolean networks of [OpenAI2026ETH], Appendix D. + +## Main definitions + +* `Cslib.Circuits.Frontier.TensorNetwork.binarize`: the binarization by a code. +* `Cslib.Circuits.Frontier.TensorNetwork.bitsOn`: the bits on the copies of an edge. + +## Main results + +* `Cslib.Circuits.Frontier.TensorNetwork.contraction_binarize`: binarization by an injective code + preserves the contraction. +* `Cslib.Circuits.Frontier.TensorNetwork.maxDegreeLE_binarize`: degrees are multiplied by the + code length. +* `Cslib.Circuits.Frontier.TensorNetwork.loopless_binarize`, + `Cslib.Circuits.Frontier.TensorNetwork.isBipartite_binarize`: loops and bipartiteness are + preserved. +* `Cslib.Circuits.Frontier.TensorNetwork.tensor_binarize_eq_zero_or`: binarized entries are zero + or original entries. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Appendix D.1 (p. 53). +-/ + +public section + +namespace Cslib.Circuits.Frontier.TensorNetwork + +open Function + +variable {R U V E : Type*} {m : ℕ} + +/-- The bits on the `m` copies of the edge `e`. -/ +@[expose] def bitsOn (y : E × Fin m → Bool) (e : E) : Fin m → Bool := + fun j => y (e, j) + +@[simp] theorem bitsOn_apply (y : E × Fin m → Bool) (e : E) (j : Fin m) : + bitsOn y e j = y (e, j) := rfl + +variable [Zero R] [Nonempty U] (N : TensorNetwork R U V E) (code : U → Fin m → Bool) + +open Classical in +/-- The *binarization* of a tensor network by a code `code : U → (Fin m → Bool)`. Every edge `e` +becomes the `m` Boolean edges `(e, j)` between the same two vertices. A vertex whose edges all +carry code words evaluates its old tensor on the decoded letters (`Function.invFun code`); a +vertex with an edge carrying a word that is not a code word has tensor zero. -/ +@[expose] noncomputable def binarize : TensorNetwork R Bool V (E × Fin m) where + src p := N.src p.1 + tgt p := N.tgt p.1 + tensor v y := + if ∀ e, N.src e = v ∨ N.tgt e = v → bitsOn y e ∈ Set.range code then + N.tensor v fun e => invFun code (bitsOn y e) + else 0 + tensor_congr v y y' h := by + have hrow : ∀ e, N.src e = v ∨ N.tgt e = v → bitsOn y e = bitsOn y' e := + fun e he => funext fun j => h (e, j) he + have hcond : (∀ e, N.src e = v ∨ N.tgt e = v → bitsOn y e ∈ Set.range code) ↔ + ∀ e, N.src e = v ∨ N.tgt e = v → bitsOn y' e ∈ Set.range code := + forall_congr' fun e => imp_congr_right fun he => by rw [hrow e he] + simp only [hcond] + split_ifs + · exact N.tensor_congr v _ _ fun e he => by rw [hrow e he] + · rfl + +@[simp] theorem binarize_src (p : E × Fin m) : (N.binarize code).src p = N.src p.1 := rfl + +@[simp] theorem binarize_tgt (p : E × Fin m) : (N.binarize code).tgt p = N.tgt p.1 := rfl + +/-- Every tensor entry of the binarization is zero or an entry of the original network at some +assignment of letters. -/ +theorem tensor_binarize_eq_zero_or (v : V) (y : E × Fin m → Bool) : + (N.binarize code).tensor v y = 0 ∨ ∃ x, (N.binarize code).tensor v y = N.tensor v x := by + classical + simp only [binarize] + split_ifs + · exact Or.inr ⟨_, rfl⟩ + · exact Or.inl rfl + +/-- Binarization keeps a network without loops loopless. -/ +theorem loopless_binarize (h : N.Loopless) : (N.binarize code).Loopless := + fun p => h p.1 + +/-- Binarization keeps a network bipartite, with the same sides. -/ +theorem isBipartite_binarize (h : N.IsBipartite) : (N.binarize code).IsBipartite := by + obtain ⟨side, hside⟩ := h + exact ⟨side, fun p => hside p.1⟩ + +/-- The edges at a vertex of the binarization are the copies of its old edges. -/ +theorem incidenceSet_binarize (v : V) : + (N.binarize code).incidenceSet v = N.incidenceSet v ×ˢ Set.univ := by + ext p + simp [Multigraph.mem_incidenceSet] + +/-- **Binarization multiplies degrees by the code length.** -/ +theorem maxDegreeLE_binarize [Finite E] {d : ℕ} (hd : N.MaxDegreeLE d) : + (N.binarize code).MaxDegreeLE (d * m) := by + intro v + rw [incidenceSet_binarize, Set.ncard_prod, Set.ncard_univ, Nat.card_eq_fintype_card, + Fintype.card_fin] + exact Nat.mul_le_mul_right m (hd v) + +/-- **Binarization preserves the contraction.** Assignments of bits in which every edge carries a +code word are the codes of the assignments of letters, and every other assignment of bits has an +edge with an invalid word, at whose source the tensor vanishes. -/ +theorem contraction_binarize {R : Type*} [CommSemiring R] [Fintype U] [Fintype V] [Fintype E] + [DecidableEq E] (N : TensorNetwork R U V E) {code : U → Fin m → Bool} + (hcode : Injective code) : (N.binarize code).contraction = N.contraction := by + classical + symm + refine Fintype.sum_of_injective (fun x p => code (x p.1) p.2) ?_ _ _ ?_ fun x => ?_ + · -- Distinct assignments of letters differ at some edge, so their codes differ there. + intro x x' hxx' + funext e + exact hcode (funext fun j => congrFun hxx' (e, j)) + · -- A word on some edge is not a code word, so the tensor at its source vanishes. + intro y hy + have : ∃ e, bitsOn y e ∉ Set.range code := by + by_contra! hall + exact hy ⟨fun e => invFun code (bitsOn y e), funext fun p => + congrFun (invFun_eq (hall p.1)) p.2⟩ + obtain ⟨e, he⟩ := this + refine Finset.prod_eq_zero (Finset.mem_univ (N.src e)) ?_ + simp only [binarize] + rw [ite_eq_right fun hall => he (hall e (Or.inl rfl))] + · -- On a code word everywhere, every vertex decodes the original assignment. + refine Finset.prod_congr rfl fun v _ => ?_ + simp only [binarize] + rw [ite_eq_left fun e _ => ⟨x e, rfl⟩] + congr 1 + funext e + exact (leftInverse_invFun hcode (x e)).symm + +end Cslib.Circuits.Frontier.TensorNetwork diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkBinarize.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkBinarize.lean new file mode 100644 index 000000000..72f6e28aa --- /dev/null +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkBinarize.lean @@ -0,0 +1,78 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: local-only (test driver) + +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Binarize +public import Mathlib.Data.Fin.VecNotation + +/-! +# Tests for binarized tensor networks + +A network with one edge over the alphabet `Fin 3`, binarized with the two-bit code of each +letter: its contraction is unchanged, the unused word `(true, true)` gets weight zero, a valid +word reads the original tensor, and the degree doubles. +-/ + +@[expose] public section + +namespace ComplexityTests.Computability.Circuit.Frontier.TensorNetworkBinarize + +open Cslib.Circuits.Frontier + +/-- Two vertices joined by one edge carrying a letter of `Fin 3`, with the tensors +`A = (1, 2, 3)` at vertex `0` and `B = (4, 5, 6)` at vertex `1`. -/ +def ternary : TensorNetwork ℕ (Fin 3) (Fin 2) Unit where + src _ := 0 + tgt _ := 1 + tensor v x := ![![1, 2, 3], ![4, 5, 6]] v (x ()) + tensor_congr v x y h := by + rw [h () (by fin_cases v <;> simp)] + +/-- By hand: `Z = 1·4 + 2·5 + 3·6 = 32`. -/ +theorem contraction_ternary : ternary.contraction = 32 := by decide + +/-- The two binary digits of a letter, least significant first. -/ +def code (u : Fin 3) : Fin 2 → Bool := + ![u.val.testBit 0, u.val.testBit 1] + +theorem code_injective : Function.Injective code := by decide + +/-- Binarization keeps the contraction `32`. -/ +example : (ternary.binarize code).contraction = 32 := by + rw [TensorNetwork.contraction_binarize _ code_injective, contraction_ternary] + +/-- The word `(true, true)` codes no letter, so a vertex reading it has weight zero. -/ +example : (ternary.binarize code).tensor 0 (fun _ => true) = 0 := by + have : TensorNetwork.bitsOn (fun _ : Unit × Fin 2 => true) () ∉ Set.range code := by + rintro ⟨u, hu⟩ + have h0 := congrFun hu 0 + have h1 := congrFun hu 1 + revert h0 h1 + fin_cases u <;> decide + simp only [TensorNetwork.binarize] + exact ite_eq_right fun h => this (h () (Or.inl rfl)) + +/-- The word `(false, true)` codes the letter `2`, so vertex `1` reads its entry `6`. -/ +example : (ternary.binarize code).tensor 1 (fun p => p.2 = 1) = 6 := by + have hword : TensorNetwork.bitsOn (fun p : Unit × Fin 2 => decide (p.2 = 1)) () = code 2 := by + funext j + fin_cases j <;> rfl + have hdec : Function.invFun code (code 2) = 2 := + Function.leftInverse_invFun code_injective 2 + simp only [TensorNetwork.binarize] + rw [ite_eq_left fun e _ => ⟨2, by cases e; exact hword.symm⟩] + simp only [ternary, hword, hdec] + rfl + +/-- Each vertex has one edge; after binarization it has two, and the network stays bipartite. -/ +example : (ternary.binarize code).MaxDegreeLE 2 ∧ (ternary.binarize code).IsBipartite := by + refine ⟨ternary.maxDegreeLE_binarize code (d := 1) fun v => ?_, + ternary.isBipartite_binarize code ⟨fun v => v = 0, fun _ => by simp [ternary]⟩⟩ + exact (Set.ncard_le_card _).trans (by simp) + +end ComplexityTests.Computability.Circuit.Frontier.TensorNetworkBinarize