Unrestricted depth-three lower bound: tape input guard

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

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

def Complexity.DepthThreeLowerBound.TapeInputGuard.positiveResult : TapeUnaryCompare.State → Bool

Read whether the unary comparison returned strictly greater.

Equations

• Complexity.DepthThreeLowerBound.TapeInputGuard.positiveResult (Complexity.DepthThreeLowerBound.TapeUnaryCompare.State.done o) = decide (o = Ordering.gt)
• Complexity.DepthThreeLowerBound.TapeInputGuard.positiveResult x✝ = false

def Complexity.DepthThreeLowerBound.TapeInputGuard.atLeastResult : TapeUnaryCompare.State → Bool

Read whether the unary comparison returned greater or equal.

Equations

• Complexity.DepthThreeLowerBound.TapeInputGuard.atLeastResult (Complexity.DepthThreeLowerBound.TapeUnaryCompare.State.done o) = decide (o ≠ Ordering.lt)
• Complexity.DepthThreeLowerBound.TapeInputGuard.atLeastResult x✝ = false

def Complexity.DepthThreeLowerBound.TapeInputGuard.atMostResult : TapeUnaryCompare.State → Bool

Read whether the unary comparison returned less or equal.

Equations

• Complexity.DepthThreeLowerBound.TapeInputGuard.atMostResult (Complexity.DepthThreeLowerBound.TapeUnaryCompare.State.done o) = decide (o ≠ Ordering.gt)
• Complexity.DepthThreeLowerBound.TapeInputGuard.atMostResult x✝ = false

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeInputGuard.positiveResult_result (d : ℕ) : positiveResult (TapeUnaryCompare.State.done (TapeUnaryCompareScan.result d 0)) = decide (0 < d)

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeInputGuard.atLeastResult_result (t : ℕ) : atLeastResult (TapeUnaryCompare.State.done (TapeUnaryCompareScan.result t 2)) = decide (2 ≤ t)

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeInputGuard.atMostResult_result (L n : ℕ) : atMostResult (TapeUnaryCompare.State.done (TapeUnaryCompareScan.result L n)) = decide (L ≤ n)

inductive Complexity.DepthThreeLowerBound.TapeInputGuard.CheckState : Type

Control states for the check stage of the input guard routine.

• data (q : TapeUnaryCompare.State) : CheckState
• order (dataOK : Bool) (q : TapeUnaryCompare.State) : CheckState
• space (smallOK : Bool) (q : TapeUnaryCompare.State) : CheckState
• clear (accepted : Bool) (q : TapeErase.State) : CheckState
• done (accepted : Bool) : CheckState

def Complexity.DepthThreeLowerBound.TapeInputGuard.instDecidableEqCheckState.decEq (x✝ x✝¹ : CheckState) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeInputGuard.instDecidableEqCheckState : DecidableEq CheckState

Equations

• Complexity.DepthThreeLowerBound.TapeInputGuard.instDecidableEqCheckState = Complexity.DepthThreeLowerBound.TapeInputGuard.instDecidableEqCheckState.decEq

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.TapeInputGuard.instFintypeCheckState : Fintype CheckState

Equations

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

def Complexity.DepthThreeLowerBound.TapeInputGuard.checkProgram : TapeMultiProgram CheckState

Transition function for the check stage of the input guard routine.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.TapeInputGuard.checkProgram (Complexity.DepthThreeLowerBound.TapeInputGuard.CheckState.done accepted) x✝ = none

def Complexity.DepthThreeLowerBound.TapeInputGuard.checkStart : CheckState

Initial control state of the check stage of the input guard routine.

Equations

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

theorem Complexity.DepthThreeLowerBound.TapeInputGuard.runs_checks (σ : TapeStore) (n d t L : ℕ) (h1 : σ 1 = List.replicate n true) (h2 : σ 2 = List.replicate d true) (h4 : σ 4 = List.replicate t true) (h5 : σ 5 = []) (h6 : σ 6 = List.replicate 2 true) (h8 : σ 8 = List.replicate L true) : RunsIn checkProgram.step (TapeMultiProgram.cfg checkStart (storeTapes σ)) (TapeMultiProgram.cfg (CheckState.done (decide (0 < d ∧ 2 ≤ t ∧ L ≤ n))) (storeTapes (Function.update σ 6 []))) (4 * n + 42)

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeInputGuard.TwoState : Type

Control states for the two stage of the input guard routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputGuard.TwoState = (Complexity.DepthThreeLowerBound.TapeUnary.IncState ⊕ Complexity.DepthThreeLowerBound.TapeUnary.IncState)

def Complexity.DepthThreeLowerBound.TapeInputGuard.twoProgram : TapeMultiProgram TwoState

Transition function for the two stage of the input guard routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeInputGuard.twoStart : TwoState

Initial control state of the two stage of the input guard routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputGuard.twoStart = Sum.inl Complexity.DepthThreeLowerBound.TapeUnary.IncState.start

def Complexity.DepthThreeLowerBound.TapeInputGuard.twoDone : TwoState

Terminal control state of the two stage of the input guard routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputGuard.twoDone = Sum.inr Complexity.DepthThreeLowerBound.TapeUnary.IncState.done

theorem Complexity.DepthThreeLowerBound.TapeInputGuard.runs_two (σ : TapeStore) (h6 : σ 6 = []) : RunsIn twoProgram.step (TapeMultiProgram.cfg twoStart (storeTapes σ)) (TapeMultiProgram.cfg twoDone (storeTapes (Function.update σ 6 (List.replicate 2 true)))) 5

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeInputGuard.TestState : Type

Control states for the test stage of the input guard routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputGuard.TestState = (Complexity.DepthThreeLowerBound.TapeInputGuard.TwoState ⊕ Complexity.DepthThreeLowerBound.TapeInputGuard.CheckState)

def Complexity.DepthThreeLowerBound.TapeInputGuard.testProgram : TapeMultiProgram TestState

Transition function for the test stage of the input guard routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeInputGuard.testStart : TestState

Initial control state of the test stage of the input guard routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputGuard.testStart = Sum.inl Complexity.DepthThreeLowerBound.TapeInputGuard.twoStart

def Complexity.DepthThreeLowerBound.TapeInputGuard.testDone (b : Bool) : TestState

Terminal control state of the test stage of the input guard routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputGuard.testDone b = Sum.inr (Complexity.DepthThreeLowerBound.TapeInputGuard.CheckState.done b)

theorem Complexity.DepthThreeLowerBound.TapeInputGuard.runs_test (σ : TapeStore) (n d t L : ℕ) (h1 : σ 1 = List.replicate n true) (h2 : σ 2 = List.replicate d true) (h4 : σ 4 = List.replicate t true) (h5 : σ 5 = []) (h6 : σ 6 = []) (h8 : σ 8 = List.replicate L true) : RunsIn testProgram.step (TapeMultiProgram.cfg testStart (storeTapes σ)) (TapeMultiProgram.cfg (testDone (decide (0 < d ∧ 2 ≤ t ∧ L ≤ n))) (storeTapes σ)) (4 * n + 48)

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.TapeInputGuard.State : Type

Control states of the input guard routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputGuard.State = (Complexity.DepthThreeLowerBound.TapeInputGuard.LengthState ⊕ Complexity.DepthThreeLowerBound.TapeInputGuard.TestState)

def Complexity.DepthThreeLowerBound.TapeInputGuard.program : TapeMultiProgram State

Transition function of the input guard routine.

Equations

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

def Complexity.DepthThreeLowerBound.TapeInputGuard.start : State

Initial control state of the input guard routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputGuard.start = Sum.inl Complexity.DepthThreeLowerBound.TapeInputGuard.lengthStart

def Complexity.DepthThreeLowerBound.TapeInputGuard.done (accepted : Bool) : State

Terminal control state of the input guard routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputGuard.done accepted = Sum.inr (Complexity.DepthThreeLowerBound.TapeInputGuard.testDone accepted)

def Complexity.DepthThreeLowerBound.TapeInputGuard.cost (n d r t : ℕ) : ℕ

Transition budget for the input guard routine.

Equations

• Complexity.DepthThreeLowerBound.TapeInputGuard.cost n d r t = Complexity.DepthThreeLowerBound.TapeInputGuard.lengthCost d r t + 4 * n + 49

theorem Complexity.DepthThreeLowerBound.TapeInputGuard.cost_eq (n d r t : ℕ) : cost n d r t = 12 * d + 20 * r + 16 * t + 10 * (t * r) + 4 * n + 94

theorem Complexity.DepthThreeLowerBound.TapeInputGuard.cost_le_square (n d r t : ℕ) (hd : d ≤ n + 1) (hr : r ≤ n + 1) (ht : t ≤ n + 1) : cost n d r t ≤ 200 * (n + 1) ^ 2

theorem Complexity.DepthThreeLowerBound.TapeInputGuard.cost_parameters_le (n : ℕ) : cost n (dataDimension n) (hashDimension (dataDimension n)) (independenceOrder (dataDimension n)) ≤ 200 * (n + 1) ^ 2

theorem Complexity.DepthThreeLowerBound.TapeInputGuard.runs_guard (σ : TapeStore) (n d r t : ℕ) (h1 : σ 1 = List.replicate n true) (h2 : σ 2 = List.replicate d true) (h3 : σ 3 = List.replicate r true) (h4 : σ 4 = List.replicate t true) (h5 : σ 5 = []) (h6 : σ 6 = []) (h8 : σ 8 = []) : RunsIn program.step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg (done (decide (0 < d ∧ 2 ≤ t ∧ requiredLength d r t ≤ n))) (storeTapes (outputStore σ d r t))) (cost n d r t)

theorem Complexity.DepthThreeLowerBound.TapeInputGuard.runs_inputFits (w : List Bool) (σ : TapeStore) (h1 : σ 1 = List.replicate w.length true) (h2 : σ 2 = List.replicate (dataDimension w.length) true) (h3 : σ 3 = List.replicate (hashDimension (dataDimension w.length)) true) (h4 : σ 4 = List.replicate (independenceOrder (dataDimension w.length)) true) (h5 : σ 5 = []) (h6 : σ 6 = []) (h8 : σ 8 = []) : RunsIn program.step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg (done (decide (InputFits w))) (storeTapes (outputStore σ (dataDimension w.length) (hashDimension (dataDimension w.length)) (independenceOrder (dataDimension w.length))))) (cost w.length (dataDimension w.length) (hashDimension (dataDimension w.length)) (independenceOrder (dataDimension w.length)))

theorem Complexity.DepthThreeLowerBound.TapeInputGuard.runs_inputFits_quadratic (w : List Bool) (σ : TapeStore) (h1 : σ 1 = List.replicate w.length true) (h2 : σ 2 = List.replicate (dataDimension w.length) true) (h3 : σ 3 = List.replicate (hashDimension (dataDimension w.length)) true) (h4 : σ 4 = List.replicate (independenceOrder (dataDimension w.length)) true) (h5 : σ 5 = []) (h6 : σ 6 = []) (h8 : σ 8 = []) : RunsIn program.step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg (done (decide (InputFits w))) (storeTapes (outputStore σ (dataDimension w.length) (hashDimension (dataDimension w.length)) (independenceOrder (dataDimension w.length))))) (200 * (w.length + 1) ^ 2)

@[simp]

theorem Complexity.DepthThreeLowerBound.TapeInputGuard.program_done (b : Bool) (h : TapeHeads) : program (done b) h = none