feat(circuit/frontier): direct-summation contraction modulo 2^P

Complexity.lean

@@ -868,6 +868,7 @@ 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.DirectContraction
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit
 public import Complexity.Computability.Circuit.Frontier.TwoSidedWitness
 public import Complexity.Computability.Circuit.Frontier.Unconditional

Complexity/Computability/GenericRAM/Native/BooleanFold.lean

@@ -26,7 +26,10 @@ The assignment list in the correctness specification is not constructed by the s
 
 This is the local Boolean-vector component of the enumeration in [OpenAI2026ETH], Lemma 3.2 and
 Proposition 3.4, pp. 22–26. It is not a mixed-radix or subset-pair enumerator, and gives no
-polynomial-time bound for a whole loop with exponentially many rounds.
+polynomial-time bound for a whole loop with exponentially many rounds. `certificate_bounds` gives
+the loop's explicit bounds instead: when the components are polynomial and every prefix keeps its
+accumulator polynomially bounded, the workspace is polynomial and the time is `2 ^ n + 1` times a
+polynomial.
 -/
 
 @[expose] public section
@@ -256,4 +259,100 @@ noncomputable def certificate {α : Type} {encIn : α ↪ List Bool}
       encIn (encPair encNat (encPair encUnary encB)) :=
   IndexFold.certificate (clock.comp cn) (cn.prod ci) (visitCertificate cb)
 
+/-- The clock is linear in the unary dimension. -/
+theorem clock_isPolynomial : clock.IsPolynomial := ⟨.self, .self⟩
+
+private theorem add_mul_le_mul_add {N X Y Y' : ℕ} (h : Y ≤ Y') :
+    X + (N + 1) * Y ≤ (N + 1) * (X + Y') := by
+  rw [Nat.mul_add]
+  exact Nat.add_le_add (Nat.le_mul_of_pos_left X (Nat.succ_pos N)) (Nat.mul_le_mul_left _ h)
+
+/-- **Explicit bounds of a streaming traversal.** Suppose the dimension, the initial state and
+the body have polynomial certificates, and every prefix keeps its accumulator within a polynomial
+bound `B` in the encoded input length. Then the traversal of all `2 ^ n` words, for `n` the
+dimension, uses polynomial workspace, and its time is `2 ^ n + 1` times a polynomial. The
+traversal count enters only the time. -/
+theorem certificate_bounds {α : Type} {encIn : α ↪ List Bool}
+    {dimension : α → ℕ} {initial : α → β} {body : (ℕ × List Bool) × β → β}
+    {cn : NativeCertificate dimension encIn encUnary}
+    {ci : NativeCertificate initial encIn encB}
+    {cb : NativeCertificate body (encPair (encPair encUnary encBits) encB) encB}
+    (hcn : cn.IsPolynomial) (hci : ci.IsPolynomial) (hcb : cb.IsPolynomial)
+    {B : α → ℕ} (hB : PolyBounded (fun a => (encIn a).length) B)
+    (hstate : ∀ a j, j ≤ 2 ^ dimension a →
+      (encB (runPrefix body (dimension a) j (initial a)).2.2).length ≤ B a) :
+    PolyBounded (fun a => (encIn a).length) (certificate cn ci cb).space ∧
+      ∃ T : α → ℕ, PolyBounded (fun a => (encIn a).length) T ∧
+        ∀ a, (certificate cn ci cb).time a ≤ (2 ^ dimension a + 1) * T a := by
+  let cstep := IndexFold.roundCertificate (visitCertificate cb)
+  have hcstep : cstep.IsPolynomial :=
+    IndexFold.roundCertificate_isPolynomial _ (visitCertificate_isPolynomial cb hcb)
+  obtain ⟨ct, dt, hct⟩ := hcstep.1.exists_le
+  obtain ⟨cs, ds, hcs⟩ := hcstep.2.exists_le
+  have hdim : PolyBounded (fun a => (encIn a).length) dimension := by
+    simpa only [encUnary_apply, List.length_replicate] using
+      (cn.polyTime hcn).polyBounded_length
+  -- Every live state: the binary index, the unary width and the accumulator.
+  let S := fun a => 4 * dimension a + 4 + B a
+  have hS : PolyBounded (fun a => (encIn a).length) S :=
+    (((PolyBounded.const 4).mul hdim).add (.const 4)).add hB
+  have hstateS (a : α) (j : ℕ) (hj : j ≤ 2 ^ dimension a) :
+      (encPair encNat (encPair encUnary encB)
+        ((IndexFold.step (visit body))^[j] (0, (dimension a, initial a)))).length ≤ S a :=
+    length_prefix_le body _ j _ _ hj (hstate a j hj)
+  have hmaxS (a : α) :
+      NativeCertificate.maxStateLength (encPair encNat (encPair encUnary encB))
+        (IndexFold.step (visit body)) (2 ^ dimension a) (0, (dimension a, initial a)) ≤ S a :=
+    NativeCertificate.maxStateLength_le _ _ _ _ (hstateS a)
+  have hmaxRT (a : α) :
+      NativeCertificate.maxRoundTime cstep (2 ^ dimension a) (0, (dimension a, initial a)) ≤
+        ct * (S a + 1) ^ dt :=
+    NativeCertificate.maxRoundTime_le cstep _ _ fun j hj => (hct _).trans
+      (Nat.mul_le_mul_left ct (Nat.pow_le_pow_left (by have := hstateS a j hj; omega) dt))
+  have hmaxRS (a : α) :
+      NativeCertificate.maxRoundSpace cstep (2 ^ dimension a) (0, (dimension a, initial a)) ≤
+        cs * (S a + 1) ^ ds :=
+    NativeCertificate.maxRoundSpace_le cstep _ _ fun j hj => (hcs _).trans
+      (Nat.mul_le_mul_left cs (Nat.pow_le_pow_left (by have := hstateS a j hj; omega) ds))
+  have htime (a : α) : (certificate cn ci cb).time a =
+      (cn.time a + (encUnary (dimension a)).length) +
+        ((encIn a).length + (cn.time a + ci.time a)) +
+        (2 ^ dimension a + 1) *
+          (NativeCertificate.maxRoundTime cstep (2 ^ dimension a) (0, (dimension a, initial a)) +
+            NativeCertificate.maxStateLength (encPair encNat (encPair encUnary encB))
+              (IndexFold.step (visit body)) (2 ^ dimension a) (0, (dimension a, initial a)) +
+            ((encNat (2 ^ dimension a)).length + 1) ^ 2) := rfl
+  have hspace (a : α) : (certificate cn ci cb).space a =
+      (cn.space a + (encUnary (dimension a)).length) +
+        ((encIn a).length + (cn.space a + ci.space a)) +
+        NativeCertificate.maxRoundSpace cstep (2 ^ dimension a) (0, (dimension a, initial a)) +
+        NativeCertificate.maxStateLength (encPair encNat (encPair encUnary encB))
+          (IndexFold.step (visit body)) (2 ^ dimension a) (0, (dimension a, initial a)) +
+        (encNat (2 ^ dimension a)).length := rfl
+  refine ⟨?_, fun a => 2 * cn.time a + dimension a + (encIn a).length + ci.time a +
+      (ct * (S a + 1) ^ dt + S a + (dimension a + 1 + 1) ^ 2), ?_, fun a => ?_⟩
+  · refine (((((((PolyBounded.const 2).mul hcn.2).add hdim).add .self).add hci.2).add
+      (NativeCertificate.polyBounded_pow_of_polyBounded hS cs ds)).add
+        (hS.add (hdim.add (.const 1)))).mono fun a => ?_
+    rw [hspace a]
+    simp only [encUnary_apply, List.length_replicate, length_clock]
+    have := hmaxRS a
+    have := hmaxS a
+    omega
+  · exact ((((((PolyBounded.const 2).mul hcn.1).add hdim).add .self).add hci.1).add
+      (((NativeCertificate.polyBounded_pow_of_polyBounded hS ct dt).add hS).add
+        (((hdim.add (.const 1)).add (.const 1)).pow 2)))
+  · have hY : NativeCertificate.maxRoundTime cstep (2 ^ dimension a)
+            (0, (dimension a, initial a)) +
+          NativeCertificate.maxStateLength (encPair encNat (encPair encUnary encB))
+            (IndexFold.step (visit body)) (2 ^ dimension a) (0, (dimension a, initial a)) +
+          ((encNat (2 ^ dimension a)).length + 1) ^ 2 ≤
+        ct * (S a + 1) ^ dt + S a + (dimension a + 1 + 1) ^ 2 := by
+      rw [length_clock]
+      exact Nat.add_le_add (Nat.add_le_add (hmaxRT a) (hmaxS a)) le_rfl
+    refine le_trans (le_of_eq ?_) (add_mul_le_mul_add (N := 2 ^ dimension a)
+      (X := 2 * cn.time a + dimension a + (encIn a).length + ci.time a) hY)
+    rw [htime a, encUnary_apply, List.length_replicate]
+    omega
+
 end Cslib.GenericRAM.BooleanFold

Complexity/Computability/GenericRAM/Native/ExhaustiveCountFallback.lean

@@ -207,11 +207,11 @@ noncomputable def countPredicateCertificate {pred : P → List Bool → Bool}
       ((NativeCertificate.linear (.of_eq fun _ => rfl)).prod (NativeCertificate.const 0))
       (NativeCertificate.ofPolyTime (computableInPolyTime_countStep hpred)))))
 
-private theorem length_prefix_state_le (pred : P → List Bool → Bool) (x : ℕ × P) {j : ℕ}
+private theorem length_prefix_accumulator_le (pred : P → List Bool → Bool) (x : ℕ × P) {j : ℕ}
     (hj : j ≤ 2 ^ x.1) :
-    (encPair encNat (encPair encUnary (encPair (encPair encUnary encP) encNat))
-      (BooleanFold.runPrefix (countStep pred) x.1 j (x, 0))).length ≤
-      7 * (encPair encUnary encP x).length + 6 := by
+    (encPair (encPair encUnary encP) encNat
+      (BooleanFold.runPrefix (countStep pred) x.1 j (x, 0)).2.2).length ≤
+      3 * (encPair encUnary encP x).length + 2 := by
   have hx_le : x.1 ≤ (encPair encUnary encP x).length := by
     simp only [length_encPair, encUnary_apply, List.length_replicate]
     omega
@@ -224,32 +224,9 @@ private theorem length_prefix_state_le (pred : P → List Bool → Bool) (x : 
       simpa [Nat.size_eq_bits_len] using Nat.size_le_size hz_le
     rw [BooleanFold.length_clock] at hm
     exact hm
-  have hacc_le :
-      (encPair (encPair encUnary encP) encNat
-        (BooleanFold.runPrefix (countStep pred) x.1 j (x, 0)).2.2).length ≤
-        3 * (encPair encUnary encP x).length + 2 := by
-    rw [length_encPair, prefix_payload_eq]
-    omega
-  have hpref := BooleanFold.length_prefix_le (countStep pred) x.1 j
-    (3 * (encPair encUnary encP x).length + 2) (x, 0) hj hacc_le
+  rw [length_encPair, prefix_payload_eq]
   omega
 
-private theorem roundCertificate_isPolynomial {β : Type} {encB : β ↪ List Bool}
-    {body : ℕ × β → β} (cb : NativeCertificate body (encPair encNat encB) encB)
-    (hcb : cb.IsPolynomial) :
-    (IndexFold.roundCertificate cb).IsPolynomial := by
-  have hsq : PolyBounded (fun p : ℕ × β => (encPair encNat encB p).length)
-      (fun p => ((encNat p.1).length + 1) ^ 2) :=
-    PolyBounded.of_forall_le 1 2 fun p => by
-      have hp1 : (encNat p.1).length ≤ (encPair encNat encB p).length := by
-        simp only [length_encPair]; omega
-      simpa only [one_mul] using Nat.pow_le_pow_left (Nat.add_le_add_right hp1 1) 2
-  have hlin : PolyBounded (fun p : ℕ × β => (encPair encNat encB p).length)
-      (fun p => (encNat p.1).length + 1) :=
-    PolyBounded.of_forall_le 1 1 fun p => by
-      simp only [length_encPair, pow_one, one_mul]; omega
-  exact ⟨(PolyBounded.self.add hsq).add hcb.1, (PolyBounded.self.add hlin).add hcb.2⟩
-
 private theorem countPredicateCertificate_bounds {pred : P → List Bool → Bool}
     (hpred : ComputableInPolyTime (fun q : P × List Bool => pred q.1 q.2) (encPair encP encBits)
       encBool) :
@@ -259,112 +236,14 @@ private theorem countPredicateCertificate_bounds {pred : P → List Bool → Boo
       PolyBounded (fun x : ℕ × P => (encPair encUnary encP x).length) P_ex ∧
       PolyBounded (fun x : ℕ × P => (encPair encUnary encP x).length) Q_ex ∧
       ∀ x : ℕ × P, (countPredicateCertificate hpred).time x ≤ (2 ^ x.1 + 1) * P_ex x + Q_ex x := by
-  let cb : NativeCertificate (countStep pred)
-      (encPair (encPair encUnary encBits) (encPair (encPair encUnary encP) encNat))
-      (encPair (encPair encUnary encP) encNat) :=
-    NativeCertificate.ofPolyTime (computableInPolyTime_countStep hpred)
-  have hcb : cb.IsPolynomial :=
-    NativeCertificate.ofPolyTime_isPolynomial (computableInPolyTime_countStep hpred)
-  let cstep := IndexFold.roundCertificate (BooleanFold.visitCertificate cb)
-  have hcstep : cstep.IsPolynomial :=
-    roundCertificate_isPolynomial (BooleanFold.visitCertificate cb)
-      (BooleanFold.visitCertificate_isPolynomial cb hcb)
-  obtain ⟨ct, dt, hct⟩ := hcstep.1.exists_le
-  obtain ⟨cs, ds, hcs⟩ := hcstep.2.exists_le
-  have hstate (x : ℕ × P) (j : ℕ) (hj : j ≤ 2 ^ x.1) :
-      (encPair encNat (encPair encUnary (encPair (encPair encUnary encP) encNat))
-        ((IndexFold.step (BooleanFold.visit (countStep pred)))^[j] (0, (x.1, (x, 0))))).length ≤
-        7 * (encPair encUnary encP x).length + 6 :=
-    length_prefix_state_le pred x hj
-  have hmaxS (x : ℕ × P) :
-      NativeCertificate.maxStateLength
-        (encPair encNat (encPair encUnary (encPair (encPair encUnary encP) encNat)))
-        (IndexFold.step (BooleanFold.visit (countStep pred)))
-        (2 ^ x.1) (0, (x.1, (x, 0))) ≤ 7 * (encPair encUnary encP x).length + 6 :=
-    NativeCertificate.maxStateLength_le _ _ (2 ^ x.1) _ (hstate x)
-  have hmaxRT (x : ℕ × P) :
-      NativeCertificate.maxRoundTime cstep (2 ^ x.1) (0, (x.1, (x, 0))) ≤
-        ct * (7 * (encPair encUnary encP x).length + 7) ^ dt :=
-    NativeCertificate.maxRoundTime_le cstep (2 ^ x.1) _ fun j hj =>
-      (hct _).trans (Nat.mul_le_mul_left ct
-        (Nat.pow_le_pow_left (by have := hstate x j hj; omega) dt))
-  have hmaxRS (x : ℕ × P) :
-      NativeCertificate.maxRoundSpace cstep (2 ^ x.1) (0, (x.1, (x, 0))) ≤
-        cs * (7 * (encPair encUnary encP x).length + 7) ^ ds :=
-    NativeCertificate.maxRoundSpace_le cstep (2 ^ x.1) _ fun j hj =>
-      (hcs _).trans (Nat.mul_le_mul_left cs
-        (Nat.pow_le_pow_left (by have := hstate x j hj; omega) ds))
-  have hx_le (x : ℕ × P) : x.1 ≤ (encPair encUnary encP x).length := by
-    simp only [length_encPair, encUnary_apply, List.length_replicate]; omega
-  have hB7 : PolyBounded (fun x : ℕ × P => (encPair encUnary encP x).length)
-      (fun x => 7 * (encPair encUnary encP x).length + 6) :=
-    ((PolyBounded.const 7).mul .self).add (.const 6)
-  have hSpace : PolyBounded (fun x : ℕ × P => (encPair encUnary encP x).length)
-      (countPredicateCertificate hpred).space := by
-    have hupper : PolyBounded (fun x : ℕ × P => (encPair encUnary encP x).length)
-        (fun x => 6 * (encPair encUnary encP x).length +
-          cs * (7 * (encPair encUnary encP x).length + 7) ^ ds +
-          (7 * (encPair encUnary encP x).length + 6) +
-          ((encPair encUnary encP x).length + 1)) :=
-      (((((PolyBounded.const 6).mul .self).add
-        (NativeCertificate.polyBounded_pow_of_polyBounded hB7 cs ds)).add hB7).add
-          (PolyBounded.self.add (.const 1)))
-    refine hupper.mono fun x => ?_
-    change (BooleanFold.clock.comp
-        (NativeCertificate.linear (ComputableInO.fst encUnary encP))).space x +
-      ((NativeCertificate.const 0).prod
-        ((NativeCertificate.linear (ComputableInO.fst encUnary encP)).prod
-          ((NativeCertificate.linear (.of_eq fun _ => rfl)).prod
-            (NativeCertificate.const 0)))).space x +
-      NativeCertificate.maxRoundSpace cstep (2 ^ x.1) (0, (x.1, (x, 0))) +
-      NativeCertificate.maxStateLength
-        (encPair encNat (encPair encUnary (encPair (encPair encUnary encP) encNat)))
-        (IndexFold.step (BooleanFold.visit (countStep pred))) (2 ^ x.1) (0, (x.1, (x, 0))) +
-      (encNat (2 ^ x.1)).length ≤ _
-    simp only [NativeCertificate.comp_space, NativeCertificate.linear_space,
-      NativeCertificate.prod_space, NativeCertificate.const_space, BooleanFold.clock,
-      encUnary_apply, List.length_replicate, BooleanFold.length_clock]
-    have h1 := hmaxRS x
-    have h2 := hmaxS x
-    have h3 := hx_le x
-    omega
-  refine ⟨hSpace, fun x => ct * (7 * (encPair encUnary encP x).length + 7) ^ dt +
-      (7 * (encPair encUnary encP x).length + 6) +
-      ((encPair encUnary encP x).length + 2) ^ 2,
-    fun x => 6 * (encPair encUnary encP x).length, ?_, (PolyBounded.const 6).mul .self, fun x => ?_⟩
-  · exact ((NativeCertificate.polyBounded_pow_of_polyBounded hB7 ct dt).add hB7).add
-      (NativeCertificate.polyBounded_pow_of_polyBounded (PolyBounded.self.add (.const 1)) 1 2
-        |>.mono fun x => by simp only [one_mul]; exact le_of_eq (by ring))
-  · change (BooleanFold.clock.comp
-        (NativeCertificate.linear (ComputableInO.fst encUnary encP))).time x +
-      ((NativeCertificate.const 0).prod
-        ((NativeCertificate.linear (ComputableInO.fst encUnary encP)).prod
-          ((NativeCertificate.linear (.of_eq fun _ => rfl)).prod
-            (NativeCertificate.const 0)))).time x +
-      (2 ^ x.1 + 1) * (NativeCertificate.maxRoundTime cstep (2 ^ x.1) (0, (x.1, (x, 0))) +
-        NativeCertificate.maxStateLength
-          (encPair encNat (encPair encUnary (encPair (encPair encUnary encP) encNat)))
-          (IndexFold.step (BooleanFold.visit (countStep pred))) (2 ^ x.1) (0, (x.1, (x, 0))) +
-        ((encNat (2 ^ x.1)).length + 1) ^ 2) ≤ _
-    simp only [NativeCertificate.comp_time, NativeCertificate.linear_time,
-      NativeCertificate.prod_time, NativeCertificate.const_time, BooleanFold.clock,
-      encUnary_apply, List.length_replicate, BooleanFold.length_clock]
-    have h1 := hmaxRT x
-    have h2 := hmaxS x
-    have h3 := hx_le x
-    have h4 : (x.1 + 1 + 1) ^ 2 ≤ ((encPair encUnary encP x).length + 2) ^ 2 :=
-      Nat.pow_le_pow_left (by omega) 2
-    have hmul :
-        (2 ^ x.1 + 1) * (NativeCertificate.maxRoundTime cstep (2 ^ x.1) (0, (x.1, (x, 0))) +
-          NativeCertificate.maxStateLength
-            (encPair encNat (encPair encUnary (encPair (encPair encUnary encP) encNat)))
-            (IndexFold.step (BooleanFold.visit (countStep pred)))
-            (2 ^ x.1) (0, (x.1, (x, 0))) + (x.1 + 1 + 1) ^ 2) ≤
-        (2 ^ x.1 + 1) * (ct * (7 * (encPair encUnary encP x).length + 7) ^ dt +
-          (7 * (encPair encUnary encP x).length + 6) +
-          ((encPair encUnary encP x).length + 2) ^ 2) :=
-      Nat.mul_le_mul_left _ (by omega)
-    omega
+  obtain ⟨hspace, T, hT, htime⟩ := BooleanFold.certificate_bounds
+    (NativeCertificate.linear_isPolynomial _)
+    (NativeCertificate.prod_isPolynomial _ _ (NativeCertificate.linear_isPolynomial _)
+      (NativeCertificate.const_isPolynomial _))
+    (NativeCertificate.ofPolyTime_isPolynomial (computableInPolyTime_countStep hpred))
+    (((PolyBounded.const 3).mul .self).add (.const 2))
+    fun x j hj => length_prefix_accumulator_le pred x hj
+  exact ⟨hspace, T, fun _ => 0, hT, .const 0, fun x => htime x⟩
 
 end StreamingCore
 

Complexity/Computability/GenericRAM/Native/IndexFold.lean

@@ -107,6 +107,23 @@ def roundCertificate {body : ℕ × β → β}
   space p := (encPair encNat encB p).length + ((encNat p.1).length + 1) + cb.space p
   computes := (ComputableInO.natSucc.comp (ComputableInO.fst encNat encB)).prod cb.computes
 
+/-- A polynomial callback gives a polynomial round: advancing the binary index costs a polynomial
+in its length. -/
+theorem roundCertificate_isPolynomial {body : ℕ × β → β}
+    (cb : NativeCertificate body (encPair encNat encB) encB) (hcb : cb.IsPolynomial) :
+    (roundCertificate cb).IsPolynomial := by
+  have hsq : PolyBounded (fun p : ℕ × β => (encPair encNat encB p).length)
+      (fun p => ((encNat p.1).length + 1) ^ 2) :=
+    PolyBounded.of_forall_le 1 2 fun p => by
+      have hp1 : (encNat p.1).length ≤ (encPair encNat encB p).length := by
+        simp only [length_encPair]; omega
+      simpa only [one_mul] using Nat.pow_le_pow_left (Nat.add_le_add_right hp1 1) 2
+  have hlin : PolyBounded (fun p : ℕ × β => (encPair encNat encB p).length)
+      (fun p => (encNat p.1).length + 1) :=
+    PolyBounded.of_forall_le 1 1 fun p => by
+      simp only [length_encPair, pow_one, one_mul]; omega
+  exact ⟨(PolyBounded.self.add hsq).add hcb.1, (PolyBounded.self.add hlin).add hcb.2⟩
+
 /-- One fixed native machine streams a runtime binary number of indices. Its bound is the
 existing iterator's trajectory-max bound; neither a finite state type nor a machine is selected
 separately for each runtime `n`. -/