Uniform logarithmic-square native frontend cost

The bound includes the complete parameter program, explicit-bit radix sorting, full multiplicities, every compact scan, all descriptor/payload setup and writes, and the final halt. It is uniform over all admitted sufficiently wide words, including empty input.

Main results

• cost_bound: an explicit Oκ((n+1) clog₂(n+2)²) instruction bound.

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

Explicit uniform coefficient; deliberately coarse and independent of physical word width.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.cost_bound (κ n : ℕ) : cost κ n ≤ costCoefficient κ * (n + 1) * Nat.clog 2 (n + 2) ^ 2

Concrete derivation from the actual charged instruction formula to logarithmic-square cost.