Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeConvolutionRows

Unrestricted depth-three lower bound: tape convolution rows #

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

Control states for the read stage of the convolution rows routine.

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

    Control states for the clear stage of the convolution rows routine.

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

      Control states for the body stage of the convolution rows routine.

      Equations
      Instances For
        source
        def Complexity.DepthThreeLowerBound.TapeConvolutionRows.readProgram :
        TapeMultiProgram ReadState

        Transition function for the read stage of the convolution rows routine.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeConvolutionRows.clearProgram :
          TapeMultiProgram ClearState

          Transition function for the clear stage of the convolution rows routine.

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

            Transition function for the body stage of the convolution rows routine.

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

              Initial control state of the body stage of the convolution rows routine.

              Equations
              Instances For
                source
                def Complexity.DepthThreeLowerBound.TapeConvolutionRows.bodyDone :
                BodyState

                Terminal control state of the body stage of the convolution rows routine.

                Equations
                Instances For
                  source
                  def Complexity.DepthThreeLowerBound.TapeConvolutionRows.bodyResult (σ : TapeStore) (i : ℕ) (out : List Bool) :
                  TapeStore

                  Update the convolution output and advance the row index.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem Complexity.DepthThreeLowerBound.TapeConvolutionRows.runs_body (σ : TapeStore) (a b out : List Bool) (i : ℕ) (hA : σ TapeRegister.hashBits = a) (hB : σ TapeRegister.accumBits = b) (hI : σ TapeRegister.indexA = List.replicate i true) (hJ : σ TapeRegister.indexB = []) (hCount : σ TapeRegister.ringDegree = List.replicate b.length true) (hLoop : σ TapeRegister.loop1 = []) (hK : σ TapeRegister.indexC = []) (hS : σ TapeRegister.scratchA = []) (hOut : σ TapeRegister.productBits = out) (hi : i < a.length) (hsize : a.length + b.length ≤ out.length) :
                    RunsIn bodyProgram.step (TapeMultiProgram.cfg bodyStart (storeTapes σ)) (TapeMultiProgram.cfg bodyDone (storeTapes (bodyResult σ i (convolutionUpdateRow a b i (List.range' 0 b.length) out)))) (b.length * (8 * a.length + 16 * b.length + 43) + 4 * b.length + 17)
                    source
                    @[simp]
                    theorem Complexity.DepthThreeLowerBound.TapeConvolutionRows.body_done (h : TapeHeads) :
                    bodyProgram bodyDone h = none
                    source
                    @[reducible, inline]
                    abbrev Complexity.DepthThreeLowerBound.TapeConvolutionRows.State :
                    Type

                    Control states of the convolution rows routine.

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

                      Transition function of the convolution rows routine.

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

                        Initial control state of the convolution rows routine.

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

                          Terminal control state of the convolution rows routine.

                          Equations
                          Instances For
                            source
                            def Complexity.DepthThreeLowerBound.TapeConvolutionRows.frame (σ : TapeStore) (remaining row : ℕ) (out : List Bool) :
                            TapeStore

                            Tape-store invariant recording the loop counters and current output.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              @[simp]
                              theorem Complexity.DepthThreeLowerBound.TapeConvolutionRows.frame_counter (σ : TapeStore) (n i : ℕ) (out : List Bool) :
                              frame σ n i out TapeRegister.loop0 = List.replicate n true
                              source
                              @[simp]
                              theorem Complexity.DepthThreeLowerBound.TapeConvolutionRows.frame_index (σ : TapeStore) (n i : ℕ) (out : List Bool) :
                              frame σ n i out TapeRegister.indexA = List.replicate i true
                              source
                              @[simp]
                              theorem Complexity.DepthThreeLowerBound.TapeConvolutionRows.frame_output (σ : TapeStore) (n i : ℕ) (out : List Bool) :
                              frame σ n i out TapeRegister.productBits = out
                              source
                              theorem Complexity.DepthThreeLowerBound.TapeConvolutionRows.update_counter (σ : TapeStore) (n n' i : ℕ) (out : List Bool) :
                              Function.update (frame σ n i out) TapeRegister.loop0 (List.replicate n' true) = frame σ n' i out
                              source
                              theorem Complexity.DepthThreeLowerBound.TapeConvolutionRows.bodyResult_frame (σ : TapeStore) (n i : ℕ) (out out' : List Bool) :
                              bodyResult (frame σ n i out) i out' = frame σ n (i + 1) out'
                              source
                              theorem Complexity.DepthThreeLowerBound.TapeConvolutionRows.runs_rows (σ : TapeStore) (a b : List Bool) (i n : ℕ) (out : List Bool) (hA : σ TapeRegister.hashBits = a) (hB : σ TapeRegister.accumBits = b) (hJ : σ TapeRegister.indexB = []) (hCount : σ TapeRegister.ringDegree = List.replicate b.length true) (hLoop : σ TapeRegister.loop1 = []) (hK : σ TapeRegister.indexC = []) (hS : σ TapeRegister.scratchA = []) (hi : i + n ≤ a.length) (hsize : a.length + b.length ≤ out.length) :
                              RunsIn program.step (TapeMultiProgram.cfg start (storeTapes (frame σ n i out))) (TapeMultiProgram.cfg done (storeTapes (frame σ 0 (i + n) (convolutionUpdateRows a b (List.range' i n) out)))) (n * (b.length * (8 * a.length + 16 * b.length + 43) + 4 * b.length + 23) + 3)
                              source
                              @[simp]
                              theorem Complexity.DepthThreeLowerBound.TapeConvolutionRows.program_done (h : TapeHeads) :
                              program done h = none