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 ae638974f0c2f9120d89832435883fcb9cdd17ae Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 17:52:13 -0400 Subject: [PATCH 2/3] feat(circuit/frontier): deformed contraction and the Cauchy kernel Start of Theorem D.1 of OpenAI's ETH manuscript (section D.4.3, (D.7)-(D.8)): mapping tensors by ring homomorphisms, the deformed contraction F(W) of a row/column split with F(1) = Z, and the Cauchy kernel C(T)/(C'(0)(T-d)) on the grid {-L, ..., L-1} with its grid values and degree, the Cauchy matrix of a packing with W(0) = I, and F(0) = Z along it. Tracking: #1538 (T2.1), #1833. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Frontier/TensorNetwork/Deformation.lean | 299 ++++++++++++++++++ .../Frontier/TensorNetworkDeformation.lean | 57 ++++ 3 files changed, 357 insertions(+) create mode 100644 Complexity/Computability/Circuit/Frontier/TensorNetwork/Deformation.lean create mode 100644 ComplexityTests/Computability/Circuit/Frontier/TensorNetworkDeformation.lean diff --git a/Complexity.lean b/Complexity.lean index 3e53d5172..8ea2c2b14 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.Deformation 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/Deformation.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Deformation.lean new file mode 100644 index 000000000..c5aa9c025 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Deformation.lean @@ -0,0 +1,299 @@ +/- +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.Data.Matrix.Mul +public import Mathlib.LinearAlgebra.Lagrange +public import Mathlib.Order.Interval.Finset.Defs +public import Mathlib.Data.Int.Interval +import Mathlib.Algebra.BigOperators.Ring.Finset +import Mathlib.Algebra.Polynomial.BigOperators + +/-! +# Deformed contractions and the Cauchy kernel + +This file starts the proof of the Boolean tensor contraction theorem of [OpenAI2026ETH] +(Theorem D.1, §D.1, p. 53) with the deformation of §D.4.3 (p. 59). + +**Deformed contraction** (`TensorNetwork.deformedContraction`). Split the vertices of a Boolean +tensor network into *rows* (`side v = true`) and *columns*. Give each edge `e` a *row bit* `Y e`, +read by the row tensors, and a *column bit* `X e`, read by the column tensors. For a matrix `W` +indexed by the edges, the deformed contraction is + + `F(W) = ∑ X Y, A(Y) B(X) ∏ e, l_{Y e}((W X) e)`, + +where `A` and `B` are the products of the row and column tensors, `l_false z = 1 - z` and +`l_true z = z` (the manuscript's (D.8), with `l₀`, `l₁`). At the identity matrix the product of +the affine factors is the indicator of `X = Y`, so `F(1)` is the contraction +(`TensorNetwork.deformedContraction_one`). Deforming `W` away from the identity lets the +interactions between groups of ports be expanded separately; that expansion is later work. + +**The Cauchy kernel** (`cauchyKernel`). On the grid `S = {-L, …, L - 1}`, with +`C(T) = ∏_{t ∈ S} (T - t)`, the kernel at `d ∈ S` is the polynomial `C(T) / (C'(0) (T - d))` of +(D.7). It is one at `T = 0` when `d = 0` and vanishes at every other grid point +(`eval_zero_cauchyKernel`, `eval_cauchyKernel_of_ne`). The *Cauchy matrix* of a packing of the +edges (`cauchyMatrix`), with entry `cauchyKernel L (slot e' - slot e)` between edges of the same +packet and zero between packets, is therefore the identity at `T = 0` when every edge has its own +slot in its packet (`cauchyMatrix_eval_zero`), and the deformed contraction along it evaluates to +the contraction at zero (`eval_zero_deformedContraction_cauchyMatrix`). + +## Main definitions + +* `Cslib.Circuits.Frontier.TensorNetwork.map`: a tensor network with its tensors mapped by a + ring homomorphism. +* `Cslib.Circuits.Frontier.TensorNetwork.affineFactor`: the affine factors `l_b`. +* `Cslib.Circuits.Frontier.TensorNetwork.deformedContraction`: the deformed contraction `F(W)`. +* `Cslib.Circuits.Frontier.cauchyGrid`, `Cslib.Circuits.Frontier.cauchyKernel`, + `Cslib.Circuits.Frontier.cauchyMatrix`: the grid, the Cauchy kernel and the Cauchy matrix of a + packing. + +## Main results + +* `Cslib.Circuits.Frontier.TensorNetwork.contraction_map`: contraction commutes with ring + homomorphisms, e.g. reduction of integer entries modulo `2 ^ P`. +* `Cslib.Circuits.Frontier.TensorNetwork.deformedContraction_one`: `F(1) = Z`. +* `Cslib.Circuits.Frontier.TensorNetwork.deformedContraction_map`: deformed contraction commutes + with ring homomorphisms. +* `Cslib.Circuits.Frontier.eval_zero_cauchyKernel`, + `Cslib.Circuits.Frontier.eval_cauchyKernel_of_ne`: values of the kernel on the grid. +* `Cslib.Circuits.Frontier.natDegree_cauchyKernel`: its degree `2 L - 1`. +* `Cslib.Circuits.Frontier.cauchyMatrix_eval_zero`: the Cauchy matrix is the identity at zero. +* `Cslib.Circuits.Frontier.TensorNetwork.eval_zero_deformedContraction_cauchyMatrix`: the + polynomial `F(T)` along the Cauchy matrix has value `Z` at `T = 0`. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.3, (D.7)–(D.8), + p. 59. +-/ + +@[expose] public section + +namespace Cslib.Circuits.Frontier + +open Polynomial + +namespace TensorNetwork + +variable {R S U V E : Type*} + +/-! ### Mapping the tensors -/ + +section Map + +variable [CommSemiring R] [CommSemiring S] (f : R →+* S) + +/-- The tensor network with every tensor entry mapped by the ring homomorphism `f`. -/ +def map (N : TensorNetwork R U V E) : TensorNetwork S U V E where + toMultigraph := N.toMultigraph + tensor v x := f (N.tensor v x) + tensor_congr v x y h := by rw [N.tensor_congr v x y h] + +@[simp] theorem map_tensor (N : TensorNetwork R U V E) (v : V) (x : E → U) : + (N.map f).tensor v x = f (N.tensor v x) := + rfl + +@[simp] theorem toMultigraph_map (N : TensorNetwork R U V E) : + (N.map f).toMultigraph = N.toMultigraph := + rfl + +/-- **Contraction commutes with ring homomorphisms.** For instance, contracting integer tensors +and reducing modulo `2 ^ P` is contracting the reduced tensors. -/ +theorem contraction_map [Fintype U] [Fintype V] [Fintype E] [DecidableEq E] + (N : TensorNetwork R U V E) : (N.map f).contraction = f N.contraction := by + simp only [contraction, map_tensor, map_sum, map_prod] + +end Map + +/-! ### Deformed contraction -/ + +section Deformed + +variable [CommRing R] [Fintype V] [Fintype E] [DecidableEq E] + +/-- The affine factor `l_b`: `l_b z = z` for `b = true` and `l_b z = 1 - z` for `b = false`. At a +bit `z`, it is the indicator of `z = b`. -/ +def affineFactor (b : Bool) (z : R) : R := + if b then z else 1 - z + +/-- At a bit, the affine factor is the indicator of equality. -/ +theorem affineFactor_bit (b c : Bool) : + affineFactor b (if c then (1 : R) else 0) = if b = c then 1 else 0 := by + cases b <;> cases c <;> simp [affineFactor] + +/-- The *deformed contraction* of a Boolean tensor network whose vertices are split into rows +(`side v = true`) and columns, along a matrix `W` indexed by the edges: every edge carries a row +bit, read by the row tensors, and a column bit, read by the column tensors, joined through the +affine factors of `W`. -/ +def deformedContraction (N : TensorNetwork R Bool V E) (side : V → Bool) (W : Matrix E E R) : R := + ∑ X : E → Bool, ∑ Y : E → Bool, + (∏ v ∈ Finset.univ.filter (side · = true), N.tensor v Y) * + (∏ v ∈ Finset.univ.filter (side · = false), N.tensor v X) * + ∏ e, affineFactor (Y e) (W.mulVec (fun e' => if X e' then 1 else 0) e) + +/-- **The deformed contraction at the identity is the contraction.** The affine factors of the +identity matrix force the row bits to equal the column bits. -/ +theorem deformedContraction_one (N : TensorNetwork R Bool V E) (side : V → Bool) : + N.deformedContraction side 1 = N.contraction := by + classical + simp only [deformedContraction, Matrix.one_mulVec, affineFactor_bit, Fintype.prod_boole, + ← funext_iff, mul_ite, mul_one, mul_zero, Finset.sum_ite_eq', Finset.mem_univ, ite_true] + refine Finset.sum_congr rfl fun X _ => ?_ + have h := Finset.prod_filter_mul_prod_filter_not Finset.univ (fun v => side v = true) + (fun v => N.tensor v X) + simp only [Bool.not_eq_true] at h + exact h + +/-- Deformed contraction commutes with ring homomorphisms. -/ +theorem deformedContraction_map {S : Type*} [CommRing S] (f : R →+* S) + (N : TensorNetwork R Bool V E) (side : V → Bool) (W : Matrix E E R) : + (N.map f).deformedContraction side (W.map f) = f (N.deformedContraction side W) := by + simp only [deformedContraction, map_sum, map_mul, map_prod, map_tensor] + refine Finset.sum_congr rfl fun X _ => Finset.sum_congr rfl fun Y _ => ?_ + congr 1 + refine Finset.prod_congr rfl fun e _ => ?_ + have hv : (W.map f).mulVec (fun e' => if X e' then (1 : S) else 0) = + fun e => f (W.mulVec (fun e' => if X e' then (1 : R) else 0) e) := by + ext e + simp only [Matrix.mulVec, dotProduct, Matrix.map_apply, map_sum, map_mul, apply_ite f, + map_one, map_zero] + rw [hv] + cases Y e <;> simp [affineFactor] + +end Deformed + +end TensorNetwork + +/-! ### The Cauchy kernel -/ + +/-- The interpolation grid `S = {-L, …, L - 1}` of a packet with `L` slots. -/ +def cauchyGrid (L : ℕ) : Finset ℤ := + Finset.Ico (-L : ℤ) L + +theorem mem_cauchyGrid {L : ℕ} {t : ℤ} : t ∈ cauchyGrid L ↔ -(L : ℤ) ≤ t ∧ t < L := + Finset.mem_Ico + +/-- The difference of two slots of a packet lies on the grid. -/ +theorem sub_mem_cauchyGrid {L : ℕ} {x y : ℕ} (hx : x < L) (hy : y < L) : + (y : ℤ) - x ∈ cauchyGrid L := by + rw [mem_cauchyGrid] + omega + +/-- The *Cauchy kernel* at `d` on the grid of `L` slots: `C(T) / (C'(0) (T - d))`, where +`C(T) = ∏_{t ∈ S} (T - t)`. For `d ∈ S` it is the polynomial `C'(0)⁻¹ ∏_{t ∈ S, t ≠ d} (T - t)` +of degree `2 L - 1`; here `C'(0) = ∏_{t ∈ S, t ≠ 0} (0 - t)`. -/ +noncomputable def cauchyKernel (L : ℕ) (d : ℤ) : ℚ[X] := + C ((Lagrange.nodal ((cauchyGrid L).erase 0) (Int.cast : ℤ → ℚ)).eval 0)⁻¹ * + Lagrange.nodal ((cauchyGrid L).erase d) (Int.cast : ℤ → ℚ) + +/-- The normalization is `C'(0)`, the derivative of `C(T) = ∏_{t ∈ S} (T - t)` at zero. -/ +theorem eval_zero_nodal_erase_zero {L : ℕ} (hL : 0 < L) : + (Lagrange.nodal ((cauchyGrid L).erase 0) (Int.cast : ℤ → ℚ)).eval 0 = + (derivative (Lagrange.nodal (cauchyGrid L) (Int.cast : ℤ → ℚ))).eval 0 := by + have h0 : (0 : ℤ) ∈ cauchyGrid L := by rw [mem_cauchyGrid]; omega + have := Lagrange.eval_nodal_derivative_eval_node_eq (v := (Int.cast : ℤ → ℚ)) h0 + simpa using this.symm + +/-- `C'(0)` is nonzero: the grid has distinct points. -/ +theorem eval_zero_nodal_erase_zero_ne_zero (L : ℕ) : + (Lagrange.nodal ((cauchyGrid L).erase 0) (Int.cast : ℤ → ℚ)).eval 0 ≠ 0 := by + rw [Lagrange.eval_nodal, Finset.prod_ne_zero_iff] + intro t ht + have : t ≠ 0 := Finset.ne_of_mem_erase ht + simpa [sub_eq_zero, eq_comm] using this + +/-- On the grid, the kernel has degree `2 L - 1`, so a deformed contraction along a Cauchy matrix +has degree at most `M (2 L - 1)` in `T` for `M` edges. -/ +theorem natDegree_cauchyKernel {L : ℕ} {d : ℤ} (hd : d ∈ cauchyGrid L) : + (cauchyKernel L d).natDegree = 2 * L - 1 := by + rw [cauchyKernel, natDegree_C_mul (inv_ne_zero (eval_zero_nodal_erase_zero_ne_zero L)), + Lagrange.natDegree_nodal, Finset.card_erase_of_mem hd, cauchyGrid, Int.card_Ico] + omega + +/-- **The kernel at zero.** The kernel at `d = 0` is one at `T = 0`. -/ +theorem eval_zero_cauchyKernel_zero (L : ℕ) : (cauchyKernel L 0).eval 0 = 1 := by + rw [cauchyKernel, eval_mul, eval_C] + exact inv_mul_cancel₀ (eval_zero_nodal_erase_zero_ne_zero L) + +/-- **The kernel vanishes at the other grid points.** The kernel at `d` vanishes at every grid +point `t ≠ d`. -/ +theorem eval_cauchyKernel_of_ne {L : ℕ} {d t : ℤ} (ht : t ∈ cauchyGrid L) (htd : t ≠ d) : + (cauchyKernel L d).eval (t : ℚ) = 0 := by + rw [cauchyKernel, eval_mul, Lagrange.eval_nodal_at_node (Finset.mem_erase.mpr ⟨htd, ht⟩), + mul_zero] + +/-- The values of the kernel at `T = 0`: one at `d = 0`, and zero at every `d ≠ 0`, because then +`T = 0` is a root of one of its factors. -/ +theorem eval_zero_cauchyKernel {L : ℕ} (hL : 0 < L) (d : ℤ) : + (cauchyKernel L d).eval 0 = if d = 0 then 1 else 0 := by + split_ifs with h + · rw [h, eval_zero_cauchyKernel_zero] + · have h0 : (0 : ℤ) ∈ cauchyGrid L := by rw [mem_cauchyGrid]; omega + simpa using eval_cauchyKernel_of_ne h0 (Ne.symm h) + +/-- The *Cauchy matrix* of a packing of the edges into packets of `L` slots: between edges `e` +and `e'` of the same packet, the Cauchy kernel at the difference `slot e' - slot e` of their +slots; zero between different packets (the manuscript's (D.7)). -/ +noncomputable def cauchyMatrix {E P : Type*} [DecidableEq P] (L : ℕ) (packet : E → P) + (slot : E → ℕ) : Matrix E E ℚ[X] := + fun e e' => if packet e = packet e' then cauchyKernel L ((slot e' : ℤ) - slot e) else 0 + +/-- **The Cauchy matrix is the identity at zero** when every edge has its own slot in its packet, +below `L`. -/ +theorem cauchyMatrix_eval_zero {E P : Type*} [DecidableEq E] [DecidableEq P] {L : ℕ} + {packet : E → P} {slot : E → ℕ} (hslot : ∀ e, slot e < L) + (hinj : ∀ e e', packet e = packet e' → slot e = slot e' → e = e') : + (cauchyMatrix L packet slot).map (eval 0) = 1 := by + ext e e' + have hL : 0 < L := lt_of_le_of_lt (Nat.zero_le _) (hslot e) + simp only [Matrix.map_apply, cauchyMatrix, Matrix.one_apply] + split_ifs with hp he he + · subst he; simp [eval_zero_cauchyKernel_zero] + · rw [eval_zero_cauchyKernel hL, ite_eq_right] + intro h + exact he (hinj e e' hp (by omega)) + · subst he; exact absurd rfl hp + · exact eval_zero + +namespace TensorNetwork + +variable {R V E P : Type*} [CommRing R] [Algebra ℚ R] [Fintype V] [Fintype E] [DecidableEq E] + [DecidableEq P] + +/-- **The deformation along the Cauchy matrix starts at the contraction.** Over a `ℚ`-algebra, +the deformed contraction along the Cauchy matrix of a packing is a polynomial `F(T)` whose value at +`T = 0` is the contraction, when every edge has its own slot in its packet. -/ +theorem eval_zero_deformedContraction_cauchyMatrix (N : TensorNetwork R Bool V E) + (side : V → Bool) {L : ℕ} {packet : E → P} {slot : E → ℕ} (hslot : ∀ e, slot e < L) + (hinj : ∀ e e', packet e = packet e' → slot e = slot e' → e = e') : + ((N.map Polynomial.C).deformedContraction side + ((cauchyMatrix L packet slot).map (Polynomial.mapRingHom (algebraMap ℚ R)))).eval 0 = + N.contraction := by + have h := deformedContraction_map (Polynomial.evalRingHom (0 : R)) (N.map Polynomial.C) side + ((cauchyMatrix L packet slot).map (Polynomial.mapRingHom (algebraMap ℚ R))) + rw [coe_evalRingHom] at h + rw [← h] + have hN : (N.map Polynomial.C).map (Polynomial.evalRingHom (0 : R)) = N := by + cases N + simp [map] + have hW : ((cauchyMatrix L packet slot).map (Polynomial.mapRingHom (algebraMap ℚ R))).map + (eval 0) = 1 := by + rw [Matrix.map_map] + have : (eval (0 : R) ∘ ⇑(Polynomial.mapRingHom (algebraMap ℚ R))) = + (algebraMap ℚ R) ∘ (eval 0) := by + ext p + simp only [Function.comp_apply, coe_mapRingHom, eval_map, eval₂_at_zero, + coeff_zero_eq_eval_zero] + rw [this, ← Matrix.map_map, cauchyMatrix_eval_zero hslot hinj, + Matrix.map_one _ (map_zero _) (map_one _)] + rw [hN, hW, deformedContraction_one] + +end TensorNetwork + +end Cslib.Circuits.Frontier diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkDeformation.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkDeformation.lean new file mode 100644 index 000000000..1f1322b39 --- /dev/null +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkDeformation.lean @@ -0,0 +1,57 @@ +/- +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.Deformation + +/-! +# Tests for deformed contractions and the Cauchy kernel + +A one-edge network deformed along a `1 × 1` matrix, checked by hand against the expansion of +`F(W)`, and the Cauchy kernel of a packet with one slot, `C(T) = T (T + 1)`. +-/ + +@[expose] public section + +namespace ComplexityTests.Computability.Circuit.Frontier.TensorNetwork.Deformation + +open Cslib.Circuits.Frontier Polynomial + +/-- A row vertex `0` and a column vertex `1` joined by one edge, with tensors `A = (1, 2)` and +`B = (3, 5)` on its bit. -/ +def oneEdge : TensorNetwork ℤ Bool (Fin 2) (Fin 1) where + src _ := 0 + tgt _ := 1 + tensor v x := if v = 0 then (if x 0 then 2 else 1) else (if x 0 then 5 else 3) + tensor_congr v x y h := by rw [h 0 (by fin_cases v <;> simp)] + +/-- The rows: vertex `0`. -/ +def side (v : Fin 2) : Bool := v = 0 + +/-- By hand, `F(w) = A₀B₀ + A₀B₁ (1 - w) + A₁B₁ w`; at `w = 2` this is `3 - 5 + 20 = 18`. -/ +example : oneEdge.deformedContraction side (fun _ _ => 2) = 18 := by decide + +/-- At `w = 1` it is the contraction `A₀B₀ + A₁B₁ = 13`. -/ +example : oneEdge.deformedContraction side 1 = 13 ∧ oneEdge.contraction = 13 := by decide + +/-- Contraction commutes with reduction modulo `8`: `13 ≡ 5`. -/ +example : (oneEdge.map (Int.castRingHom (ZMod 8))).contraction = 5 := by + rw [TensorNetwork.contraction_map] + decide + +/-- With one slot the grid is `{-1, 0}`, `C'(0) = 1`, and the kernel at `-1` is `T`, whose value +at `T = 1` is `1`; the kernel at `0` is `T + 1`. -/ +example : (cauchyKernel 1 (-1)).eval 1 = 1 ∧ (cauchyKernel 1 0).eval 1 = 2 := by + have hS : cauchyGrid 1 = {-1, 0} := by decide + have h0 : ({-1, 0} : Finset ℤ).erase 0 = {-1} := by decide + have h1 : ({-1, 0} : Finset ℤ).erase (-1) = {0} := by decide + simp only [cauchyKernel, hS, h0, h1, eval_mul, eval_C, Lagrange.eval_nodal, + Finset.prod_singleton] + norm_num + +end ComplexityTests.Computability.Circuit.Frontier.TensorNetwork.Deformation From b06c2112f2badd9381e157200e2880137e5a13db Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:19:33 -0400 Subject: [PATCH 3/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. -/