Unrestricted depth-three lower bound: tape rewind

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

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

theorem Complexity.DepthThreeLowerBound.cursorTape_left_nil (after : List Bool) : Turing.Tape.move Turing.Dir.left (cursorTape [] after) = wordTape after

theorem Complexity.DepthThreeLowerBound.cursorTape_left_append (before after : List Bool) (b : Bool) : Turing.Tape.move Turing.Dir.left (cursorTape (before ++ [b]) after) = cursorTape before (b :: after)

inductive Complexity.DepthThreeLowerBound.TapeRewind.State : Type

Control states of the rewind routine.

• run : State
• done : State

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeRewind.instDecidableEqState : DecidableEq State

Equations

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

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeRewind.instInhabitedState : Inhabited State

Equations

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

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeRewind.instFintypeState : Fintype State

Equations

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

def Complexity.DepthThreeLowerBound.TapeRewind.program (r : TapeRegister) : TapeMultiProgram State

Transition function of the rewind routine.

Equations

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

theorem Complexity.DepthThreeLowerBound.TapeRewind.step_cursor (r : TapeRegister) (T : TapeTapes) (before after : List Bool) : (program r).step (TapeMultiProgram.cfg State.run (Function.update T r (cursorTape before after))) = some (TapeMultiProgram.cfg State.run (Function.update T r (Turing.Tape.move Turing.Dir.left (cursorTape before after))))

theorem Complexity.DepthThreeLowerBound.TapeRewind.step_home (r : TapeRegister) (T : TapeTapes) (bits : List Bool) : (program r).step (TapeMultiProgram.cfg State.run (Function.update T r (wordTape bits))) = some (TapeMultiProgram.cfg State.done (Function.update T r (wordTape bits)))

theorem Complexity.DepthThreeLowerBound.TapeRewind.runs_cursor (r : TapeRegister) (T : TapeTapes) (before after : List Bool) : RunsIn (program r).step (TapeMultiProgram.cfg State.run (Function.update T r (cursorTape before after))) (TapeMultiProgram.cfg State.done (Function.update T r (wordTape (before ++ after)))) (before.length + 2)