From 0906c9ce7ebe4a54e8ca45ccc2751a43376998c5 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 03:08:22 -0400 Subject: [PATCH 1/2] refactor(circuit/frontier): one rows-first predicate on described networks ExplicitTensorNetwork R is DescribedNetwork (List R), so ExplicitTensorNetwork.IsRowsFirstBipartite and DescribedNetwork.IsRowsFirstBipartite were the same definition twice. Keep only DescribedNetwork.IsRowsFirstBipartite, defined beside DescribedNetwork in Explicit.lean; dot notation on explicit networks resolves to it. Remove isRowsFirstBipartite_explicit and update the docs and the test that named the explicit predicate. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Frontier/TensorNetwork/DescribedLift.lean | 27 +++------------ .../Frontier/TensorNetwork/Explicit.lean | 34 +++++++++---------- .../CountingSimulation/Admissible.lean | 2 +- .../Probabilistic/ExplicitBlockNetwork.lean | 2 +- .../Circuit/Frontier/TensorNetwork.lean | 2 +- 5 files changed, 24 insertions(+), 43 deletions(-) diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean index e0d0e1a0da..365c6ca9ff 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean @@ -30,11 +30,10 @@ for. and reducing the lift modulo `2 ^ p` gives the value of `c` in `A_p` (`GaloisRingArith.reduction_liftO`). This is the canonical lifting of representatives of §D.4.1 (p. 58): a retained vertex is read through the lift of its entry at every later precision. -* **Rows first.** A described network is *rows-first bipartite* at `r` - (`DescribedNetwork.IsRowsFirstBipartite`, the condition of - `ExplicitTensorNetwork.IsRowsFirstBipartite`) when every port names an edge and every edge is a - port of exactly one of the first `r` vertices, once, and of exactly one of the others, once. The - ends of the edges are then computed by listing the vertices at each edge +* **Rows first.** When a described network is *rows-first bipartite* at `r` + (`DescribedNetwork.IsRowsFirstBipartite`), every port names an edge and every edge is a port of + exactly one of the first `r` vertices, once, and of exactly one of the others, once. The ends of + the edges are then computed by listing the vertices at each edge (`DescribedNetwork.incident`, `DescribedNetwork.edgeEnds`), in polynomial time (`DescribedNetwork.computableInPolyTime_edgeEnds`). * **The network** (`DescribedNetwork.toNetwork`). A rows-first described network and an evaluator @@ -47,7 +46,6 @@ for. ## Main definitions * `Cslib.GaloisRingArith.liftO`: the lift of a coefficient list to `O`. -* `Cslib.Circuits.Frontier.DescribedNetwork.IsRowsFirstBipartite`: rows first. * `Cslib.Circuits.Frontier.DescribedNetwork.incident`, `Cslib.Circuits.Frontier.DescribedNetwork.edgeEnds`: the ends of the edges. * `Cslib.Circuits.Frontier.DescribedNetwork.toNetwork`: the network of a described network. @@ -160,23 +158,6 @@ variable {T : Type} (D : DescribedNetwork T) /-! ### Rows first -/ -/-- **Rows-first bipartite**: the first `r` vertices are the *rows* and the others the *columns*, -every port names an edge, and every edge is a port of the rows exactly once and of the columns -exactly once (the condition of `ExplicitTensorNetwork.IsRowsFirstBipartite`). -/ -@[expose] def IsRowsFirstBipartite (r : ℕ) : Prop := - (∀ v ∈ D.vertices, ∀ i ∈ v.1, i < D.numEdges) ∧ - ∀ i < D.numEdges, ((D.vertices.take r).map fun v => v.1.count i).sum = 1 ∧ - ((D.vertices.drop r).map fun v => v.1.count i).sum = 1 - -instance (r : ℕ) : Decidable (D.IsRowsFirstBipartite r) := by - unfold IsRowsFirstBipartite - infer_instance - -/-- An explicit network is rows-first exactly when it is as a described network. -/ -theorem isRowsFirstBipartite_explicit (d : ExplicitTensorNetwork ℕ) (r : ℕ) : - DescribedNetwork.IsRowsFirstBipartite d r ↔ ExplicitTensorNetwork.IsRowsFirstBipartite d r := - Iff.rfl - /-- Being rows-first depends only on the ports, not on the descriptors. -/ theorem isRowsFirstBipartite_map {T' : Type} (f : T → T') (r : ℕ) : (⟨D.numEdges, D.vertices.map fun v => (v.1, f v.2)⟩ : diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean index 313760ebfc..a48aad9bc6 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean @@ -37,9 +37,9 @@ 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`). A network is *rows-first bipartite* with `r` rows -(`ExplicitTensorNetwork.IsRowsFirstBipartite`) when every edge is a port of exactly one of its -first `r` vertices and of exactly one of the others. +(`ExplicitTensorNetwork.tableLength`). A described network is *rows-first bipartite* with `r` +rows (`DescribedNetwork.IsRowsFirstBipartite`) when every port names an edge and every edge is a +port of exactly one of its first `r` vertices and of exactly one of the others. **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 @@ -55,6 +55,8 @@ one end of every edge below `r` and the other at or above it gives a rows-first the descriptors of its vertices. * `Cslib.Circuits.Frontier.DescribedNetwork.contraction`: its contraction, for an evaluator of the descriptors. +* `Cslib.Circuits.Frontier.DescribedNetwork.IsRowsFirstBipartite`: the bipartition with the first + `r` vertices as rows. * `Cslib.Circuits.Frontier.ExplicitTensorNetwork`: an explicit Boolean tensor network, with tables as descriptors. * `Cslib.Circuits.Frontier.ExplicitTensorNetwork.entry`, @@ -63,8 +65,6 @@ one end of every edge below `r` and the other at or above it gives a rows-first * `Cslib.Circuits.Frontier.ExplicitTensorNetwork.contraction`: the contraction. * `Cslib.Circuits.Frontier.ExplicitTensorNetwork.maxDegree`, `Cslib.Circuits.Frontier.ExplicitTensorNetwork.tableLength`: size measures. -* `Cslib.Circuits.Frontier.ExplicitTensorNetwork.IsRowsFirstBipartite`: the bipartition with the - first `r` vertices as rows. * `Cslib.Circuits.Frontier.TensorNetwork.explicitPorts`, `Cslib.Circuits.Frontier.TensorNetwork.explicitTable`, `Cslib.Circuits.Frontier.TensorNetwork.toExplicit`: writing a Boolean tensor network out. @@ -137,6 +137,18 @@ theorem map_contraction {R S : Type*} [CommSemiring R] [CommSemiring S] (ψ : R rw [map_list_prod, List.map_map] rfl +/-- **Rows-first bipartite**: the first `r` vertices are the *rows* and the others the *columns*, +every port names an edge, and every edge is a port of the rows exactly once and of the columns +exactly once. So every edge joins a row to a column. -/ +def IsRowsFirstBipartite (d : DescribedNetwork T) (r : ℕ) : Prop := + (∀ v ∈ d.vertices, ∀ i ∈ v.1, i < d.numEdges) ∧ + ∀ i < d.numEdges, ((d.vertices.take r).map fun v => v.1.count i).sum = 1 ∧ + ((d.vertices.drop r).map fun v => v.1.count i).sum = 1 + +instance (d : DescribedNetwork T) (r : ℕ) : Decidable (d.IsRowsFirstBipartite r) := by + unfold IsRowsFirstBipartite + infer_instance + end DescribedNetwork /-- An *explicit Boolean tensor network* over `R`: a network whose descriptors are *tables*. The @@ -190,18 +202,6 @@ 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 -/-- **Rows-first bipartite**: the first `r` vertices are the *rows* and the others the *columns*, -every port names an edge, and every edge is a port of the rows exactly once and of the columns -exactly once. So every edge joins a row to a column. -/ -def IsRowsFirstBipartite (r : ℕ) : Prop := - (∀ v ∈ d.vertices, ∀ i ∈ v.1, i < d.numEdges) ∧ - ∀ i < d.numEdges, ((d.vertices.take r).map fun v => v.1.count i).sum = 1 ∧ - ((d.vertices.drop r).map fun v => v.1.count i).sum = 1 - -instance (r : ℕ) : Decidable (d.IsRowsFirstBipartite r) := by - unfold IsRowsFirstBipartite - infer_instance - end ExplicitTensorNetwork private theorem getD_ofFn {n : ℕ} (x : Fin n → Bool) (i : ℕ) : diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/Admissible.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/Admissible.lean index d1afe23004..80fd8c882e 100644 --- a/Complexity/Computability/Complexity/Classes/CountingSimulation/Admissible.lean +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/Admissible.lean @@ -22,7 +22,7 @@ explicit Boolean tensor networks with a number of row vertices, networks are built (milestone H3) and the contraction theorem consumes them (milestone T2). A network `(r, G)` is admissible at size `s` with constant `C` when `G` is bipartite with its -first `r` vertices as rows (`Cslib.Circuits.Frontier.ExplicitTensorNetwork.IsRowsFirstBipartite`), +first `r` vertices as rows (`Cslib.Circuits.Frontier.DescribedNetwork.IsRowsFirstBipartite`), it has at most `C s` edges and at most `C s` vertices, its maximum degree is at most `C ⌊log₂ s⌋`, every table lists the values at all bit strings on its ports, and it has at least `s` edges. The last two conditions spare the contraction algorithm short tables and networks much smaller than diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork.lean index 56ed22be45..da05642876 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork.lean @@ -43,7 +43,7 @@ accepting count (`Turing.MultiTapePTM.sum_contraction_explicitBlockNetwork`). `2 * (q * (3 * k + 1) * m)` edges and maximum degree at most `2 * (3 * k + 1) * m`, both `O(b)` per interval. Its first `q * (3 * k + 2)` vertices are the rows of a bipartition: every edge has exactly one port at a row and one at a column -(`Cslib.Circuits.Frontier.ExplicitTensorNetwork.IsRowsFirstBipartite`). Every table has length +(`Cslib.Circuits.Frontier.DescribedNetwork.IsRowsFirstBipartite`). Every table has length `2 ^ (number of ports)`, and its entries are at most `2 ^ b`. These are the inputs of the Boolean tensor contraction theorem [OpenAI2026ETH, Theorem D.1] diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean index 9206e0547a..dcde7ed35a 100644 --- a/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetwork.lean @@ -103,7 +103,7 @@ example : ¬ parallel.IsRowsFirstBipartite 2 := by decide example : ¬ (cycle eqTable).IsRowsFirstBipartite 2 := by decide /-- A port naming no edge is excluded. -/ -example : ¬ ExplicitTensorNetwork.IsRowsFirstBipartite +example : ¬ DescribedNetwork.IsRowsFirstBipartite (⟨1, [([0], [1, 1]), ([0, 5], [1, 1, 1, 1])]⟩ : ExplicitTensorNetwork ℕ) 1 := by decide /-- Written out with the old vertices first, the subdivision of `parallelNetwork` is rows-first From 8bd4f74d69c4e863357dc68db5a1e20a6de48d67 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 03:09:03 -0400 Subject: [PATCH 2/2] doc(circuit/frontier): keep the rows-first bullet's first line Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Circuit/Frontier/TensorNetwork/DescribedLift.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean index 365c6ca9ff..e3f6ad7c22 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean @@ -30,10 +30,10 @@ for. and reducing the lift modulo `2 ^ p` gives the value of `c` in `A_p` (`GaloisRingArith.reduction_liftO`). This is the canonical lifting of representatives of §D.4.1 (p. 58): a retained vertex is read through the lift of its entry at every later precision. -* **Rows first.** When a described network is *rows-first bipartite* at `r` - (`DescribedNetwork.IsRowsFirstBipartite`), every port names an edge and every edge is a port of - exactly one of the first `r` vertices, once, and of exactly one of the others, once. The ends of - the edges are then computed by listing the vertices at each edge +* **Rows first.** A described network is *rows-first bipartite* at `r` + (`DescribedNetwork.IsRowsFirstBipartite`) when every port names an edge and every edge is a port + of exactly one of the first `r` vertices, once, and of exactly one of the others, once. The ends + of the edges are then computed by listing the vertices at each edge (`DescribedNetwork.incident`, `DescribedNetwork.edgeEnds`), in polynomial time (`DescribedNetwork.computableInPolyTime_edgeEnds`). * **The network** (`DescribedNetwork.toNetwork`). A rows-first described network and an evaluator