Unrestricted depth-three lower bound: tape input prepare

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

Control states for the sum minus stage of the input prepare routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeInputPrepare.sumMinusProgram (dst : TapeRegister) : TapeMultiProgram SumMinusState

Transition function for the sum minus stage of the input prepare routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeInputPrepare.sumMinusStart : SumMinusState

Initial control state of the sum minus stage of the input prepare routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputPrepare.sumMinusStart = Sum.inl Complexity.DepthThreeLowerBound.TapeCopy.State.start

def Complexity.DepthThreeLowerBound.TapeInputPrepare.sumMinusDone (d r : ℕ) : SumMinusState

Terminal control state of the sum minus stage of the input prepare routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputPrepare.sumMinusDone d r = Sum.inr (Sum.inr (Complexity.DepthThreeLowerBound.TapeUnary.DecState.done (decide (0 < d + r))))

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeInputPrepare.sumMinusProgram_done (dst : TapeRegister) (d r : ℕ) (h : TapeHeads) : sumMinusProgram dst (sumMinusDone d r) h = none

theorem Complexity.DepthThreeLowerBound.TapeInputPrepare.runs_sumMinus {dst : TapeRegister} (h2 : 2 ≠ dst) (h3 : 3 ≠ dst) (h31 : 31 ≠ dst) (σ : TapeStore) (d r : ℕ) (hd : σ 2 = List.replicate d true) (hr : σ 3 = List.replicate r true) (he : σ dst = []) (hc : σ 31 = []) : RunsIn (sumMinusProgram dst).step (TapeMultiProgram.cfg sumMinusStart (storeTapes σ)) (TapeMultiProgram.cfg (sumMinusDone d r) (storeTapes (Function.update σ dst (List.replicate (d + r - 1) true)))) (2 * d + 10 * r + 18)

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeInputPrepare.OffsetState : Type

Control states for the offset stage of the input prepare routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputPrepare.OffsetState = (Complexity.DepthThreeLowerBound.TapeInputPrepare.SumMinusState ⊕ Complexity.DepthThreeLowerBound.TapeCopyAdd.State)

def Complexity.DepthThreeLowerBound.TapeInputPrepare.offsetProgram : TapeMultiProgram OffsetState

Transition function for the offset stage of the input prepare routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeInputPrepare.offsetStart : OffsetState

Initial control state of the offset stage of the input prepare routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputPrepare.offsetStart = Sum.inl Complexity.DepthThreeLowerBound.TapeInputPrepare.sumMinusStart

def Complexity.DepthThreeLowerBound.TapeInputPrepare.offsetDone : OffsetState

Terminal control state of the offset stage of the input prepare routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputPrepare.offsetDone = Sum.inr Complexity.DepthThreeLowerBound.TapeCopyAdd.done

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeInputPrepare.offsetProgram_done (h : TapeHeads) : offsetProgram offsetDone h = none

theorem Complexity.DepthThreeLowerBound.TapeInputPrepare.runs_offset (σ : TapeStore) (d r : ℕ) (hd : σ 2 = List.replicate d true) (hr : σ 3 = List.replicate r true) (he : σ 29 = []) (hc : σ 31 = []) : RunsIn offsetProgram.step (TapeMultiProgram.cfg offsetStart (storeTapes σ)) (TapeMultiProgram.cfg offsetDone (storeTapes (Function.update σ 29 (List.replicate (d + (d + r - 1)) true)))) (12 * d + 10 * r + 27)

def Complexity.DepthThreeLowerBound.TapeInputPrepare.terminalProgram : TapeMultiProgram Unit

Transition function for the terminal stage of the input prepare routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputPrepare.terminalProgram x✝¹ x✝ = none

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeInputPrepare.HashState : Type

Control states for the hash stage of the input prepare routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputPrepare.HashState = (Complexity.DepthThreeLowerBound.TapeCopy.State ⊕ Complexity.DepthThreeLowerBound.TapeInputPrepare.SumMinusState ⊕ Unit)

def Complexity.DepthThreeLowerBound.TapeInputPrepare.hashProgram : TapeMultiProgram HashState

Transition function for the hash stage of the input prepare routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeInputPrepare.hashStart : HashState

Initial control state of the hash stage of the input prepare routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputPrepare.hashStart = Sum.inl Complexity.DepthThreeLowerBound.TapeCopy.State.start

def Complexity.DepthThreeLowerBound.TapeInputPrepare.hashDone : HashState

Terminal control state of the hash stage of the input prepare routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputPrepare.hashDone = Sum.inr (Sum.inr ())

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeInputPrepare.PolynomialState : Type

Control states for the polynomial stage of the input prepare routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputPrepare.PolynomialState = (Complexity.DepthThreeLowerBound.TapeInputPrepare.OffsetState ⊕ Complexity.DepthThreeLowerBound.TapeCopy.State)

def Complexity.DepthThreeLowerBound.TapeInputPrepare.polynomialProgram : TapeMultiProgram PolynomialState

Transition function for the polynomial stage of the input prepare routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeInputPrepare.polynomialStart : PolynomialState

Initial control state of the polynomial stage of the input prepare routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputPrepare.polynomialStart = Sum.inl Complexity.DepthThreeLowerBound.TapeInputPrepare.offsetStart

def Complexity.DepthThreeLowerBound.TapeInputPrepare.polynomialDone : PolynomialState

Terminal control state of the polynomial stage of the input prepare routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputPrepare.polynomialDone = Sum.inr Complexity.DepthThreeLowerBound.TapeCopy.State.done

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeInputPrepare.CoefficientsState : Type

Control states for the coefficients stage of the input prepare routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeInputPrepare.coefficientsProgram : TapeMultiProgram CoefficientsState

Transition function for the coefficients stage of the input prepare routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeInputPrepare.coefficientsStart : CoefficientsState

Initial control state of the coefficients stage of the input prepare routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputPrepare.coefficientsStart = Sum.inl Complexity.DepthThreeLowerBound.TapeInputPrepare.offsetStart

def Complexity.DepthThreeLowerBound.TapeInputPrepare.coefficientsDone : CoefficientsState

Terminal control state of the coefficients stage of the input prepare routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputPrepare.coefficientsDone = Sum.inr (Sum.inr Complexity.DepthThreeLowerBound.TapeProductLength.done)

def Complexity.DepthThreeLowerBound.TapeInputPrepare.State : InputBlockKind → Type

Control states of the input prepare routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputPrepare.State Complexity.DepthThreeLowerBound.InputBlockKind.data = Complexity.DepthThreeLowerBound.TapeCopy.State
• Complexity.DepthThreeLowerBound.TapeInputPrepare.State Complexity.DepthThreeLowerBound.InputBlockKind.hash = Complexity.DepthThreeLowerBound.TapeInputPrepare.HashState
• Complexity.DepthThreeLowerBound.TapeInputPrepare.State Complexity.DepthThreeLowerBound.InputBlockKind.polynomial = Complexity.DepthThreeLowerBound.TapeInputPrepare.PolynomialState
• Complexity.DepthThreeLowerBound.TapeInputPrepare.State Complexity.DepthThreeLowerBound.InputBlockKind.coefficients = Complexity.DepthThreeLowerBound.TapeInputPrepare.CoefficientsState

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeInputPrepare.instFintypeState (kind : InputBlockKind) : Fintype (State kind)

Equations

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

def Complexity.DepthThreeLowerBound.TapeInputPrepare.program (kind : InputBlockKind) : TapeMultiProgram (State kind)

Transition function of the input prepare routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputPrepare.program Complexity.DepthThreeLowerBound.InputBlockKind.data = Complexity.DepthThreeLowerBound.TapeCopy.code 2 30
• Complexity.DepthThreeLowerBound.TapeInputPrepare.program Complexity.DepthThreeLowerBound.InputBlockKind.hash = Complexity.DepthThreeLowerBound.TapeInputPrepare.hashProgram
• Complexity.DepthThreeLowerBound.TapeInputPrepare.program Complexity.DepthThreeLowerBound.InputBlockKind.polynomial = Complexity.DepthThreeLowerBound.TapeInputPrepare.polynomialProgram
• Complexity.DepthThreeLowerBound.TapeInputPrepare.program Complexity.DepthThreeLowerBound.InputBlockKind.coefficients = Complexity.DepthThreeLowerBound.TapeInputPrepare.coefficientsProgram

def Complexity.DepthThreeLowerBound.TapeInputPrepare.start (kind : InputBlockKind) : State kind

Initial control state of the input prepare routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputPrepare.start Complexity.DepthThreeLowerBound.InputBlockKind.data = Complexity.DepthThreeLowerBound.TapeCopy.State.start
• Complexity.DepthThreeLowerBound.TapeInputPrepare.start Complexity.DepthThreeLowerBound.InputBlockKind.hash = Complexity.DepthThreeLowerBound.TapeInputPrepare.hashStart
• Complexity.DepthThreeLowerBound.TapeInputPrepare.start Complexity.DepthThreeLowerBound.InputBlockKind.polynomial = Complexity.DepthThreeLowerBound.TapeInputPrepare.polynomialStart
• Complexity.DepthThreeLowerBound.TapeInputPrepare.start Complexity.DepthThreeLowerBound.InputBlockKind.coefficients = Complexity.DepthThreeLowerBound.TapeInputPrepare.coefficientsStart

def Complexity.DepthThreeLowerBound.TapeInputPrepare.done (kind : InputBlockKind) : State kind

Terminal control state of the input prepare routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputPrepare.done Complexity.DepthThreeLowerBound.InputBlockKind.data = Complexity.DepthThreeLowerBound.TapeCopy.State.done
• Complexity.DepthThreeLowerBound.TapeInputPrepare.done Complexity.DepthThreeLowerBound.InputBlockKind.hash = Complexity.DepthThreeLowerBound.TapeInputPrepare.hashDone
• Complexity.DepthThreeLowerBound.TapeInputPrepare.done Complexity.DepthThreeLowerBound.InputBlockKind.polynomial = Complexity.DepthThreeLowerBound.TapeInputPrepare.polynomialDone
• Complexity.DepthThreeLowerBound.TapeInputPrepare.done Complexity.DepthThreeLowerBound.InputBlockKind.coefficients = Complexity.DepthThreeLowerBound.TapeInputPrepare.coefficientsDone

def Complexity.DepthThreeLowerBound.TapeInputPrepare.outputStore (σ : TapeStore) (n : ℕ) (kind : InputBlockKind) : TapeStore

Tape-store contents at the output stage of the input prepare routine.

Equations

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

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeInputPrepare.outputStore_offset (σ : TapeStore) (n : ℕ) (kind : InputBlockKind) : outputStore σ n kind 29 = List.replicate (inputBlockOffset n kind) true

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeInputPrepare.outputStore_length (σ : TapeStore) (n : ℕ) (kind : InputBlockKind) : outputStore σ n kind 30 = List.replicate (inputBlockLength n kind) true

theorem Complexity.DepthThreeLowerBound.TapeInputPrepare.outputStore_other (σ : TapeStore) (n : ℕ) (kind : InputBlockKind) (s : TapeRegister) (h29 : s ≠ 29) (h30 : s ≠ 30) : outputStore σ n kind s = σ s

def Complexity.DepthThreeLowerBound.TapeInputPrepare.cost (n : ℕ) : InputBlockKind → ℕ

Transition budget for the input prepare routine.

Equations

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

theorem Complexity.DepthThreeLowerBound.TapeInputPrepare.runs_prepare (σ : TapeStore) (n : ℕ) (kind : InputBlockKind) (hd : σ 2 = List.replicate (dataDimension n) true) (hr : σ 3 = List.replicate (hashDimension (dataDimension n)) true) (ht : σ 4 = List.replicate (independenceOrder (dataDimension n)) true) (h29 : σ 29 = []) (h30 : σ 30 = []) (h31 : σ 31 = []) (h5 : σ 5 = []) (h6 : σ 6 = []) (_h7 : σ 7 = []) : RunsIn (program kind).step (TapeMultiProgram.cfg (start kind) (storeTapes σ)) (TapeMultiProgram.cfg (done kind) (storeTapes (outputStore σ n kind))) (cost n kind)

theorem Complexity.DepthThreeLowerBound.TapeInputPrepare.cost_le (n : ℕ) (kind : InputBlockKind) : cost n kind ≤ 128 * (n + 1) ^ 2

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeInputPrepare.program_done (kind : InputBlockKind) (h : TapeHeads) : program kind (done kind) h = none