Unrestricted depth-three lower bound: tape branch

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/TapeBranch.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.TapeBranch.State (Q : Type uDepth1) (R : Type uDepth2) : Type (max uDepth1 uDepth2)

Control states of the branch routine.

Equations

• Complexity.DepthThreeLowerBound.TapeBranch.State Q R = (Q ⊕ R ⊕ Unit)

def Complexity.DepthThreeLowerBound.TapeBranch.test {Q : Type uDepth3} {R : Type uDepth4} (q : Q) : State Q R

Embed a test-stage state in the conditional routine.

Equations

• Complexity.DepthThreeLowerBound.TapeBranch.test q = Sum.inl q

def Complexity.DepthThreeLowerBound.TapeBranch.body {Q : Type uDepth5} {R : Type uDepth6} (r : R) : State Q R

Embed a body-stage state in the conditional routine.

Equations

• Complexity.DepthThreeLowerBound.TapeBranch.body r = Sum.inr (Sum.inl r)

def Complexity.DepthThreeLowerBound.TapeBranch.rejected {Q : Type uDepth7} {R : Type uDepth8} : State Q R

The conditional routine's rejecting terminal state.

Equations

• Complexity.DepthThreeLowerBound.TapeBranch.rejected = Sum.inr (Sum.inr ())

def Complexity.DepthThreeLowerBound.TapeBranch.program {Q : Type uDepth9} {R : Type uDepth10} (P : TapeMultiProgram Q) (B : TapeMultiProgram R) (entry : R) (accept : Q → Bool) : TapeMultiProgram (State Q R)

Transition function of the branch routine.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.TapeBranch.program P B entry accept (Sum.inr (Sum.inr val)) x✝ = none

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeBranch.rejected_halts {Q : Type uDepth11} {R : Type uDepth12} (P : TapeMultiProgram Q) (B : TapeMultiProgram R) (entry : R) (accept : Q → Bool) (h : TapeHeads) : program P B entry accept rejected h = none

theorem Complexity.DepthThreeLowerBound.TapeBranch.body_halts {Q : Type uDepth13} {R : Type uDepth14} (P : TapeMultiProgram Q) (B : TapeMultiProgram R) (entry : R) (accept : Q → Bool) (r : R) (h : TapeHeads) (hr : B r h = none) : program P B entry accept (body r) h = none

theorem Complexity.DepthThreeLowerBound.TapeBranch.runs_test {Q : Type uDepth15} {R : Type uDepth16} (P : TapeMultiProgram Q) (B : TapeMultiProgram R) (entry : R) (accept : Q → Bool) {q q' : Q} {T U : TapeTapes} {m : ℕ} (h : RunsIn P.step (TapeMultiProgram.cfg q T) (TapeMultiProgram.cfg q' U) m) : RunsIn (program P B entry accept).step (TapeMultiProgram.cfg (test q) T) (TapeMultiProgram.cfg (test q') U) m

theorem Complexity.DepthThreeLowerBound.TapeBranch.runs_reject {Q : Type uDepth17} {R : Type uDepth18} (P : TapeMultiProgram Q) (B : TapeMultiProgram R) (entry : R) (accept : Q → Bool) {q q' : Q} {T U : TapeTapes} {m : ℕ} (h : RunsIn P.step (TapeMultiProgram.cfg q T) (TapeMultiProgram.cfg q' U) m) (hhalt : P q' (TapeMultiProgram.heads U) = none) (hno : accept q' = false) : RunsIn (program P B entry accept).step (TapeMultiProgram.cfg (test q) T) (TapeMultiProgram.cfg rejected U) (m + 1)

theorem Complexity.DepthThreeLowerBound.TapeBranch.runs_accept {Q : Type uDepth19} {R : Type uDepth20} (P : TapeMultiProgram Q) (B : TapeMultiProgram R) (entry : R) (accept : Q → Bool) {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) (hyes : accept q' = true) (hB : RunsIn B.step (TapeMultiProgram.cfg entry U) (TapeMultiProgram.cfg r V) n) : RunsIn (program P B entry accept).step (TapeMultiProgram.cfg (test q) T) (TapeMultiProgram.cfg (body r) V) (m + 1 + n)