Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeConvolutionPrepare

Unrestricted depth-three lower bound: tape convolution prepare #

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

Control states for the copy stage of the convolution prepare routine.

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

    Control states for the add stage of the convolution prepare routine.

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

      Control states for the fill stage of the convolution prepare routine.

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

        Control states of the convolution prepare routine.

        Equations
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeConvolutionPrepare.copies :
          TapeMultiProgram CopyState

          Copy the ring degree into the two convolution loop counters.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Complexity.DepthThreeLowerBound.TapeConvolutionPrepare.addition :
            TapeMultiProgram AddState

            Add the copied counters to determine the convolution workspace length.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Complexity.DepthThreeLowerBound.TapeConvolutionPrepare.filling :
              TapeMultiProgram FillState

              Fill the convolution output workspace with false bits.

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

                Transition function of the convolution prepare routine.

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

                  Initial control state of the convolution prepare routine.

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

                    Terminal control state of the convolution prepare routine.

                    Equations
                    Instances For
                      source
                      theorem Complexity.DepthThreeLowerBound.TapeConvolutionPrepare.runs_prepare (σ : TapeStore) (r : ℕ) (hr : σ TapeRegister.ringDegree = List.replicate r true) (hL0 : σ TapeRegister.loop0 = []) (hL1 : σ TapeRegister.loop1 = []) (hI : σ TapeRegister.indexA = []) (hOut : σ TapeRegister.productBits = []) :
                      RunsIn program.step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (TapeConvolutionRows.frame σ r 0 (List.replicate (r + r) false)))) (30 * r + 22)
                      source
                      @[simp]
                      theorem Complexity.DepthThreeLowerBound.TapeConvolutionPrepare.program_done (h : TapeHeads) :
                      program done h = none