Dense-overlay public-input initialization

The optimized initializer retains the public bits on the immutable input tape, materializes only the positive-tagged length register, installs the reusable program ABI, and rewinds the input for dense fallback reads.

theorem Complexity.RAM.RegisterStore.Machine.denseProgramInitTM_hoareTime {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) : (denseProgramInitTM tapes).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool input) ∧ (work = fun (x : Fin (n + 1)) => Tape.init []) ∧ out = Tape.init []) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ work = denseProgramSnapshotWork tapes (DenseOverlay.Snapshot.initial input) ∧ out = TM.resetBinaryBlank) (denseProgramInitTime tapes input)

Complete dense public-input initialization reaches the exact one-entry snapshot image with the immutable input bank parked at cell one.