Unrestricted depth-three lower bound: tape routing

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

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

def Complexity.DepthThreeLowerBound.TapeRouting.joinCode {Q : Type uDepth1} {R : Type uDepth2} (P : TapeMultiProgram Q) (B : TapeMultiProgram R) (entry : Q → R) : TapeMultiProgram (Q ⊕ R)

Transition function for the join stage of the routing routine.

Equations

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

theorem Complexity.DepthThreeLowerBound.TapeRouting.join_runs {Q : Type uDepth3} {R : Type uDepth4} (P : TapeMultiProgram Q) (B : TapeMultiProgram R) (entry : Q → R) {q q' : Q} {r : R} {T U V : TapeTapes} {m n : ℕ} (hP : RunsIn P.step (TapeMultiProgram.cfg q T) (TapeMultiProgram.cfg q' U) m) (hhalt : P q' (TapeMultiProgram.heads U) = none) (hB : RunsIn B.step (TapeMultiProgram.cfg (entry q') U) (TapeMultiProgram.cfg r V) n) : RunsIn (joinCode P B entry).step (TapeMultiProgram.cfg (Sum.inl q) T) (TapeMultiProgram.cfg (Sum.inr r) V) (m + 1 + n)

theorem Complexity.DepthThreeLowerBound.TapeRouting.join_done {Q : Type uDepth5} {R : Type uDepth6} (P : TapeMultiProgram Q) (B : TapeMultiProgram R) (entry : Q → R) (r : R) (h : TapeHeads) (hh : B r h = none) : joinCode P B entry (Sum.inr r) h = none

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeRouting.LoopState (Q : Type uDepth7) (R : Type uDepth8) : Type (max uDepth8 uDepth7)

Control states for the loop stage of the routing routine.

Equations

• Complexity.DepthThreeLowerBound.TapeRouting.LoopState Q R = ((Q ⊕ R) ⊕ Unit)

def Complexity.DepthThreeLowerBound.TapeRouting.loopTest {Q : Type uDepth9} {R : Type uDepth10} (q : Q) : LoopState Q R

Embed a test-stage state in the loop control.

Equations

• Complexity.DepthThreeLowerBound.TapeRouting.loopTest q = Sum.inl (Sum.inl q)

def Complexity.DepthThreeLowerBound.TapeRouting.loopBody {Q : Type uDepth11} {R : Type uDepth12} (r : R) : LoopState Q R

Embed a body-stage state in the loop control.

Equations

• Complexity.DepthThreeLowerBound.TapeRouting.loopBody r = Sum.inl (Sum.inr r)

def Complexity.DepthThreeLowerBound.TapeRouting.loopDone {Q : Type uDepth13} {R : Type uDepth14} : LoopState Q R

Terminal control state of the loop stage of the routing routine.

Equations

• Complexity.DepthThreeLowerBound.TapeRouting.loopDone = Sum.inr ()

def Complexity.DepthThreeLowerBound.TapeRouting.loopCode {Q : Type uDepth15} {R : Type uDepth16} (P : TapeMultiProgram Q) (B : TapeMultiProgram R) (testEntry : Q) (bodyEntry : R) (again : Q → Bool) : TapeMultiProgram (LoopState Q R)

Transition function for the loop stage of the routing routine.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.TapeRouting.loopCode P B testEntry bodyEntry again (Sum.inr val) x✝ = none

theorem Complexity.DepthThreeLowerBound.TapeRouting.loop_test_runs {Q : Type uDepth17} {R : Type uDepth18} (P : TapeMultiProgram Q) (B : TapeMultiProgram R) (testEntry : Q) (bodyEntry : R) (again : Q → Bool) {q q' : Q} {T U : TapeTapes} {m : ℕ} (h : RunsIn P.step (TapeMultiProgram.cfg q T) (TapeMultiProgram.cfg q' U) m) : RunsIn (loopCode P B testEntry bodyEntry again).step (TapeMultiProgram.cfg (loopTest q) T) (TapeMultiProgram.cfg (loopTest q') U) m

theorem Complexity.DepthThreeLowerBound.TapeRouting.loop_body_runs {Q : Type uDepth19} {R : Type uDepth20} (P : TapeMultiProgram Q) (B : TapeMultiProgram R) (testEntry : Q) (bodyEntry : R) (again : Q → Bool) {r r' : R} {T U : TapeTapes} {m : ℕ} (h : RunsIn B.step (TapeMultiProgram.cfg r T) (TapeMultiProgram.cfg r' U) m) : RunsIn (loopCode P B testEntry bodyEntry again).step (TapeMultiProgram.cfg (loopBody r) T) (TapeMultiProgram.cfg (loopBody r') U) m

theorem Complexity.DepthThreeLowerBound.TapeRouting.loop_exit {Q : Type uDepth21} {R : Type uDepth22} (P : TapeMultiProgram Q) (B : TapeMultiProgram R) (testEntry : Q) (bodyEntry : R) (again : Q → Bool) {q : Q} {T U : TapeTapes} {m : ℕ} (h : RunsIn P.step (TapeMultiProgram.cfg testEntry T) (TapeMultiProgram.cfg q U) m) (hhalt : P q (TapeMultiProgram.heads U) = none) (hstop : again q = false) : RunsIn (loopCode P B testEntry bodyEntry again).step (TapeMultiProgram.cfg (loopTest testEntry) T) (TapeMultiProgram.cfg loopDone U) (m + 1)

theorem Complexity.DepthThreeLowerBound.TapeRouting.loop_iter {Q : Type uDepth23} {R : Type uDepth24} (P : TapeMultiProgram Q) (B : TapeMultiProgram R) (testEntry : Q) (bodyEntry : R) (again : Q → Bool) {q : Q} {r : R} {T U V : TapeTapes} {m n : ℕ} (hP : RunsIn P.step (TapeMultiProgram.cfg testEntry T) (TapeMultiProgram.cfg q U) m) (hPhalt : P q (TapeMultiProgram.heads U) = none) (hgo : again q = true) (hB : RunsIn B.step (TapeMultiProgram.cfg bodyEntry U) (TapeMultiProgram.cfg r V) n) (hBhalt : B r (TapeMultiProgram.heads V) = none) : RunsIn (loopCode P B testEntry bodyEntry again).step (TapeMultiProgram.cfg (loopTest testEntry) T) (TapeMultiProgram.cfg (loopTest testEntry) V) (m + 1 + n + 1)

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeRouting.loop_done {Q : Type uDepth25} {R : Type uDepth26} (P : TapeMultiProgram Q) (B : TapeMultiProgram R) (testEntry : Q) (bodyEntry : R) (again : Q → Bool) (h : TapeHeads) : loopCode P B testEntry bodyEntry again loopDone h = none