Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeDecodeBlocks

Unrestricted depth-three lower bound: tape decode blocks #

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

Control states for the tail stage of the decode blocks routine.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Complexity.DepthThreeLowerBound.TapeDecodeBlocks.tailProgram :
    TapeMultiProgram TailState

    Transition function for the tail stage of the decode blocks routine.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.DepthThreeLowerBound.TapeDecodeBlocks.tailStart :
      TailState

      Initial control state of the tail stage of the decode blocks routine.

      Equations
      Instances For
        source
        def Complexity.DepthThreeLowerBound.TapeDecodeBlocks.tailDone :
        TailState

        Terminal control state of the tail stage of the decode blocks routine.

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

          Control states for the rest stage of the decode blocks routine.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Complexity.DepthThreeLowerBound.TapeDecodeBlocks.restProgram :
            TapeMultiProgram RestState

            Transition function for the rest stage of the decode blocks routine.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Complexity.DepthThreeLowerBound.TapeDecodeBlocks.restStart :
              RestState

              Initial control state of the rest stage of the decode blocks routine.

              Equations
              Instances For
                source
                def Complexity.DepthThreeLowerBound.TapeDecodeBlocks.restDone :
                RestState

                Terminal control state of the rest stage of the decode blocks routine.

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

                  Control states of the decode blocks routine.

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

                    Transition function of the decode blocks routine.

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

                      Initial control state of the decode blocks routine.

                      Equations
                      Instances For
                        source
                        def Complexity.DepthThreeLowerBound.TapeDecodeBlocks.done :
                        State

                        Terminal control state of the decode blocks routine.

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

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

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            @[simp]
                            theorem Complexity.DepthThreeLowerBound.TapeDecodeBlocks.outputStore_block (σ : TapeStore) (w : List Bool) (kind : InputBlockKind) :
                            outputStore σ w (TapeInputBlocks.outputRegister kind) = inputBlockData w kind
                            source
                            theorem Complexity.DepthThreeLowerBound.TapeDecodeBlocks.outputStore_other (σ : TapeStore) (w : List Bool) (q : TapeRegister) (h15 : q ≠ 15) (h16 : q ≠ 16) (h17 : q ≠ 17) (h18 : q ≠ 18) :
                            outputStore σ w q = σ q
                            source
                            theorem Complexity.DepthThreeLowerBound.TapeDecodeBlocks.runs_decode (σ : TapeStore) (w : List Bool) (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 = []) (h15 : σ 15 = []) (h16 : σ 16 = []) (h17 : σ 17 = []) (h18 : σ 18 = []) :
                            RunsIn program.step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (outputStore σ w))) (804 * (w.length + 1) ^ 2)