Unrestricted depth-three lower bound: tape power search

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

Register allocation for the power search routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapePowerSearch.candidateStore (R : Registers) (σ : TapeStore) (c : ℕ) : TapeStore

Tape-store contents at the candidate stage of the power search routine.

Equations

• Complexity.DepthThreeLowerBound.TapePowerSearch.candidateStore R σ c = Function.update σ (R 1) (List.replicate c true)

def Complexity.DepthThreeLowerBound.TapePowerSearch.flag (k : ℕ) (again : Ordering → Bool) : TapePowerCompare.State k → Bool

Read the continuation predicate from a terminal power comparison.

Equations

• Complexity.DepthThreeLowerBound.TapePowerSearch.flag k again (Sum.inr (Sum.inr (Complexity.DepthThreeLowerBound.TapeUnaryCompare.State.done o))) = again o
• Complexity.DepthThreeLowerBound.TapePowerSearch.flag k again x✝ = false

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapePowerSearch.State (k : ℕ) : Type

Control states of the power search routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapePowerSearch.program (k : ℕ) (two : Bool) (again : Ordering → Bool) (R : Registers) : TapeMultiProgram (State k)

Transition function of the power search routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapePowerSearch.start (k : ℕ) : State k

Initial control state of the power search routine.

Equations

• Complexity.DepthThreeLowerBound.TapePowerSearch.start k = Complexity.DepthThreeLowerBound.TapeRouting.loopTest (Complexity.DepthThreeLowerBound.TapePowerCompare.start k)

def Complexity.DepthThreeLowerBound.TapePowerSearch.done (k : ℕ) : State k

Terminal control state of the power search routine.

Equations

• Complexity.DepthThreeLowerBound.TapePowerSearch.done k = Complexity.DepthThreeLowerBound.TapeRouting.loopDone

def Complexity.DepthThreeLowerBound.TapePowerSearch.cost (k : ℕ) (two : Bool) (D : ℕ) : ℕ → ℕ → ℕ

Transition budget for the power search routine.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.TapePowerSearch.cost k two D 0 x✝ = Complexity.DepthThreeLowerBound.TapePowerCompare.cost k x✝ D + 1

theorem Complexity.DepthThreeLowerBound.TapePowerSearch.runs_search (k : ℕ) (two : Bool) (again : Ordering → Bool) (R : Registers) (σ : TapeStore) (D fuel c : ℕ) (ho : σ (R 0) = []) (hs : σ (R 2) = []) (hd : σ (R 3) = []) (ht : σ (R 4) = List.replicate D true) (hgo : ∀ j < fuel, again (TapeUnaryCompareScan.result ((c + TapeSearchBody.amount two * j) ^ k) D) = true) (hstop : again (TapeUnaryCompareScan.result ((c + TapeSearchBody.amount two * fuel) ^ k) D) = false) : RunsIn (program k two again R).step (TapeMultiProgram.cfg (start k) (storeTapes (candidateStore R σ c))) (TapeMultiProgram.cfg (done k) (storeTapes (TapePowerCompare.outputStore k (R 0) (R 3) (candidateStore R σ (c + TapeSearchBody.amount two * fuel)) (c + TapeSearchBody.amount two * fuel)))) (cost k two D fuel c)

@[simp]

theorem Complexity.DepthThreeLowerBound.TapePowerSearch.program_done (k : ℕ) (two : Bool) (again : Ordering → Bool) (R : Registers) (h : TapeHeads) : program k two again R (done k) h = none

def Complexity.DepthThreeLowerBound.TapePowerSearch.continueLt (o : Ordering) : Bool

Continue the search exactly when the comparison returns less-than.

Equations

• Complexity.DepthThreeLowerBound.TapePowerSearch.continueLt o = decide (o = Ordering.lt)

def Complexity.DepthThreeLowerBound.TapePowerSearch.continueLe (o : Ordering) : Bool

Continue the search unless the comparison returns greater-than.

Equations

• Complexity.DepthThreeLowerBound.TapePowerSearch.continueLe o = !decide (o = Ordering.gt)

theorem Complexity.DepthThreeLowerBound.TapePowerSearch.continueLt_result (a b : ℕ) : continueLt (TapeUnaryCompareScan.result a b) = decide (a < b)

theorem Complexity.DepthThreeLowerBound.TapePowerSearch.continueLe_result (a b : ℕ) : continueLe (TapeUnaryCompareScan.result a b) = decide (a ≤ b)

theorem Complexity.DepthThreeLowerBound.TapePowerSearch.runs_cube (R : Registers) (σ : TapeStore) (d : ℕ) (ho : σ (R 0) = []) (hs : σ (R 2) = []) (hd : σ (R 3) = []) (ht : σ (R 4) = List.replicate (d ^ 2) true) : RunsIn (program 3 false continueLt R).step (TapeMultiProgram.cfg (start 3) (storeTapes (candidateStore R σ 0))) (TapeMultiProgram.cfg (done 3) (storeTapes (TapePowerCompare.outputStore 3 (R 0) (R 3) (candidateStore R σ (hashDimension d)) (hashDimension d)))) (cost 3 false (d ^ 2) (hashDimension d) 0)

theorem Complexity.DepthThreeLowerBound.TapePowerSearch.runs_sixth_boundary (R : Registers) (σ : TapeStore) (d : ℕ) (ho : σ (R 0) = []) (hs : σ (R 2) = []) (hd : σ (R 3) = []) (ht : σ (R 4) = List.replicate d true) : RunsIn (program 6 true continueLe R).step (TapeMultiProgram.cfg (start 6) (storeTapes (candidateStore R σ 0))) (TapeMultiProgram.cfg (done 6) (storeTapes (TapePowerCompare.outputStore 6 (R 0) (R 3) (candidateStore R σ (independenceOrder d + 2)) (independenceOrder d + 2)))) (cost 6 true d (independenceOrder d / 2 + 1) 0)