Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.MachineLanguage

Unrestricted depth-three lower bound: machine language #

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

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

source
theorem Complexity.DepthThreeLowerBound.MachineLanguage.decoded_prepared (w : List Bool) :
TapeEvaluation.Prepared (TapeDecodeParsed.outputStore w) w
source
@[reducible, inline]
abbrev Complexity.DepthThreeLowerBound.MachineLanguage.BodyState :
Type

Control states for the body stage of the complete language decider.

Equations
Instances For
    source
    def Complexity.DepthThreeLowerBound.MachineLanguage.bodyProgram :
    TapeMultiProgram BodyState

    Transition function for the body stage of the complete language decider.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.DepthThreeLowerBound.MachineLanguage.bodyStart :
      BodyState

      Initial control state of the body stage of the complete language decider.

      Equations
      Instances For
        source
        def Complexity.DepthThreeLowerBound.MachineLanguage.bodyDone (answer : Bool) :
        BodyState

        Terminal control state of the body stage of the complete language decider.

        Equations
        Instances For
          source
          @[simp]
          theorem Complexity.DepthThreeLowerBound.MachineLanguage.bodyProgram_done (answer : Bool) (h : TapeHeads) :
          bodyProgram (bodyDone answer) h = none
          source
          theorem Complexity.DepthThreeLowerBound.MachineLanguage.runs_body (w : List Bool) (hfit : InputFits w) :
          RunsIn bodyProgram.step (TapeMultiProgram.cfg bodyStart (storeTapes (TapeParse.outputStore w))) (TapeMultiProgram.cfg (bodyDone (language w)) (storeTapes (TapeEvaluation.outputStore (TapeDecodeParsed.outputStore w) w))) (21000 * (w.length + 1) ^ 4)
          source
          @[reducible, inline]
          abbrev Complexity.DepthThreeLowerBound.MachineLanguage.State :
          Type

          Control states of the complete language decider.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Complexity.DepthThreeLowerBound.MachineLanguage.program :
            TapeMultiProgram State

            Transition function of the complete language decider.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Complexity.DepthThreeLowerBound.MachineLanguage.start :
              State

              Initial control state of the complete language decider.

              Equations
              Instances For
                source
                def Complexity.DepthThreeLowerBound.MachineLanguage.acceptFlag :
                State → Bool

                Read the Boolean verdict from the terminal control state of the complete language decider.

                Equations
                Instances For
                  source
                  @[instance_reducible]
                  instance Complexity.DepthThreeLowerBound.MachineLanguage.stateFintype :
                  Fintype State
                  Equations
                  source
                  def Complexity.DepthThreeLowerBound.MachineLanguage.machine :
                  FiniteMultiTapeMachine

                  The bundled finite multitape machine deciding the explicit language.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem Complexity.DepthThreeLowerBound.MachineLanguage.machine_init (w : List Bool) :
                    machine.init w = TapeMultiProgram.cfg start (rawInputTapes w)
                    source
                    theorem Complexity.DepthThreeLowerBound.MachineLanguage.halts (w : List Bool) :
                    MultiTapeHaltsIn machine w (language w) (24000 * (w.length + 3) ^ 8)
                    source
                    theorem Complexity.DepthThreeLowerBound.MachineLanguage.cost_le_standard (n : ℕ) :
                    24000 * (n + 3) ^ 8 ≤ 24000 * 3 ^ 8 * (n + 1) ^ 8
                    source
                    theorem Complexity.DepthThreeLowerBound.MachineLanguage.polynomial_time :
                    MultiTapePolynomialTimeDecider language
                    source
                    theorem Complexity.DepthThreeLowerBound.language_polynomial_time :
                    MultiTapePolynomialTimeDecider language