feat(CountingSimulation): Theorem D.1 for entry procedures (#1538 E1.3)

Complexity.lean

@@ -937,6 +937,8 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Deformatio
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DescribedContraction
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DescribedLift
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DirectContraction
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.EntryContraction
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.EntryContractionMachine
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContraction
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionDerivation
@@ -962,6 +964,7 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.PacketTerm
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Recursion
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ReductionLift
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Reindex
+public import Complexity.Computability.Circuit.Frontier.TensorNetwork.RowsFirstPolyTime
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Schedule
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ScheduleCount
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ScheduledRecursion
@@ -1165,6 +1168,7 @@ public import Complexity.Computability.Complexity.Classes.CountingSimulation.Blo
 public import Complexity.Computability.Complexity.Classes.CountingSimulation.Containments
 public import Complexity.Computability.Complexity.Classes.CountingSimulation.Count
 public import Complexity.Computability.Complexity.Classes.CountingSimulation.CountingClasses
+public import Complexity.Computability.Complexity.Classes.CountingSimulation.EntryAnalysis
 public import Complexity.Computability.Complexity.Classes.CountingSimulation.FastAlgorithm
 public import Complexity.Computability.Complexity.Classes.CountingSimulation.FastAnalysis
 public import Complexity.Computability.Complexity.Classes.CountingSimulation.FastLeaves

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

@@ -28,6 +28,10 @@ fields are bounded (`FastContraction.PacketBound`). It passes to the native chil
 at most `p + 40 m²` since `2 ^ a ≤ m`, and it adds at most `M (2 ^ a) ^ 12 ≤ m²` packet vertices
 (`NativeChild.numPackets_nativeParentPacking_le`).
 
+**Root descriptors** keep their number of ports along the recursion
+(`FastContraction.Reach.exists_root_of_inl`), since the native child renumbers the ports of the
+vertices it keeps (`NativeChild.exists_mem_of_mem_nativeChild_inl`).
+
 ## Main definitions
 
 * `Cslib.Circuits.Frontier.FastContraction.PacketBound`: the bounded packet descriptors.
@@ -38,6 +42,8 @@ at most `p + 40 m²` since `2 ^ a ≤ m`, and it adds at most `M (2 ^ a) ^ 12 
 * `Cslib.Circuits.Frontier.FastContraction.Shape.child`: the invariant passes to the native
   children.
 * `Cslib.Circuits.Frontier.FastContraction.Reach.shape`: every reached call satisfies it.
+* `Cslib.Circuits.Frontier.FastContraction.Reach.exists_root_of_inl`: root descriptors keep their
+  number of ports.
 
 ## References
 
@@ -315,4 +321,17 @@ theorem Reach.shape (h₀s : x₀.scale = x₀.edges) (h₀b : x₀.bound + x₀
 
 end Child
 
+/-- **Root descriptors keep their number of ports along the recursion**: every root descriptor of a
+call reached by the native child builder is the descriptor of a vertex of the root with as many
+ports. -/
+theorem Reach.exists_root_of_inl {x₀ x : Call T} (h : Reach nativeMk x₀ x)
+    {v : List ℕ × VertexDesc T} (hv : v ∈ x.net.vertices) {t : T} (ht : v.2 = .inl t) :
+    ∃ w ∈ x₀.net.vertices, w.2 = .inl t ∧ w.1.length = v.1.length := by
+  induction h generalizing v with
+  | root => exact ⟨v, hv, ht, rfl⟩
+  | step c _ _ _ ih =>
+    obtain ⟨u, hu, hut, hlen⟩ := NativeChild.exists_mem_of_mem_nativeChild_inl hv ht
+    obtain ⟨w, hw, hwt, hwlen⟩ := ih hu hut
+    exact ⟨w, hw, hwt, hwlen.trans hlen⟩
+
 end Cslib.Circuits.Frontier.FastContraction

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

@@ -69,6 +69,8 @@ vertices as rows (`NativeChild.isRowsFirstBipartite_nativeChild`).
 * `Cslib.Circuits.Frontier.NativeChild.isRowsFirstBipartite_nativeChild`: it is rows-first.
 * `Cslib.Circuits.Frontier.NativeChild.desc_of_mem_nativeChild`: its retained and packet
   descriptors.
+* `Cslib.Circuits.Frontier.NativeChild.exists_mem_of_mem_nativeChild_inl`: a retained vertex keeps
+  its number of ports.
 
 ## References
 
@@ -1081,6 +1083,20 @@ theorem desc_of_mem_nativeChild (hD : D.IsRowsFirstBipartite r) {fl : List ℕ}
         · simp at hl₂
       · simp at hl₁
 
+/-- **A kept vertex of the native child keeps its descriptor and its number of ports**: every root
+descriptor of the native child is the descriptor of a parent vertex with as many ports. -/
+theorem exists_mem_of_mem_nativeChild_inl {fl : List ℕ} {a i pt : ℕ} {τ : ℤ} {ζ : List ℕ}
+    {pk : (List (List ℕ) × List (List ℕ)) × ℕ × List (ℕ × ℕ)} {β : List ℕ} {g : ℕ}
+    {v : List ℕ × VertexDesc T} (hv : v ∈ (nativeChild fl a i pt τ ζ r D pk β g).vertices)
+    {t : T} (ht : v.2 = .inl t) :
+    ∃ u ∈ D.vertices, u.2 = .inl t ∧ u.1.length = v.1.length := by
+  simp only [nativeChild, List.mem_append, List.mem_map, List.mem_filter, List.mem_range] at hv
+  rcases hv with ⟨k, ⟨hk, -⟩, rfl⟩ | ⟨q, -, rfl⟩
+  · refine ⟨D.vertices[k], List.getElem_mem hk, ?_, ?_⟩
+    · simpa only [List.getD_eq_getElem _ _ hk] using ht
+    · simp only [List.length_map, List.getD_eq_getElem _ _ hk]
+  · cases ht
+
 end NativeChild
 
 end Cslib.Circuits.Frontier

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

@@ -0,0 +1,136 @@
+/-
+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.DescribedContraction
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryPrimitives
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeNatFrontends
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimePrimitives
+
+/-!
+# Rows-first bipartiteness in polynomial time
+
+Rows-first bipartiteness of a described network at a number of rows
+(`DescribedNetwork.IsRowsFirstBipartite`) is decidable in polynomial time, from the number of rows
+in binary and the network as encoded by `DescribedNetwork.encDescribed`. The test checks that every
+port names an edge and counts, for each edge, its ports among the first `r` vertices and among the
+others. It is the rows-first part of the guards of the contraction machines, for explicit networks
+and for entry procedures.
+
+## Main results
+
+* `Cslib.Circuits.Frontier.DescribedNetwork.rowsFirst_polyTime`: rows-first bipartiteness is
+  decidable in polynomial time.
+-/
+
+public section
+
+namespace Cslib.Circuits.Frontier.DescribedNetwork
+
+open Turing.MultiTapeTM
+
+variable {T : Type} {encT : T ↪ List Bool}
+
+/-- Rows-first bipartiteness as a conjunction of list tests. -/
+private def rowsTest (r : ℕ) (d : DescribedNetwork T) : Bool :=
+  d.vertices.all (fun v => v.1.all fun i => decide (i < d.numEdges)) &&
+    (List.range d.numEdges).all (fun i =>
+      decide (((d.vertices.take r).flatMap Prod.fst).count i = 1) &&
+        decide (((d.vertices.drop r).flatMap Prod.fst).count i = 1))
+
+private theorem decide_eq_rowsTest (r : ℕ) (d : DescribedNetwork T) :
+    decide (d.IsRowsFirstBipartite r) = rowsTest r d := by
+  refine Bool.eq_iff_iff.mpr ?_
+  simp only [rowsTest, IsRowsFirstBipartite, decide_eq_true_eq, Bool.and_eq_true,
+    List.all_eq_true, List.mem_range, List.count_flatMap, Function.comp_def]
+
+/-- Taking or dropping `min |l| r` elements is taking or dropping `r`. -/
+private theorem take_drop_min {α : Type} (l : List α) (r : ℕ) :
+    l.take (min l.length r) = l.take r ∧ l.drop (min l.length r) = l.drop r := by
+  rcases le_total l.length r with hle | hle
+  · rw [min_eq_left hle, List.take_length, List.take_of_length_le hle, List.drop_length,
+      List.drop_of_length_le hle]
+    exact ⟨rfl, rfl⟩
+  · rw [min_eq_right hle]
+    exact ⟨rfl, rfl⟩
+
+/-- **Rows-first bipartiteness is decidable in polynomial time**, from the number of rows and the
+network. -/
+theorem rowsFirst_polyTime :
+    ComputableInPolyTime
+      (fun ((r, d) : ℕ × DescribedNetwork T) => decide (d.IsRowsFirstBipartite r))
+      (encPair encNat (encDescribed encT)) encBool := by
+  have hr := ComputableInPolyTime.fst encNat (encDescribed encT)
+  have hm : ComputableInPolyTime (fun G : ℕ × DescribedNetwork T => G.2.numEdges)
+      (encPair encNat (encDescribed encT)) encUnary :=
+    numEdges_polyTime.comp (ComputableInPolyTime.snd _ _)
+  have hvs : ComputableInPolyTime (fun G : ℕ × DescribedNetwork T => G.2.vertices)
+      (encPair encNat (encDescribed encT)) (encList (encPair (encList encNat) encT)) :=
+    vertices_polyTime.comp (ComputableInPolyTime.snd _ _)
+  -- Ports in range.
+  have h1 : ComputableInPolyTime (fun G : ℕ × DescribedNetwork T =>
+      G.2.vertices.all (fun v => v.1.all fun i => decide (i < G.2.numEdges)))
+      (encPair encNat (encDescribed encT)) encBool := by
+    refine ComputableInPolyTime.allWithInput hvs ?_
+    refine ComputableInPolyTime.allWithInput
+      ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _)) ?_
+    exact ComputableInPolyTime.binary_lt.comp ((ComputableInPolyTime.snd _ _).prod
+      (ComputableInPolyTime.unary_to_binary.comp (hm.comp ((ComputableInPolyTime.fst _ _).comp
+        (ComputableInPolyTime.fst _ _)))))
+  -- Each edge has one row port and one column port.
+  have hlen := (ComputableInPolyTime.length_list _).comp hvs
+  have hcap := ComputableInPolyTime.binary_min_unary' hlen hr
+  have htake : ComputableInPolyTime (fun G : ℕ × DescribedNetwork T =>
+      G.2.vertices.take (min G.2.vertices.length G.1)) (encPair encNat (encDescribed encT))
+      (encList (encPair (encList encNat) encT)) :=
+    .of_tidy (ComputableTidilyInPolyTime.listTakeWithInput hvs.tidy hcap.tidy)
+  have hdrop : ComputableInPolyTime (fun G : ℕ × DescribedNetwork T =>
+      G.2.vertices.drop (min G.2.vertices.length G.1)) (encPair encNat (encDescribed encT))
+      (encList (encPair (encList encNat) encT)) :=
+    .of_tidy (ComputableTidilyInPolyTime.listDropWithInput hvs.tidy hcap.tidy)
+  have hflat {l : ℕ × DescribedNetwork T → List (List ℕ × T)}
+      (hl : ComputableInPolyTime l (encPair encNat (encDescribed encT))
+        (encList (encPair (encList encNat) encT))) :
+      ComputableInPolyTime (fun G => (l G).flatMap Prod.fst) (encPair encNat (encDescribed encT))
+        (encList encNat) :=
+    ComputableInPolyTime.flatMapWithInput (f := fun _ v => v.1) hl
+      ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _))
+  have hcount {l : ℕ × DescribedNetwork T → List ℕ}
+      (hl : ComputableInPolyTime l (encPair encNat (encDescribed encT)) (encList encNat)) :
+      ComputableInPolyTime (fun p : (ℕ × DescribedNetwork T) × ℕ =>
+        decide ((l p.1).count p.2 = 1))
+        (encPair (encPair encNat (encDescribed encT)) encUnary) encBool := by
+    have hc := ComputableInPolyTime.countPWithInput (test := fun p a => decide (a = p.2))
+      (hl.comp (ComputableInPolyTime.fst (encPair encNat (encDescribed encT)) encUnary))
+      (ComputableInPolyTime.decide_eq' (ComputableInPolyTime.snd _ _)
+        (ComputableInPolyTime.unary_to_binary.comp ((ComputableInPolyTime.snd _ _).comp
+          (ComputableInPolyTime.fst _ _))))
+    refine (ComputableInPolyTime.decide_eq' hc (ComputableInPolyTime.const 1)).of_enc_eq
+      fun p => ?_
+    simp only [Function.comp_apply, List.count_eq_countP]
+    congr 3
+  have h2 : ComputableInPolyTime (fun G : ℕ × DescribedNetwork T =>
+      (List.range G.2.numEdges).all (fun i =>
+        decide (((G.2.vertices.take (min G.2.vertices.length G.1)).flatMap Prod.fst).count i =
+          1) &&
+          decide (((G.2.vertices.drop (min G.2.vertices.length G.1)).flatMap Prod.fst).count i =
+            1))) (encPair encNat (encDescribed encT)) encBool :=
+    ComputableInPolyTime.allWithInput (ComputableInPolyTime.range.comp hm)
+      (ComputableInPolyTime.bool_and.comp ((hcount (hflat htake)).prod (hcount (hflat hdrop))))
+  refine (ComputableInPolyTime.bool_and.comp (h1.prod h2)).of_enc_eq fun ⟨r, d⟩ => ?_
+  obtain ⟨ht, hdr⟩ := take_drop_min d.vertices r
+  dsimp only
+  rw [decide_eq_rowsTest, rowsTest]
+  simp only [Function.comp_apply, ht, hdr]
+
+end Cslib.Circuits.Frontier.DescribedNetwork

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

@@ -32,7 +32,8 @@ p. 64).
 * Labels have `a_d = 2 ∑_{j ≤ d} u_j` coordinates (`slotBits`), packets `L = 2 ^ a_d` slots, and
   there are `D_arr = 64 ^ (2 a_d)` pairs of labels (`r = 64`).
 * The degree bound is `Δ = 2 ^ (⌊9 λ / 10⌋ + 2)` (`degreeBound`), a power of two that is at least
-  `s ^ (9/10)` (`pow_nine_le_degreeBound_pow_ten`) and at most `2 ^ 20 s ^ 9` in tenth power.
+  `s ^ (9/10)` (`pow_nine_le_degreeBound_pow_ten`) and at most `2 ^ 20 s ^ 9` in tenth power,
+  and monotone in `s` (`degreeBound_mono`).
 * The node `t` of valuation `i` is recovered from its children at precision
   `p_t = p + 8 h 2 ^ (a - i) + 8 M (a + 1)` (`nodePrecision`), as in Lemma D.5, where
   `D_t = L / 2 ^ i`.
@@ -209,6 +210,10 @@ theorem degreeBound_pow_ten_le {s : ℕ} (hs : s ≠ 0) : degreeBound s ^ 10 ≤
     _ = 2 ^ 20 * (2 ^ Nat.log 2 s) ^ 9 := by rw [← pow_mul, ← pow_add]; ring_nf
     _ ≤ 2 ^ 20 * s ^ 9 := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left h2 9)
 
+/-- **The degree bound is monotone.** -/
+theorem degreeBound_mono {a b : ℕ} (h : a ≤ b) : degreeBound a ≤ degreeBound b :=
+  Nat.pow_le_pow_right (by norm_num) (by have := Nat.log_mono_right (b := 2) h; omega)
+
 /-- **The precision bound** of (D.11), `p ≤ s λ^{O(1)} 2 ^ (a_{d - 1})`:
 `precisionBound C s d ≤ C s 2 ^ (a_{d - 1}) (1 + d (8 λ + 40))`. -/
 theorem precisionBound_le (C s d : ℕ) :