Unrestricted depth-three lower bound: tape parameters

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

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

def Complexity.DepthThreeLowerBound.TapeParameters.cubeRegisters : TapePowerSearch.Registers

Allocate registers for the cube-root parameter search.

Equations

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

def Complexity.DepthThreeLowerBound.TapeParameters.sixthRegisters : TapePowerSearch.Registers

Allocate registers for the sixth-power parameter search.

Equations

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

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeParameters.cubeRegisters_zero : cubeRegisters 0 = 7

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeParameters.cubeRegisters_one : cubeRegisters 1 = 3

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeParameters.cubeRegisters_two : cubeRegisters 2 = 9

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeParameters.cubeRegisters_three : cubeRegisters 3 = 5

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeParameters.cubeRegisters_four : cubeRegisters 4 = 6

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeParameters.sixthRegisters_zero : sixthRegisters 0 = 7

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeParameters.sixthRegisters_one : sixthRegisters 1 = 4

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeParameters.sixthRegisters_two : sixthRegisters 2 = 9

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeParameters.sixthRegisters_three : sixthRegisters 3 = 5

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeParameters.sixthRegisters_four : sixthRegisters 4 = 2

def Complexity.DepthThreeLowerBound.TapeParameters.dataStore (σ : TapeStore) (n : ℕ) : TapeStore

Store the data dimension in unary in its designated register.

Equations

• Complexity.DepthThreeLowerBound.TapeParameters.dataStore σ n = Function.update σ 2 (List.replicate (Complexity.DepthThreeLowerBound.dataDimension n) true)

def Complexity.DepthThreeLowerBound.TapeParameters.outputStore (σ : TapeStore) (n : ℕ) : TapeStore

Tape-store contents at the output stage of the parameters routine.

Equations

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

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeParameters.outputStore_data (σ : TapeStore) (n : ℕ) : outputStore σ n 2 = List.replicate (dataDimension n) true

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeParameters.outputStore_hash (σ : TapeStore) (n : ℕ) : outputStore σ n 3 = List.replicate (hashDimension (dataDimension n)) true

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeParameters.outputStore_order (σ : TapeStore) (n : ℕ) : outputStore σ n 4 = List.replicate (independenceOrder (dataDimension n)) true

theorem Complexity.DepthThreeLowerBound.TapeParameters.outputStore_other (σ : TapeStore) (n : ℕ) (r : TapeRegister) (h2 : r ≠ 2) (h3 : r ≠ 3) (h4 : r ≠ 4) : outputStore σ n r = σ r

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeParameters.LengthState : Type

Control states for the length stage of the parameters routine.

Equations

• Complexity.DepthThreeLowerBound.TapeParameters.LengthState = (Complexity.DepthThreeLowerBound.TapeCopy.State ⊕ Complexity.DepthThreeLowerBound.TapeDivideFive.State)

def Complexity.DepthThreeLowerBound.TapeParameters.lengthProgram : TapeMultiProgram LengthState

Transition function for the length stage of the parameters routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeParameters.lengthStart : LengthState

Initial control state of the length stage of the parameters routine.

Equations

• Complexity.DepthThreeLowerBound.TapeParameters.lengthStart = Sum.inl Complexity.DepthThreeLowerBound.TapeCopy.State.start

def Complexity.DepthThreeLowerBound.TapeParameters.lengthDone (n : ℕ) : LengthState

Terminal control state of the length stage of the parameters routine.

Equations

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

theorem Complexity.DepthThreeLowerBound.TapeParameters.runs_length (σ : TapeStore) (n : ℕ) (h1 : σ 1 = List.replicate n true) (h2 : σ 2 = []) (h5 : σ 5 = []) : RunsIn lengthProgram.step (TapeMultiProgram.cfg lengthStart (storeTapes σ)) (TapeMultiProgram.cfg (lengthDone n) (storeTapes (dataStore σ n))) (10 * n + 8)

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeParameters.SquareState : Type

Control states for the square stage of the parameters routine.

Equations

• Complexity.DepthThreeLowerBound.TapeParameters.SquareState = (Complexity.DepthThreeLowerBound.TapeUnary.IncState ⊕ Complexity.DepthThreeLowerBound.TapePower.State 2)

def Complexity.DepthThreeLowerBound.TapeParameters.squareProgram : TapeMultiProgram SquareState

Transition function for the square stage of the parameters routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeParameters.squareStart : SquareState

Initial control state of the square stage of the parameters routine.

Equations

• Complexity.DepthThreeLowerBound.TapeParameters.squareStart = Sum.inl Complexity.DepthThreeLowerBound.TapeUnary.IncState.start

def Complexity.DepthThreeLowerBound.TapeParameters.squareDone : SquareState

Terminal control state of the square stage of the parameters routine.

Equations

• Complexity.DepthThreeLowerBound.TapeParameters.squareDone = Sum.inr (Complexity.DepthThreeLowerBound.TapePower.done 2)

def Complexity.DepthThreeLowerBound.TapeParameters.squareCost (d : ℕ) : ℕ

Transition budget for the parameters routine at its square stage.

Equations

• Complexity.DepthThreeLowerBound.TapeParameters.squareCost d = 2 + 1 + Complexity.DepthThreeLowerBound.TapePower.cost 2 1 d

theorem Complexity.DepthThreeLowerBound.TapeParameters.runs_square (σ : TapeStore) (d : ℕ) (h2 : σ 2 = List.replicate d true) (h5 : σ 5 = []) (h6 : σ 6 = []) (h7 : σ 7 = []) : RunsIn squareProgram.step (TapeMultiProgram.cfg squareStart (storeTapes σ)) (TapeMultiProgram.cfg squareDone (storeTapes (Function.update σ 6 (List.replicate (d ^ 2) true)))) (squareCost d)

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeParameters.FinishState : Type

Control states for the finish stage of the parameters routine.

Equations

• Complexity.DepthThreeLowerBound.TapeParameters.FinishState = (Complexity.DepthThreeLowerBound.TapeErase.State ⊕ Complexity.DepthThreeLowerBound.TapeParameterSearch.SixthState)

def Complexity.DepthThreeLowerBound.TapeParameters.finishProgram : TapeMultiProgram FinishState

Transition function for the finish stage of the parameters routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeParameters.finishStart : FinishState

Initial control state of the finish stage of the parameters routine.

Equations

• Complexity.DepthThreeLowerBound.TapeParameters.finishStart = Sum.inl Complexity.DepthThreeLowerBound.TapeErase.State.start

def Complexity.DepthThreeLowerBound.TapeParameters.finishDone : FinishState

Terminal control state of the finish stage of the parameters routine.

Equations

• Complexity.DepthThreeLowerBound.TapeParameters.finishDone = Sum.inr Complexity.DepthThreeLowerBound.TapeParameterSearch.sixthDone

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeParameters.RootsState : Type

Control states for the roots stage of the parameters routine.

Equations

• Complexity.DepthThreeLowerBound.TapeParameters.RootsState = (Complexity.DepthThreeLowerBound.TapeParameterSearch.CubeState ⊕ Complexity.DepthThreeLowerBound.TapeParameters.FinishState)

def Complexity.DepthThreeLowerBound.TapeParameters.rootsProgram : TapeMultiProgram RootsState

Transition function for the roots stage of the parameters routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeParameters.rootsStart : RootsState

Initial control state of the roots stage of the parameters routine.

Equations

• Complexity.DepthThreeLowerBound.TapeParameters.rootsStart = Sum.inl Complexity.DepthThreeLowerBound.TapeParameterSearch.cubeStart

def Complexity.DepthThreeLowerBound.TapeParameters.rootsDone : RootsState

Terminal control state of the roots stage of the parameters routine.

Equations

• Complexity.DepthThreeLowerBound.TapeParameters.rootsDone = Sum.inr Complexity.DepthThreeLowerBound.TapeParameters.finishDone

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeParameters.WorkState : Type

Control states for the work stage of the parameters routine.

Equations

• Complexity.DepthThreeLowerBound.TapeParameters.WorkState = (Complexity.DepthThreeLowerBound.TapeParameters.SquareState ⊕ Complexity.DepthThreeLowerBound.TapeParameters.RootsState)

def Complexity.DepthThreeLowerBound.TapeParameters.workProgram : TapeMultiProgram WorkState

Transition function for the work stage of the parameters routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeParameters.workStart : WorkState

Initial control state of the work stage of the parameters routine.

Equations

• Complexity.DepthThreeLowerBound.TapeParameters.workStart = Sum.inl Complexity.DepthThreeLowerBound.TapeParameters.squareStart

def Complexity.DepthThreeLowerBound.TapeParameters.workDone : WorkState

Terminal control state of the work stage of the parameters routine.

Equations

• Complexity.DepthThreeLowerBound.TapeParameters.workDone = Sum.inr Complexity.DepthThreeLowerBound.TapeParameters.rootsDone

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeParameters.State : Type

Control states of the parameters routine.

Equations

• Complexity.DepthThreeLowerBound.TapeParameters.State = (Complexity.DepthThreeLowerBound.TapeParameters.LengthState ⊕ Complexity.DepthThreeLowerBound.TapeParameters.WorkState)

def Complexity.DepthThreeLowerBound.TapeParameters.program : TapeMultiProgram State

Transition function of the parameters routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeParameters.start : State

Initial control state of the parameters routine.

Equations

• Complexity.DepthThreeLowerBound.TapeParameters.start = Sum.inl Complexity.DepthThreeLowerBound.TapeParameters.lengthStart

def Complexity.DepthThreeLowerBound.TapeParameters.done : State

Terminal control state of the parameters routine.

Equations

• Complexity.DepthThreeLowerBound.TapeParameters.done = Sum.inr Complexity.DepthThreeLowerBound.TapeParameters.workDone

def Complexity.DepthThreeLowerBound.TapeParameters.cost (n : ℕ) : ℕ

Transition budget for the parameters routine.

Equations

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

theorem Complexity.DepthThreeLowerBound.TapeParameters.runs_parameters (σ : TapeStore) (n : ℕ) (h1 : σ 1 = List.replicate n true) (h2 : σ 2 = []) (h3 : σ 3 = []) (h4 : σ 4 = []) (h5 : σ 5 = []) (h6 : σ 6 = []) (h7 : σ 7 = []) (h9 : σ 9 = []) : RunsIn program.step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (outputStore σ n))) (cost n)

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeParameters.program_done (h : TapeHeads) : program done h = none