Unrestricted depth-three lower bound: tape multiply

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

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

def Complexity.DepthThreeLowerBound.TapeMultiply.tapes (outer source scratch destination : TapeRegister) (T : TapeTapes) (n m k z : ℕ) : TapeTapes

The four counter tapes used in the multiplication invariant.

Equations

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

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeMultiply.tapes_outer (outer source scratch destination : TapeRegister) (T : TapeTapes) (n m k z : ℕ) : tapes outer source scratch destination T n m k z outer = TapeUnary.counterTape n

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeMultiply.tapes_source {outer source scratch destination : TapeRegister} (hos : outer ≠ source) (T : TapeTapes) (n m k z : ℕ) : tapes outer source scratch destination T n m k z source = TapeUnary.counterTape m

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeMultiply.tapes_scratch {outer source scratch destination : TapeRegister} (hoc : outer ≠ scratch) (hsc : source ≠ scratch) (T : TapeTapes) (n m k z : ℕ) : tapes outer source scratch destination T n m k z scratch = TapeUnary.counterTape k

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeMultiply.tapes_destination {outer source scratch destination : TapeRegister} (hod : outer ≠ destination) (hsd : source ≠ destination) (hcd : scratch ≠ destination) (T : TapeTapes) (n m k z : ℕ) : tapes outer source scratch destination T n m k z destination = TapeUnary.counterTape z

theorem Complexity.DepthThreeLowerBound.TapeMultiply.tapes_other (outer source scratch destination : TapeRegister) (T : TapeTapes) (n m k z : ℕ) (r : TapeRegister) (ho : r ≠ outer) (hs : r ≠ source) (hc : r ≠ scratch) (hd : r ≠ destination) : tapes outer source scratch destination T n m k z r = T r

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeMultiply.BodyState : Type

Control states for the body stage of the multiply routine.

Equations

• Complexity.DepthThreeLowerBound.TapeMultiply.BodyState = (Complexity.DepthThreeLowerBound.TapeCopy.State ⊕ Complexity.DepthThreeLowerBound.TapeArithmetic.AddState)

def Complexity.DepthThreeLowerBound.TapeMultiply.bodyProgram (source scratch destination : TapeRegister) : TapeMultiProgram BodyState

Transition function for the body stage of the multiply routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeMultiply.bodyStart : BodyState

Initial control state of the body stage of the multiply routine.

Equations

• Complexity.DepthThreeLowerBound.TapeMultiply.bodyStart = Sum.inl Complexity.DepthThreeLowerBound.TapeCopy.State.start

def Complexity.DepthThreeLowerBound.TapeMultiply.bodyDone : BodyState

Terminal control state of the body stage of the multiply routine.

Equations

• Complexity.DepthThreeLowerBound.TapeMultiply.bodyDone = Sum.inr Complexity.DepthThreeLowerBound.TapeArithmetic.addDone

theorem Complexity.DepthThreeLowerBound.TapeMultiply.runs_body {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 z : ℕ) : RunsIn (bodyProgram source scratch destination).step (TapeMultiProgram.cfg bodyStart (tapes outer source scratch destination T n m 0 z)) (TapeMultiProgram.cfg bodyDone (tapes outer source scratch destination T n m 0 (z + m))) (10 * m + 8)

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeMultiply.body_done (source scratch destination : TapeRegister) (h : TapeHeads) : bodyProgram source scratch destination bodyDone h = none

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeMultiply.State : Type

Control states of the multiply routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeMultiply.program (outer source scratch destination : TapeRegister) : TapeMultiProgram State

Transition function of the multiply routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeMultiply.start : State

Initial control state of the multiply routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeMultiply.done : State

Terminal control state of the multiply routine.

Equations

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

theorem Complexity.DepthThreeLowerBound.TapeMultiply.runs_mul {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 z : ℕ) : RunsIn (program outer source scratch destination).step (TapeMultiProgram.cfg start (tapes outer source scratch destination T n m 0 z)) (TapeMultiProgram.cfg done (tapes outer source scratch destination T 0 m 0 (z + n * m))) (n * (10 * m + 14) + 3)

@[simp]

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