Unrestricted depth-three lower bound: tape evaluation

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

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

structure Complexity.DepthThreeLowerBound.TapeEvaluation.Prepared (σ : TapeStore) (w : List Bool) : Prop

The workspace, parameter, and decoded-input invariants required by evaluation.

• workspace : TapeHornerMultiply.Workspace σ (decodeInput w).ringDegree
• clean : TapeHornerPrepare.Clean σ
• data_length : σ TapeRegister.dataLength = List.replicate (decodeInput w).dataSize true
• coefficient_count : σ TapeRegister.coeffCount = List.replicate (decodeInput w).coefficientCount true
• data_bits : σ TapeRegister.dataBits = inputBlockData w InputBlockKind.data
• key_bits : σ TapeRegister.keyBits = inputBlockData w InputBlockKind.hash
• polynomial_bits : σ TapeRegister.polyBits = inputBlockData w InputBlockKind.polynomial
• coefficient_bits : σ TapeRegister.coeffBits = inputBlockData w InputBlockKind.coefficients
• hash_empty : σ TapeRegister.hashBits = []

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeEvaluation.WorkState : Type

Control states for the work stage of the evaluation routine.

Equations

• Complexity.DepthThreeLowerBound.TapeEvaluation.WorkState = (Complexity.DepthThreeLowerBound.TapeHashClean.State ⊕ Complexity.DepthThreeLowerBound.TapeHorner.State)

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeEvaluation.State : Type

Control states of the evaluation routine.

Equations

• Complexity.DepthThreeLowerBound.TapeEvaluation.State = (Complexity.DepthThreeLowerBound.TapeEvaluation.WorkState ⊕ Complexity.DepthThreeLowerBound.TapeOutput.State)

def Complexity.DepthThreeLowerBound.TapeEvaluation.work : TapeMultiProgram WorkState

Compose the main computational stages of the routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeEvaluation.program : TapeMultiProgram State

Transition function of the evaluation routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeEvaluation.start : State

Initial control state of the evaluation routine.

Equations

• Complexity.DepthThreeLowerBound.TapeEvaluation.start = Sum.inl (Sum.inl Complexity.DepthThreeLowerBound.TapeHashClean.start)

def Complexity.DepthThreeLowerBound.TapeEvaluation.done (answer : Bool) : State

Terminal control state of the evaluation routine.

Equations

• Complexity.DepthThreeLowerBound.TapeEvaluation.done answer = Sum.inr (Complexity.DepthThreeLowerBound.TapeOutput.done answer)

def Complexity.DepthThreeLowerBound.TapeEvaluation.acceptFlag : State → Bool

Read the Boolean verdict from the terminal control state of the evaluation routine.

Equations

• Complexity.DepthThreeLowerBound.TapeEvaluation.acceptFlag (Sum.inr (Sum.inr b)) = b
• Complexity.DepthThreeLowerBound.TapeEvaluation.acceptFlag x✝ = false

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeEvaluation.acceptFlag_done (b : Bool) : acceptFlag (done b) = b

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeEvaluation.program_done (b : Bool) (h : TapeHeads) : program (done b) h = none

def Complexity.DepthThreeLowerBound.TapeEvaluation.hashWord (w : List Bool) : List Bool

The bit list produced by hashing the decoded input data.

Equations

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

def Complexity.DepthThreeLowerBound.TapeEvaluation.evaluationWord (w : List Bool) : List Bool

The bit list representing the decoded evaluation remainder.

Equations

• Complexity.DepthThreeLowerBound.TapeEvaluation.evaluationWord w = List.ofFn (Complexity.DepthThreeLowerBound.decodeInput w).evaluationBits

def Complexity.DepthThreeLowerBound.TapeEvaluation.outputStore (σ : TapeStore) (w : List Bool) : TapeStore

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

Equations

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

def Complexity.DepthThreeLowerBound.TapeEvaluation.cost (w : List Bool) : ℕ

Transition budget for the evaluation routine.

Equations

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

theorem Complexity.DepthThreeLowerBound.TapeEvaluation.cost_le (w : List Bool) : cost w ≤ 20000 * (w.length + 1) ^ 4

theorem Complexity.DepthThreeLowerBound.TapeEvaluation.runs_evaluate_cost (w : List Bool) (σ : TapeStore) (hfit : InputFits w) (hprep : Prepared σ w) : RunsIn program.step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg (done (language w)) (storeTapes (outputStore σ w))) (cost w)

theorem Complexity.DepthThreeLowerBound.TapeEvaluation.runs_evaluate (w : List Bool) (σ : TapeStore) (hfit : InputFits w) (hprep : Prepared σ w) : RunsIn program.step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg (done (language w)) (storeTapes (outputStore σ w))) (20000 * (w.length + 1) ^ 4)