Unrestricted depth-three lower bound: tape erase

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

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

inductive Complexity.DepthThreeLowerBound.TapeErase.State : Type

Control states of the erase routine.

• start : State
• scan : State
• erase : State
• install : State
• done : State

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeErase.instDecidableEqState : DecidableEq State

Equations

• Complexity.DepthThreeLowerBound.TapeErase.instDecidableEqState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeErase.instInhabitedState : Inhabited State

Equations

• Complexity.DepthThreeLowerBound.TapeErase.instInhabitedState = { default := Complexity.DepthThreeLowerBound.TapeErase.instInhabitedState.default }

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeErase.instFintypeState : Fintype State

Equations

• One or more equations did not get rendered due to their size.

def Complexity.DepthThreeLowerBound.TapeErase.code (r : TapeRegister) : TapeMultiProgram State

Transition function of the erase routine.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.TapeErase.code r Complexity.DepthThreeLowerBound.TapeErase.State.done x✝ = none

theorem Complexity.DepthThreeLowerBound.TapeErase.step_start (r : TapeRegister) (T : TapeTapes) (S : Turing.Tape TapeSymbol) : (code r).step (TapeMultiProgram.cfg State.start (Function.update T r S)) = some (TapeMultiProgram.cfg State.scan (Function.update T r (Turing.Tape.move Turing.Dir.right S)))

theorem Complexity.DepthThreeLowerBound.TapeErase.step_scan_bit (r : TapeRegister) (T : TapeTapes) (S : Turing.Tape TapeSymbol) (b : Bool) (hS : S.head = rawInputSymbol b) : (code r).step (TapeMultiProgram.cfg State.scan (Function.update T r S)) = some (TapeMultiProgram.cfg State.scan (Function.update T r (Turing.Tape.move Turing.Dir.right S)))

theorem Complexity.DepthThreeLowerBound.TapeErase.step_scan_end (r : TapeRegister) (T : TapeTapes) (S : Turing.Tape TapeSymbol) (hS : S.head = cleanAtom TapeAtom.endMark) : (code r).step (TapeMultiProgram.cfg State.scan (Function.update T r S)) = some (TapeMultiProgram.cfg State.erase (Function.update T r S))

theorem Complexity.DepthThreeLowerBound.TapeErase.step_erase_symbol (r : TapeRegister) (T : TapeTapes) (S : Turing.Tape TapeSymbol) (hS : S.head.1 ≠ TapeAtom.home) : (code r).step (TapeMultiProgram.cfg State.erase (Function.update T r S)) = some (TapeMultiProgram.cfg State.erase (Function.update T r (Turing.Tape.move Turing.Dir.left (Turing.Tape.write blankSymbol S))))

theorem Complexity.DepthThreeLowerBound.TapeErase.step_erase_home (r : TapeRegister) (T : TapeTapes) (S : Turing.Tape TapeSymbol) (hS : S.head.1 = TapeAtom.home) : (code r).step (TapeMultiProgram.cfg State.erase (Function.update T r S)) = some (TapeMultiProgram.cfg State.install (Function.update T r (Turing.Tape.move Turing.Dir.right S)))

theorem Complexity.DepthThreeLowerBound.TapeErase.step_install (r : TapeRegister) (T : TapeTapes) (S : Turing.Tape TapeSymbol) : (code r).step (TapeMultiProgram.cfg State.install (Function.update T r S)) = some (TapeMultiProgram.cfg State.done (Function.update T r (Turing.Tape.move Turing.Dir.left (Turing.Tape.write (cleanAtom TapeAtom.endMark) S))))

theorem Complexity.DepthThreeLowerBound.TapeErase.mk₂_append_blanks (L R : List TapeSymbol) (n : ℕ) : Turing.Tape.mk₂ L (R ++ List.replicate n blankSymbol) = Turing.Tape.mk₂ L R

theorem Complexity.DepthThreeLowerBound.TapeErase.runs_scan (r : TapeRegister) (T : TapeTapes) (bits : List Bool) (L : List TapeSymbol) : RunsIn (code r).step (TapeMultiProgram.cfg State.scan (Function.update T r (Turing.Tape.mk₂ L (encodeInput bits ++ [cleanAtom TapeAtom.endMark])))) (TapeMultiProgram.cfg State.erase (Function.update T r (Turing.Tape.mk₂ ((encodeInput bits).reverse ++ L) [cleanAtom TapeAtom.endMark]))) (bits.length + 1)

theorem Complexity.DepthThreeLowerBound.TapeErase.runs_finish (r : TapeRegister) (T : TapeTapes) (n : ℕ) : RunsIn (code r).step (TapeMultiProgram.cfg State.erase (Function.update T r (Turing.Tape.mk₂ [] (cleanAtom TapeAtom.home :: blankSymbol :: List.replicate n blankSymbol)))) (TapeMultiProgram.cfg State.done (Function.update T r (wordTape []))) 2

theorem Complexity.DepthThreeLowerBound.TapeErase.runs_erase_back (r : TapeRegister) (T : TapeTapes) (bits : List Bool) (a : TapeSymbol) (n : ℕ) (ha : a.1 ≠ TapeAtom.home) : RunsIn (code r).step (TapeMultiProgram.cfg State.erase (Function.update T r (Turing.Tape.mk₂ (encodeInput bits ++ [cleanAtom TapeAtom.home]) (a :: List.replicate n blankSymbol)))) (TapeMultiProgram.cfg State.done (Function.update T r (wordTape []))) (bits.length + 3)

theorem Complexity.DepthThreeLowerBound.TapeErase.runs_erase (r : TapeRegister) (T : TapeTapes) (bits : List Bool) : RunsIn (code r).step (TapeMultiProgram.cfg State.start (Function.update T r (wordTape bits))) (TapeMultiProgram.cfg State.done (Function.update T r (wordTape []))) (2 * bits.length + 5)

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeErase.step_done (r : TapeRegister) (T : TapeTapes) : (code r).step (TapeMultiProgram.cfg State.done T) = none