Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeParse

Unrestricted depth-three lower bound: tape parse #

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

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

source
def Complexity.DepthThreeLowerBound.TapeParse.inputStore (w : List Bool) :
TapeStore

The input bits and their unary length, with every other register empty.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Complexity.DepthThreeLowerBound.TapeParse.initializedTapes_eq_store (w : List Bool) :
    initializedTapes w = storeTapes (inputStore w)
    source
    def Complexity.DepthThreeLowerBound.TapeParse.outputStore (w : List Bool) :
    TapeStore

    Tape-store contents at the output stage of the parse routine.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem Complexity.DepthThreeLowerBound.TapeParse.outputStore_input (w : List Bool) :
      outputStore w 0 = w
      source
      @[simp]
      theorem Complexity.DepthThreeLowerBound.TapeParse.outputStore_data (w : List Bool) :
      outputStore w 2 = List.replicate (dataDimension w.length) true
      source
      @[simp]
      theorem Complexity.DepthThreeLowerBound.TapeParse.outputStore_hash (w : List Bool) :
      outputStore w 3 = List.replicate (hashDimension (dataDimension w.length)) true
      source
      @[simp]
      theorem Complexity.DepthThreeLowerBound.TapeParse.outputStore_order (w : List Bool) :
      outputStore w 4 = List.replicate (independenceOrder (dataDimension w.length)) true
      source
      theorem Complexity.DepthThreeLowerBound.TapeParse.outputStore_empty (w : List Bool) (r : TapeRegister) (h0 : r ≠ 0) (h1 : r ≠ 1) (h2 : r ≠ 2) (h3 : r ≠ 3) (h4 : r ≠ 4) (h8 : r ≠ 8) :
      outputStore w r = []
      source
      @[reducible, inline]
      abbrev Complexity.DepthThreeLowerBound.TapeParse.WorkState :
      Type

      Control states for the work stage of the parse routine.

      Equations
      Instances For
        source
        def Complexity.DepthThreeLowerBound.TapeParse.workProgram :
        TapeMultiProgram WorkState

        Transition function for the work stage of the parse routine.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeParse.workStart :
          WorkState

          Initial control state of the work stage of the parse routine.

          Equations
          Instances For
            source
            def Complexity.DepthThreeLowerBound.TapeParse.workDone (accepted : Bool) :
            WorkState

            Terminal control state of the work stage of the parse routine.

            Equations
            Instances For
              source
              @[reducible, inline]
              abbrev Complexity.DepthThreeLowerBound.TapeParse.State :
              Type

              Control states of the parse routine.

              Equations
              Instances For
                source
                def Complexity.DepthThreeLowerBound.TapeParse.program :
                TapeMultiProgram State

                Transition function of the parse routine.

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

                  Initial control state of the parse routine.

                  Equations
                  Instances For
                    source
                    def Complexity.DepthThreeLowerBound.TapeParse.done (accepted : Bool) :
                    State

                    Terminal control state of the parse routine.

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

                      Read the Boolean verdict from the terminal control state of the parse routine.

                      Equations
                      Instances For
                        source
                        @[simp]
                        theorem Complexity.DepthThreeLowerBound.TapeParse.acceptFlag_done (b : Bool) :
                        acceptFlag (done b) = b
                        source
                        @[simp]
                        theorem Complexity.DepthThreeLowerBound.TapeParse.program_done (b : Bool) (h : TapeHeads) :
                        program (done b) h = none
                        source
                        theorem Complexity.DepthThreeLowerBound.TapeParse.runs_parse (w : List Bool) :
                        RunsIn program.step (TapeMultiProgram.cfg start (rawInputTapes w)) (TapeMultiProgram.cfg (done (decide (InputFits w))) (storeTapes (outputStore w))) (1000 * (w.length + 3) ^ 8)