Unrestricted depth-three lower bound: tape unary

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

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

def Complexity.DepthThreeLowerBound.TapeUnary.counterTape (n : ℕ) : Turing.Tape TapeSymbol

Represent a natural number by a unary word of true bits.

Equations

• Complexity.DepthThreeLowerBound.TapeUnary.counterTape n = Complexity.DepthThreeLowerBound.wordTape (List.replicate n true)

theorem Complexity.DepthThreeLowerBound.TapeUnary.prepend_home (bits : List Bool) (b : Bool) : Turing.Tape.write (cleanAtom TapeAtom.home) (Turing.Tape.move Turing.Dir.left (Turing.Tape.write (rawInputSymbol b) (wordTape bits))) = wordTape (b :: bits)

theorem Complexity.DepthThreeLowerBound.TapeUnary.remove_home (bits : List Bool) (b : Bool) : Turing.Tape.write (cleanAtom TapeAtom.home) (Turing.Tape.move Turing.Dir.right (Turing.Tape.write blankSymbol (wordTape (b :: bits)))) = wordTape bits

inductive Complexity.DepthThreeLowerBound.TapeUnary.IncState : Type

Control states for the inc stage of the unary routine.

• start : IncState
• newHome : IncState
• done : IncState

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeUnary.instDecidableEqIncState : DecidableEq IncState

Equations

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

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeUnary.instFintypeIncState : Fintype IncState

Equations

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

def Complexity.DepthThreeLowerBound.TapeUnary.incProgram (r : TapeRegister) : TapeMultiProgram IncState

Transition function for the inc stage of the unary routine.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.TapeUnary.incProgram r Complexity.DepthThreeLowerBound.TapeUnary.IncState.done x✝ = none

theorem Complexity.DepthThreeLowerBound.TapeUnary.increment_word (r : TapeRegister) (T : TapeTapes) (bits : List Bool) (hT : T r = wordTape bits) : RunsIn (incProgram r).step (TapeMultiProgram.cfg IncState.start T) (TapeMultiProgram.cfg IncState.done (Function.update T r (wordTape (true :: bits)))) 2

theorem Complexity.DepthThreeLowerBound.TapeUnary.increment (r : TapeRegister) (T : TapeTapes) (n : ℕ) (hT : T r = counterTape n) : RunsIn (incProgram r).step (TapeMultiProgram.cfg IncState.start T) (TapeMultiProgram.cfg IncState.done (Function.update T r (counterTape (n + 1)))) 2

inductive Complexity.DepthThreeLowerBound.TapeUnary.DecState : Type

Control states for the dec stage of the unary routine.

• start : DecState
• inspect : DecState
• eraseHome : DecState
• newHome : DecState
• done (wasPositive : Bool) : DecState

def Complexity.DepthThreeLowerBound.TapeUnary.instDecidableEqDecState.decEq (x✝ x✝¹ : DecState) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeUnary.instDecidableEqDecState : DecidableEq DecState

Equations

• Complexity.DepthThreeLowerBound.TapeUnary.instDecidableEqDecState = Complexity.DepthThreeLowerBound.TapeUnary.instDecidableEqDecState.decEq

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeUnary.instFintypeDecState : Fintype DecState

Equations

• Complexity.DepthThreeLowerBound.TapeUnary.instFintypeDecState = Fintype.ofEquiv (Unit ⊕ Unit ⊕ Unit ⊕ Unit ⊕ Bool) Complexity.DepthThreeLowerBound.TapeUnary.DecState.proxyTypeEquiv

def Complexity.DepthThreeLowerBound.TapeUnary.decProgram (r : TapeRegister) : TapeMultiProgram DecState

Transition function for the dec stage of the unary routine.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.TapeUnary.decProgram r (Complexity.DepthThreeLowerBound.TapeUnary.DecState.done wasPositive) x✝ = none

theorem Complexity.DepthThreeLowerBound.TapeUnary.decrement_empty (r : TapeRegister) (T : TapeTapes) (hT : T r = wordTape []) : RunsIn (decProgram r).step (TapeMultiProgram.cfg DecState.start T) (TapeMultiProgram.cfg (DecState.done false) T) 2

theorem Complexity.DepthThreeLowerBound.TapeUnary.decrement_cons (r : TapeRegister) (T : TapeTapes) (bits : List Bool) (b : Bool) (hT : T r = wordTape (b :: bits)) : RunsIn (decProgram r).step (TapeMultiProgram.cfg DecState.start T) (TapeMultiProgram.cfg (DecState.done true) (Function.update T r (wordTape bits))) 4

theorem Complexity.DepthThreeLowerBound.TapeUnary.decrement (r : TapeRegister) (T : TapeTapes) (n : ℕ) (hT : T r = counterTape n) : RunsIn (decProgram r).step (TapeMultiProgram.cfg DecState.start T) (TapeMultiProgram.cfg (DecState.done (decide (0 < n))) (Function.update T r (counterTape (n - 1)))) 4