Polynomial global preprocessing reservations

Every frontend allocation, explicit-stack reservation and root allocation is bounded by a fixed power of the existing parameter budget. This derives local kernel fits from logarithmic width.

Main results

• arena_envelope_le: the complete global signed envelope has polynomial magnitude.

These coarse resource estimates are original. Charged subquadratic time is a separate bound.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.arena_envelope_le (κ n : ℕ) (retained : ℕ → ℕ) : have a := arena κ n retained; Traversal.envelope a.ceiling a.n a.m a.Λ a.U a.N ≤ Parameters.Math.budget n ((n + 2) ^ κ) ^ 52

The complete global envelope is a fixed power of the already bounded native parameter budget.