refactor(circuit/frontier): one rows-first predicate on described networks

Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean

@@ -31,10 +31,9 @@
   (`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
+  (`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
@@ -47,7 +46,6 @@
 ## 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.
@@ -90,12 +88,12 @@
 variable {fl : List ℕ} (hirr : Irreducible ((monicOf fl).map (Int.castRingHom (ZMod 2))))
 
 /-- The class of `U` in the valuation ring `O = ℤ_(2)[U] / (f)`, `f = monicOf fl`. -/
 noncomputable def rootO : (padicValuation 2 (monic_monicOf fl) hirr).integer :=
   ⟨map (Int.castRingHom ℚ) (monicOf fl) _ dvd_rfl (root _),
     (Valuation.mem_integer_iff _ _).mpr (padicValuation_map_le_one _ hirr _)⟩
 
 /-- **The lift of a coefficient list to `O`**: `∑ i < e, c_i U ^ i`, with `e = fl.length`. -/
 noncomputable def liftO (c : List ℕ) : (padicValuation 2 (monic_monicOf fl) hirr).integer :=
   ∑ i ∈ range fl.length, ((c.getD i 0 : ℕ) : (padicValuation 2 (monic_monicOf fl) hirr).integer) *
     rootO hirr ^ i
 
@@ -160,23 +158,6 @@
 
 /-! ### 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)⟩ :

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 : ℕ) :

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

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]

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