Unrestricted depth-three lower bound: multi tape machine

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

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

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.instDecidableEqHeadMove : DecidableEq HeadMove

Equations

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

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.instInhabitedHeadMove : Inhabited HeadMove

Equations

• Complexity.DepthThreeLowerBound.instInhabitedHeadMove = { default := Complexity.DepthThreeLowerBound.instInhabitedHeadMove.default }

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.instFintypeHeadMove : Fintype HeadMove

Equations

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

@[simp]

theorem Complexity.DepthThreeLowerBound.HeadMove.apply_left {Γ : Type uDepth1} [Inhabited Γ] (t : Turing.Tape Γ) : left.apply t = Turing.Tape.move Turing.Dir.left t

@[simp]

theorem Complexity.DepthThreeLowerBound.HeadMove.apply_stay {Γ : Type uDepth2} [Inhabited Γ] (t : Turing.Tape Γ) : stay.apply t = t

@[simp]

theorem Complexity.DepthThreeLowerBound.HeadMove.apply_right {Γ : Type uDepth3} [Inhabited Γ] (t : Turing.Tape Γ) : right.apply t = Turing.Tape.move Turing.Dir.right t

theorem Complexity.DepthThreeLowerBound.multiTapeStep_eq_some {K : Type uDepth4} {Γ : Type uDepth5} {Q : Type uDepth6} [Inhabited Γ] {code : MultiTapeCode K Γ Q} {c : MultiTapeCfg K Γ Q} {q : Q} {writes : K → Γ} {moves : K → HeadMove} (h : (code c.q fun (k : K) => (c.tapes k).head) = some (q, writes, moves)) : multiTapeStep code c = some (multiTapeUpdate c q writes moves)

@[simp]

theorem Complexity.DepthThreeLowerBound.multiTapeStep_eq_none_iff {K : Type uDepth7} {Γ : Type uDepth8} {Q : Type uDepth9} [Inhabited Γ] (code : MultiTapeCode K Γ Q) (c : MultiTapeCfg K Γ Q) : multiTapeStep code c = none ↔ (code c.q fun (k : K) => (c.tapes k).head) = none

@[simp]

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeMachine.init_q (M : FiniteMultiTapeMachine) (input : List Bool) : (M.init input).q = M.initialState

@[simp]

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeMachine.init_inputTape (M : FiniteMultiTapeMachine) (input : List Bool) : (M.init input).tapes M.inputTape = Turing.Tape.mk₁ (List.map M.inputSymbol input)

theorem Complexity.DepthThreeLowerBound.FiniteMultiTapeMachine.init_otherTape (M : FiniteMultiTapeMachine) (input : List Bool) (k : M.K) (hk : k ≠ M.inputTape) : (M.init input).tapes k = Turing.Tape.mk₁ []

theorem Complexity.DepthThreeLowerBound.multiTapeHaltsIn_iff_runsIn (M : FiniteMultiTapeMachine) (input : List Bool) (output : Bool) (time : ℕ) : MultiTapeHaltsIn M input output time ↔ ∃ (c : M.Cfg), RunsIn M.step (M.init input) c time ∧ M.step c = none ∧ M.accept c.q = output

theorem Complexity.DepthThreeLowerBound.MultiTapeHaltsIn.mono {M : FiniteMultiTapeMachine} {input : List Bool} {output : Bool} {m n : ℕ} (h : MultiTapeHaltsIn M input output m) (hmn : m ≤ n) : MultiTapeHaltsIn M input output n

def Complexity.DepthThreeLowerBound.MultiTapePolynomialTimeDecider (f : List Bool → Bool) : Prop

A fixed finite multitape machine decides the language in polynomial time.

Equations

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