diff --git a/Complexity.lean b/Complexity.lean index 84615f7149..85815932c5 100644 --- a/Complexity.lean +++ b/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 diff --git a/Complexity/Algorithms/ThreeSum/ChanHe/ConvolutionSizes.lean b/Complexity/Algorithms/ThreeSum/ChanHe/ConvolutionSizes.lean new file mode 100644 index 0000000000..994acc02ca --- /dev/null +++ b/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 diff --git a/Complexity/Algorithms/ThreeSum/ChanHe/ShiftedSizes.lean b/Complexity/Algorithms/ThreeSum/ChanHe/ShiftedSizes.lean index adb73ffd09..a87a8daecf 100644 --- a/Complexity/Algorithms/ThreeSum/ChanHe/ShiftedSizes.lean +++ b/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 ≤ diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/ParameterSelecting/Asymptotics.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/ParameterSelecting/Asymptotics.lean new file mode 100644 index 0000000000..f5d6e1ab2e --- /dev/null +++ b/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 diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/ParameterSelecting/Callee.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/ParameterSelecting/Callee.lean index 60c639ca50..bfaeb5a029 100644 --- a/Complexity/Algorithms/WordRAM/ExactTriangle/ParameterSelecting/Callee.lean +++ b/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 ℤ) diff --git a/Complexity/Algorithms/WordRAM/ThreeSum/Decision/DyadicCost.lean b/Complexity/Algorithms/WordRAM/ThreeSum/Decision/DyadicCost.lean new file mode 100644 index 0000000000..8a4b9cbd86 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ThreeSum/Decision/DyadicCost.lean @@ -0,0 +1,243 @@ +/- +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.ThreeSum.Decision.Execute +public import Complexity.Algorithms.ThreeSum.ChanHe.ConvolutionSizes +public import Complexity.Foundations.Data.Nat.LogRpow +public import Complexity.Algorithms.WordRAM.ExactTriangle.ParameterSelecting.Asymptotics + +/-! +# Complete conservative runtime composition for the ordinary native host + +The original host supplies magnitude `2*(n+2)^E+1` at actual side `sqrt(8*mPar²)+1`. +Finite dimension bounds transfer this magnitude to a polynomial in that side. The actual +parameter-selecting callee, native preprocessing, catalogue count, matrix construction and +all call/control reserves are then charged at those original arguments. + +## Main results + +* `packed_side_eventually_le_rpow`: the actual side is below every power above square root. +* `instanceBound_le_numBound`, `instanceBound_eventually_le_rpow`: polylogarithmic native count. +* `callerTime_add_twelve_le`: full Convolution caller work plus its outer control reserve. +* `exists_packed_calleeTime_bound`: the real callee time at actual dimension and magnitude. +* `exists_cost_subquadratic_bound`: complete charged host budget is `Oκ(n^(2−1/5184))`. + +This original conservative analysis uses the real native callee, not a supplied time law. +Actual initialized execution is composed in the consumer theorem. It does not prove the +source's tuned exponent 1.9992. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ThreeSum.Decision + +open Cslib.Algorithms.ThreeSum.ChanHe +open Cslib.Algorithms.WordRAM.ExactTriangle + +open Filter + +/-- The exact packed side grows more slowly than every fixed power strictly above square +root. All coefficients and logarithmic factors are absorbed before the varying outer input. -/ +theorem packed_side_eventually_le_rpow (κ : ℕ) {ε : ℝ} (hε : 0 < ε) : + ∀ᶠ n : ℕ in atTop, + (Nat.sqrt (8 * mPar n (2 * (n + 2) ^ κ) ^ 2) + 1 : ℕ) ≤ + (n : ℝ) ^ (1 / 2 + ε : ℝ) := by + let A := (5 * κ + 16) * (10 * κ + 40) + have he := Nat.eventually_mul_log_add_pow_le_rpow (by decide : 1 < (2 : ℕ)) + 2 1 4 (K := (8 * (3 * A + 1) ^ 2 : ℕ)) (by positivity) (by positivity : 0 < 2 * ε) + filter_upwards [he, eventually_ge_atTop (2 : ℕ)] with n hlog hn + let t := Nat.sqrt (8 * mPar n (2 * (n + 2) ^ κ) ^ 2) + 1 + have hns : n + 2 ≤ 2 * n := by omega + have hs := packed_side_sq_le κ n + have hs' : t ^ 2 ≤ 8 * (3 * A + 1) ^ 2 * n * (Nat.log 2 (n + 2) + 1) ^ 4 := by + have hm := Nat.mul_le_mul_right ((Nat.log 2 (n + 2) + 1) ^ 4) + (Nat.mul_le_mul_left (4 * (3 * A + 1) ^ 2) hns) + change t ^ 2 ≤ 4 * (3 * A + 1) ^ 2 * (n + 2) * _ at hs + exact hs.trans (hm.trans_eq (by ring)) + have hsR := (Nat.cast_le (α := ℝ)).mpr hs' + have hmul := mul_le_mul_of_nonneg_left hlog (show (0 : ℝ) ≤ n by positivity) + have hexp : (n : ℝ) * (n : ℝ) ^ (2 * ε) = (n : ℝ) ^ (1 + 2 * ε) := by + rw [Real.rpow_add (by positivity), Real.rpow_one] + have hsq : (t : ℝ) ^ 2 ≤ (n : ℝ) ^ (1 + 2 * ε) := by + push_cast at hsR hmul + rw [hexp] at hmul + nlinarith only [hsR, hmul] + have hroot : ((n : ℝ) ^ (1 / 2 + ε : ℝ)) ^ 2 = + (n : ℝ) ^ (1 + 2 * ε) := by + rw [← Real.rpow_natCast, ← Real.rpow_mul (by positivity)] + congr 1 + ring + have ht0 : (0 : ℝ) ≤ t := by positivity + have hr0 : (0 : ℝ) ≤ (n : ℝ) ^ (1 / 2 + ε : ℝ) := Real.rpow_nonneg (by positivity) _ + change (t : ℝ) ≤ _ + nlinarith only [hsq, hroot, ht0, hr0] + +/-- The actual native catalogue allowance has the same degree-seven logarithmic estimate +as the finite instance count. The shared finite lemma avoids a duplicate counting proof. -/ +theorem instanceBound_le_numBound (κ n : ℕ) : instanceBound κ n ≤ numBound κ (n + 2) := + shifted_count_bound_le n κ + +/-- Every fixed positive real power eventually absorbs the actual catalogue allowance. -/ +theorem instanceBound_eventually_le_rpow (κ : ℕ) {ε : ℝ} (hε : 0 < ε) : + ∀ᶠ n : ℕ in atTop, (instanceBound κ n : ℝ) ≤ (n : ℝ) ^ ε := by + have h := Nat.eventually_mul_log_add_pow_le_rpow (by decide : 1 < (2 : ℕ)) + 2 1 7 (K := (128 * (κ + 2) ^ 2 : ℕ)) (by positivity) hε + filter_upwards [h] with n hn + have hb := (Nat.cast_le (α := ℝ)).mpr (instanceBound_le_numBound κ n) + unfold numBound at hb + push_cast at hb hn + exact hb.trans hn + +/-- Actual Convolution caller work, with its outer control reserve, is a cubic side term +plus the true number of callee invocations. -/ +theorem callerTime_add_twelve_le (N T : ℕ) : + Host.callerTime N T + 12 ≤ + 2 * Host.sideLength N * T + 355 * Host.sideLength N ^ 3 := by + have ht : 1 ≤ Host.sideLength N := by dsimp only [Host.sideLength]; omega + have hp : Host.sideLength N ≤ Host.sideLength N ^ 3 := + Nat.le_self_pow (by decide) _ + have hp1 : 1 ≤ Host.sideLength N ^ 3 := Nat.one_le_pow _ _ ht + unfold Host.callerTime + have hs : Nat.sqrt N ≤ Host.sideLength N := by dsimp only [Host.sideLength]; omega + nlinarith only [hs, hp, hp1] + +/-- The same original input length controls both native packed geometry and its magnitude. +The coefficient and threshold precede every outer input. No magnitude or time certificate +is supplied. -/ +theorem exists_packed_calleeTime_bound (κ E : ℕ) : + ∃ C : ℝ, 0 < C ∧ ∃ N : ℕ, ∀ n ≥ N, + let t := Nat.sqrt (8 * mPar n (2 * (n + 2) ^ κ) ^ 2) + 1 + (ParameterSelecting.callee.time t (2 * (n + 2) ^ E + 1) : ℝ) ≤ + C * (t : ℝ) ^ (3 - 1 / 1296 : ℝ) := by + obtain ⟨C, hC, N, hN, htime⟩ := ParameterSelecting.exists_time_subcubic_bound + (by omega : 1 ≤ 2 * E + 2) + refine ⟨C, hC, N ^ 2, ?_⟩ + intro n hn + exact htime _ (le_packed_side_of_sq_le hn _) _ (packed_weight_le κ E n) + +private theorem preprocessing_eventually_le (κ : ℕ) : + ∀ᶠ n : ℕ in atTop, + (ChanHe.Preprocessing.cost κ n : ℝ) ≤ (n : ℝ) ^ (2 - 1 / 5184 : ℝ) := by + let ε : ℝ := 1 / 65536 + let K := 6 * ChanHe.Preprocessing.costCoefficient κ + 1 + have hlog := Nat.eventually_mul_log_add_pow_le_rpow (by decide : 1 < (2 : ℕ)) + 2 1 13 (K := (K : ℝ)) (by dsimp only [K]; positivity) (show 0 < ε by norm_num [ε]) + filter_upwards [hlog, packed_side_eventually_le_rpow κ (show 0 < ε by norm_num [ε]), + eventually_ge_atTop (2 : ℕ)] with n hlog ht hn + let t := Host.sideLength (instanceLength κ n) + change (t : ℝ) ≤ (n : ℝ) ^ (1 / 2 + ε : ℝ) at ht + have ht1 : 1 ≤ t := by dsimp only [t, Host.sideLength]; omega + have hnt : n < t ^ 2 := input_lt_packed_side_sq n _ + have hsqrt : Nat.sqrt (n + 2) + 1 ≤ 3 * t := by + have h : n + 2 < (t + 2) ^ 2 := by nlinarith + have h' := Nat.sqrt_lt'.mpr h + omega + have hp := ChanHe.Preprocessing.cost_bound κ n + have hp' : ChanHe.Preprocessing.cost κ n ≤ + K * n * t * (Nat.log 2 (n + 2) + 1) ^ 13 := by + calc + _ ≤ ChanHe.Preprocessing.costCoefficient κ * (2 * n) * (3 * t) * + (Nat.log 2 (n + 2) + 1) ^ 13 := by + apply hp.trans + gcongr + omega + _ = (6 * ChanHe.Preprocessing.costCoefficient κ) * n * t * + (Nat.log 2 (n + 2) + 1) ^ 13 := by ring + _ ≤ K * n * t * (Nat.log 2 (n + 2) + 1) ^ 13 := + Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ + (show 6 * ChanHe.Preprocessing.costCoefficient κ ≤ K from Nat.le_succ _))) + have hpR := (Nat.cast_le (α := ℝ)).mpr hp' + have hm := mul_le_mul_of_nonneg_left hlog (show (0 : ℝ) ≤ (n : ℝ) * t by positivity) + have hp'' : (ChanHe.Preprocessing.cost κ n : ℝ) ≤ + (n : ℝ) * (n : ℝ) ^ (1 / 2 + ε : ℝ) * (n : ℝ) ^ ε := by + push_cast at hpR hm + have hsmall : (ChanHe.Preprocessing.cost κ n : ℝ) ≤ + (n : ℝ) * t * (n : ℝ) ^ ε := by nlinarith only [hpR, hm] + exact hsmall.trans (by gcongr) + calc + _ ≤ (n : ℝ) * (n : ℝ) ^ (1 / 2 + ε : ℝ) * (n : ℝ) ^ ε := hp'' + _ = (n : ℝ) ^ (3 / 2 + 2 * ε : ℝ) := by + calc + _ = (n : ℝ) ^ (1 + (1 / 2 + ε) + ε : ℝ) := by + rw [Real.rpow_add (by positivity) (1 + (1 / 2 + ε) : ℝ) ε, + Real.rpow_add (by positivity) (1 : ℝ) (1 / 2 + ε : ℝ), Real.rpow_one] + _ = _ := by congr 1; ring + _ ≤ _ := Real.rpow_le_rpow_of_exponent_le (by exact_mod_cast (by omega : 1 ≤ n)) + (by norm_num [ε]) + +/-- The complete charged ordinary-host budget with the actual parameter-selecting callee +is strictly subquadratic. The single coefficient and threshold depend only on the original +fixed weight exponent, not on input data, layout, physical width or selected primes. -/ +theorem exists_cost_subquadratic_bound (κ : ℕ) : + ∃ C : ℝ, 0 < C ∧ ∃ N : ℕ, ∀ n ≥ N, + (cost κ ParameterSelecting.callee n : ℝ) ≤ + C * (n : ℝ) ^ (2 - 1 / 5184 : ℝ) := by + let ε : ℝ := 1 / 65536 + let E := envelopeExponent κ + obtain ⟨C, hC, N, htime⟩ := exists_packed_calleeTime_bound κ E + have hevent : ∀ᶠ n : ℕ in atTop, + (cost κ ParameterSelecting.callee n : ℝ) ≤ + (2 * C + 4 * E + 388) * (n : ℝ) ^ (2 - 1 / 5184 : ℝ) := by + filter_upwards [eventually_ge_atTop N, eventually_ge_atTop (2 : ℕ), + instanceBound_eventually_le_rpow κ (show 0 < ε by norm_num [ε]), + packed_side_eventually_le_rpow κ (show 0 < ε by norm_num [ε]), + preprocessing_eventually_le κ] with n hnN hn hq ht hpp + let t := Host.sideLength (instanceLength κ n) + let T := ParameterSelecting.callee.time t (2 * (n + 2) ^ E + 1) + have ht1 : (1 : ℝ) ≤ t := by + have h : 1 ≤ t := by dsimp only [t, Host.sideLength]; omega + exact_mod_cast h + have hn1 : (1 : ℝ) ≤ n := by exact_mod_cast (by omega : 1 ≤ n) + have ht0 : (0 : ℝ) < t := by linarith + change (t : ℝ) ≤ (n : ℝ) ^ (1 / 2 + ε : ℝ) at ht + have hb : (T : ℝ) ≤ C * (t : ℝ) ^ (3 - 1 / 1296 : ℝ) := htime n hnN + have hpow : (t : ℝ) ^ (4 - 1 / 1296 : ℝ) = + (t : ℝ) * (t : ℝ) ^ (3 - 1 / 1296 : ℝ) := by + have h : (4 - 1 / 1296 : ℝ) = 1 + (3 - 1 / 1296) := by ring + rw [h, Real.rpow_add ht0, Real.rpow_one] + have hT : 2 * (t : ℝ) * T ≤ 2 * C * (t : ℝ) ^ (4 - 1 / 1296 : ℝ) := by + calc + _ ≤ 2 * (t : ℝ) * (C * (t : ℝ) ^ (3 - 1 / 1296 : ℝ)) := by gcongr + _ = _ := by rw [hpow]; ring + have hcube : (t : ℝ) ^ 3 ≤ (t : ℝ) ^ (4 - 1 / 1296 : ℝ) := by + rw [← Real.rpow_natCast] + exact Real.rpow_le_rpow_of_exponent_le ht1 (by norm_num) + have hc : ((Host.callerTime (instanceLength κ n) T + 12 : ℕ) : ℝ) ≤ + 2 * (t : ℝ) * T + 355 * (t : ℝ) ^ 3 := by + exact_mod_cast callerTime_add_twelve_le (instanceLength κ n) T + have hcall : (Host.callerTime (instanceLength κ n) T + 12 : ℕ) ≤ + (2 * C + 355) * (t : ℝ) ^ (4 - 1 / 1296 : ℝ) := by + nlinarith only [hc, hT, hcube] + have hscale : (n : ℝ) ^ ε * (t : ℝ) ^ (4 - 1 / 1296 : ℝ) ≤ + (n : ℝ) ^ (2 - 1 / 5184 : ℝ) := by + calc + _ ≤ (n : ℝ) ^ ε * ((n : ℝ) ^ (1 / 2 + ε : ℝ)) ^ (4 - 1 / 1296 : ℝ) := by + gcongr + _ = (n : ℝ) ^ (ε + (1 / 2 + ε) * (4 - 1 / 1296) : ℝ) := by + rw [← Real.rpow_mul (by positivity), ← Real.rpow_add (by positivity)] + _ ≤ _ := Real.rpow_le_rpow_of_exponent_le hn1 (by norm_num [ε]) + have hprod : (instanceBound κ n : ℝ) * (Host.callerTime (instanceLength κ n) T + 12 : ℕ) ≤ + (2 * C + 355) * (n : ℝ) ^ (2 - 1 / 5184 : ℝ) := by + calc + _ ≤ (n : ℝ) ^ ε * ((2 * C + 355) * (t : ℝ) ^ (4 - 1 / 1296 : ℝ)) := by gcongr + _ = (2 * C + 355) * ((n : ℝ) ^ ε * (t : ℝ) ^ (4 - 1 / 1296 : ℝ)) := by ring + _ ≤ _ := mul_le_mul_of_nonneg_left hscale (by positivity) + have hone : (1 : ℝ) ≤ (n : ℝ) ^ (2 - 1 / 5184 : ℝ) := by + simpa only [Real.rpow_zero] using + (Real.rpow_le_rpow_of_exponent_le hn1 (show (0 : ℝ) ≤ 2 - 1 / 5184 by norm_num)) + have hconst := mul_le_mul_of_nonneg_left hone (show (0 : ℝ) ≤ 4 * E + 32 by positivity) + unfold cost + change ((ChanHe.Preprocessing.cost κ n + 4 * E + 32 + + instanceBound κ n * (Host.callerTime (instanceLength κ n) T + 12) : ℕ) : ℝ) ≤ _ + push_cast at hprod ⊢ + nlinarith only [hpp, hprod, hconst] + obtain ⟨M, hM⟩ := eventually_atTop.mp hevent + exact ⟨2 * C + 4 * E + 388, by positivity, M, hM⟩ + +end Cslib.Algorithms.WordRAM.ThreeSum.Decision diff --git a/Complexity/Algorithms/WordRAM/ThreeSum/Decision/Subquadratic.lean b/Complexity/Algorithms/WordRAM/ThreeSum/Decision/Subquadratic.lean new file mode 100644 index 0000000000..fc78057b00 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ThreeSum/Decision/Subquadratic.lean @@ -0,0 +1,87 @@ +/- +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.ThreeSum.Decision.DyadicCost +public import Complexity.Algorithms.WordRAM.ThreeSum.Decision.Intermediates + +/-! +# Actual native ordinary 3SUM execution with a strict-subquadratic charge + +For each fixed natural magnitude exponent, the existing ordinary host and the concrete +parameter-selecting ET callee form one fixed native standard Word-RAM program. It begins at +actual initialized canonical signed input, admits every sufficiently wide logarithmic word, +and decides the existing distinct-position integer 3SUM predicate, including repeated values. + +Correctness covers every input length; only the bound `Oκ(n^(2−1/5184))` is eventual. One +coefficient and threshold precede every input and physical width. The program computes its +parameters, primes, matrices and answers; no execution, time, layout or solver law is supplied. + +## Main results + +* `exists_subquadratic_runs`: actual initialized prefix and charged halt, exact original verdict, + and uniform strict-subquadratic charged steps for polynomially bounded integer inputs. + +This is original conservative composition of the existing native reductions and actual ET +solver. It concerns charged standard Word-RAM instructions, not bit/Turing time or arbitrary +real-number 3SUM. It does not prove the source's tuned exponent 1.9992. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ThreeSum.Decision + +open Cslib.WordRAM Cslib.Algorithms.WordRAM.ExactTriangle +open Cslib.Algorithms.ThreeSum (HasSolution) + +/-- The fixed native program is correct at every admitted input length; its strict-subquadratic +step bound is uniform beyond one threshold per original magnitude exponent. Both actual runs +use the same initialized state and pre-halt witness, with the halt included in steps. -/ +theorem exists_subquadratic_runs (κ : ℕ) : + ∃ C : ℝ, 0 < C ∧ ∃ N : ℕ, + ¬(program κ ParameterSelecting.callee).ReadsWidth ∧ ∀ (input : List ℤ) (W : ℕ), + width κ 123357 input.length ≤ W → + (∀ z ∈ input, |z| ≤ ((input.length + 2) ^ κ : ℕ)) → + InputFits W (input.map Signed.encode) ∧ ∃ (y : Data 848) (steps : ℕ), + Executes W (flatProgram κ ParameterSelecting.callee) + (State.init (input.map Signed.encode)) (y.regs (controllerRegisters 633 answer)) steps ∧ + Runs W (flatProgram κ ParameterSelecting.callee) + (State.init (input.map Signed.encode)) ⟨(program κ ParameterSelecting.callee).size, y⟩ + (steps - 1) ∧ + steps ≤ cost κ ParameterSelecting.callee input.length ∧ + (N ≤ input.length → (steps : ℝ) ≤ C * (input.length : ℝ) ^ (2 - 1 / 5184 : ℝ)) ∧ + y.regs (controllerRegisters 633 answer) ≤ 1 ∧ + (y.regs (controllerRegisters 633 answer) = 1 ↔ + HasSolution (fun i : Fin input.length => input[i])) ∧ y.Bounded W ∧ + ∀ (s : State 848) (t : ℕ), + Runs W (flatProgram κ ParameterSelecting.callee) + (State.init (input.map Signed.encode)) s t → + (∀ i, s.data.regs i < (input.length + 2) ^ (2 * widthCoefficient κ 123357)) ∧ + (∀ a, s.data.mem a < (input.length + 2) ^ (2 * widthCoefficient κ 123357)) ∧ + (∀ a, (input.length + 2) ^ (2 * widthCoefficient κ 123357) ≤ a → s.data.mem a = 0) := by + obtain ⟨C, hC, N, hc⟩ := exists_cost_subquadratic_bound κ + refine ⟨C, hC, N, not_readsWidth κ ParameterSelecting.callee, ?_⟩ + intro input W hW' hv + have hW : width κ ParameterSelecting.callee.widthCoefficient input.length ≤ W := by + simpa only [ParameterSelecting.callee_widthCoefficient] using hW' + have hi := ChanHe.Preprocessing.input_fits input + ((preprocessing_width_le κ ParameterSelecting.callee.widthCoefficient input.length).trans hW) hv + obtain ⟨y, steps, he, hr, ht, hb, hiff, hbounded⟩ := + runs_input input ParameterSelecting.callee hW hv + refine ⟨hi, y, steps, he, hr, ht, + fun hn => ((Nat.cast_le (α := ℝ)).mpr ht).trans (hc input.length hn), hb, hiff, hbounded, ?_⟩ + intro s t hs + obtain ⟨hregs, hmem⟩ := intermediates_polynomial input ParameterSelecting.callee hW hv hs + refine ⟨?_, ?_, ?_⟩ + · simpa only [ParameterSelecting.callee_widthCoefficient] using hregs + · simpa only [ParameterSelecting.callee_widthCoefficient] using hmem + · intro a ha + apply space_polynomial input ParameterSelecting.callee hW hv hs + simpa only [ParameterSelecting.callee_widthCoefficient] using ha + +end Cslib.Algorithms.WordRAM.ThreeSum.Decision diff --git a/Complexity/Foundations/Data/Nat/LogRpow.lean b/Complexity/Foundations/Data/Nat/LogRpow.lean new file mode 100644 index 0000000000..52d398385e --- /dev/null +++ b/Complexity/Foundations/Data/Nat/LogRpow.lean @@ -0,0 +1,85 @@ +/- +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.Init +public import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics +public import Mathlib.Analysis.SpecialFunctions.Log.Base +import Mathlib.Analysis.Complex.ExponentialBounds +import Mathlib.Tactic.GCongr +import Mathlib.Tactic.Linarith + +/-! +# Fixed powers of shifted natural logarithms are subpolynomial + +This bridge applies Mathlib's real logarithm little-o estimate to natural logarithms with +fixed base, input shift and additive constant. It is general mathematics intended for Mathlib. +The native 3SUM host uses it for packed-side, catalogue-count and preprocessing logarithms. + +## Main results + +* `Nat.eventually_mul_log_add_pow_le_rpow`: every fixed positive multiple of a fixed + logarithmic power is eventually bounded by any positive real power of the original input. +-/ + +public section + +open Filter + +namespace Nat + +/-- Fixed shifts and additive constants do not change the subpolynomial growth of a natural +logarithm. The threshold may depend on all fixed parameters, but not on the varying input. -/ +theorem eventually_mul_log_add_pow_le_rpow {b : ℕ} (hb : 1 < b) (s c d : ℕ) + {K ε : ℝ} (hK : 0 < K) (hε : 0 < ε) : + ∀ᶠ n : ℕ in atTop, + K * ((Nat.log b (n + s) : ℝ) + c) ^ d ≤ (n : ℝ) ^ ε := by + let a : ℝ := 2 / Real.log b + c + have hlogb : 0 < Real.log (b : ℝ) := Real.log_pos (by exact_mod_cast hb) + have ha : 0 < a := by dsimp only [a]; positivity + have hcoeff : 0 < K * a ^ d := mul_pos hK (pow_pos ha _) + have hsmall := (isLittleO_log_rpow_rpow_atTop (d : ℝ) hε).comp_tendsto + tendsto_natCast_atTop_atTop + filter_upwards [hsmall.bound (inv_pos.mpr hcoeff), + eventually_ge_atTop (max 16 (s + 2))] with n he hn + have hn16 : 16 ≤ n := (le_max_left _ _).trans hn + have hn2 : 2 ≤ n := by omega + have hn0 : (0 : ℝ) < n := by exact_mod_cast (by omega : 0 < n) + have hnR : (16 : ℝ) ≤ n := by exact_mod_cast hn16 + have hlog1 : 1 ≤ Real.log (n : ℝ) := + (Real.le_log_iff_exp_le hn0).mpr (Real.exp_one_lt_three.le.trans (by linarith)) + have hshiftN : n + s ≤ n ^ 2 := by have := (le_max_right _ _).trans hn; nlinarith + have hshiftR : (n : ℝ) + s ≤ (n : ℝ) ^ 2 := by exact_mod_cast hshiftN + have hlogShift : Real.log (n + s : ℝ) ≤ 2 * Real.log (n : ℝ) := by + calc _ ≤ Real.log ((n : ℝ) ^ 2) := + Real.log_le_log (by positivity) hshiftR + _ = _ := by rw [Real.log_pow]; norm_num + have hnlog : (Nat.log b (n + s) : ℝ) ≤ Real.log (n + s : ℝ) / Real.log b := by + simpa only [Real.logb, Nat.cast_add] using Real.natLog_le_logb (n + s) b + have hbase : (Nat.log b (n + s) : ℝ) + c ≤ a * Real.log (n : ℝ) := by + have hdiv := div_le_div_of_nonneg_right hlogShift hlogb.le + have hc := mul_le_mul_of_nonneg_left hlog1 (show (0 : ℝ) ≤ c by positivity) + have hsum := _root_.add_le_add (hnlog.trans hdiv) hc + calc + _ ≤ (2 * Real.log (n : ℝ)) / Real.log b + c * Real.log (n : ℝ) := by + simpa only [_root_.mul_one] using hsum + _ = _ := by dsimp only [a]; ring + have hp := pow_le_pow_left₀ (by positivity : (0 : ℝ) ≤ (Nat.log b (n + s) : ℝ) + c) + hbase d + have hpow0 : 0 ≤ (n : ℝ) ^ ε := Real.rpow_nonneg (by positivity) _ + dsimp only [Function.comp_apply] at he + rw [Real.norm_eq_abs, Real.rpow_natCast, abs_of_nonneg (pow_nonneg (by linarith) _), + Real.norm_eq_abs, abs_of_nonneg hpow0] at he + calc K * ((Nat.log b (n + s) : ℝ) + c) ^ d + ≤ K * (a * Real.log (n : ℝ)) ^ d := mul_le_mul_of_nonneg_left hp hK.le + _ = (K * a ^ d) * Real.log (n : ℝ) ^ d := by rw [mul_pow]; ring + _ ≤ (K * a ^ d) * ((K * a ^ d)⁻¹ * (n : ℝ) ^ ε) := + mul_le_mul_of_nonneg_left he hcoeff.le + _ = _ := by rw [← mul_assoc, mul_inv_cancel₀ hcoeff.ne', one_mul] + +end Nat diff --git a/ComplexityTests/WordRAMSubquadraticThreeSum.lean b/ComplexityTests/WordRAMSubquadraticThreeSum.lean new file mode 100644 index 0000000000..e3785b1515 --- /dev/null +++ b/ComplexityTests/WordRAMSubquadraticThreeSum.lean @@ -0,0 +1,111 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +-- upstream: local-only (tests) + +import Complexity.Algorithms.WordRAM.ThreeSum.Decision.Subquadratic + +/-! +# Admitted initialized ordinary 3SUM at the strict-subquadratic charge + +Constant zero inputs of every admitted large length return one, using three distinct positions +with repeated values. Positive-one and negative-one inputs return zero at the same uniform +asymptotic charge. The two-zero boundary client returns zero because positions must be distinct. +These are kernel-checked clients of the actual initialized program, not supplied executions, +restatements of signatures or enormous VM fixtures. +-/ + +namespace ComplexityTests.WordRAMSubquadraticThreeSum + +open Cslib.WordRAM Cslib.Algorithms.ThreeSum +open Cslib.Algorithms.WordRAM.ThreeSum.Decision +open Cslib.Algorithms.WordRAM.ExactTriangle + +private def values (n : ℕ) (z : ℤ) : List ℤ := List.replicate n z +private def W (n : ℕ) : ℕ := width 1 123357 n + +private theorem constant_solution_iff {n : ℕ} (hn : 3 ≤ n) (z : ℤ) : + HasSolution (fun _ : Fin n => z) ↔ z = 0 := by + constructor + · rintro ⟨i, j, k, _, _, _, h⟩ + change z + z + z = 0 at h + omega + · intro hz + refine ⟨(⟨0, by omega⟩ : Fin n), (⟨1, by omega⟩ : Fin n), (⟨2, by omega⟩ : Fin n), + by simp, by simp, by simp, ?_⟩ + simp [hz] + +private def TimedConstant (z : ℤ) (answer : ℕ) : Prop := + ∃ C : ℝ, 0 < C ∧ ∃ N : ℕ, 3 ≤ N ∧ ∀ n ≥ N, + ∃ (y : Data 848) (steps : ℕ), + InputFits (W n) ((values n z).map Signed.encode) ∧ + Executes (W n) (flatProgram 1 ParameterSelecting.callee) + (State.init ((values n z).map Signed.encode)) answer steps ∧ + Runs (W n) (flatProgram 1 ParameterSelecting.callee) + (State.init ((values n z).map Signed.encode)) + ⟨(program 1 ParameterSelecting.callee).size, y⟩ (steps - 1) ∧ + (steps : ℝ) ≤ C * (n : ℝ) ^ (2 - 1 / 5184 : ℝ) ∧ + y.regs (controllerRegisters 633 Cslib.Algorithms.WordRAM.ThreeSum.Decision.answer) = answer + +private theorem timed_constant (z : ℤ) (hz : |z| ≤ (1 : ℤ)) : + TimedConstant z (if z = 0 then 1 else 0) := by + obtain ⟨C, hC, N, _, hrun⟩ := exists_subquadratic_runs 1 + refine ⟨C, hC, max N 3, le_max_right _ _, ?_⟩ + intro n hn + have hnN : N ≤ n := (le_max_left _ _).trans hn + have hn3 : 3 ≤ n := (le_max_right _ _).trans hn + have hv : ∀ v ∈ values n z, |v| ≤ (((values n z).length + 2) ^ 1 : ℕ) := by + intro v hv + have heq : v = z := (List.mem_replicate.mp hv).2 + subst v + simp only [values, List.length_replicate, pow_one] + exact hz.trans (by omega) + obtain ⟨hi, y, steps, he, hr, _, ht, hb, hiff, hbounded, hprefix⟩ := + hrun (values n z) (W n) (by simp only [values, List.length_replicate, W]; rfl) hv + have ht' : (steps : ℝ) ≤ C * (n : ℝ) ^ (2 - 1 / 5184 : ℝ) := by + simpa only [values, List.length_replicate] using ht (by simpa only [values, + List.length_replicate] using hnN) + have hiff' : y.regs (controllerRegisters 633 answer) = 1 ↔ z = 0 := by + have hiff0 : y.regs (controllerRegisters 633 answer) = 1 ↔ + HasSolution (fun _ : Fin (values n z).length => z) := by + simpa only [values, Fin.getElem_fin, List.getElem_replicate] using hiff + exact hiff0.trans (constant_solution_iff (by simpa only [values, + List.length_replicate] using hn3) z) + have hans : y.regs (controllerRegisters 633 answer) = (if z = 0 then 1 else 0) := by + split_ifs with hz0 + · exact hiff'.mpr hz0 + · have hnot : y.regs (controllerRegisters 633 answer) ≠ 1 := + fun h => hz0 (hiff'.mp h) + omega + exact ⟨y, steps, hi, by simpa only [hans] using he, hr, ht', hans⟩ + +example : TimedConstant 0 1 := by simpa using timed_constant 0 (by decide) +example : TimedConstant 1 0 := by simpa using timed_constant 1 (by decide) +example : TimedConstant (-1) 0 := by simpa using timed_constant (-1) (by decide) + +example : ∃ (y : Data 848) (steps : ℕ), + Executes (W 2) (flatProgram 1 ParameterSelecting.callee) + (State.init ([0, 0].map Signed.encode)) 0 steps ∧ + Runs (W 2) (flatProgram 1 ParameterSelecting.callee) + (State.init ([0, 0].map Signed.encode)) + ⟨(program 1 ParameterSelecting.callee).size, y⟩ (steps - 1) := by + obtain ⟨_, _, _, _, hrun⟩ := exists_subquadratic_runs 1 + obtain ⟨_, y, steps, he, hr, _, _, hb, hiff, _, _⟩ := + hrun [0, 0] (W 2) (by decide) (by simp) + have hno : ¬HasSolution (fun _ : Fin 2 => (0 : ℤ)) := by + dsimp only [HasSolution] + decide + have hans : y.regs (controllerRegisters 633 answer) = 0 := by + have hnot : y.regs (controllerRegisters 633 answer) ≠ 1 := by + intro h + apply hno + have hs := hiff.mp h + change HasSolution (fun i : Fin 2 => (List.replicate 2 (0 : ℤ))[i]) at hs + simpa only [Fin.getElem_fin, List.getElem_replicate] using hs + omega + exact ⟨y, steps, by simpa only [hans] using he, hr⟩ + +end ComplexityTests.WordRAMSubquadraticThreeSum diff --git a/ROADMAP.md b/ROADMAP.md index d96d6627fc..3154ccbbd7 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -645,24 +645,23 @@ reusing graph and matroid foundations and the shared data-structure interfaces. expected-time rules for unbounded almost-surely terminating structured loops; random-tape equivalence and BPP/RP/ZPP simulation bridges for the randomized word RAM ([#1124]); transfer of cell-probe lower bounds; and the Horn-SAT, 2SAT, matching and domino-tiling clients. -- **Direct 3SUM adaptation** ([#1394]): global parameter/asymptotic composition, using the concrete - native cyclic-Strassen counter ([#1701]), minimum-count selector ([#2098]) and conservative - computed dyadic parameters ([#2127]); unrestricted small geometry; the aggregate - subcubic Exact Triangle bound and source exponent; and the unconditional ordinary-3SUM - input/time/width/asymptotic composition, including the improved Section 4 route to exponent - 1.9992. These build on the native Chan–He preprocessing, queried thin products, fixed-prime - Exact Triangle solving and the conditional Convolution-3SUM host. The counter computes its - own residues, padding/table, seven-product recursion and exact raw modular count, within - `3704*(p+1)²*(n+1)^2.81` instructions including halt. Its source-regime admission and - width-independent prefix bounds are proved. The selector computes the actual attained window - minimum with native trial division and real counter calls, preserving the explicit window - cost factor. The dyadic parameter kernel computes geometry-compatible values and explicitly - classifies the small regime. The assembled solver ([#2146]) executes actual parameter - preparation, selection and the complete fixed-prime solver, or the real exhaustive small - branch, restoring the original host arguments. It supplies the concrete host callee and - initialized correctness, logarithmic admission and polynomial prefix/support guarantees. - Remaining are global asymptotic composition using the component-cost bridge ([#2145]), - outer-host execution, the tuned source exponent and the full endpoint. +- **Direct 3SUM adaptation** ([#1394]): integrate the improved Section 4 route and native + exponent 1.9992 from [#2358](https://github.com/cslib-community/complexitylib/pull/2358). + Conservative native ordinary integer 3SUM is proved in + `WordRAM/ThreeSum/Decision/Subquadratic.lean`: for each fixed polynomial magnitude exponent, + one fixed 848-register program has charged time `Oκ(n^(2−1/5184))`, logarithmic physical + admission and polynomial words/support at every wider execution prefix. Correctness includes + every length, distinct positions and repeated values; only the time estimate is eventual. + This is standard Word-RAM instruction time, not bit/Turing time or arbitrary-real 3SUM. + The concrete cyclic-Strassen counter ([#1701]), minimum-count selector ([#2098]) and computed + conservative parameters ([#2127]) feed the actual assembled ET callee ([#2146]). Its time + field is `Oκ(n^(3−1/1296))` for polynomial weights. The ordinary proof charges native Chan–He + preprocessing, actual packed dimensions, all matrix/callee calls, control work and halt; + it does not assume a fast solver, prime procedure, layout or time contract. The counter + computes residues, padding, seven-product recursion and exact modular counts within + `3704*(p+1)²*(n+1)^2.81` instructions. The selected prime is computed by trial division and + actual counter calls; the assembled solver runs the real exhaustive branch at smaller + geometry. These conservative original estimates do not establish the source's tuned endpoint. - **Memory-oracle realization** ([#2205], [#2213]): the foundational graded kernel certifies all four memory queries, register-word glue, native branches and binds with one fixed continuation emitter for all runtime replies. Its functional representation retains the diff --git a/UPSTREAM.md b/UPSTREAM.md index 6eedda30b1..42b8f4602a 100644 --- a/UPSTREAM.md +++ b/UPSTREAM.md @@ -212,11 +212,10 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he all `2t` instances and a finite solver program in a disjoint register bank. Its initialized run theorem connects the actual pre-halt state to the Convolution-3SUM answer and preserves the input. The host's source-width threshold is `(20κ+125)clog₂(N+2)`; signed kernels use target width `w+2`. - This remains conditional on the supplied solver's native execution/correctness/frame theorem; - it does not establish a fast solver. Fast Exact Triangle and its final native backend/asymptotic - composition remain in - [#1394](https://github.com/cslib-community/complexitylib/issues/1394), including the improved - Section 4 route needed for the published exponent 1.9992. Anthropic's copyright and attribution + This host module remains parametric in a concrete solver's execution/correctness/frame theorem; + the actual solver and conservative ordinary-host composition are described below. The improved + Section 4 route needed for the published exponent 1.9992 remains in + [#1394](https://github.com/cslib-community/complexitylib/issues/1394). Anthropic's copyright and attribution are retained; the native proofs and representation choices are local. Native numeric parameter computation, signed-residue/histogram counting, trial-division prime tables, collision-tested least-prime scans and complete two-prime modulus selection also use @@ -240,11 +239,23 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he logarithmic physical width, polynomial words/space at every admitted-width prefix, and a fully charged compositional bound at the actual packed size. `Host.Callee` requires actual finite-code execution, matrix correctness, logarithmic width and a protected-prefix frame on arbitrary old - scratch memory; `Host.Slow.callee` is a proved exhaustive native instance. This conditional host - does not provide a fast solver. The unconditional native solver/backend and final asymptotic - composition, including exponent 1.9992, remain #1394. These components do not affect the curated - headlines. The caller layout, exhaustive callee and ordinary composition are original; the - underlying finite reductions and builder retain their existing Anthropic credit. + scratch memory; `Host.Slow.callee` is a proved exhaustive native instance. + `ExactTriangle/ParameterSelecting.callee` now provides the actual fast/small-branch solver. + Its `Asymptotics` module proves the concrete time field is `Oκ(n^(3−1/1296))` at polynomial + original magnitudes, without a selected-prime or running-time hypothesis. + `ThreeSum/Decision/Subquadratic.exists_subquadratic_runs` composes that exact callee with the + actual ordinary host: one fixed 848-register standard program per magnitude exponent, complete + initialized same-state prefix/halt, original distinct-position verdict, logarithmic width, + polynomial prefix words/support and charged `Oκ(n^(2−1/5184))` time. Correctness covers every + length and repeated values. The theorem concerns polynomially bounded integer inputs and + charged Word-RAM instructions, not arbitrary-real or bit/Turing time. No new abstract is + selected. The improved Section 4/tuned1.9992 endpoint remains #1394. The native glue and these + conservative quantitative estimates are original; existing finite reductions and builder + retain their Anthropic credit. `ChanHe/ConvolutionSizes` transfers original magnitudes to the + actual packed side; the existing finite and native count proofs share `shifted_count_bound_le`. + The small `Foundations/Data/Nat/LogRpow` topic is general mathematics intended for Mathlib: + it transports Mathlib's real log little-o theorem to shifted natural logs and is consumed by + all three side/count/preprocessing estimates, without adding to a widely imported hub. Bounded API follow-ups from the traversal/preprocessing reviews: merge the stage proof modules `PreprocessingSnapshot`, `PreprocessingPrimes`, `PreprocessingSetup`, `PreprocessingFinish`, diff --git a/manual/algorithms-and-memory/algorithm-endpoints.md b/manual/algorithms-and-memory/algorithm-endpoints.md index 537dfe5c6f..e3dac25553 100644 --- a/manual/algorithms-and-memory/algorithm-endpoints.md +++ b/manual/algorithms-and-memory/algorithm-endpoints.md @@ -168,6 +168,42 @@ bit-time or arbitrary-real theorem. The large-family client is a checked symboli enormous interpreter benchmark. This conservative automatic component is distinct from the later box-backed ordinary 1.9992 endpoint in [PR #2358](https://github.com/cslib-community/complexitylib/pull/2358). +## Conservative ordinary integer 3SUM + +Import `Complexity.Algorithms.WordRAM.ThreeSum.Decision.Subquadratic`. In namespace +`Cslib.Algorithms.WordRAM.ThreeSum.Decision`, apply `exists_subquadratic_runs κ` to the actual +ordinary host with `ParameterSelecting.callee`. The complete +[checked client](https://github.com/cslib-community/complexitylib/blob/2f6fb39d034b8a27ddcd56dd7779b67ef9a236b9/ComplexityTests/WordRAMSubquadraticThreeSum.lean) +includes imports, positive repeated-zero inputs, negative all-one/all-minus-one inputs, and +rejection of two zeros because the positions must be distinct. From an endpoint checkout: + +```bash +scripts/build.sh --wfail --iofail ComplexityTests.WordRAMSubquadraticThreeSum +``` + +Fix a natural magnitude exponent `κ`. For `input : List ℤ` of length n, prove each +`|z| <= (n+2)^κ` and supply `Decision.width κ 123357 n <= W`. The starting state is +`State.init (input.map Signed.encode)`: address 0 holds n, signed input words start at 1, +and remaining memory is zero. If application fails, check the signed encoding, original list +length, magnitude bound, width and import against the complete client. + +One fixed 848-register standard Word-RAM program per κ returns one exactly for a zero sum at +three distinct original positions; repeated values are allowed. Correctness holds at every +length and every admitted wider width. The actual halt and prehalt prefix share a final state. +For each κ, one positive C and threshold N precede all inputs and physical widths; for n >= N, +charged steps are at most `C*n^(2-1/5184)`. Actual preprocessing, parameters, prime selection, +matrix construction, solver calls, control and halt are included in `Decision.cost`. No solver, +prime, layout, run or time law is supplied. Initial input placement/output extraction follow +the model convention. These clients consume checked run theorems; they are not VM benchmarks. + +Every reachable prefix has register/memory words below +`(n+2)^(2*Decision.widthCoefficient κ 123357)` and memory zero at or above that address envelope; +final data also satisfy the physical width bound. Time counts standard unit instructions, +including multiplication, division, bitwise operations and shifts, with overflow faults. +This is polynomially bounded integer Word-RAM time, not bit/Turing time or arbitrary-real +3SUM. Its conservative exponent is `2-1/5184`; the sharper box-backed 1.9992 theorem is the +separate [PR #2358](https://github.com/cslib-community/complexitylib/pull/2358). + ## Tree Evaluation The [Cook–Mertz endpoint](catalytic-and-tree-evaluation.md) computes the root of an explicitly table-encoded perfect binary tree in native independent workspace `O(log n · log log n)` for positive value length and height. The output is not charged to workspace, and the theorem leaves time existential. The same page distinguishes borrowed-register restoration and fan-in/packed procedure variants.