Unrestricted depth-three lower bound: tape multi routines

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

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

theorem Complexity.DepthThreeLowerBound.runSteps_map_of_some {S : Type uDepth1} {T : Type uDepth2} {step : S → Option S} {next : T → Option T} (f : S → T) (hstep : ∀ (a b : S), step a = some b → next (f a) = some (f b)) {n : ℕ} {a b : S} (h : runSteps step n (some a) = some b) : runSteps next n (some (f a)) = some (f b)

theorem Complexity.DepthThreeLowerBound.RunsIn.map {S : Type uDepth3} {T : Type uDepth4} {step : S → Option S} {next : T → Option T} (f : S → T) (hstep : ∀ (a b : S), step a = some b → next (f a) = some (f b)) {a b : S} {n : ℕ} (h : RunsIn step a b n) : RunsIn next (f a) (f b) n

def Complexity.DepthThreeLowerBound.TapeMultiProgram.mapCfg {Q : Type uDepth5} {R : Type uDepth6} (f : Q → R) (c : TapeMultiCfg Q) : TapeMultiCfg R

Map a configuration's control state while retaining all of its tapes.

Equations

• Complexity.DepthThreeLowerBound.TapeMultiProgram.mapCfg f c = { q := f c.q, tapes := c.tapes }

theorem Complexity.DepthThreeLowerBound.TapeMultiProgram.step_jump {Q : Type uDepth7} (P : TapeMultiProgram Q) (q q' : Q) (T : TapeTapes) (h : P q (heads T) = jump q' (heads T)) : P.step (cfg q T) = some (cfg q' T)

theorem Complexity.DepthThreeLowerBound.TapeMultiProgram.step_move {Q : Type uDepth8} (P : TapeMultiProgram Q) (q q' : Q) (T : TapeTapes) (r : TapeRegister) (d : HeadMove) (h : P q (heads T) = move r d q' (heads T)) : P.step (cfg q T) = some (cfg q' (Function.update T r (d.apply (T r))))

theorem Complexity.DepthThreeLowerBound.TapeMultiProgram.step_writeMove {Q : Type uDepth9} (P : TapeMultiProgram Q) (q q' : Q) (T : TapeTapes) (r : TapeRegister) (symbol : TapeSymbol) (d : HeadMove) (h : P q (heads T) = writeMove r symbol d q' (heads T)) : P.step (cfg q T) = some (cfg q' (Function.update T r (d.apply (Turing.Tape.write symbol (T r)))))

theorem Complexity.DepthThreeLowerBound.TapeMultiProgram.step_map {Q : Type uDepth10} {R : Type uDepth11} (P : TapeMultiProgram Q) (P' : TapeMultiProgram R) (f : Q → R) (hcode : ∀ (q : Q) (h : TapeHeads) (q' : Q) (writes : TapeHeads) (moves : TapeMoves), P q h = some (q', writes, moves) → P' (f q) h = some (f q', writes, moves)) (a b : TapeMultiCfg Q) (h : P.step a = some b) : P'.step (mapCfg f a) = some (mapCfg f b)

theorem Complexity.DepthThreeLowerBound.TapeMultiProgram.runs_map {Q : Type uDepth12} {R : Type uDepth13} (P : TapeMultiProgram Q) (P' : TapeMultiProgram R) (f : Q → R) (hcode : ∀ (q : Q) (h : TapeHeads) (q' : Q) (writes : TapeHeads) (moves : TapeMoves), P q h = some (q', writes, moves) → P' (f q) h = some (f q', writes, moves)) {a b : TapeMultiCfg Q} {n : ℕ} (h : RunsIn P.step a b n) : RunsIn P'.step (mapCfg f a) (mapCfg f b) n