Unrestricted depth-three lower bound: model

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

Boolean assignments to a set of input variables.

Equations

• Complexity.DepthThreeLowerBound.Cube V = (V → Bool)

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.Literal (V : Type uV) : Type uV

An input variable paired with the value making its literal true.

Equations

• Complexity.DepthThreeLowerBound.Literal V = (V × Bool)

def Complexity.DepthThreeLowerBound.Literal.eval {V : Type uV} (l : Literal V) (x : Cube V) : Bool

Evaluate a signed input literal.

Equations

• l.eval x = decide (x l.1 = l.2)

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.GateInput (V : Type uV) : Type uV

A signed input literal or a Boolean constant.

Equations

• Complexity.DepthThreeLowerBound.GateInput V = (Complexity.DepthThreeLowerBound.Literal V ⊕ Bool)

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.RawClause (V : Type uV) : Type uV

An OR gate represented by a list of signed literals and constants.

Equations

• Complexity.DepthThreeLowerBound.RawClause V = List (Complexity.DepthThreeLowerBound.GateInput V)

def Complexity.DepthThreeLowerBound.GateInput.eval {V : Type uV} : GateInput V → Cube V → Bool

Evaluate a literal or constant gate input.

Equations

• Complexity.DepthThreeLowerBound.GateInput.eval (Sum.inl l) x✝ = l.eval x✝
• Complexity.DepthThreeLowerBound.GateInput.eval (Sum.inr b) x✝ = b

noncomputable def Complexity.DepthThreeLowerBound.RawClause.eval {V : Type uV} (C : RawClause V) (x : Cube V) : Bool

Evaluate the disjunction of a raw clause.

Equations

• C.eval x = decide (∃ l ∈ C, l.eval x = true)

structure Complexity.DepthThreeLowerBound.Circuit3 (V : Type uV) : Type uV

An OR-AND-OR circuit with arbitrary fan-in, constants, and shared lower gates.

• bottomCount : ℕ

  The number of bottom OR gates.

• middleCount : ℕ

  The number of middle AND gates.

• bottom : Fin self.bottomCount → RawClause V

  The literals and constants feeding each bottom OR gate.

• middle : Fin self.middleCount → Finset (Fin self.bottomCount)

  The bottom gates feeding each middle AND gate.

• top : Finset (Fin self.middleCount)

  The middle gates feeding the top OR gate.

def Complexity.DepthThreeLowerBound.Circuit3.gateCount {V : Type uV} (C : Circuit3 V) : ℕ

Count every bottom and middle gate and the single top OR gate.

Equations

• C.gateCount = C.bottomCount + C.middleCount + 1

noncomputable def Complexity.DepthThreeLowerBound.Circuit3.middleEval {V : Type uV} (C : Circuit3 V) (j : Fin C.middleCount) (x : Cube V) : Bool

Evaluate one middle AND gate on its selected bottom gates.

Equations

• C.middleEval j x = decide (∀ i ∈ C.middle j, (C.bottom i).eval x = true)

noncomputable def Complexity.DepthThreeLowerBound.Circuit3.eval {V : Type uV} (C : Circuit3 V) (x : Cube V) : Bool

Evaluate the top OR of the selected middle AND gates.

Equations

• C.eval x = decide (∃ j ∈ C.top, C.middleEval j x = true)

def Complexity.DepthThreeLowerBound.Circuit3.Computes {V : Type uV} (C : Circuit3 V) (f : Cube V → Bool) : Prop

The circuit agrees with the specified Boolean function on every input.

Equations

• C.Computes f = ∀ (x : Complexity.DepthThreeLowerBound.Cube V), C.eval x = f x

def Complexity.DepthThreeLowerBound.runSteps {S : Type uS} (step : S → Option S) (n : ℕ) (c : Option S) : Option S

Iterate an optional transition, propagating none after halting.

Equations

• Complexity.DepthThreeLowerBound.runSteps step n c = (fun (oc : Option S) => oc.bind step)^[n] c

inductive Complexity.DepthThreeLowerBound.HeadMove : Type

A left, stationary, or right move on a bilateral tape.

• left : HeadMove
• stay : HeadMove
• right : HeadMove

def Complexity.DepthThreeLowerBound.HeadMove.apply {Γ : Type uGamma} [Inhabited Γ] : HeadMove → Turing.Tape Γ → Turing.Tape Γ

Apply a head movement to a Mathlib bilateral tape.

Equations

• Complexity.DepthThreeLowerBound.HeadMove.left.apply x✝ = Turing.Tape.move Turing.Dir.left x✝
• Complexity.DepthThreeLowerBound.HeadMove.stay.apply x✝ = x✝
• Complexity.DepthThreeLowerBound.HeadMove.right.apply x✝ = Turing.Tape.move Turing.Dir.right x✝

structure Complexity.DepthThreeLowerBound.MultiTapeCfg (K : Type uK) (Γ : Type uGamma) (Q : Type uQ) [Inhabited Γ] : Type (max (max uGamma uK) uQ)

A control state and a tape for each tape index.

• q : Q

  The finite control state.

• tapes : K → Turing.Tape Γ

  The bilateral tape contents and head positions.

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.MultiTapeCode (K : Type uK) (Γ : Type uGamma) (Q : Type uQ) : Type (max (max (max uGamma uK) uQ) (max uGamma uK) uQ)

Read all heads, then halt or choose a state, writes, and head moves.

Equations

• Complexity.DepthThreeLowerBound.MultiTapeCode K Γ Q = (Q → (K → Γ) → Option (Q × (K → Γ) × (K → Complexity.DepthThreeLowerBound.HeadMove)))

def Complexity.DepthThreeLowerBound.multiTapeUpdate {K : Type uK} {Γ : Type uGamma} {Q : Type uQ} [Inhabited Γ] (c : MultiTapeCfg K Γ Q) (q : Q) (writes : K → Γ) (moves : K → HeadMove) : MultiTapeCfg K Γ Q

Write the scanned cells and then move every tape head.

Equations

• Complexity.DepthThreeLowerBound.multiTapeUpdate c q writes moves = { q := q, tapes := fun (k : K) => (moves k).apply (Turing.Tape.write (writes k) (c.tapes k)) }

def Complexity.DepthThreeLowerBound.multiTapeStep {K : Type uK} {Γ : Type uGamma} {Q : Type uQ} [Inhabited Γ] (code : MultiTapeCode K Γ Q) (c : MultiTapeCfg K Γ Q) : Option (MultiTapeCfg K Γ Q)

Execute one transition of a multitape program.

Equations

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

structure Complexity.DepthThreeLowerBound.FiniteMultiTapeMachine : Type 1

A multitape machine with finite control, alphabet, and tape set. The input occupies one designated read-write tape; the default symbol is blank.

• K : Type

  Tape indices.

• tapeFinite : Fintype self.K
• tapeDecidableEq : DecidableEq self.K
• inputTape : self.K

  The tape initially containing the input word.

• Γ : Type

  The tape alphabet; its default value is blank.

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

  Control states.

• stateFinite : Fintype self.Q
• initialState : self.Q

  The initial control state.

• 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 : MultiTapeCode self.K self.Γ self.Q

  The partial transition function; none halts.

• accept : self.Q → Bool

  The Boolean verdict read from a halting control state.

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.FiniteMultiTapeMachine.Cfg (M : FiniteMultiTapeMachine) : Type

Configurations of the bundled finite multitape machine.

Equations

• M.Cfg = Complexity.DepthThreeLowerBound.MultiTapeCfg M.K M.Γ M.Q

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.FiniteMultiTapeMachine.step (M : FiniteMultiTapeMachine) : M.Cfg → Option M.Cfg

The bundled machine's partial transition function.

Equations

• M.step = Complexity.DepthThreeLowerBound.multiTapeStep M.code

def Complexity.DepthThreeLowerBound.FiniteMultiTapeMachine.init (M : FiniteMultiTapeMachine) (input : List Bool) : M.Cfg

Initialize the input tape at its first bit and all other tapes blank.

Equations

• M.init input = { q := M.initialState, tapes := fun (k : M.K) => if k = M.inputTape then Turing.Tape.mk₁ (List.map M.inputSymbol input) else Turing.Tape.mk₁ [] }

def Complexity.DepthThreeLowerBound.MultiTapeHaltsIn (M : FiniteMultiTapeMachine) (input : List Bool) (output : Bool) (time : ℕ) : Prop

Within the stated time, reach a halting state with the specified Boolean verdict.

Equations

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