Unrestricted depth-three lower bound: tape multi program

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

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

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeHeads : Type

One scanned tape symbol for each register.

Equations

• Complexity.DepthThreeLowerBound.TapeHeads = (Complexity.DepthThreeLowerBound.TapeRegister → Complexity.DepthThreeLowerBound.TapeSymbol)

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeMoves : Type

One head movement for each register.

Equations

• Complexity.DepthThreeLowerBound.TapeMoves = (Complexity.DepthThreeLowerBound.TapeRegister → Complexity.DepthThreeLowerBound.HeadMove)

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeTapes : Type

The collection of tapes indexed by registers.

Equations

• Complexity.DepthThreeLowerBound.TapeTapes = (Complexity.DepthThreeLowerBound.TapeRegister → Turing.Tape Complexity.DepthThreeLowerBound.TapeSymbol)

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeMultiCfg (Q : Type uDepth1) : Type uDepth1

Multitape configurations for the register and symbol types used by the evaluator.

Equations

• Complexity.DepthThreeLowerBound.TapeMultiCfg Q = Complexity.DepthThreeLowerBound.MultiTapeCfg Complexity.DepthThreeLowerBound.TapeRegister Complexity.DepthThreeLowerBound.TapeSymbol Q

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeMultiProgram (Q : Type uDepth2) : Type uDepth2

Transition programs over the evaluator's fixed register and symbol types.

Equations

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

def Complexity.DepthThreeLowerBound.wordTape (bits : List Bool) : Turing.Tape TapeSymbol

Encode a bit word on a tape with its head at the start of the word.

Equations

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

def Complexity.DepthThreeLowerBound.cursorTape (before after : List Bool) : Turing.Tape TapeSymbol

Encode a bit word with a specified prefix already passed by the head.

Equations

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

@[simp]

theorem Complexity.DepthThreeLowerBound.wordTape_head (bits : List Bool) : (wordTape bits).head = cleanAtom TapeAtom.home

@[simp]

theorem Complexity.DepthThreeLowerBound.cursorTape_head_cons (before after : List Bool) (b : Bool) : (cursorTape before (b :: after)).head = rawInputSymbol b

@[simp]

theorem Complexity.DepthThreeLowerBound.cursorTape_head_nil (before : List Bool) : (cursorTape before []).head = cleanAtom TapeAtom.endMark

@[simp]

theorem Complexity.DepthThreeLowerBound.wordTape_right (bits : List Bool) : Turing.Tape.move Turing.Dir.right (wordTape bits) = cursorTape [] bits

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

def Complexity.DepthThreeLowerBound.TapeMultiProgram.step {Q : Type uDepth3} (P : TapeMultiProgram Q) : TapeMultiCfg Q → Option (TapeMultiCfg Q)

Execute one transition of the fixed-register multitape program.

Equations

• P.step = Complexity.DepthThreeLowerBound.multiTapeStep P

def Complexity.DepthThreeLowerBound.TapeMultiProgram.cfg {Q : Type uDepth4} (q : Q) (T : TapeTapes) : TapeMultiCfg Q

Bundle a control state with the collection of tapes.

Equations

• Complexity.DepthThreeLowerBound.TapeMultiProgram.cfg q T = { q := q, tapes := T }

def Complexity.DepthThreeLowerBound.TapeMultiProgram.heads (T : TapeTapes) : TapeHeads

Read the scanned symbol of every tape.

Equations

• Complexity.DepthThreeLowerBound.TapeMultiProgram.heads T r = (T r).head

def Complexity.DepthThreeLowerBound.TapeMultiProgram.stayMoves : TapeMoves

Keep every tape head stationary.

Equations

• Complexity.DepthThreeLowerBound.TapeMultiProgram.stayMoves x✝ = Complexity.DepthThreeLowerBound.HeadMove.stay

def Complexity.DepthThreeLowerBound.TapeMultiProgram.moveOnly (r : TapeRegister) (d : HeadMove) : TapeMoves

Move the selected tape head and keep the remaining heads stationary.

Equations

• Complexity.DepthThreeLowerBound.TapeMultiProgram.moveOnly r d = Function.update Complexity.DepthThreeLowerBound.TapeMultiProgram.stayMoves r d

def Complexity.DepthThreeLowerBound.TapeMultiProgram.writeOnly (r : TapeRegister) (symbol : TapeSymbol) (h : TapeHeads) : TapeHeads

Change the selected scanned symbol and retain all other scanned symbols.

Equations

• Complexity.DepthThreeLowerBound.TapeMultiProgram.writeOnly r symbol h = Function.update h r symbol

def Complexity.DepthThreeLowerBound.TapeMultiProgram.jump {Q : Type uDepth5} (q : Q) (h : TapeHeads) : Option (Q × TapeHeads × TapeMoves)

Change only the control state, leaving all tape contents and heads fixed.

Equations

• Complexity.DepthThreeLowerBound.TapeMultiProgram.jump q h = some (q, h, Complexity.DepthThreeLowerBound.TapeMultiProgram.stayMoves)

def Complexity.DepthThreeLowerBound.TapeMultiProgram.move {Q : Type uDepth6} (r : TapeRegister) (d : HeadMove) (q : Q) (h : TapeHeads) : Option (Q × TapeHeads × TapeMoves)

Move a selected tape head while changing the control state.

Equations

• Complexity.DepthThreeLowerBound.TapeMultiProgram.move r d q h = some (q, h, Complexity.DepthThreeLowerBound.TapeMultiProgram.moveOnly r d)

def Complexity.DepthThreeLowerBound.TapeMultiProgram.writeMove {Q : Type uDepth7} (r : TapeRegister) (symbol : TapeSymbol) (d : HeadMove) (q : Q) (h : TapeHeads) : Option (Q × TapeHeads × TapeMoves)

Write and move on a selected tape while changing the control state.

Equations

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

def Complexity.DepthThreeLowerBound.TapeMultiProgram.isAtom (a : TapeAtom) (r : TapeRegister) (h : TapeHeads) : Bool

Test whether the selected tape head scans the specified atom.

Equations

• Complexity.DepthThreeLowerBound.TapeMultiProgram.isAtom a r h = decide ((h r).1 = a)

def Complexity.DepthThreeLowerBound.TapeMultiProgram.machine {Q : Type} [Fintype Q] (P : TapeMultiProgram Q) (initial : Q) (accept : Q → Bool) : FiniteMultiTapeMachine

Bundle a finite-state register program, initial state, and verdict function as a machine.

Equations

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