Unrestricted depth-three lower bound: tape word

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/TapeWord.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.head_mk₂_cons {Γ : Type uDepth1} [Inhabited Γ] (L R : List Γ) (a : Γ) : (Turing.Tape.mk₂ L (a :: R)).head = a

@[simp]

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

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeWord.write_mk₂_cons {Γ : Type uDepth1} [Inhabited Γ] (L R : List Γ) (a b : Γ) : Turing.Tape.write b (Turing.Tape.mk₂ L (a :: R)) = Turing.Tape.mk₂ L (b :: R)

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