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/4] 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/4] 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/4] 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 adeeddc47d7dce6dc8f3da3a1866df592de1c22d Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 19:10:47 -0400 Subject: [PATCH 4/4] feat(circuit/frontier): mode expansion and the child identity (D.16) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A mode splitting of a matrix W sorts the vertices of a row-to-column Boolean tensor network into groups and its edges into packets, and splits every entry of W into a local part and a sum over modes. Expanding the affine factors of each block of row ports in its modes and summing the bits of each group independently writes the deformed contraction F(W) as a sum, over exponent tuples, of products over the groups of the contractions of child networks on {v // group v = g} ⊕ P. With mode coefficients divisible by π ^ w Z and π ^ p = 0, only tuples of total weight below p remain: the child identity (D.16) of OpenAI2026ETH, §D.4.5–§D.4.6, pp. 62–63. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Frontier/TensorNetwork/ModeExpansion.lean | 684 ++++++++++++++++++ .../Frontier/TensorNetworkModeExpansion.lean | 103 +++ 3 files changed, 788 insertions(+) create mode 100644 Complexity/Computability/Circuit/Frontier/TensorNetwork/ModeExpansion.lean create mode 100644 ComplexityTests/Computability/Circuit/Frontier/TensorNetworkModeExpansion.lean diff --git a/Complexity.lean b/Complexity.lean index 8ea2c2b14..72282f4bf 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -861,6 +861,7 @@ 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.TensorNetwork.ModeExpansion 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/ModeExpansion.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ModeExpansion.lean new file mode 100644 index 000000000..422460a8e --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ModeExpansion.lean @@ -0,0 +1,684 @@ +/- +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.Deformation +public import Mathlib.Data.Fintype.Option +import Mathlib.Algebra.BigOperators.Ring.Finset +import Mathlib.Data.Fintype.BigOperators + +/-! +# Modes and the child networks of a deformed contraction + +This file proves the child identity (D.16) of [OpenAI2026ETH] (§D.4.5–§D.4.6, pp. 62–63), the +step of the proof of the Boolean tensor contraction theorem (Theorem D.1) that turns one +deformed contraction into a sum of products of smaller contractions. + +**Setting.** Let `N` be a Boolean tensor network whose edges run from *rows* (their sources) to +*columns* (their targets), and let `W` be a matrix indexed by the edges. The deformed contraction +(`TensorNetwork.deformedContraction`, the manuscript's (D.8)) is + + `F(W) = ∑ X Y, A(Y) B(X) ∏ e, l_{Y e}((W X) e)`. + +A *mode splitting* (`TensorNetwork.ModeSplitting`) sorts the vertices on both sides into +*groups* and the edges into *packets*, and splits every entry of `W` as + + `W e e' = localPart e e' + ∑ Z, coeff e Z * form Z e'`, + +where the local part only joins a row port to a column port of the same packet and group, and +each *mode* `Z` has a packet, a *target* group, whose row ports carry its coefficients, and a +*source* group, whose column ports its linear form `L_Z(X) = ∑ e', form Z e' X e'` reads. In the +manuscript the modes are the terms of the geometric expansion (D.12) of the crossing entries of +the Cauchy matrix; here they are arbitrary. + +**Mode expansion.** Each affine factor `l_{Y e}((W X) e)` is affine in the mode values, so the +product of the affine factors of the row ports of one packet and group (a *block*) expands as a +polynomial in the modes targeted at that block. Its coefficient at the exponents `β` +(`ModeSplitting.blockCoeff`) sums, over the ways to pick the local term or one mode in each +factor with the multiplicities `β`, the product of the picked coefficients. + +**Children** (`ModeSplitting.child`). For a tuple of exponents `β` and a group `g`, the child +network has the vertices of group `g` from both sides of `N`, with their tensors, and one new +vertex per packet. Its edges are the ports of group `g`: an edge from the row of `e` to the packet +of `e` for each row port `e` of group `g`, carrying the row bit `Y e`, and one from the column of +`e` to the packet of `e` for each column port of group `g`, carrying the column bit `X e`. The +tensor at a packet (`ModeSplitting.packetTensor`) is the coefficient at `β` for that packet and +group times `∏ L_Z(X) ^ β Z` over the modes of that packet with source `g`. So children are +tensor networks on `{v // group v = g} ⊕ P`, bipartite with the old vertices as rows +(`ModeSplitting.isBipartite_child`). + +**The child identity** (`ModeSplitting.deformedContraction_eq_sum_prod_contraction_child`, the +manuscript's (D.16)). If the coefficient of each mode `Z` is divisible by `π ^ w Z` with +`w Z ≥ 1`, and `π ^ p = 0`, then + + `F(W) = ∑ β ∈ modeBudget w p, ∏ g, Z_{g, β}`, + +where `Z_{g, β}` is the contraction of the child of group `g` and `modeBudget w p` is the set of +tuples with `∑ Z, w Z * β Z < p` (the manuscript's (D.14)). The manuscript works modulo `2 ^ p_t` +with `π = 2` and `w Z = b + 1`; here the ring itself has `π ^ p = 0`, as in `A / 2 ^ p_t`, and a +congruence in a larger ring follows by mapping to its quotient +(`TensorNetwork.deformedContraction_map`). Without truncation, the same expansion gives +`F(W) = ∑ β, ∏ g, Z_{g, β}` over all tuples with entries at most the number of edges, in every +commutative ring (`ModeSplitting.deformedContraction_eq_sum_prod_contraction_child_of_le`). + +The proof is the manuscript's: distribute the product of the affine factors over the blocks, +expand each block in its modes, substitute the mode values, and sum the bits of each group +independently. The construction of the modes from the Cauchy kernel ((D.12)–(D.13)), the count +(D.15) of the tuples, and the size bounds on the children are separate steps. + +## Main definitions + +* `TensorNetwork.affineSign`: the sign of the variable part of an affine factor. +* `TensorNetwork.ModeSplitting`: groups, packets, and the splitting of a matrix into a local part + and modes. +* `TensorNetwork.modeBudget`: the tuples of exponents of total weight below `p`. +* `TensorNetwork.ModeSplitting.blockCoeff`: the coefficient of a mode monomial in the product of + the affine factors of a block. +* `TensorNetwork.ModeSplitting.packetTensor`: the tensor at a packet vertex of a child. +* `TensorNetwork.ModeSplitting.child`: the child network of a group. + +## Main results + +* `TensorNetwork.affineFactor_add`: `l_b (u + w) = l_b u ± w`. +* `TensorNetwork.mem_modeBudget`: membership in the budget. +* `TensorNetwork.ModeSplitting.packetTensor_congr`: a packet tensor reads only the ports of its + packet and group. +* `TensorNetwork.ModeSplitting.pow_dvd_blockCoeff`: the coefficient of a mode monomial is + divisible by `π` to its total weight. +* `TensorNetwork.ModeSplitting.isBipartite_child`, `TensorNetwork.ModeSplitting.card_edges_child`: + children are bipartite, with one edge per port of their group. +* `TensorNetwork.ModeSplitting.deformedContraction_eq_sum_prod_contraction_child_of_le`: the + exact expansion of `F(W)` into children. +* `TensorNetwork.ModeSplitting.deformedContraction_eq_sum_prod_contraction_child`: the child + identity (D.16). + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.5–§D.4.6, + (D.14) and (D.16), pp. 62–63. +-/ + +public section + +namespace Cslib.Circuits.Frontier + +open Finset + +namespace TensorNetwork + +variable {R V E : Type*} [CommRing R] + +/-! ### Affine factors of a sum -/ + +/-- The sign of the variable part of an affine factor: `affineSign true = 1` and +`affineSign false = -1`, so that `l_b (u + w) = l_b u + affineSign b * w`. -/ +@[expose] def affineSign (b : Bool) : R := + if b then 1 else -1 + +/-- An affine factor of a sum: `l_b (u + w) = l_b u + affineSign b * w`. -/ +theorem affineFactor_add (b : Bool) (u w : R) : + affineFactor b (u + w) = affineFactor b u + affineSign b * w := by + cases b <;> simp only [affineFactor, affineSign, Bool.false_eq_true, ite_false, ite_true] <;> + ring + +/-! ### Mode splittings -/ + +/-- A *mode splitting* (§D.4.5 of [OpenAI2026ETH]) of the deformed contraction of a Boolean tensor +network `N` along a matrix `W`. The rows of `N` (`side v = true`) are the sources of its edges and +the columns their targets. The vertices on both sides are sorted into *groups* and the edges into +*packets*, and every entry of `W` splits into a *local part*, which joins a row port to a column +port of the same packet and group, and a sum over the *modes* `Z`, each contributing +`coeff e Z * form Z e'`. A mode has a packet, a *target* group, the only row ports of its packet +whose forms contain it, and a *source* group, the only column ports of its packet that its linear +form reads. -/ +structure ModeSplitting (N : TensorNetwork R Bool V E) (W : Matrix E E R) (G P M : Type*) + [Fintype M] where + /-- The side of a vertex: `true` for rows, `false` for columns. -/ + side : V → Bool + /-- The group of a vertex. -/ + group : V → G + /-- The packet of an edge. -/ + packet : E → P + /-- The local part of the matrix. -/ + localPart : Matrix E E R + /-- The packet of a mode. -/ + modePacket : M → P + /-- The source group of a mode: its form reads the column ports of this group. -/ + source : M → G + /-- The target group of a mode: it occurs in the forms of the row ports of this group. -/ + target : M → G + /-- The coefficient of a mode in the form of a row port. -/ + coeff : E → M → R + /-- The linear form in the column bits that a mode stands for. -/ + form : M → E → R + /-- Edges start at rows. -/ + side_src : ∀ e, side (N.src e) = true + /-- Edges end at columns. -/ + side_tgt : ∀ e, side (N.tgt e) = false + /-- The splitting of the matrix. -/ + apply_eq : ∀ e e', W e e' = localPart e e' + ∑ Z, coeff e Z * form Z e' + /-- The local part joins ports of the same packet and group. -/ + localPart_ne_zero : ∀ e e', localPart e e' ≠ 0 → + packet e' = packet e ∧ group (N.tgt e') = group (N.src e) + /-- A mode occurs only in the forms of the row ports of its packet and target group. -/ + coeff_ne_zero : ∀ e Z, coeff e Z ≠ 0 → modePacket Z = packet e ∧ target Z = group (N.src e) + /-- A mode reads only the column ports of its packet and source group. -/ + form_ne_zero : ∀ Z e, form Z e ≠ 0 → modePacket Z = packet e ∧ source Z = group (N.tgt e) + +/-- The tuples of exponents `β` of total weight `∑ Z, w Z * β Z` below `p`, the index set of the +manuscript's (D.14). -/ +@[expose] def modeBudget {M : Type*} [Fintype M] [DecidableEq M] (w : M → ℕ) (p : ℕ) : + Finset (M → ℕ) := + {β ∈ Fintype.piFinset fun _ => range p | ∑ Z, w Z * β Z < p} + +/-- For positive weights, the budget holds exactly the tuples of total weight below `p`. -/ +theorem mem_modeBudget {M : Type*} [Fintype M] [DecidableEq M] {w : M → ℕ} (hw : ∀ Z, 0 < w Z) + {p : ℕ} {β : M → ℕ} : β ∈ modeBudget w p ↔ ∑ Z, w Z * β Z < p := by + simp only [modeBudget, mem_filter, Fintype.mem_piFinset, mem_range, and_iff_right_iff_imp] + intro h Z + calc β Z ≤ w Z * β Z := Nat.le_mul_of_pos_left _ (hw Z) + _ ≤ ∑ Z, w Z * β Z := single_le_sum (fun Z _ => Nat.zero_le (w Z * β Z)) (mem_univ Z) + _ < p := h + +namespace ModeSplitting + +variable {G P M : Type*} [Fintype M] {N : TensorNetwork R Bool V E} {W : Matrix E E R} + (S : ModeSplitting N W G P M) + +/-- The block of a row port: its packet and the group of its row. -/ +@[expose] def rowBlock (e : E) : P × G := + (S.packet e, S.group (N.src e)) + +/-- The block of a mode: its packet and its target group. -/ +@[expose] def targetBlock (Z : M) : P × G := + (S.modePacket Z, S.target Z) + +/-- The source block of a mode: its packet and its source group. -/ +@[expose] def sourceBlock (Z : M) : P × G := + (S.modePacket Z, S.source Z) + +section Forms + +variable [Fintype E] + +/-- The local form of a row port on the column bits `X`. -/ +@[expose] def localForm (X : E → Bool) (e : E) : R := + ∑ e', S.localPart e e' * if X e' then 1 else 0 + +/-- The value `L_Z(X) = ∑ e', form Z e' X e'` of a mode on the column bits `X`. -/ +@[expose] def modeValue (X : E → Bool) (Z : M) : R := + ∑ e', S.form Z e' * if X e' then 1 else 0 + +/-- The terms of the expansion of the affine factor of a row port: the local term, and the +coefficient of each mode. -/ +@[expose] def choiceTerm (Y X : E → Bool) (e : E) : Option M → R + | none => affineFactor (Y e) (S.localForm X e) + | some Z => affineSign (Y e) * S.coeff e Z + +theorem localForm_congr {X X' : E → Bool} {e : E} + (h : ∀ e', S.packet e' = S.packet e → S.group (N.tgt e') = S.group (N.src e) → X e' = X' e') : + S.localForm X e = S.localForm X' e := by + refine sum_congr rfl fun e' _ => ?_ + by_cases h0 : S.localPart e e' = 0 + · rw [h0, zero_mul, zero_mul] + · obtain ⟨hp, hg⟩ := S.localPart_ne_zero e e' h0 + rw [h e' hp hg] + +theorem modeValue_congr {X X' : E → Bool} {Z : M} + (h : ∀ e, S.packet e = S.modePacket Z → S.group (N.tgt e) = S.source Z → X e = X' e) : + S.modeValue X Z = S.modeValue X' Z := by + refine sum_congr rfl fun e _ => ?_ + by_cases h0 : S.form Z e = 0 + · rw [h0, zero_mul, zero_mul] + · obtain ⟨hp, hg⟩ := S.form_ne_zero Z e h0 + rw [h e hp.symm hg.symm] + +/-- The form of a row port splits into its local form and its modes. -/ +theorem mulVec_apply (X : E → Bool) (e : E) : + W.mulVec (fun e' => if X e' then 1 else 0) e = + S.localForm X e + ∑ Z, S.coeff e Z * S.modeValue X Z := by + simp only [Matrix.mulVec, dotProduct, S.apply_eq, add_mul, sum_add_distrib, localForm, + modeValue, mul_sum, sum_mul] + rw [sum_comm (s := univ) (t := univ) (f := fun e' Z => S.coeff e Z * S.form Z e' * _)] + simp only [mul_assoc] + +/-- The affine factor of a row port as the sum of its terms, each times the value of its mode. -/ +theorem affineFactor_mulVec (Y X : E → Bool) (e : E) : + affineFactor (Y e) (W.mulVec (fun e' => if X e' then 1 else 0) e) = + ∑ o : Option M, S.choiceTerm Y X e o * o.elim 1 (S.modeValue X) := by + rw [S.mulVec_apply, affineFactor_add, Fintype.sum_option, mul_sum] + simp only [choiceTerm, Option.elim, mul_one, mul_assoc] + +end Forms + +/-! ### Coefficients of mode monomials -/ + +section Coefficients + +variable [Fintype E] [DecidableEq E] [DecidableEq P] [DecidableEq G] [DecidableEq M] + +/-- The coefficient of the mode monomial with exponents `β` in the product of the affine factors +of the row ports of the block `k`. It sums, over the ways `φ` to pick in each factor either its +local term or one of the modes targeted at `k`, each mode `Z` of `k` picked `β Z` times, the +product of the picked terms. It depends only on the exponents of the modes of `k`. -/ +@[expose] def blockCoeff (k : P × G) (β : M → ℕ) (Y X : E → Bool) : R := + ∑ φ : {e // S.rowBlock e = k} → Option M, + if (∀ e Z, φ e = some Z → S.targetBlock Z = k) ∧ + ∀ Z, S.targetBlock Z = k → #{e | φ e = some Z} = β Z then + ∏ e, S.choiceTerm Y X e.1 (φ e) + else 0 + +/-- The tensor at the vertex of packet `q` in the child of group `g`: the coefficient of the mode +monomial `β` for the row ports of `q` in group `g`, times `L_Z(X) ^ β Z` for the modes of `q` with +source `g`. -/ +@[expose] def packetTensor (β : M → ℕ) (q : P) (g : G) (Y X : E → Bool) : R := + S.blockCoeff (q, g) β Y X * ∏ Z with S.sourceBlock Z = (q, g), S.modeValue X Z ^ β Z + +/-- A block coefficient depends only on the exponents of the modes of its block. -/ +theorem blockCoeff_congr_exponents {k : P × G} {β β' : M → ℕ} + (h : ∀ Z, S.targetBlock Z = k → β Z = β' Z) (Y X : E → Bool) : + S.blockCoeff k β Y X = S.blockCoeff k β' Y X := by + refine sum_congr rfl fun φ _ => ?_ + refine if_congr (and_congr Iff.rfl (forall_congr' fun Z => imp_congr_right fun hZ => ?_)) rfl + rfl + rw [h Z hZ] + +/-- **A packet tensor is local:** it reads only the row and column ports of its packet and +group. -/ +theorem packetTensor_congr (β : M → ℕ) (q : P) (g : G) {Y Y' X X' : E → Bool} + (hY : ∀ e, S.packet e = q → S.group (N.src e) = g → Y e = Y' e) + (hX : ∀ e, S.packet e = q → S.group (N.tgt e) = g → X e = X' e) : + S.packetTensor β q g Y X = S.packetTensor β q g Y' X' := by + unfold packetTensor blockCoeff + congr 1 + · refine sum_congr rfl fun φ _ => if_congr Iff.rfl (prod_congr rfl fun e _ => ?_) rfl + obtain ⟨e, he⟩ := e + simp only [rowBlock, Prod.mk.injEq] at he + have hl : S.localForm X e = S.localForm X' e := S.localForm_congr fun e' hp hg => + hX e' (hp.trans he.1) (hg.trans he.2) + cases φ ⟨e, _⟩ <;> simp only [choiceTerm, hY e he.1 he.2, hl] + · refine prod_congr rfl fun Z hZ => ?_ + simp only [sourceBlock, mem_filter, mem_univ, true_and, Prod.mk.injEq] at hZ + rw [S.modeValue_congr fun e hp hg => hX e (hp.trans hZ.1) (hg.trans hZ.2)] + +/-- A choice of terms with exponent `β Z` above the number of edges never exists, so the block +coefficient of such a mode's block vanishes. -/ +theorem blockCoeff_eq_zero_of_card_lt {Z : M} {β : M → ℕ} (hZ : Fintype.card E < β Z) + (Y X : E → Bool) : S.blockCoeff (S.targetBlock Z) β Y X = 0 := by + refine sum_eq_zero fun φ _ => ite_eq_right fun h => ?_ + have hle : #{e | φ e = some Z} ≤ Fintype.card E := + (card_filter_le _ _).trans (by rw [card_univ]; exact Fintype.card_subtype_le _) + rw [h.2 Z rfl] at hle + omega + +omit [DecidableEq E] in +/-- The weight of a picked term: zero for the local term and `w Z` for the mode `Z`. -/ +private theorem sum_elim_weight {k : P × G} (w : M → ℕ) (φ : {e // S.rowBlock e = k} → Option M) : + ∑ e, (φ e).elim 0 w = ∑ Z, #{e | φ e = some Z} * w Z := by + rw [← sum_fiberwise' univ φ (fun o => o.elim 0 w)] + simp only [sum_const, smul_eq_mul, Fintype.sum_option, Option.elim, mul_zero, zero_add] + +/-- **The coefficient of a mode monomial is divisible by `π` to its total weight**, when the +coefficient of each mode `Z` is divisible by `π ^ w Z`. -/ +theorem pow_dvd_blockCoeff (w : M → ℕ) {π : R} (hdiv : ∀ e Z, π ^ w Z ∣ S.coeff e Z) + (k : P × G) (β : M → ℕ) (Y X : E → Bool) : + π ^ (∑ Z with S.targetBlock Z = k, w Z * β Z) ∣ S.blockCoeff k β Y X := by + refine dvd_sum fun φ _ => ?_ + split_ifs with h + · have hexp : ∑ Z with S.targetBlock Z = k, w Z * β Z = ∑ e, (φ e).elim 0 w := by + rw [sum_elim_weight, sum_filter] + refine sum_congr rfl fun Z _ => ?_ + split_ifs with hZ + · rw [h.2 Z hZ, mul_comm] + · have : #{e | φ e = some Z} = 0 := card_eq_zero.mpr (filter_eq_empty_iff.mpr + fun e _ he => hZ (h.1 e Z he)) + rw [this, zero_mul] + rw [hexp, ← prod_pow_eq_pow_sum] + refine prod_dvd_prod_of_dvd _ _ fun e _ => ?_ + cases φ e with + | none => simp only [Option.elim, pow_zero, one_dvd] + | some Z => exact Dvd.dvd.mul_left (hdiv e.1 Z) _ + · exact dvd_zero _ + +/-- The product of the block coefficients vanishes when the total weight reaches `p`, if +`π ^ p = 0`. -/ +theorem prod_blockCoeff_eq_zero (w : M → ℕ) {π : R} (hdiv : ∀ e Z, π ^ w Z ∣ S.coeff e Z) + {p : ℕ} (hπ : π ^ p = 0) [Fintype P] [Fintype G] {β : M → ℕ} + (hβ : p ≤ ∑ Z, w Z * β Z) (Y X : E → Bool) : ∏ k, S.blockCoeff k β Y X = 0 := by + have hdvd : π ^ (∑ Z, w Z * β Z) ∣ ∏ k, S.blockCoeff k β Y X := by + rw [← sum_fiberwise univ S.targetBlock (fun Z => w Z * β Z), ← prod_pow_eq_pow_sum] + exact prod_dvd_prod_of_dvd _ _ fun k _ => S.pow_dvd_blockCoeff w hdiv k β Y X + rw [← Nat.add_sub_cancel' hβ, pow_add, hπ, zero_mul] at hdvd + exact zero_dvd_iff.mp hdvd + +end Coefficients + +/-! ### The mode expansion -/ + +section Expansion + +variable [Fintype E] [DecidableEq E] [DecidableEq P] [DecidableEq G] [DecidableEq M] + +omit [DecidableEq E] in +/-- The product of the values of the picked modes, the local term counting as one. -/ +private theorem prod_elim_modeValue {k : P × G} (φ : {e // S.rowBlock e = k} → Option M) + (X : E → Bool) : + ∏ e, (φ e).elim 1 (S.modeValue X) = ∏ Z, S.modeValue X Z ^ #{e | φ e = some Z} := by + rw [← prod_fiberwise' univ φ (fun o => o.elim 1 (S.modeValue X))] + simp only [prod_const, Fintype.prod_option, Option.elim, one_pow, one_mul] + +/-- The exponent tuples supported on the modes of one block, with entries at most `n`. -/ +private abbrev blockBox (n : ℕ) (k : P × G) : Finset (M → ℕ) := + {β ∈ Fintype.piFinset fun _ => range (n + 1) | ∀ Z, S.targetBlock Z ≠ k → β Z = 0} + +/-- **Mode expansion of one block.** The product of the affine factors of the row ports of a +block is a polynomial in the values of the modes targeted at it, with the block coefficients. -/ +private theorem prod_block (Y X : E → Bool) (k : P × G) : + ∏ e : {e // S.rowBlock e = k}, + affineFactor (Y e) (W.mulVec (fun e' => if X e' then 1 else 0) e) = + ∑ β ∈ S.blockBox (Fintype.card E) k, S.blockCoeff k β Y X * ∏ Z, S.modeValue X Z ^ β Z := by + simp only [S.affineFactor_mulVec, Fintype.prod_sum, prod_mul_distrib, S.prod_elim_modeValue, + blockCoeff, sum_mul, ite_mul, zero_mul] + rw [sum_comm] + refine sum_congr rfl fun φ _ => ?_ + set c : M → ℕ := fun Z => #{e | φ e = some Z} with hc + by_cases hv : ∀ e Z, φ e = some Z → S.targetBlock Z = k + · rw [sum_eq_single c] + · rw [ite_eq_left ⟨hv, fun Z _ => rfl⟩] + · intro β hβ hne + refine ite_eq_right fun h => hne (funext fun Z => ?_) + by_cases hZ : S.targetBlock Z = k + · exact (h.2 Z hZ).symm + · rw [(mem_filter.mp hβ).2 Z hZ] + exact (card_eq_zero.mpr (filter_eq_empty_iff.mpr fun e _ he => hZ (hv e Z he))).symm + · intro hn + refine absurd ?_ hn + simp only [mem_filter, Fintype.mem_piFinset, mem_range] + refine ⟨fun Z => Nat.lt_succ_of_le ((card_filter_le _ _).trans ?_), fun Z hZ => ?_⟩ + · rw [card_univ] + exact Fintype.card_subtype_le _ + · exact card_eq_zero.mpr (filter_eq_empty_iff.mpr fun e _ he => hZ (hv e Z he)) + · push Not at hv + obtain ⟨e, Z, he, hZ⟩ := hv + rw [sum_eq_zero fun β _ => ite_eq_right fun h => hZ (h.1 e Z he)] + refine mul_eq_zero_of_left (prod_eq_zero (mem_univ e) ?_) _ + rw [he, choiceTerm] + refine mul_eq_zero_of_right _ (by_contra fun h0 => hZ ?_) + obtain ⟨hp, hg⟩ := S.coeff_ne_zero e.1 Z h0 + rw [targetBlock, hp, hg] + exact e.2 + +omit [Fintype E] [DecidableEq E] in +/-- Sums over the tuples supported on each block combine into one sum over all tuples. -/ +private theorem prod_sum_blockBox (n : ℕ) [Fintype P] [Fintype G] (f : P × G → (M → ℕ) → R) : + ∏ k, ∑ β ∈ S.blockBox n k, f k β = + ∑ β ∈ Fintype.piFinset (fun _ : M => range (n + 1)), + ∏ k, f k (fun Z => if S.targetBlock Z = k then β Z else 0) := by + rw [prod_univ_sum] + refine sum_nbij' (fun x Z => x (S.targetBlock Z) Z) + (fun β k Z => if S.targetBlock Z = k then β Z else 0) ?_ ?_ ?_ ?_ ?_ + · intro x hx + simp only [Fintype.mem_piFinset, mem_filter] at hx ⊢ + exact fun Z => (hx (S.targetBlock Z)).1 Z + · intro β hβ + simp only [Fintype.mem_piFinset, mem_filter, mem_range] at hβ ⊢ + refine fun k => ⟨fun Z => ?_, fun Z hZ => ite_eq_right hZ⟩ + split_ifs + exacts [hβ Z, Nat.succ_pos n] + · intro x hx + simp only [Fintype.mem_piFinset, mem_filter] at hx + funext k Z + split_ifs with h + · subst h + rfl + · exact ((hx k).2 Z h).symm + · intro β _ + funext Z + simp only [ite_true] + · intro x hx + simp only [Fintype.mem_piFinset, mem_filter] at hx + refine prod_congr rfl fun k _ => congrArg (f k) (funext fun Z => ?_) + split_ifs with h + · subst h + rfl + · exact (hx k).2 Z h + +/-- **Mode expansion.** The product of all affine factors is a sum over exponent tuples of the +product of the block coefficients times the mode monomial. -/ +private theorem prod_affineFactor_eq_sum [Fintype P] [Fintype G] (Y X : E → Bool) : + ∏ e, affineFactor (Y e) (W.mulVec (fun e' => if X e' then 1 else 0) e) = + ∑ β ∈ Fintype.piFinset (fun _ : M => range (Fintype.card E + 1)), + (∏ k, S.blockCoeff k β Y X) * ∏ Z, S.modeValue X Z ^ β Z := by + rw [← Fintype.prod_fiberwise S.rowBlock] + simp only [S.prod_block, S.prod_sum_blockBox] + refine sum_congr rfl fun β _ => ?_ + rw [prod_mul_distrib] + congr 1 + · exact prod_congr rfl fun k _ => S.blockCoeff_congr_exponents (fun Z hZ => ite_eq_left hZ) Y X + · rw [prod_comm] + refine prod_congr rfl fun Z _ => ?_ + simp only [pow_ite, pow_zero] + exact Fintype.prod_ite_eq (S.targetBlock Z) _ + +/-- **Truncated mode expansion.** When `π ^ p = 0`, only the tuples in the budget remain. -/ +private theorem prod_affineFactor_eq_sum_modeBudget [Fintype P] [Fintype G] (w : M → ℕ) + (hw : ∀ Z, 0 < w Z) {π : R} {p : ℕ} (hπ : π ^ p = 0) (hdiv : ∀ e Z, π ^ w Z ∣ S.coeff e Z) + (Y X : E → Bool) : + ∏ e, affineFactor (Y e) (W.mulVec (fun e' => if X e' then 1 else 0) e) = + ∑ β ∈ modeBudget w p, (∏ k, S.blockCoeff k β Y X) * ∏ Z, S.modeValue X Z ^ β Z := by + rw [S.prod_affineFactor_eq_sum] + set box := Fintype.piFinset (fun _ : M => range (Fintype.card E + 1)) + rw [← sum_subset (inter_subset_left (s₁ := box) (s₂ := modeBudget w p)), + ← sum_subset (inter_subset_right (s₁ := box) (s₂ := modeBudget w p))] + · intro β hβ hn + have hbox : β ∉ box := fun h => hn (mem_inter.mpr ⟨h, hβ⟩) + simp only [box, Fintype.mem_piFinset, mem_range, not_forall, not_lt] at hbox + obtain ⟨Z, hZ⟩ := hbox + have hZ' : Fintype.card E < β Z := by omega + rw [prod_eq_zero (i := S.targetBlock Z) (mem_univ _) + (S.blockCoeff_eq_zero_of_card_lt hZ' Y X), zero_mul] + · intro β hβ hn + have hb : β ∉ modeBudget w p := fun h => hn (mem_inter.mpr ⟨hβ, h⟩) + rw [mem_modeBudget hw, not_lt] at hb + rw [S.prod_blockCoeff_eq_zero w hdiv hπ hb, zero_mul] + +end Expansion + +/-! ### Child networks -/ + +section Child + +variable [Fintype E] [DecidableEq E] [DecidableEq P] [DecidableEq G] [DecidableEq M] + [DecidableEq V] + +/-- The *child network* of the group `g` for the exponents `β` (§D.4.6). Its vertices are the +vertices of group `g`, from both sides, and one vertex per packet. For every row port `e` of group +`g` it has an edge from the row of `e` to the packet of `e`, and for every column port of group +`g` an edge from the column of `e` to the packet of `e`. A row keeps its tensor, reading the row +bits on its edges, and a column keeps its tensor, reading the column bits; the tensor at a packet +is `packetTensor`. -/ +@[expose] def child (β : M → ℕ) (g : G) : + TensorNetwork R Bool ({v // S.group v = g} ⊕ P) + ({e // S.group (N.src e) = g} ⊕ {e // S.group (N.tgt e) = g}) where + src := Sum.elim (fun e => .inl ⟨N.src e.1, e.2⟩) (fun e => .inl ⟨N.tgt e.1, e.2⟩) + tgt := Sum.elim (fun e => .inr (S.packet e.1)) (fun e => .inr (S.packet e.1)) + tensor + | .inl v, y => + if S.side v.1 then + N.tensor v.1 fun e => if h : N.src e = v.1 then y (.inl ⟨e, h ▸ v.2⟩) else false + else + N.tensor v.1 fun e => if h : N.tgt e = v.1 then y (.inr ⟨e, h ▸ v.2⟩) else false + | .inr q, y => + S.packetTensor β q g (fun e => if h : S.group (N.src e) = g then y (.inl ⟨e, h⟩) else false) + (fun e => if h : S.group (N.tgt e) = g then y (.inr ⟨e, h⟩) else false) + tensor_congr := by + rintro (v | q) y y' h + · have hs : ∀ e (he : N.src e = v.1), y (.inl ⟨e, he ▸ v.2⟩) = y' (.inl ⟨e, he ▸ v.2⟩) := by + intro e he + exact h _ (Or.inl (congrArg Sum.inl (Subtype.ext he))) + have ht : ∀ e (he : N.tgt e = v.1), y (.inr ⟨e, he ▸ v.2⟩) = y' (.inr ⟨e, he ▸ v.2⟩) := by + intro e he + exact h _ (Or.inl (congrArg Sum.inl (Subtype.ext he))) + simp only + split_ifs + · congr 1 + funext e + split_ifs with he + exacts [hs e he, rfl] + · congr 1 + funext e + split_ifs with he + exacts [ht e he, rfl] + · refine S.packetTensor_congr β q g (fun e hq hg => ?_) (fun e hq hg => ?_) + · simp only [hg, dite_true] + exact h _ (Or.inr (by simp only [Sum.elim_inl, hq])) + · simp only [hg, dite_true] + exact h _ (Or.inr (by simp only [Sum.elim_inr, hq])) + +@[simp] theorem child_src_inl (β : M → ℕ) (g : G) (e : {e // S.group (N.src e) = g}) : + (S.child β g).src (.inl e) = .inl ⟨N.src e.1, e.2⟩ := + rfl + +@[simp] theorem child_src_inr (β : M → ℕ) (g : G) (e : {e // S.group (N.tgt e) = g}) : + (S.child β g).src (.inr e) = .inl ⟨N.tgt e.1, e.2⟩ := + rfl + +@[simp] theorem child_tgt_inl (β : M → ℕ) (g : G) (e : {e // S.group (N.src e) = g}) : + (S.child β g).tgt (.inl e) = .inr (S.packet e.1) := + rfl + +@[simp] theorem child_tgt_inr (β : M → ℕ) (g : G) (e : {e // S.group (N.tgt e) = g}) : + (S.child β g).tgt (.inr e) = .inr (S.packet e.1) := + rfl + +/-- **Children are bipartite**, with the old vertices on one side and the packets on the other; +every edge runs from an old vertex to a packet. -/ +theorem isBipartite_child (β : M → ℕ) (g : G) : (S.child β g).IsBipartite := + ⟨Sum.isLeft, by rintro (e | e) <;> simp⟩ + +omit [DecidableEq E] [DecidableEq P] [DecidableEq M] [DecidableEq V] in +/-- A child has one edge for each port of its group. -/ +theorem card_edges_child (g : G) : + Fintype.card ({e // S.group (N.src e) = g} ⊕ {e // S.group (N.tgt e) = g}) = + #{e | S.group (N.src e) = g} + #{e | S.group (N.tgt e) = g} := by + rw [Fintype.card_sum, Fintype.card_subtype, Fintype.card_subtype] + +/-- The bits of the ports of group `g`, read off the row bits `Y` and the column bits `X`. -/ +private abbrev groupBits (Y X : E → Bool) (g : G) : + {e // S.group (N.src e) = g} ⊕ {e // S.group (N.tgt e) = g} → Bool := + Sum.elim (fun e => Y e.1) (fun e => X e.1) + +/-- On the bits of its group, an old vertex of a child reads the row bits if it is a row and the +column bits if it is a column. -/ +private theorem child_tensor_inl_groupBits (β : M → ℕ) (g : G) (v : {v // S.group v = g}) + (Y X : E → Bool) : + (S.child β g).tensor (.inl v) (S.groupBits Y X g) = + if S.side v.1 then N.tensor v.1 Y else N.tensor v.1 X := by + simp only [child] + split_ifs with hv + · refine N.tensor_congr v.1 _ _ fun e he => ?_ + by_cases hs : N.src e = v.1 + · simp only [hs, dite_true, Sum.elim_inl] + · have ht : N.tgt e = v.1 := he.resolve_left hs + have := S.side_tgt e + rw [ht, hv] at this + exact absurd this (by decide) + · refine N.tensor_congr v.1 _ _ fun e he => ?_ + by_cases ht : N.tgt e = v.1 + · simp only [ht, dite_true, Sum.elim_inr] + · have hs : N.src e = v.1 := he.resolve_right ht + have := S.side_src e + rw [hs] at this + exact absurd this hv + +/-- On the bits of its group, a packet of a child reads the row and column bits. -/ +private theorem child_tensor_inr_groupBits (β : M → ℕ) (g : G) (q : P) (Y X : E → Bool) : + (S.child β g).tensor (.inr q) (S.groupBits Y X g) = S.packetTensor β q g Y X := by + simp only [child] + refine S.packetTensor_congr β q g (fun e _ hg => ?_) (fun e _ hg => ?_) + · simp only [hg, dite_true, Sum.elim_inl] + · simp only [hg, dite_true, Sum.elim_inr] + +/-- **The weight of an assignment factors over the groups.** For every tuple `β`, the term of +the expanded deformed contraction at the row bits `Y` and column bits `X` is the product, over the +groups, of the weights of the bits of each group in its child. -/ +private theorem weight_eq_prod_child [Fintype V] [Fintype P] [Fintype G] (β : M → ℕ) + (Y X : E → Bool) : + (∏ v ∈ univ.filter (S.side · = true), N.tensor v Y) * + (∏ v ∈ univ.filter (S.side · = false), N.tensor v X) * + ((∏ k, S.blockCoeff k β Y X) * ∏ Z, S.modeValue X Z ^ β Z) = + ∏ g, ∏ x, (S.child β g).tensor x (S.groupBits Y X g) := by + simp only [Fintype.prod_sum_type, S.child_tensor_inl_groupBits, S.child_tensor_inr_groupBits, + prod_mul_distrib] + rw [Fintype.prod_fiberwise S.group (fun v => if S.side v then N.tensor v Y else N.tensor v X), + prod_ite] + simp only [Bool.not_eq_true] + have hk : ∏ k, S.blockCoeff k β Y X = ∏ g, ∏ q, S.blockCoeff (q, g) β Y X := by + rw [Fintype.prod_prod_type, prod_comm] + have hZ : ∏ Z, S.modeValue X Z ^ β Z = + ∏ g, ∏ q, ∏ Z with S.sourceBlock Z = (q, g), S.modeValue X Z ^ β Z := by + rw [prod_comm, ← Fintype.prod_prod_type (f := fun k => ∏ Z with S.sourceBlock Z = k, + S.modeValue X Z ^ β Z), prod_fiberwise] + simp only [packetTensor, prod_mul_distrib, hk, hZ] + +/-- Splitting the row and column bits by group. -/ +private def splitBits : + (E → Bool) × (E → Bool) ≃ + ∀ g, ({e // S.group (N.src e) = g} ⊕ {e // S.group (N.tgt e) = g} → Bool) where + toFun YX g := S.groupBits YX.1 YX.2 g + invFun y := (fun e => y _ (.inl ⟨e, rfl⟩), fun e => y _ (.inr ⟨e, rfl⟩)) + left_inv _ := rfl + right_inv y := by + funext g c + rcases c with ⟨e, rfl⟩ | ⟨e, rfl⟩ <;> rfl + +/-- **The sum over the bits factors over the groups**: for each tuple `β`, the sum over all row +and column bits of the expanded term is the product of the contractions of the children. -/ +private theorem sum_weight_eq_prod_contraction_child [Fintype V] [Fintype P] [Fintype G] + (β : M → ℕ) : + ∑ X : E → Bool, ∑ Y : E → Bool, + (∏ v ∈ univ.filter (S.side · = true), N.tensor v Y) * + (∏ v ∈ univ.filter (S.side · = false), N.tensor v X) * + ((∏ k, S.blockCoeff k β Y X) * ∏ Z, S.modeValue X Z ^ β Z) = + ∏ g, (S.child β g).contraction := by + simp only [S.weight_eq_prod_child, contraction] + rw [Fintype.prod_sum, sum_comm, ← Fintype.sum_prod_type'] + exact Fintype.sum_equiv S.splitBits _ _ fun _ => rfl + +/-- **The exact child expansion.** In every commutative ring, the deformed contraction is the sum, +over the exponent tuples with entries at most the number of edges, of the products over the +groups of the contractions of the children. -/ +theorem deformedContraction_eq_sum_prod_contraction_child_of_le [Fintype V] [Fintype P] + [Fintype G] : + N.deformedContraction S.side W = + ∑ β ∈ Fintype.piFinset (fun _ : M => range (Fintype.card E + 1)), + ∏ g, (S.child β g).contraction := by + simp only [deformedContraction, S.prod_affineFactor_eq_sum, mul_sum] + exact (sum_congr rfl fun X _ => sum_comm).trans + (sum_comm.trans (sum_congr rfl fun β _ => S.sum_weight_eq_prod_contraction_child β)) + +/-- **The child identity** ((D.16) of [OpenAI2026ETH]). If the coefficient of every mode `Z` is +divisible by `π ^ w Z`, with positive weights, and `π ^ p = 0`, then the deformed contraction is +the sum, over the exponent tuples of total weight below `p`, of the products over the groups of +the contractions of the children. In the manuscript, `π = 2`, `p = p_t` and the ring is +`A / 2 ^ p_t`. -/ +theorem deformedContraction_eq_sum_prod_contraction_child [Fintype V] [Fintype P] [Fintype G] + (w : M → ℕ) (hw : ∀ Z, 0 < w Z) {π : R} {p : ℕ} (hπ : π ^ p = 0) + (hdiv : ∀ e Z, π ^ w Z ∣ S.coeff e Z) : + N.deformedContraction S.side W = ∑ β ∈ modeBudget w p, ∏ g, (S.child β g).contraction := by + simp only [deformedContraction, S.prod_affineFactor_eq_sum_modeBudget w hw hπ hdiv, mul_sum] + exact (sum_congr rfl fun X _ => sum_comm).trans + (sum_comm.trans (sum_congr rfl fun β _ => S.sum_weight_eq_prod_contraction_child β)) + +end Child + +end ModeSplitting + +end TensorNetwork + +end Cslib.Circuits.Frontier diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkModeExpansion.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkModeExpansion.lean new file mode 100644 index 000000000..227e628e6 --- /dev/null +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkModeExpansion.lean @@ -0,0 +1,103 @@ +/- +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.ModeExpansion + +/-! +# Tests for the mode expansion and the child identity + +Two edges `0 : 0 → 2` and `1 : 1 → 3`, from the rows `0, 1` to the columns `2, 3`, in one packet. +Vertex `v` is in group `v % 2`, so edge `e` joins two vertices of group `e`, and the entries of the +matrix `W = !![1, 2; 2, 3]` off the diagonal cross between the groups. Over `ZMod 4` they become two +modes of weight one, since `2 ∣ 2` and `2 ^ 2 = 0`: mode `Z` reads the column bit of edge `1 - Z` +and enters the form of row port `Z`. The child identity (D.16) then writes the deformed +contraction as a sum over the three tuples `β` of total weight below two. +-/ + +@[expose] public section + +namespace ComplexityTests.Computability.Circuit.Frontier.TensorNetwork.ModeExpansion + +open Cslib.Circuits.Frontier TensorNetwork + +/-- The edge at a vertex: vertices `0` and `2` are the ends of edge `0`, and `1` and `3` of +edge `1`. -/ +def edgeAt (v : Fin 4) : Fin 2 := ⟨v.val % 2, Nat.mod_lt _ (by decide)⟩ + +/-- The two-edge network, with tensor `(1, v + 1)` on the bit of the edge at `v`. -/ +def net : TensorNetwork (ZMod 4) Bool (Fin 4) (Fin 2) where + src e := ⟨e.val, by omega⟩ + tgt e := ⟨e.val + 2, by omega⟩ + tensor v x := if x (edgeAt v) then (v.val + 1 : ZMod 4) else 1 + tensor_congr v x y h := by rw [h (edgeAt v) (by fin_cases v <;> decide)] + +/-- The matrix: the identity on the diagonal, and `2` between the groups. -/ +def W : Matrix (Fin 2) (Fin 2) (ZMod 4) := !![1, 2; 2, 3] + +/-- The splitting of `W` into its diagonal and two modes. -/ +def S : net.ModeSplitting W (Fin 2) Unit (Fin 2) where + side v := decide (v.val < 2) + group := edgeAt + packet _ := () + localPart e e' := if e = e' then W e e else 0 + modePacket _ := () + source Z := Z + 1 + target Z := Z + coeff e Z := if e = Z then W Z (Z + 1) else 0 + form Z e' := if e' = Z + 1 then 1 else 0 + side_src := by decide + side_tgt := by decide + apply_eq e e' := by fin_cases e <;> fin_cases e' <;> decide + localPart_ne_zero e e' := by fin_cases e <;> fin_cases e' <;> decide + coeff_ne_zero e Z := by fin_cases e <;> fin_cases Z <;> decide + form_ne_zero Z e := by fin_cases Z <;> fin_cases e <;> decide + +/-- Both modes have coefficients divisible by `2`. -/ +theorem two_dvd_coeff (e Z : Fin 2) : 2 ^ 1 ∣ S.coeff e Z := by + have h : S.coeff e Z = 2 * (if e = Z then 1 else 0) := by + fin_cases e <;> fin_cases Z <;> decide + rw [h, pow_one] + exact dvd_mul_right _ _ + +/-- **The child identity** for this splitting, with weights one and `2 ^ 2 = 0` in `ZMod 4`. -/ +theorem deformedContraction_eq : + net.deformedContraction S.side W = + ∑ β ∈ modeBudget (fun _ : Fin 2 => 1) 2, ∏ g, (S.child β g).contraction := + S.deformedContraction_eq_sum_prod_contraction_child _ (fun _ => Nat.one_pos) + (by decide : (2 : ZMod 4) ^ 2 = 0) two_dvd_coeff + +/-- The budget holds the three tuples of total weight below two. -/ +example : modeBudget (fun _ : Fin 2 => 1) 2 = {![0, 0], ![1, 0], ![0, 1]} := by decide + +/-- The deformed contraction is `2`. -/ +example : net.deformedContraction S.side W = 2 := by decide + +/-- Without modes, the child of group `0` contracts to `1 + 3 = 0` and that of group `1` to `1`. +With mode `0`, whose coefficient `2` enters the row form of group `0`, the child of group `0` +vanishes. -/ +example : (S.child ![0, 0] 0).contraction = 0 ∧ (S.child ![0, 0] 1).contraction = 1 ∧ + (S.child ![1, 0] 0).contraction = 0 := by + decide + +/-- With mode `1`, the child of group `0` carries the mode value `L(X) = X₀` on its packet and +contracts to `3`, and the child of group `1` carries the coefficient `±2` and contracts to `2`. So +the only surviving term of (D.16) is `3 * 2 = 2`, the deformed contraction. -/ +example : (S.child ![0, 1] 0).contraction = 3 ∧ (S.child ![0, 1] 1).contraction = 2 := by + decide + +/-- The children are bipartite. -/ +example (β : Fin 2 → ℕ) (g : Fin 2) : (S.child β g).IsBipartite := S.isBipartite_child β g + +/-- Each child has the row port and the column port of its group. -/ +example (g : Fin 2) : + Fintype.card ({e // S.group (net.src e) = g} ⊕ {e // S.group (net.tgt e) = g}) = 2 := by + rw [S.card_edges_child] + fin_cases g <;> decide + +end ComplexityTests.Computability.Circuit.Frontier.TensorNetwork.ModeExpansion