Unrestricted depth-three lower bound: tape input block loop

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/TapeInputBlockLoop.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.TapeInputBlockLoop.Registers : Type

Register allocation for the input block loop routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputBlockLoop.Registers = (Fin 5 ↪ Complexity.DepthThreeLowerBound.TapeRegister)

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeInputBlockLoop.source (R : Registers) : TapeRegister

The source register of the block-copy loop.

Equations

• Complexity.DepthThreeLowerBound.TapeInputBlockLoop.source R = R 0

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeInputBlockLoop.index (R : Registers) : TapeRegister

The source-position counter of the block-copy loop.

Equations

• Complexity.DepthThreeLowerBound.TapeInputBlockLoop.index R = R 1

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeInputBlockLoop.count (R : Registers) : TapeRegister

The remaining-length counter of the block-copy loop.

Equations

• Complexity.DepthThreeLowerBound.TapeInputBlockLoop.count R = R 2

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeInputBlockLoop.scratch (R : Registers) : TapeRegister

The scratch register of the block-copy loop.

Equations

• Complexity.DepthThreeLowerBound.TapeInputBlockLoop.scratch R = R 3

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeInputBlockLoop.destination (R : Registers) : TapeRegister

The output register of the block-copy loop.

Equations

• Complexity.DepthThreeLowerBound.TapeInputBlockLoop.destination R = R 4

theorem Complexity.DepthThreeLowerBound.TapeInputBlockLoop.register_eq (R : Registers) (i j : Fin 5) : R i = R j ↔ i = j

theorem Complexity.DepthThreeLowerBound.TapeInputBlockLoop.index_ne_source (R : Registers) : index R ≠ source R

def Complexity.DepthThreeLowerBound.TapeInputBlockLoop.blockStore (R : Registers) (σ : TapeStore) (pos remaining : ℕ) (bits : List Bool) : TapeStore

Tape-store contents at the block stage of the input block loop routine.

Equations

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

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeInputBlockLoop.blockStore_source (R : Registers) (σ : TapeStore) (pos remaining : ℕ) (bits : List Bool) : blockStore R σ pos remaining bits (source R) = σ (source R)

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeInputBlockLoop.blockStore_index (R : Registers) (σ : TapeStore) (pos remaining : ℕ) (bits : List Bool) : blockStore R σ pos remaining bits (index R) = List.replicate pos true

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeInputBlockLoop.blockStore_count (R : Registers) (σ : TapeStore) (pos remaining : ℕ) (bits : List Bool) : blockStore R σ pos remaining bits (count R) = List.replicate remaining true

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeInputBlockLoop.blockStore_destination (R : Registers) (σ : TapeStore) (pos remaining : ℕ) (bits : List Bool) : blockStore R σ pos remaining bits (destination R) = bits

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeInputBlockLoop.update_blockStore_count (R : Registers) (σ : TapeStore) (pos remaining remaining' : ℕ) (bits : List Bool) : Function.update (blockStore R σ pos remaining bits) (count R) (List.replicate remaining' true) = blockStore R σ pos remaining' bits

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeInputBlockLoop.update_blockStore_index (R : Registers) (σ : TapeStore) (pos pos' remaining : ℕ) (bits : List Bool) : Function.update (blockStore R σ pos remaining bits) (index R) (List.replicate pos' true) = blockStore R σ pos' remaining bits

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeInputBlockLoop.update_blockStore_destination (R : Registers) (σ : TapeStore) (pos remaining : ℕ) (bits bits' : List Bool) : Function.update (blockStore R σ pos remaining bits) (destination R) bits' = blockStore R σ pos remaining bits'

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeInputBlockLoop.BodyState : Type

Control states for the body stage of the input block loop routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputBlockLoop.BodyState = (Complexity.DepthThreeLowerBound.TapeUnary.DecState ⊕ Complexity.DepthThreeLowerBound.TapeReadPush.State)

def Complexity.DepthThreeLowerBound.TapeInputBlockLoop.bodyProgram (R : Registers) : TapeMultiProgram BodyState

Transition function for the body stage of the input block loop routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeInputBlockLoop.bodyStart : BodyState

Initial control state of the body stage of the input block loop routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputBlockLoop.bodyStart = Sum.inl Complexity.DepthThreeLowerBound.TapeUnary.DecState.start

def Complexity.DepthThreeLowerBound.TapeInputBlockLoop.bodyDone (b : Bool) : BodyState

Terminal control state of the body stage of the input block loop routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputBlockLoop.bodyDone b = Sum.inr (Complexity.DepthThreeLowerBound.TapeReadPush.done b)

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeInputBlockLoop.body_done (R : Registers) (b : Bool) (h : TapeHeads) : bodyProgram R (bodyDone b) h = none

theorem Complexity.DepthThreeLowerBound.TapeInputBlockLoop.runs_body (R : Registers) (σ : TapeStore) («prefix» suffix acc : List Bool) (b : Bool) (remaining : ℕ) (hsource : σ (source R) = «prefix» ++ b :: suffix) : RunsIn (bodyProgram R).step (TapeMultiProgram.cfg bodyStart (storeTapes (blockStore R σ («prefix».length + 1) remaining acc))) (TapeMultiProgram.cfg (bodyDone b) (storeTapes (blockStore R σ «prefix».length remaining (b :: acc)))) (2 * «prefix».length + 12)

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeInputBlockLoop.State : Type

Control states of the input block loop routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeInputBlockLoop.program (R : Registers) : TapeMultiProgram State

Transition function of the input block loop routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeInputBlockLoop.start : State

Initial control state of the input block loop routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputBlockLoop.start = Complexity.DepthThreeLowerBound.TapeRouting.loopTest Complexity.DepthThreeLowerBound.TapeUnary.DecState.start

def Complexity.DepthThreeLowerBound.TapeInputBlockLoop.done : State

Terminal control state of the input block loop routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputBlockLoop.done = Complexity.DepthThreeLowerBound.TapeRouting.loopDone

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeInputBlockLoop.program_done (R : Registers) (h : TapeHeads) : program R done h = none

theorem Complexity.DepthThreeLowerBound.TapeInputBlockLoop.runs_block (R : Registers) (σ : TapeStore) («prefix» block suffix acc : List Bool) (hsource : σ (source R) = «prefix» ++ block ++ suffix) : RunsIn (program R).step (TapeMultiProgram.cfg start (storeTapes (blockStore R σ («prefix».length + block.length) block.length acc))) (TapeMultiProgram.cfg done (storeTapes (blockStore R σ «prefix».length 0 (block ++ acc)))) (block.length * (2 * «prefix».length + block.length + 17) + 3)