Sparse RAM public-input initialization -- proof internals

theorem Complexity.RAM.RegisterStore.Machine.initialLoopWork_ready_internal {n : ℕ} (tapes : ControlInstructionTapes n) (address count : ℕ) (entries : Store) : InitialLoopReady tapes address count entries (initialLoopWork tapes address count entries)

theorem Complexity.RAM.RegisterStore.Machine.initialZeroBitTM_hoareTime_internal {n : ℕ} (tapes : ControlInstructionTapes n) (address count : ℕ) (entries : Store) (inp₀ : Tape) (work₀ : Fin (n + 1) → Tape) (out₀ : Tape) (hready : InitialLoopReady tapes address count entries work₀) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (initialZeroBitTM tapes).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ InitialLoopReady tapes (address + 1) count entries work ∧ out = out₀) (TM.binarySuccTime address)

A zero input bit preserves the streaming frame and advances only the current register address.

theorem Complexity.RAM.RegisterStore.Machine.initialOneBitTM_hoareTime_internal {n : ℕ} (tapes : ControlInstructionTapes n) (address count : ℕ) (entries : Store) (inp₀ : Tape) (work₀ : Fin (n + 1) → Tape) (out₀ : Tape) (hready : InitialLoopReady tapes address count entries work₀) (hinput : TM.Parked inp₀) (houtput : out₀ = TM.resetBinaryBlank) : (initialOneBitTM tapes).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ InitialLoopReady tapes (address + 1) (count + 1) (entries ++ [(address, 1)]) work ∧ out = out₀) (rewindEntryEncodeRestoreTime (address, 1) + 1 + (TM.binarySuccTime count + 1 + TM.binarySuccTime address))

A one input bit appends the current (address, 1) entry and advances the entry count and current address, restoring every reusable source cursor.

theorem Complexity.RAM.RegisterStore.Machine.initialInputLoopTM_hoareTime_internal {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) (address count : ℕ) (entries : Store) (inp₀ : Tape) (work₀ : Fin (n + 1) → Tape) (out₀ : Tape) (hinput : inp₀.HasBinarySuffix input) (hready : InitialLoopReady tapes address count entries work₀) (houtput : out₀ = TM.resetBinaryBlank) : (initialInputLoopTM tapes).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp.HasBinarySuffix [] ∧ InitialLoopReady tapes (address + input.length) (count + inputTrueCount input) (entries ++ inputBitStoreFrom address input) work ∧ out = out₀) (initialInputLoopTime tapes address count input)

The custom scanner consumes exactly the advertised Boolean suffix, streaming its nonzero entries into the sparse-store buffer.

theorem Complexity.RAM.RegisterStore.Machine.initialSetupTM_hoareTime_internal {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) : (initialSetupTM 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 input ∧ inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ InitialLoopReady tapes 1 0 [] work ∧ out = TM.resetBinaryBlank) (1 + 1 + (TM.binarySuccTime 0 + 1 + TM.binarySuccTime 0))

The setup phase turns the standard all-heads-on-marker configuration into the exact address-one/count-zero streaming boundary.

theorem Complexity.RAM.RegisterStore.Machine.initialLengthEmitTM_hoareTime_internal {n : ℕ} (tapes : ControlInstructionTapes n) (length count : ℕ) (entries : Store) (inp₀ : Tape) (work₀ : Fin (n + 1) → Tape) (out₀ : Tape) (hready : InitialLoopReady tapes length count entries work₀) (hinput : TM.Parked inp₀) (houtput : out₀ = TM.resetBinaryBlank) : (initialLengthEmitTM tapes).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ InitialLoopReady tapes length (count + 1) (entries ++ [(0, length)]) work ∧ out = out₀) (rewindEntryEncodeRestoreTime (0, length) + 1 + TM.binarySuccTime count)

Emit the length register into the sparse buffer and increment the runtime entry count, restoring both encoder sources exactly.

theorem Complexity.RAM.RegisterStore.Machine.initialLengthTM_hoareTime_internal {n : ℕ} (tapes : ControlInstructionTapes n) (length count : ℕ) (entries : Store) (inp₀ : Tape) (work₀ : Fin (n + 1) → Tape) (out₀ : Tape) (hready : InitialLoopReady tapes length count entries work₀) (hinput : TM.Parked inp₀) (houtput : out₀ = TM.resetBinaryBlank) : (initialLengthTM tapes).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ InitialLoopReady tapes length (count + if length = 0 then 0 else 1) (entries ++ if length = 0 then [] else [(0, length)]) work ∧ out = out₀) (initialLengthTime length count)

Optional length emission skips zero and appends exactly one nonzero R₀ entry otherwise.

theorem Complexity.RAM.RegisterStore.Machine.initialLengthInstallTM_hoareTime_internal {n : ℕ} (tapes : ControlInstructionTapes n) (length count : ℕ) (entries : Store) (inp₀ : Tape) (work₀ : Fin (n + 1) → Tape) (out₀ : Tape) (hready : InitialLoopReady tapes (length + 1) count entries work₀) (hinput : TM.Parked inp₀) (houtput : out₀ = TM.resetBinaryBlank) : (initialLengthInstallTM tapes).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ InitialLoopReady tapes length (count + if length = 0 then 0 else 1) (entries ++ if length = 0 then [] else [(0, length)]) work ∧ out = out₀) (TM.binaryPredTime length + 1 + initialLengthTime length count)

Restore the post-loop address and install the optional length entry.

theorem Complexity.RAM.RegisterStore.Machine.initialAbiInstallTM_hoareTime_internal {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (length : ℕ) (inp₀ : Tape) (work₀ : Fin (n + 1) → Tape) (out₀ : Tape) (hready : InitialLoopReady tapes length (List.length store) store work₀) (hbufferStart : (work₀ tapes.buffer).cells 0 = Γ.start) (hinput : TM.Parked inp₀) (houtput : out₀ = TM.resetBinaryBlank) : (initialAbiInstallTM tapes).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ work = programSnapshotWork tapes { pc := 0, store := store } ∧ out = out₀) (initialAbiInstallTime tapes store length)

Install the completed sparse buffer into the exact clean program-loop snapshot image.

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

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

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

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

theorem Complexity.RAM.RegisterStore.Machine.programInitTM_hoareTime_internal {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.