Concrete global layout of native Chan–He preprocessing

The prime bitmap follows the frontend. A seven-word-per-entry stack and a pointer table precede all heavy and packed arrays. Reservations use the actual input length and actual computed fuel.

Main definitions

• arena: complete finite memory layout, including every root's allocation reservation.

Main results

• arena_separated: concrete stack, bitmap, table and heap reservations are disjoint.

The layout and resource estimates are original. They do not change the existing finite instances.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.arena (κ n : ℕ) (retained : ℕ → ℕ) : Traversal.Arena

All memory regions computed by the actual native forest controller.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.arena_separated (κ n : ℕ) (retained : ℕ → ℕ) : (arena κ n retained).Separated

The actual reservations put the bitmap, bounded stack, pointer table and arrays in order.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.arena_frontend_before (κ n : ℕ) (retained : ℕ → ℕ) : (Frontend.layout κ n).endpoint ≤ (arena κ n retained).stack

Every actual frontend payload precedes the reserved shared stack.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.work_le_power (f : ℕ) : Traversal.Math.work f ≤ 3 ^ (f + 1)

Full ternary work never exceeds the native controller's computed power reservation.