refactor(tensor-network): place reusable lemmas beside their models

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

@@ -60,6 +60,7 @@ for.
 * `Cslib.GaloisRingArith.reduction_liftO`, `Cslib.GaloisRingArith.mk_liftO`: reducing a lift.
 * `Cslib.GaloisRingArith.isUnit_liftO_sub`,
   `Cslib.GaloisRingArith.pairwise_isUnit_liftO_sub_digits`: binary lists as interpolation points.
+* `Cslib.Circuits.Frontier.DescribedNetwork.rows_le_of_isRowsFirstBipartite`: row count bound.
 * `Cslib.Circuits.Frontier.DescribedNetwork.incident_eq`: the vertices at an edge.
 * `Cslib.Circuits.Frontier.DescribedNetwork.contraction_toNetwork`,
   `Cslib.Circuits.Frontier.DescribedNetwork.reduction_contraction_toNetwork`: the contraction.
@@ -250,6 +251,14 @@ theorem isRowsFirstBipartite_map {T' : Type} (f : T → T') (r : ℕ) :
 
 variable {D}
 
+/-- A rows-first network with an edge has at most as many rows as vertices. -/
+theorem rows_le_of_isRowsFirstBipartite {D : DescribedNetwork T} {r : ℕ}
+    (hD : D.IsRowsFirstBipartite r) (hM : 1 ≤ D.numEdges) : r ≤ D.vertices.length := by
+  by_contra h
+  have h1 := (hD.2 0 hM).2
+  rw [List.drop_of_length_le (by omega)] at h1
+  simp at h1
+
 theorem getD_map_fst (v : ℕ) (hv : v < D.vertices.length) :
     (D.vertices.map Prod.fst).getD v [] = D.vertices[v].1 := by
   rw [List.getD_eq_getElem _ _ (by simpa using hv), List.getElem_map]

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

@@ -51,8 +51,6 @@ but a polynomial in `n` is a constant.
 ## Main results
 
 * `Cslib.Circuits.Frontier.FastContraction.leafCertificate_le`: the cost of a leaf.
-* `Cslib.Circuits.Frontier.NativeChild.desc_of_mem_nativeChild`: the descriptors of a native
-  child.
 * `Cslib.Circuits.Frontier.FastContraction.packetShape_root`,
   `Cslib.Circuits.Frontier.FastContraction.packetShape_child`: the packet shape on the reached
   calls.
@@ -71,65 +69,6 @@ public section
 
 namespace Cslib.Circuits.Frontier
 
-/-! ### The descriptors of the native children -/
-
-namespace NativeChild
-
-open ChildNumbering
-
-variable {D : DescribedNetwork VertexDesc} {r : ℕ}
-
-/-- **The descriptors of the native child.** A vertex of the native child of a rows-first parent
-with at least `64 ^ a` edges keeps the descriptor of a parent vertex, or is the packet `q`, with
-the packet context of `q`, the slice of `β` at `q`, and tags whose slots are below `2 ^ a` and
-distinct among its row ports. -/
-theorem desc_of_mem_nativeChild (hD : D.IsRowsFirstBipartite r) {fl : List ℕ} {a i : ℕ}
-    (hK : 64 ^ a ≤ D.numEdges) (hia : i < a) (pt : ℕ) (t : ℤ) (ζ β : List ℕ) (g : Fin 64)
-    {v : List ℕ × VertexDesc}
-    (hv : v ∈ (nativeChild fl a i pt t ζ r D (nativeParentPacking r a D) β g).vertices) :
-    (∃ w ∈ D.vertices, v.2 = w.2) ∨
-      ∃ q tags, v.2 = .inr (packetCtx fl a i pt t ζ g q, tags, betaSlice i pt β q) ∧
-        (∀ y ∈ tags, y.2 < 2 ^ a) ∧ ((tags.filter (·.1)).map (·.2)).Nodup := by
-  have hgroups := groupsOf_eq hD hK hia
-  have hpk1 : (nativeParentPacking r a D).2.1 = (parentPacking hD a).numPackets := by
-    rw [nativeParentPacking_eq hD hK]
-  have hpk2 : (nativeParentPacking r a D).2.2 = List.ofFn fun e =>
-      (((parentPacking hD a).packet e : ℕ), ((parentPacking hD a).slot e : ℕ)) := by
-    rw [nativeParentPacking_eq hD hK]
-  rw [nativeChild_eq hD _ (parentPacking hD a).packet (fun e => ((parentPacking hD a).slot e : ℕ))
-    g fl a i pt t ζ β _ hgroups hpk1 hpk2] at hv
-  simp only [List.mem_ofFn] at hv
-  obtain ⟨c, rfl⟩ := hv
-  rcases hc : (childVertexEquiv (P := (parentPacking hD a).numPackets)
-      (packingGroup (parentSide r) (parentPacking hD a) ⟨i, hia⟩) g).symm c with w | q
-  · left
-    refine ⟨D.vertices[(w.1 : ℕ)], List.getElem_mem _, ?_⟩
-    simp only [numberedDesc, Sum.elim_inl]
-  · right
-    simp only [numberedDesc, Sum.elim_inr]
-    refine ⟨q, _, rfl, ?_, ?_⟩
-    · intro y hy
-      simp only [List.mem_map] at hy
-      obtain ⟨e, -, rfl⟩ := hy
-      exact Fin.isLt _
-    · rw [List.filter_map, List.map_map]
-      refine List.Nodup.map_on ?_ ((nodup_packetPorts hD _ _ g q).filter _)
-      intro c₁ hc₁ c₂ hc₂ heq
-      simp only [List.mem_filter, Function.comp_apply] at hc₁ hc₂
-      obtain ⟨hm₁, hl₁⟩ := hc₁
-      obtain ⟨hm₂, hl₂⟩ := hc₂
-      rw [mem_packetPorts] at hm₁ hm₂
-      rcases c₁ with e₁ | e₁
-      · rcases c₂ with e₂ | e₂
-        · simp only [Function.comp_apply, Sum.elim_inl] at heq hm₁ hm₂
-          have hinj := (parentPacking hD a).injective (a₁ := e₁.1) (a₂ := e₂.1)
-            (Prod.ext (hm₁.trans hm₂.symm) (Fin.ext heq))
-          rw [Subtype.ext hinj]
-        · simp at hl₂
-      · simp at hl₁
-
-end NativeChild
-
 namespace FastContraction
 
 open GaloisRingArith NativePacket ChildCursor NativeRecovery ContractionSchedule NativeChild

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

@@ -274,7 +274,7 @@ theorem length_children_le (hB : ∀ d M p, Active C m d M p → ActiveBounds C
   have hK := pow_slots_le_edges_of_active ha
   have hslots : slots x = slotBits m x.depth := by rw [slots, h.scale_eq]
   have hlevels : levels x = taper m x.depth := by rw [levels, h.scale_eq]
-  have hr := rows_le_of_isRowsFirstBipartite h.wf.2 (one_le_edges_of_active ha)
+  have hr := DescribedNetwork.rows_le_of_isRowsFirstBipartite h.wf.2 (one_le_edges_of_active ha)
   have hP : (packing x).2.1 * 2 ^ slots x ≤ 3 * x.edges :=
     packing_eq hr ▸ numPackets_nativeParentPacking_mul_le h.wf.2 hK h.degree_le
       (by rw [hslots]; exact hb.degree_mul_pairs_sq_le)

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

@@ -71,14 +71,6 @@ row and stores the exponents in unary. -/
 
 variable {x : Call}
 
-/-- A rows-first network with an edge has at most as many rows as vertices. -/
-theorem rows_le_of_isRowsFirstBipartite {D : DescribedNetwork VertexDesc} {r : ℕ}
-    (hD : D.IsRowsFirstBipartite r) (hM : 1 ≤ D.numEdges) : r ≤ D.vertices.length := by
-  by_contra h
-  have h1 := (hD.2 0 hM).2
-  rw [List.drop_of_length_le (by omega)] at h1
-  simp at h1
-
 /-- The cap of `nativeMk` leaves a tuple of weight below `p` unchanged, for positive weights. -/
 theorem map_min_of_mem_budgetTuples {ws : List ℕ} (hw : ∀ w ∈ ws, 0 < w) {p : ℕ} {β : List ℕ}
     (hβ : β ∈ BudgetTuples.budgetTuples ws p) : β.map (min · p) = β := by
@@ -97,7 +89,7 @@ theorem nativeMk_eq (hx : WF x) (ha : active x = true) {c : State} (hc : c ∈ c
       nativeChild x.fl (slots x) (level x ((nodes x).getD c.1 0)) (nodePrec x c.1)
         (node (slots x) ((nodes x).getD c.1 0)) ((points x).getD c.2.1 []) x.rows x.net
         (nativeParentPacking x.rows (slots x) x.net) c.2.2.1 c.2.2.2) := by
-  have hr := rows_le_of_isRowsFirstBipartite hx.2 (one_le_edges_of_active ha)
+  have hr := DescribedNetwork.rows_le_of_isRowsFirstBipartite hx.2 (one_le_edges_of_active ha)
   have hβ : c.2.2.1 ∈ BudgetTuples.budgetTuples (weights x c.1) (nodePrec x c.1) := by
     simp only [children, cursorList, nodeBlock, pointBlock, groupBlock, List.mem_flatMap,
       List.mem_range, List.mem_map] at hc
@@ -154,7 +146,7 @@ theorem stepCorrect_nativeMk : StepCorrect nativeMk WF := by
   simp only [active, decide_eq_true_eq] at ha'
   obtain ⟨-, hu, huM, hua, -, -, -⟩ := ha'
   have hlen : (points x).length = numPoints x := by simp [points]
-  have hr := rows_le_of_isRowsFirstBipartite hD (one_le_edges_of_active ha)
+  have hr := DescribedNetwork.rows_le_of_isRowsFirstBipartite hD (one_le_edges_of_active ha)
   refine NativeCall.val_recover_eq_contraction hirr hD hu huM hua (le_taperStep_mul hu)
     (taperStep_mul_le _ _ _) (pow_slots_le_edges_of_active ha) ?_ (points x)
     (pairwise_isUnit_points hirr ha)

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

@@ -67,6 +67,8 @@ vertices as rows (`NativeChild.isRowsFirstBipartite_nativeChild`).
 * `Cslib.Circuits.Frontier.NativeChild.contraction_nativeChild`: the native child has the
   contraction of the child.
 * `Cslib.Circuits.Frontier.NativeChild.isRowsFirstBipartite_nativeChild`: it is rows-first.
+* `Cslib.Circuits.Frontier.NativeChild.desc_of_mem_nativeChild`: its retained and packet
+  descriptors.
 
 ## References
 
@@ -1022,6 +1024,59 @@ end Child
 
 end Parent
 
+/-! ### The descriptors of the native children -/
+
+variable {D : DescribedNetwork VertexDesc} {r : ℕ}
+
+/-- **The descriptors of the native child.** A vertex of the native child of a rows-first parent
+with at least `64 ^ a` edges keeps the descriptor of a parent vertex, or is the packet `q`, with
+the packet context of `q`, the slice of `β` at `q`, and tags whose slots are below `2 ^ a` and
+distinct among its row ports. -/
+theorem desc_of_mem_nativeChild (hD : D.IsRowsFirstBipartite r) {fl : List ℕ} {a i : ℕ}
+    (hK : 64 ^ a ≤ D.numEdges) (hia : i < a) (pt : ℕ) (t : ℤ) (ζ β : List ℕ) (g : Fin 64)
+    {v : List ℕ × VertexDesc}
+    (hv : v ∈ (nativeChild fl a i pt t ζ r D (nativeParentPacking r a D) β g).vertices) :
+    (∃ w ∈ D.vertices, v.2 = w.2) ∨
+      ∃ q tags, v.2 = .inr (packetCtx fl a i pt t ζ g q, tags, betaSlice i pt β q) ∧
+        (∀ y ∈ tags, y.2 < 2 ^ a) ∧ ((tags.filter (·.1)).map (·.2)).Nodup := by
+  have hgroups := groupsOf_eq hD hK hia
+  have hpk1 : (nativeParentPacking r a D).2.1 = (parentPacking hD a).numPackets := by
+    rw [nativeParentPacking_eq hD hK]
+  have hpk2 : (nativeParentPacking r a D).2.2 = List.ofFn fun e =>
+      (((parentPacking hD a).packet e : ℕ), ((parentPacking hD a).slot e : ℕ)) := by
+    rw [nativeParentPacking_eq hD hK]
+  rw [nativeChild_eq hD _ (parentPacking hD a).packet (fun e => ((parentPacking hD a).slot e : ℕ))
+    g fl a i pt t ζ β _ hgroups hpk1 hpk2] at hv
+  simp only [List.mem_ofFn] at hv
+  obtain ⟨c, rfl⟩ := hv
+  rcases hc : (childVertexEquiv (P := (parentPacking hD a).numPackets)
+      (packingGroup (parentSide r) (parentPacking hD a) ⟨i, hia⟩) g).symm c with w | q
+  · left
+    refine ⟨D.vertices[(w.1 : ℕ)], List.getElem_mem _, ?_⟩
+    simp only [numberedDesc, Sum.elim_inl]
+  · right
+    simp only [numberedDesc, Sum.elim_inr]
+    refine ⟨q, _, rfl, ?_, ?_⟩
+    · intro y hy
+      simp only [List.mem_map] at hy
+      obtain ⟨e, -, rfl⟩ := hy
+      exact Fin.isLt _
+    · rw [List.filter_map, List.map_map]
+      refine List.Nodup.map_on ?_ ((nodup_packetPorts hD _ _ g q).filter _)
+      intro c₁ hc₁ c₂ hc₂ heq
+      simp only [List.mem_filter, Function.comp_apply] at hc₁ hc₂
+      obtain ⟨hm₁, hl₁⟩ := hc₁
+      obtain ⟨hm₂, hl₂⟩ := hc₂
+      rw [mem_packetPorts] at hm₁ hm₂
+      rcases c₁ with e₁ | e₁
+      · rcases c₂ with e₂ | e₂
+        · simp only [Function.comp_apply, Sum.elim_inl] at heq hm₁ hm₂
+          have hinj := (parentPacking hD a).injective (a₁ := e₁.1) (a₂ := e₂.1)
+            (Prod.ext (hm₁.trans hm₂.symm) (Fin.ext heq))
+          rw [Subtype.ext hinj]
+        · simp at hl₂
+      · simp at hl₁
+
 end NativeChild
 
 end Cslib.Circuits.Frontier

ComplexityTests/DescribedNetworkRows.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+import Complexity.Computability.Circuit.Frontier.TensorNetwork.DescribedLift
+
+/-! The row-count API works independently of the algorithm's vertex descriptors.
+The edge hypothesis matters: an edgeless network can have a vacuous oversized row prefix. -/
+
+namespace ComplexityTests.DescribedNetworkRows
+
+open Cslib.Circuits.Frontier
+
+private def edge : DescribedNetwork Unit := ⟨1, [([0], ()), ([0], ())]⟩
+
+example : 1 ≤ edge.vertices.length :=
+  DescribedNetwork.rows_le_of_isRowsFirstBipartite
+    (D := edge) (r := 1) (by decide) (by decide)
+
+example : (⟨0, []⟩ : DescribedNetwork Unit).IsRowsFirstBipartite 7 := by decide
+example : ¬7 ≤ (⟨0, []⟩ : DescribedNetwork Unit).vertices.length := by decide
+
+end ComplexityTests.DescribedNetworkRows