Sparse RAM public-input initialization

The concrete initializer streams nonzero public-input bits into a canonical sparse store, installs the optional length register, and produces the exact clean work-tape image consumed by the reusable RAM program controller.

theorem Complexity.RAM.RegisterStore.Machine.programInitialStore_eq_append (input : List Bool) : programInitialStore input = inputBitStoreFrom 1 input ++ if input.length = 0 then [] else [(0, input.length)]

The concrete initializer's sparse store is the streamed nonzero input entries followed by the optional nonzero length register.

theorem Complexity.RAM.RegisterStore.Machine.programInitialStore_length (input : List Bool) : List.length (programInitialStore input) = inputTrueCount input + if input.length = 0 then 0 else 1

The concrete initializer emits one entry per true input bit and one more exactly when the input is nonempty.

theorem Complexity.RAM.RegisterStore.Machine.programInitialStore_canonical (input : List Bool) : Canonical (programInitialStore input)

The sparse store produced from public input is canonical.

theorem Complexity.RAM.RegisterStore.Machine.programInitialSnapshot_represents (input : List Bool) : (programInitialSnapshot input).Represents (initCfg input)

The initializer's pure sparse snapshot represents the RAM public-input configuration exactly.

theorem Complexity.RAM.RegisterStore.Machine.programInitTM_hoareTime {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) : (programInitTM 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.HasBinarySuffix [] ∧ work = programSnapshotWork tapes (programInitialSnapshot input) ∧ out = TM.resetBinaryBlank) (programInitTime tapes input)

Complete public-input initialization reaches the exact sparse snapshot image consumed by the reusable program loop.