Dense-overlay public-input initialization -- proofs

theorem Complexity.RAM.RegisterStore.Machine.denseInitialLengthLoopTM_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) : (denseInitialLengthLoopTM 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 [] ∧ inp.head = inp₀.head + input.length ∧ InitialLoopReady tapes (address + input.length) count entries work ∧ out = out₀) (denseInitialLengthLoopTime address input)

theorem Complexity.RAM.RegisterStore.Machine.denseProgramInitTM_hoareTime_internal {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 and rewinds the immutable input bank to cell one.