Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeDecodeBlock

Unrestricted depth-three lower bound: tape decode block #

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

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

source
@[reducible, inline]
abbrev Complexity.DepthThreeLowerBound.TapeDecodeBlock.FinishState :
Type

Control states for the finish stage of the decode block routine.

Equations
Instances For
    source
    def Complexity.DepthThreeLowerBound.TapeDecodeBlock.finishProgram (kind : InputBlockKind) :
    TapeMultiProgram FinishState

    Transition function for the finish stage of the decode block routine.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.DepthThreeLowerBound.TapeDecodeBlock.finishStart :
      FinishState

      Initial control state of the finish stage of the decode block routine.

      Equations
      Instances For
        source
        def Complexity.DepthThreeLowerBound.TapeDecodeBlock.finishDone :
        FinishState

        Terminal control state of the finish stage of the decode block routine.

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev Complexity.DepthThreeLowerBound.TapeDecodeBlock.State (kind : InputBlockKind) :
          Type

          Control states of the decode block routine.

          Equations
          Instances For
            source
            def Complexity.DepthThreeLowerBound.TapeDecodeBlock.program (kind : InputBlockKind) :
            TapeMultiProgram (State kind)

            Transition function of the decode block routine.

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

              Initial control state of the decode block routine.

              Equations
              Instances For
                source
                def Complexity.DepthThreeLowerBound.TapeDecodeBlock.done (kind : InputBlockKind) :
                State kind

                Terminal control state of the decode block routine.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem Complexity.DepthThreeLowerBound.TapeDecodeBlock.program_done (kind : InputBlockKind) (h : TapeHeads) :
                  program kind (done kind) h = none
                  source
                  def Complexity.DepthThreeLowerBound.TapeDecodeBlock.outputStore (σ : TapeStore) (w : List Bool) (kind : InputBlockKind) :
                  TapeStore

                  Tape-store contents at the output stage of the decode block routine.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem Complexity.DepthThreeLowerBound.TapeDecodeBlock.runs_block (σ : TapeStore) (w : List Bool) (kind : InputBlockKind) (hfit : InputFits w) (hw : σ TapeRegister.input = w) (hd : σ 2 = List.replicate (dataDimension w.length) true) (hr : σ 3 = List.replicate (hashDimension (dataDimension w.length)) true) (ht : σ 4 = List.replicate (independenceOrder (dataDimension w.length)) true) (h29 : σ 29 = []) (h30 : σ 30 = []) (h31 : σ 31 = []) (h5 : σ 5 = []) (h6 : σ 6 = []) (h7 : σ 7 = []) (hout : σ (TapeInputBlocks.outputRegister kind) = []) :
                    RunsIn (program kind).step (TapeMultiProgram.cfg (start kind) (storeTapes σ)) (TapeMultiProgram.cfg (done kind) (storeTapes (outputStore σ w kind))) (200 * (w.length + 1) ^ 2)