Verified structured RAM Hamming weight

Hamming.program is a structured imperative program over the reserved-register layout Hamming.inputStore. Its correctness and resource bounds are proved in the independent source semantics. Hamming.compiled_performance then applies the generic compiler theorem, carrying the result to the concrete logarithmic-cost RAM with an exact transition count, explicit length-indexed budgets, and quasilinear asymptotic corollaries.

theorem Complexity.RAM.Structured.Hamming.program_performance (bits : List Bool) : ∃ (final : Store) (cost : ℕ) (space : ℕ), Exec program (inputStore bits) final (stepCount bits) cost space ∧ cost ≤ timeBound bits.length ∧ space ≤ spaceBound bits.length ∧ final lengthReg = weight bits

Source-level correctness with an exact transition count and explicit logarithmic-cost time and peak-space bounds.

theorem Complexity.RAM.Structured.Hamming.compiled_performance (bits : List Bool) : ∃ (final : Store) (cost : ℕ) (space : ℕ), Exec program (inputStore bits) final (stepCount bits) cost space ∧ run compiled (stepCount bits) { pc := 0, regs := inputStore bits } = { pc := program.codeSize, regs := final } ∧ Halted compiled (run compiled (stepCount bits) { pc := 0, regs := inputStore bits }) ∧ logTimeUpto compiled (stepCount bits) { pc := 0, regs := inputStore bits } ≤ timeBound bits.length ∧ spaceUpto compiled (stepCount bits) { pc := 0, regs := inputStore bits } ≤ spaceBound bits.length ∧ (run compiled (stepCount bits) { pc := 0, regs := inputStore bits }).regs lengthReg = weight bits

End-to-end compiled performance theorem. The concrete RAM reaches its halt instruction after exactly stepCount bits transitions, within the explicit logarithmic-cost time and peak-space budgets, and returns the Hamming weight.

theorem Complexity.RAM.Structured.Hamming.timeBound_bigO_quasilinear : BigO timeBound quasilinearBound

The explicit logarithmic-cost time budget is quasilinear.

theorem Complexity.RAM.Structured.Hamming.spaceBound_bigO_quasilinear : BigO spaceBound quasilinearBound

The explicit peak-space budget is quasilinear under the reserved-register input representation.