feat(ThreeSum): prove conservative native subquadratic execution

Complexity.lean

@@ -84,6 +84,7 @@ public import Complexity.Algorithms.Reachability.Savitch
 public import Complexity.Algorithms.Sorting.Counting
 public import Complexity.Algorithms.ThreeSum.ArrayPacking
 public import Complexity.Algorithms.ThreeSum.ChanHe.Collisions
+public import Complexity.Algorithms.ThreeSum.ChanHe.ConvolutionSizes
 public import Complexity.Algorithms.ThreeSum.ChanHe.Defs
 public import Complexity.Algorithms.ThreeSum.ChanHe.FromNumbers
 public import Complexity.Algorithms.ThreeSum.ChanHe.Recursion
@@ -195,6 +196,7 @@ public import Complexity.Algorithms.WordRAM.ExactTriangle.Instances
 public import Complexity.Algorithms.WordRAM.ExactTriangle.MatrixSpec
 public import Complexity.Algorithms.WordRAM.ExactTriangle.ParameterSelecting
 public import Complexity.Algorithms.WordRAM.ExactTriangle.ParameterSelecting.Admission
+public import Complexity.Algorithms.WordRAM.ExactTriangle.ParameterSelecting.Asymptotics
 public import Complexity.Algorithms.WordRAM.ExactTriangle.ParameterSelecting.Callee
 public import Complexity.Algorithms.WordRAM.ExactTriangle.ParameterSelecting.Delivery
 public import Complexity.Algorithms.WordRAM.ExactTriangle.ParameterSelecting.Exec
@@ -562,6 +564,7 @@ public import Complexity.Algorithms.WordRAM.ThreeSum.Decision.Body
 public import Complexity.Algorithms.WordRAM.ThreeSum.Decision.Boundary
 public import Complexity.Algorithms.WordRAM.ThreeSum.Decision.Call
 public import Complexity.Algorithms.WordRAM.ThreeSum.Decision.Controls
+public import Complexity.Algorithms.WordRAM.ThreeSum.Decision.DyadicCost
 public import Complexity.Algorithms.WordRAM.ThreeSum.Decision.Execute
 public import Complexity.Algorithms.WordRAM.ThreeSum.Decision.Input
 public import Complexity.Algorithms.WordRAM.ThreeSum.Decision.Intermediates
@@ -570,6 +573,7 @@ public import Complexity.Algorithms.WordRAM.ThreeSum.Decision.Program
 public import Complexity.Algorithms.WordRAM.ThreeSum.Decision.Registers
 public import Complexity.Algorithms.WordRAM.ThreeSum.Decision.Reserve
 public import Complexity.Algorithms.WordRAM.ThreeSum.Decision.Scalar
+public import Complexity.Algorithms.WordRAM.ThreeSum.Decision.Subquadratic
 public import Complexity.Algorithms.WordRAM.ThreeSum.Decision.Width
 public import Complexity.Algorithms.WordRAM.ThreeSum.Fill
 public import Complexity.Algorithms.WordRAM.ThreeSum.Frontend
@@ -3536,6 +3540,7 @@ public import Complexity.Foundations.Data.Nat.Factorial
 public import Complexity.Foundations.Data.Nat.Fields
 public import Complexity.Foundations.Data.Nat.IntermediateValue
 public import Complexity.Foundations.Data.Nat.Log
+public import Complexity.Foundations.Data.Nat.LogRpow
 public import Complexity.Foundations.Data.Nat.Morton
 public import Complexity.Foundations.Data.Nat.OddMulMod
 public import Complexity.Foundations.Data.Nat.OfDigits

Complexity/Algorithms/ThreeSum/ChanHe/ConvolutionSizes.lean

@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.ThreeSum.ChanHe.ShiftedSizes
+
+/-!
+# Dimension and magnitude transfer to the actual convolution host
+
+The native host passes side `sqrt(8*mPar²)+1` to its Exact Triangle callee. Lower bounds
+on this actual side transfer original polynomial magnitudes to polynomial magnitudes in
+that callee dimension. Upper bounds retain the square-root scale and logarithmic factors.
+No output lengths or original inputs are replaced by padded values.
+
+## Main results
+
+* `input_lt_mPar_sq`: the candidate window dominates the original square-root dimension.
+* `input_lt_packed_side_sq`: the actual callee side is large enough for magnitude transfer.
+* `le_packed_side_of_sq_le`: explicit transport of eventual thresholds.
+* `packed_side_le`: explicit square-root times squared-logarithm side bound.
+* `packed_side_sq_le`: a linear-times-fourth-logarithm bound on squared side.
+* `packed_weight_le`: original polynomial filler remains polynomial in the actual side.
+
+These are original elementary consequences of the existing parameter definitions, for use
+by the charged ordinary-host composition. They assert no running-time or execution theorem.
+-/
+
+public section
+
+namespace Cslib.Algorithms.ThreeSum.ChanHe
+
+/-- Every magnitude parameter gives a candidate window larger than the input square root. -/
+theorem input_lt_mPar_sq (n U : ℕ) : n < mPar n U ^ 2 := by
+  have hb : 1 ≤ labelBits U := by unfold labelBits; omega
+  have hw : Nat.sqrt n + 1 ≤ wPar n U + 1 := by
+    unfold wPar
+    nlinarith
+  have hm : wPar n U + 1 ≤ mPar n U := by
+    unfold mPar
+    have h : 1 ≤ 2 * Nat.log 2 (wPar n U + 1) + 4 := by omega
+    exact Nat.le_mul_of_pos_right _ (by omega)
+  exact (Nat.lt_succ_sqrt' n).trans_le (Nat.pow_le_pow_left (hw.trans hm) 2)
+
+/-- The actual packed side, rather than a padded proxy, controls the original length. -/
+theorem input_lt_packed_side_sq (n U : ℕ) :
+    n < (Nat.sqrt (8 * mPar n U ^ 2) + 1) ^ 2 := by
+  have hm : mPar n U ≤ Nat.sqrt (8 * mPar n U ^ 2) :=
+    Nat.le_sqrt'.mpr (by omega)
+  exact (input_lt_mPar_sq n U).trans_le (Nat.pow_le_pow_left (by omega) 2)
+
+/-- An outer dimension threshold squared admits the same threshold at the actual callee side. -/
+theorem le_packed_side_of_sq_le {N n : ℕ} (h : N ^ 2 ≤ n) (U : ℕ) :
+    N ≤ Nat.sqrt (8 * mPar n U ^ 2) + 1 := by
+  have ht := input_lt_packed_side_sq n U
+  nlinarith
+
+/-- The host's actual Exact Triangle dimension is at most three times the candidate window,
+plus one, and hence retains its explicit square-root/logarithmic parameter estimate. -/
+theorem packed_side_le (κ n : ℕ) :
+    Nat.sqrt (8 * mPar n (2 * (n + 2) ^ κ) ^ 2) + 1 ≤
+      3 * ((5 * κ + 16) * (10 * κ + 40)) * (Nat.sqrt (n + 2) + 1) *
+        (Nat.log 2 (n + 2) + 1) ^ 2 + 1 := by
+  have hs : Nat.sqrt (8 * mPar n (2 * (n + 2) ^ κ) ^ 2) ≤
+      3 * mPar n (2 * (n + 2) ^ κ) := by
+    have h := Nat.sqrt_le' (8 * mPar n (2 * (n + 2) ^ κ) ^ 2)
+    nlinarith
+  have hm := mPar_shifted_pow_le n κ
+  nlinarith only [hs, Nat.mul_le_mul_left 3 hm]
+
+/-- Squaring the actual side removes the square root while preserving only a fixed fourth
+power of the logarithm. This is a bound on dimensions, not on any solver's running time. -/
+theorem packed_side_sq_le (κ n : ℕ) :
+    (Nat.sqrt (8 * mPar n (2 * (n + 2) ^ κ) ^ 2) + 1) ^ 2 ≤
+      4 * (3 * ((5 * κ + 16) * (10 * κ + 40)) + 1) ^ 2 * (n + 2) *
+        (Nat.log 2 (n + 2) + 1) ^ 4 := by
+  let A := (5 * κ + 16) * (10 * κ + 40)
+  let S := Nat.sqrt (n + 2) + 1
+  let L := Nat.log 2 (n + 2) + 1
+  have hunit : 1 ≤ S * L ^ 2 := by
+    have : 0 < S * L ^ 2 := by dsimp only [S, L]; positivity
+    omega
+  have hs := packed_side_le κ n
+  have ht : Nat.sqrt (8 * mPar n (2 * (n + 2) ^ κ) ^ 2) + 1 ≤
+      (3 * A + 1) * S * L ^ 2 := by
+    change _ ≤ 3 * A * S * L ^ 2 + 1 at hs
+    nlinarith only [hs, hunit]
+  have hS : S ^ 2 ≤ 4 * (n + 2) := by
+    have h := Nat.sqrt_le (n + 2)
+    have h' := Nat.sqrt_le_self (n + 2)
+    dsimp only [S]
+    nlinarith
+  calc
+    _ ≤ ((3 * A + 1) * S * L ^ 2) ^ 2 := Nat.pow_le_pow_left ht 2
+    _ = (3 * A + 1) ^ 2 * S ^ 2 * L ^ 4 := by ring
+    _ ≤ (3 * A + 1) ^ 2 * (4 * (n + 2)) * L ^ 4 := by gcongr
+    _ = _ := by dsimp only [A, L]; ring
+
+/-- The filler sent by the ordinary host is polynomial in its actual callee dimension,
+including lengths zero and one. This bridges the caller's original magnitude convention
+without a separate runtime magnitude certificate. -/
+theorem packed_weight_le (κ E n : ℕ) :
+    2 * (n + 2) ^ E + 1 ≤
+      (Nat.sqrt (8 * mPar n (2 * (n + 2) ^ κ) ^ 2) + 3) ^ (2 * E + 2) := by
+  let t := Nat.sqrt (8 * mPar n (2 * (n + 2) ^ κ) ^ 2) + 1
+  have hn : n < t ^ 2 := input_lt_packed_side_sq n _
+  have hb : 2 ≤ t + 2 := by omega
+  have hp : n + 2 ≤ (t + 2) ^ 2 := by nlinarith
+  have hpow : (n + 2) ^ E ≤ (t + 2) ^ (2 * E) :=
+    (Nat.pow_le_pow_left hp E).trans_eq (by rw [← pow_mul])
+  have hunit : 1 ≤ (t + 2) ^ (2 * E) := Nat.one_le_pow _ _ (by omega)
+  change 2 * (n + 2) ^ E + 1 ≤ (t + 2) ^ (2 * E + 2)
+  rw [pow_add]
+  have hb2 : 3 ≤ (t + 2) ^ 2 := by nlinarith
+  nlinarith only [hpow, hunit, Nat.mul_le_mul_left ((t + 2) ^ (2 * E)) hb2]
+
+end Cslib.Algorithms.ThreeSum.ChanHe

Complexity/Algorithms/ThreeSum/ChanHe/ShiftedSizes.lean

@@ -20,6 +20,7 @@ bounds are compared with the existing estimates at `n+2`.
 
 * `mPar_mono_input`: candidate bounds are monotone in input length.
 * `mPar_shifted_pow_le`: square-root times squared-logarithm bound for the actual native modulus.
+* `shifted_count_bound_le`: degree-seven bound on the native count allowance.
 * `length_instances_shifted_pow_le`: degree-seven logarithmic instance count at every length.
 * `packed_length_shifted_pow_le`: linear times fourth-logarithm common packed length.
 
@@ -44,23 +45,27 @@ theorem mPar_shifted_pow_le (n κ : ℕ) :
         (Nat.log 2 (n + 2) + 1) ^ 2 :=
   (mPar_mono_input (show n ≤ n + 2 by omega) _).trans (mPar_pow_le (n + 2) κ)
 
-/-- The unchanged actual finite instance list has a logarithmic count even at lengths zero/one. -/
-theorem length_instances_shifted_pow_le (n κ : ℕ) (x : Fin n → ℤ) :
-    (instances n ((n + 2) ^ κ) x).length ≤ numBound κ (n + 2) := by
+/-- The explicit native count allowance itself is bounded, independently of any list. -/
+theorem shifted_count_bound_le (n κ : ℕ) :
+    (2 * labelBits (2 * (n + 2) ^ κ) ^ 2 + 2) * (2 * Nat.log 2 n + 2) ^ 5 ≤
+      numBound κ (n + 2) := by
   have hlog : 1 ≤ Nat.log 2 (n + 2) := Nat.log_pos (by decide) (by omega)
   have hΛ : labelBits (2 * (n + 2) ^ κ) ≤ (κ + 2) * (Nat.log 2 (n + 2) + 1) :=
     (labelBits_pow_le (n + 2) κ).trans (by rw [add_mul]; omega)
   have hone : 1 ≤ ((κ + 2) * (Nat.log 2 (n + 2) + 1)) ^ 2 :=
     Nat.one_le_pow _ _ (by positivity)
   have hn : Nat.log 2 n ≤ Nat.log 2 (n + 2) := Nat.log_mono_right (by omega)
-  calc (instances n ((n + 2) ^ κ) x).length
-      ≤ (2 * labelBits (2 * (n + 2) ^ κ) ^ 2 + 2) * (2 * Nat.log 2 n + 2) ^ 5 :=
-        length_instances_le ..
-    _ ≤ (2 * ((κ + 2) * (Nat.log 2 (n + 2) + 1)) ^ 2 +
+  calc (2 * labelBits (2 * (n + 2) ^ κ) ^ 2 + 2) * (2 * Nat.log 2 n + 2) ^ 5
+      ≤ (2 * ((κ + 2) * (Nat.log 2 (n + 2) + 1)) ^ 2 +
         2 * ((κ + 2) * (Nat.log 2 (n + 2) + 1)) ^ 2) *
           (2 * Nat.log 2 (n + 2) + 2) ^ 5 := by gcongr; omega
     _ = numBound κ (n + 2) := by unfold numBound; ring
 
+/-- The unchanged actual finite instance list has a logarithmic count even at lengths zero/one. -/
+theorem length_instances_shifted_pow_le (n κ : ℕ) (x : Fin n → ℤ) :
+    (instances n ((n + 2) ^ κ) x).length ≤ numBound κ (n + 2) :=
+  (length_instances_le ..).trans (shifted_count_bound_le n κ)
+
 /-- The unchanged common packed length is bounded by the old estimate evaluated at `n+2`. -/
 theorem packed_length_shifted_pow_le (κ n : ℕ) :
     8 * mPar n (2 * (n + 2) ^ κ) ^ 2 ≤

Complexity/Algorithms/WordRAM/ExactTriangle/ParameterSelecting/Asymptotics.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.ExactTriangle.ParameterSelecting.Callee
+
+/-!
+# Strict-subcubic time of the actual parameter-selecting ET callee
+
+The concrete host interface selects the real fast branch beyond a fixed threshold. Its
+content-independent time field is then the already proved natural dyadic allowance. The
+threshold is chosen before all original weight bounds, matrices, layout and physical width.
+
+## Main results
+
+* `exists_time_subcubic_bound`: the actual callee time field is uniformly strict-subcubic
+  for polynomial original weights. The callee's unconditional semantics still use the real
+  exhaustive branch at smaller dimensions.
+
+This original composition does not assume a fast solver, supplied time law or selected prime.
+It does not yet bound the repeated ordinary 3SUM host calls or prove the tuned 1.9992 endpoint.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.ParameterSelecting
+
+open Cslib.Algorithms.ExactTriangle
+
+-- Normalize only the existing fixed fast-threshold numeral while transporting its bound.
+set_option exponentiation.threshold 1296 in
+/-- A single coefficient and dimension threshold per weight exponent bound the actual
+Host.Callee time field, uniformly before every admitted original magnitude. -/
+theorem exists_time_subcubic_bound {κ : ℕ} (hκ : 1 ≤ κ) :
+    ∃ C : ℝ, 0 < C ∧ ∃ N : ℕ, 2 ^ 1296 ≤ N ∧
+      ∀ n ≥ N, ∀ F ≤ (n + 2) ^ κ,
+        (callee.time n F : ℝ) ≤ C * (n : ℝ) ^ (3 - 1 / 1296 : ℝ) := by
+  obtain ⟨C, hC, N, hN, ht⟩ := CallableFixedPrime.exists_dyadicTime_subcubic_bound hκ
+  refine ⟨C, hC, N, hN, ?_⟩
+  intro n hn F hF
+  rw [callee_time, callerTime, ite_eq_left ((ParameterChoice.blocks_pos_iff n).mpr (hN.trans hn))]
+  exact ht n hn F hF
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.ParameterSelecting

Complexity/Algorithms/WordRAM/ExactTriangle/ParameterSelecting/Callee.lean

@@ -80,6 +80,16 @@ noncomputable def callee : ThreeSum.Host.Callee 633 where
     change y.regs Reg.result ≤ 1
     rcases hf with h | h <;> omega
 
+/-- The concrete host interface uses the proved original-input allowance. This projection
+lemma lets asymptotic clients inspect the time field without exposing the whole certificate. -/
+theorem callee_time (n F : ℕ) : callee.time n F = callerTime n F := by
+  simp only [callee]
+
+/-- The actual fixed logarithmic admission coefficient, available without unfolding the
+semantic execution certificate. -/
+theorem callee_widthCoefficient : callee.widthCoefficient = 123357 := by
+  simp only [callee]
+
 /-- Every admitted initialized run has the same original-scalar time allowance as the host
 callee. Prefix, verdict, restored arguments and charged halt refer to the same final state. -/
 theorem runs_input_uniform {W n F : ℕ} (values : List ℤ)