Unrestricted depth-three lower bound: machine basic

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

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

@[simp]

theorem Complexity.DepthThreeLowerBound.runSteps_zero {S : Type uDepth1} (step : S → Option S) (c : Option S) : runSteps step 0 c = c

theorem Complexity.DepthThreeLowerBound.runSteps_succ {S : Type uDepth2} (step : S → Option S) (n : ℕ) (c : Option S) : runSteps step (n + 1) c = (runSteps step n c).bind step

theorem Complexity.DepthThreeLowerBound.runSteps_succ_left {S : Type uDepth3} (step : S → Option S) (n : ℕ) (c : Option S) : runSteps step (n + 1) c = runSteps step n (c.bind step)

@[simp]

theorem Complexity.DepthThreeLowerBound.runSteps_none {S : Type uDepth4} (step : S → Option S) (n : ℕ) : runSteps step n none = none

theorem Complexity.DepthThreeLowerBound.runSteps_add {S : Type uDepth5} (step : S → Option S) (m n : ℕ) (c : Option S) : runSteps step (m + n) c = runSteps step m (runSteps step n c)

theorem Complexity.DepthThreeLowerBound.runSteps_succ_eq_of_step_eq {S : Type uDepth6} {step : S → Option S} {a b : S} (h : step a = step b) (n : ℕ) : runSteps step (n + 1) (some a) = runSteps step (n + 1) (some b)

theorem Complexity.DepthThreeLowerBound.runSteps_eq_of_step_eq {S : Type uDepth7} {step : S → Option S} {a b : S} (h : step a = step b) {n : ℕ} (hn : 0 < n) : runSteps step n (some a) = runSteps step n (some b)

def Complexity.DepthThreeLowerBound.RunsIn {S : Type uDepth8} (step : S → Option S) (a b : S) (bound : ℕ) : Prop

Reach the target configuration in at most the stated number of transitions.

Equations

• Complexity.DepthThreeLowerBound.RunsIn step a b bound = ∃ n ≤ bound, Complexity.DepthThreeLowerBound.runSteps step n (some a) = some b

theorem Complexity.DepthThreeLowerBound.RunsIn.refl {S : Type uDepth9} (step : S → Option S) (a : S) : RunsIn step a a 0

theorem Complexity.DepthThreeLowerBound.RunsIn.single {S : Type uDepth10} {step : S → Option S} {a b : S} (h : step a = some b) : RunsIn step a b 1

theorem Complexity.DepthThreeLowerBound.RunsIn.mono {S : Type uDepth11} {step : S → Option S} {a b : S} {m n : ℕ} (h : RunsIn step a b m) (hmn : m ≤ n) : RunsIn step a b n

theorem Complexity.DepthThreeLowerBound.RunsIn.trans {S : Type uDepth12} {step : S → Option S} {a b c : S} {m n : ℕ} (h₁ : RunsIn step a b m) (h₂ : RunsIn step b c n) : RunsIn step a c (m + n)

structure Complexity.DepthThreeLowerBound.FiniteMachine : Type 1

A finite-state machine over a fixed tape alphabet.

• Γ : Type

  The finite tape alphabet.

• alphabetInhabited : Inhabited self.Γ
• alphabetFinite : Fintype self.Γ
• Λ : Type

  The finite set of control labels.

• stateInhabited : Inhabited self.Λ
• stateFinite : Fintype self.Λ
• inputSymbol : Bool → self.Γ

  Encode input bits as tape symbols.

• input_injective : Function.Injective self.inputSymbol
• input_ne_blank (b : Bool) : self.inputSymbol b ≠ default
• code : Turing.TM0.Machine self.Γ self.Λ

  The finite machine program.

• accept : self.Λ → Bool

  Read the Boolean verdict from the control label.

def Complexity.DepthThreeLowerBound.HaltsIn (M : FiniteMachine) (input : List Bool) (output : Bool) (time : ℕ) : Prop

Reach a halting configuration with the specified verdict within the time bound.

Equations

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

def Complexity.DepthThreeLowerBound.PolynomialTimeDecider (f : List Bool → Bool) : Prop

A fixed finite machine decides the language within a polynomial time bound.

Equations

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