Unrestricted depth-three lower bound: tape array

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

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

inductive Complexity.DepthThreeLowerBound.TapeArray.State : Type

Control states of the array routine.

• start : State
• scan : State
• rewind (read : Bool) : State
• done (read : Bool) : State

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeArray.instDecidableEqState : DecidableEq State

Equations

• Complexity.DepthThreeLowerBound.TapeArray.instDecidableEqState = Complexity.DepthThreeLowerBound.TapeArray.instDecidableEqState.decEq

def Complexity.DepthThreeLowerBound.TapeArray.instDecidableEqState.decEq (x✝ x✝¹ : State) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.TapeArray.instDecidableEqState.decEq Complexity.DepthThreeLowerBound.TapeArray.State.start Complexity.DepthThreeLowerBound.TapeArray.State.start = isTrue ⋯
• Complexity.DepthThreeLowerBound.TapeArray.instDecidableEqState.decEq Complexity.DepthThreeLowerBound.TapeArray.State.scan Complexity.DepthThreeLowerBound.TapeArray.State.scan = isTrue ⋯
• Complexity.DepthThreeLowerBound.TapeArray.instDecidableEqState.decEq Complexity.DepthThreeLowerBound.TapeArray.State.scan (Complexity.DepthThreeLowerBound.TapeArray.State.done read) = isFalse ⋯
• Complexity.DepthThreeLowerBound.TapeArray.instDecidableEqState.decEq (Complexity.DepthThreeLowerBound.TapeArray.State.done read) Complexity.DepthThreeLowerBound.TapeArray.State.scan = isFalse ⋯

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeArray.instFintypeState : Fintype State

Equations

• Complexity.DepthThreeLowerBound.TapeArray.instFintypeState = Fintype.ofEquiv (Unit ⊕ Unit ⊕ Bool ⊕ Bool) Complexity.DepthThreeLowerBound.TapeArray.State.proxyTypeEquiv

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeArray.instInhabitedState : Inhabited State

Equations

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

def Complexity.DepthThreeLowerBound.TapeArray.code (index array : TapeRegister) (f : Bool → Bool) : TapeMultiProgram State

Transition function of the array routine.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.TapeArray.code index array f (Complexity.DepthThreeLowerBound.TapeArray.State.done read) x✝ = none

theorem Complexity.DepthThreeLowerBound.TapeArray.step_start {index array : TapeRegister} (hne : index ≠ array) (f : Bool → Bool) (T : TapeTapes) (I A : Turing.Tape TapeSymbol) : (code index array f).step (TapeMultiProgram.cfg State.start (TapeCopy.onPair index array T I A)) = some (TapeMultiProgram.cfg State.scan (TapeCopy.onPair index array T (Turing.Tape.move Turing.Dir.right I) (Turing.Tape.move Turing.Dir.right A)))

theorem Complexity.DepthThreeLowerBound.TapeArray.step_scan_bit {index array : TapeRegister} (hne : index ≠ array) (f : Bool → Bool) (T : TapeTapes) (I A : Turing.Tape TapeSymbol) (hI : I.head = rawInputSymbol true) : (code index array f).step (TapeMultiProgram.cfg State.scan (TapeCopy.onPair index array T I A)) = some (TapeMultiProgram.cfg State.scan (TapeCopy.onPair index array T (Turing.Tape.move Turing.Dir.right I) (Turing.Tape.move Turing.Dir.right A)))

theorem Complexity.DepthThreeLowerBound.TapeArray.step_scan_end {index array : TapeRegister} (hne : index ≠ array) (f : Bool → Bool) (T : TapeTapes) (I A : Turing.Tape TapeSymbol) (b : Bool) (hI : I.head = cleanAtom TapeAtom.endMark) (hA : A.head = rawInputSymbol b) : (code index array f).step (TapeMultiProgram.cfg State.scan (TapeCopy.onPair index array T I A)) = some (TapeMultiProgram.cfg (State.rewind b) (TapeCopy.onPair index array T I (Turing.Tape.write (rawInputSymbol (f b)) A)))

theorem Complexity.DepthThreeLowerBound.TapeArray.step_rewind_move {index array : TapeRegister} (hne : index ≠ array) (f : Bool → Bool) (T : TapeTapes) (I A : Turing.Tape TapeSymbol) (b : Bool) (hI : I.head.1 ≠ TapeAtom.home) : (code index array f).step (TapeMultiProgram.cfg (State.rewind b) (TapeCopy.onPair index array T I A)) = some (TapeMultiProgram.cfg (State.rewind b) (TapeCopy.onPair index array T (Turing.Tape.move Turing.Dir.left I) (Turing.Tape.move Turing.Dir.left A)))

theorem Complexity.DepthThreeLowerBound.TapeArray.step_rewind_home {index array : TapeRegister} (hne : index ≠ array) (f : Bool → Bool) (T : TapeTapes) (I A : Turing.Tape TapeSymbol) (b : Bool) (hI : I.head.1 = TapeAtom.home) : (code index array f).step (TapeMultiProgram.cfg (State.rewind b) (TapeCopy.onPair index array T I A)) = some (TapeMultiProgram.cfg (State.done b) (TapeCopy.onPair index array T I A))

theorem Complexity.DepthThreeLowerBound.TapeArray.runs_scan {index array : TapeRegister} (hne : index ≠ array) (f : Bool → Bool) (T : TapeTapes) («prefix» : List Bool) (LI LA R : List TapeSymbol) : RunsIn (code index array f).step (TapeMultiProgram.cfg State.scan (TapeCopy.onPair index array T (Turing.Tape.mk₂ LI (List.replicate «prefix».length (rawInputSymbol true) ++ [cleanAtom TapeAtom.endMark])) (Turing.Tape.mk₂ LA (encodeInput «prefix» ++ R)))) (TapeMultiProgram.cfg State.scan (TapeCopy.onPair index array T (Turing.Tape.mk₂ (List.replicate «prefix».length (rawInputSymbol true) ++ LI) [cleanAtom TapeAtom.endMark]) (Turing.Tape.mk₂ ((encodeInput «prefix»).reverse ++ LA) R))) «prefix».length

theorem Complexity.DepthThreeLowerBound.TapeArray.runs_rewind {index array : TapeRegister} (hne : index ≠ array) (f : Bool → Bool) (T : TapeTapes) (left : List Bool) (b : Bool) (i : TapeSymbol) (RI RA : List TapeSymbol) (hi : i.1 ≠ TapeAtom.home) : RunsIn (code index array f).step (TapeMultiProgram.cfg (State.rewind b) (TapeCopy.onPair index array T (Turing.Tape.mk₂ (List.replicate left.length (rawInputSymbol true) ++ [cleanAtom TapeAtom.home]) (i :: RI)) (Turing.Tape.mk₂ (encodeInput left ++ [cleanAtom TapeAtom.home]) RA))) (TapeMultiProgram.cfg (State.done b) (TapeCopy.onPair index array T (Turing.Tape.mk₂ [] (cleanAtom TapeAtom.home :: (List.replicate left.length (rawInputSymbol true) ++ i :: RI))) (Turing.Tape.mk₂ [] (cleanAtom TapeAtom.home :: ((encodeInput left).reverse ++ RA))))) (left.length + 2)

theorem Complexity.DepthThreeLowerBound.TapeArray.runs_modify {index array : TapeRegister} (hne : index ≠ array) (f : Bool → Bool) (T : TapeTapes) («prefix» suffix : List Bool) (b : Bool) : RunsIn (code index array f).step (TapeMultiProgram.cfg State.start (TapeCopy.onPair index array T (wordTape (List.replicate «prefix».length true)) (wordTape («prefix» ++ b :: suffix)))) (TapeMultiProgram.cfg (State.done b) (TapeCopy.onPair index array T (wordTape (List.replicate «prefix».length true)) (wordTape («prefix» ++ f b :: suffix)))) (2 * «prefix».length + 4)

theorem Complexity.DepthThreeLowerBound.TapeArray.runs_read {index array : TapeRegister} (hne : index ≠ array) (T : TapeTapes) («prefix» suffix : List Bool) (b : Bool) : RunsIn (code index array id).step (TapeMultiProgram.cfg State.start (TapeCopy.onPair index array T (wordTape (List.replicate «prefix».length true)) (wordTape («prefix» ++ b :: suffix)))) (TapeMultiProgram.cfg (State.done b) (TapeCopy.onPair index array T (wordTape (List.replicate «prefix».length true)) (wordTape («prefix» ++ b :: suffix)))) (2 * «prefix».length + 4)

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeArray.step_done (index array : TapeRegister) (f : Bool → Bool) (T : TapeTapes) (b : Bool) : (code index array f).step (TapeMultiProgram.cfg (State.done b) T) = none