Unrestricted depth-three lower bound: tape word rewind

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/TapeWordRewind.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeWord.move_left_mk₂_cons {Γ : Type uDepth1} [Inhabited Γ] (L R : List Γ) (a : Γ) : Turing.Tape.move Turing.Dir.left (Turing.Tape.mk₂ (a :: L) R) = Turing.Tape.mk₂ L (a :: R)

theorem Complexity.DepthThreeLowerBound.TapeWord.move_left_iterate_mk₂_append {Γ : Type uDepth1} [Inhabited Γ] («prefix» L R : List Γ) : (Turing.Tape.move Turing.Dir.left)^[«prefix».length] (Turing.Tape.mk₂ («prefix» ++ L) R) = Turing.Tape.mk₂ L («prefix».reverse ++ R)

theorem Complexity.DepthThreeLowerBound.TapeWord.move_left_iterate_reverse_mk₂ {Γ : Type uDepth1} [Inhabited Γ] («prefix» L R : List Γ) : (Turing.Tape.move Turing.Dir.left)^[«prefix».length] (Turing.Tape.mk₂ («prefix».reverse ++ L) R) = Turing.Tape.mk₂ L («prefix» ++ R)

theorem Complexity.DepthThreeLowerBound.TapeWord.move_right_then_left_mk₂_append {Γ : Type uDepth1} [Inhabited Γ] («prefix» L R : List Γ) : (Turing.Tape.move Turing.Dir.left)^[«prefix».length] ((Turing.Tape.move Turing.Dir.right)^[«prefix».length] (Turing.Tape.mk₂ L («prefix» ++ R))) = Turing.Tape.mk₂ L («prefix» ++ R)