Unrestricted depth-three lower bound: tape power compare

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

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

theorem Complexity.DepthThreeLowerBound.TapePowerCompare.resultTapes_eq_frame (k : ℕ) (outer source scratch destination : TapeRegister) (T : TapeTapes) (n m : ℕ) : TapePower.resultTapes k outer source scratch destination T n m = TapeMultiply.tapes (TapePower.resultRegister k outer destination) source scratch (TapePower.resultRegister k destination outer) T (n * m ^ k) m 0 0

theorem Complexity.DepthThreeLowerBound.TapePowerCompare.resultRegister_pair (k : ℕ) (outer destination : TapeRegister) : TapePower.resultRegister k outer destination = outer ∧ TapePower.resultRegister k destination outer = destination ∨ TapePower.resultRegister k outer destination = destination ∧ TapePower.resultRegister k destination outer = outer

theorem Complexity.DepthThreeLowerBound.TapePowerCompare.resultRegister_ne (k : ℕ) {outer destination target : TapeRegister} (hot : outer ≠ target) (hdt : destination ≠ target) : TapePower.resultRegister k outer destination ≠ target

def Complexity.DepthThreeLowerBound.TapePowerCompare.outputStore (k : ℕ) (outer destination : TapeRegister) (σ : TapeStore) (c : ℕ) : TapeStore

Tape-store contents at the output stage of the power compare routine.

Equations

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

theorem Complexity.DepthThreeLowerBound.TapePowerCompare.result_store (k : ℕ) {outer source scratch destination : TapeRegister} (hos : outer ≠ source) (hoc : outer ≠ scratch) (hod : outer ≠ destination) (hsc : source ≠ scratch) (hsd : source ≠ destination) (hcd : scratch ≠ destination) (σ : TapeStore) (c : ℕ) (ho : σ outer = []) (hs : σ source = List.replicate c true) (hc : σ scratch = []) (hd : σ destination = []) : TapePower.resultTapes k outer source scratch destination (storeTapes σ) 1 c = storeTapes (outputStore k outer destination σ c)

@[simp]

theorem Complexity.DepthThreeLowerBound.TapePowerCompare.outputStore_result (k : ℕ) (outer destination : TapeRegister) (σ : TapeStore) (c : ℕ) : outputStore k outer destination σ c (TapePower.resultRegister k outer destination) = List.replicate (c ^ k) true

theorem Complexity.DepthThreeLowerBound.TapePowerCompare.outputStore_other (k : ℕ) (outer destination : TapeRegister) (σ : TapeStore) (c : ℕ) (r : TapeRegister) (hr : r ≠ TapePower.resultRegister k outer destination) : outputStore k outer destination σ c r = σ r

theorem Complexity.DepthThreeLowerBound.TapePowerCompare.outputStore_clear (k : ℕ) (outer destination : TapeRegister) (σ : TapeStore) (c : ℕ) (ho : σ outer = []) (hd : σ destination = []) : Function.update (outputStore k outer destination σ c) (TapePower.resultRegister k outer destination) [] = σ

@[reducible, inline]

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

Control states of the power compare routine.

Equations

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

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

Transition function of the power compare routine.

Equations

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

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

Initial control state of the power compare routine.

Equations

• Complexity.DepthThreeLowerBound.TapePowerCompare.start k = Sum.inl Complexity.DepthThreeLowerBound.TapeUnary.IncState.start

def Complexity.DepthThreeLowerBound.TapePowerCompare.done (k : ℕ) (o : Ordering) : State k

Terminal control state of the power compare routine.

Equations

• Complexity.DepthThreeLowerBound.TapePowerCompare.done k o = Sum.inr (Sum.inr (Complexity.DepthThreeLowerBound.TapeUnaryCompare.State.done o))

def Complexity.DepthThreeLowerBound.TapePowerCompare.cost (k c D : ℕ) : ℕ

Transition budget for the power compare routine.

Equations

• Complexity.DepthThreeLowerBound.TapePowerCompare.cost k c D = 2 + 1 + Complexity.DepthThreeLowerBound.TapePower.cost k 1 c + 1 + (4 * min (c ^ k) D + 7)

theorem Complexity.DepthThreeLowerBound.TapePowerCompare.runs_compare (k : ℕ) {outer source scratch destination target : TapeRegister} (hos : outer ≠ source) (hoc : outer ≠ scratch) (hod : outer ≠ destination) (hsc : source ≠ scratch) (hsd : source ≠ destination) (hcd : scratch ≠ destination) (hot : outer ≠ target) (hdt : destination ≠ target) (σ : TapeStore) (c D : ℕ) (ho : σ outer = []) (hs : σ source = List.replicate c true) (hc : σ scratch = []) (hd : σ destination = []) (ht : σ target = List.replicate D true) : RunsIn (program k outer source scratch destination target).step (TapeMultiProgram.cfg (start k) (storeTapes σ)) (TapeMultiProgram.cfg (done k (TapeUnaryCompareScan.result (c ^ k) D)) (storeTapes (outputStore k outer destination σ c))) (cost k c D)

@[simp]

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