Subquadratic charged native preprocessing cost

The bound counts complete initialized-input execution, trial division, all descriptor loads, every recursion transition, native collision/heavy computation, array writes and the final halt. Its polynomial factor is (n+2)(sqrt(n+2)+1) and its logarithm has fixed degree thirteen.

Main definitions

• rootCoefficient, costCoefficient: explicit constants depending only on the fixed exponent.

Main results

• cost_bound: the actual native instruction count is at most square-root times linear times a fixed logarithmic power, uniformly over physical width.

These charged estimates are original. The existing mathematical prime/instance bounds are reused.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.rootCoefficient (κ : ℕ) : ℕ

Uniform complete-root coefficient after substituting the actual candidate bound.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.costCoefficient (κ : ℕ) : ℕ

Explicit whole-program coefficient, independent of input length, data and physical width.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.root_cost_bound (κ n : ℕ) : have m := ThreeSum.ChanHe.mPar n (2 * (n + 2) ^ κ); Traversal.rootTime (ThreeSum.ChanHe.fuel n) (n + 1) m (2 * m ^ 2) ≤ rootCoefficient κ * (n + 2) * ((n + 2).sqrt + 1) * (Nat.log 2 (n + 2) + 1) ^ 11

The complete root cost at the actual magnitude-derived candidate window.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.cost_bound (κ n : ℕ) : cost κ n ≤ costCoefficient κ * (n + 2) * ((n + 2).sqrt + 1) * (Nat.log 2 (n + 2) + 1) ^ 13

The actual native program has a genuinely subquadratic polynomial factor and fixed polylog.