Fresh-input entry for proof-carrying binary routines -- proof internals

theorem Complexity.BinaryRoutine.Sound.afterInputLength_hoareTimeSpace_internal {n : ℕ} {routine : BinaryRoutine n} (hsound : routine.Sound) (lengthIdx : Fin n) (input : List Bool) (hrequires : routine.requires (inputLengthValues lengthIdx input.length)) : (afterInputLength lengthIdx routine).HoareTimeSpace (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool input) ∧ (work = fun (x : Fin n) => Tape.init []) ∧ out = Tape.init []) (fun (x : Tape) (x_1 : Fin n → Tape) (out : Tape) => out.HasOutput (afterInputLengthFunction lengthIdx routine input)) (afterInputLengthTime lengthIdx routine input.length) input.length (afterInputLengthSpace lengthIdx routine input.length)

theorem Complexity.BinaryRoutine.Sound.afterInputLength_computesInSpace_internal {n : ℕ} {routine : BinaryRoutine n} (hsound : routine.Sound) (lengthIdx : Fin n) (hrequires : ∀ (length : ℕ), routine.requires (inputLengthValues lengthIdx length)) : (afterInputLength lengthIdx routine).ComputesInSpace (afterInputLengthFunction lengthIdx routine) (afterInputLengthSpace lengthIdx routine)

theorem Complexity.BinaryRoutine.afterInputLengthSpace_bigO_log_internal {n : ℕ} (lengthIdx : Fin n) (routine : BinaryRoutine n) (hroutine : BigO (fun (length : ℕ) => routine.spaceBound (TM.binaryLengthSpace length) (inputLengthValues lengthIdx length)) fun (length : ℕ) => Nat.log 2 length) : BigO (afterInputLengthSpace lengthIdx routine) fun (length : ℕ) => Nat.log 2 length