Unrestricted depth-three lower bound: tape power

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

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

def Complexity.DepthThreeLowerBound.TapePower.State : ℕ → Type

Control states of the power routine.

Equations

• Complexity.DepthThreeLowerBound.TapePower.State 0 = Unit
• Complexity.DepthThreeLowerBound.TapePower.State k.succ = (Complexity.DepthThreeLowerBound.TapeMultiply.State ⊕ Complexity.DepthThreeLowerBound.TapePower.State k)

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapePower.instFintypeState (k : ℕ) : Fintype (State k)

Equations

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

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

Initial control state of the power routine.

Equations

• Complexity.DepthThreeLowerBound.TapePower.start 0 = ()
• Complexity.DepthThreeLowerBound.TapePower.start k.succ = Sum.inl Complexity.DepthThreeLowerBound.TapeMultiply.start

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

Terminal control state of the power routine.

Equations

• Complexity.DepthThreeLowerBound.TapePower.done 0 = ()
• Complexity.DepthThreeLowerBound.TapePower.done k.succ = Sum.inr (Complexity.DepthThreeLowerBound.TapePower.done k)

def Complexity.DepthThreeLowerBound.TapePower.program (k : ℕ) (outer source scratch destination : TapeRegister) : TapeMultiProgram (State k)

Transition function of the power routine.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.TapePower.program 0 x✝³ x✝² x✝¹ x✝ = fun (x : Complexity.DepthThreeLowerBound.TapePower.State 0) (x_1 : Complexity.DepthThreeLowerBound.TapeHeads) => none

def Complexity.DepthThreeLowerBound.TapePower.resultTapes : ℕ → TapeRegister → TapeRegister → TapeRegister → TapeRegister → TapeTapes → ℕ → ℕ → TapeTapes

The counter-tape contents after the recursive power computation.

Equations

• Complexity.DepthThreeLowerBound.TapePower.resultTapes 0 x✝⁶ x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ = Complexity.DepthThreeLowerBound.TapeMultiply.tapes x✝⁶ x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ 0 0
• Complexity.DepthThreeLowerBound.TapePower.resultTapes k.succ x✝⁶ x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ = Complexity.DepthThreeLowerBound.TapePower.resultTapes k x✝³ x✝⁵ x✝⁴ x✝⁶ x✝² (x✝¹ * x✝) x✝

def Complexity.DepthThreeLowerBound.TapePower.resultRegister : ℕ → TapeRegister → TapeRegister → TapeRegister

Select the register holding the result after alternating power stages.

Equations

• Complexity.DepthThreeLowerBound.TapePower.resultRegister 0 x✝¹ x✝ = x✝¹
• Complexity.DepthThreeLowerBound.TapePower.resultRegister k.succ x✝¹ x✝ = Complexity.DepthThreeLowerBound.TapePower.resultRegister k x✝ x✝¹

def Complexity.DepthThreeLowerBound.TapePower.cost : ℕ → ℕ → ℕ → ℕ

Transition budget for the power routine.

Equations

• Complexity.DepthThreeLowerBound.TapePower.cost 0 x✝¹ x✝ = 0
• Complexity.DepthThreeLowerBound.TapePower.cost k.succ x✝¹ x✝ = x✝¹ * (10 * x✝ + 14) + 3 + 1 + Complexity.DepthThreeLowerBound.TapePower.cost k (x✝¹ * x✝) x✝

theorem Complexity.DepthThreeLowerBound.TapePower.runs_power (k : ℕ) {outer source scratch destination : TapeRegister} (hos : outer ≠ source) (hoc : outer ≠ scratch) (hod : outer ≠ destination) (hsc : source ≠ scratch) (hsd : source ≠ destination) (hcd : scratch ≠ destination) (T : TapeTapes) (n m : ℕ) : RunsIn (program k outer source scratch destination).step (TapeMultiProgram.cfg (start k) (TapeMultiply.tapes outer source scratch destination T n m 0 0)) (TapeMultiProgram.cfg (done k) (resultTapes k outer source scratch destination T n m)) (cost k n m)

theorem Complexity.DepthThreeLowerBound.TapePower.program_done (k : ℕ) (outer source scratch destination : TapeRegister) (h : TapeHeads) : program k outer source scratch destination (done k) h = none

theorem Complexity.DepthThreeLowerBound.TapePower.resultTapes_result (k : ℕ) (outer source scratch destination : TapeRegister) (T : TapeTapes) (n m : ℕ) : resultTapes k outer source scratch destination T n m (resultRegister k outer destination) = TapeUnary.counterTape (n * m ^ k)

theorem Complexity.DepthThreeLowerBound.TapePower.resultTapes_source (k : ℕ) {outer source scratch destination : TapeRegister} (hos : outer ≠ source) (hsd : source ≠ destination) (T : TapeTapes) (n m : ℕ) : resultTapes k outer source scratch destination T n m source = TapeUnary.counterTape m

theorem Complexity.DepthThreeLowerBound.TapePower.resultTapes_scratch (k : ℕ) {outer source scratch destination : TapeRegister} (hoc : outer ≠ scratch) (hsc : source ≠ scratch) (hcd : scratch ≠ destination) (T : TapeTapes) (n m : ℕ) : resultTapes k outer source scratch destination T n m scratch = TapeUnary.counterTape 0

theorem Complexity.DepthThreeLowerBound.TapePower.resultTapes_other (k : ℕ) (outer source scratch destination : TapeRegister) (T : TapeTapes) (n m : ℕ) (r : TapeRegister) (ho : r ≠ outer) (hs : r ≠ source) (hc : r ≠ scratch) (hd : r ≠ destination) : resultTapes k outer source scratch destination T n m r = T r

theorem Complexity.DepthThreeLowerBound.TapePower.cost_eq_sum (k n m : ℕ) : cost k n m = n * (10 * m + 14) * ∑ j ∈ Finset.range k, m ^ j + 4 * k