Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeConvolutionStep

Unrestricted depth-three lower bound: tape convolution step #

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

Control states for the setup stage of the convolution step routine.

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

    Control states for the sum stage of the convolution step routine.

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

      Control states for the term stage of the convolution step routine.

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

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

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

          Control states of the convolution step routine.

          Equations
          Instances For
            source
            def Complexity.DepthThreeLowerBound.TapeConvolutionStep.copyIndices :
            TapeMultiProgram SetupState

            Copy the current row and column indices into temporary counters.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Complexity.DepthThreeLowerBound.TapeConvolutionStep.sumIndices :
              TapeMultiProgram SumState

              Add the copied indices to locate the output coefficient.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Complexity.DepthThreeLowerBound.TapeConvolutionStep.term :
                TapeMultiProgram TermState

                Accumulate the selected input-bit product into its output coefficient.

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

                  Clear the temporary output index after accumulating a convolution term.

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

                    Transition function of the convolution step routine.

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

                      Initial control state of the convolution step routine.

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

                        Terminal control state of the convolution step routine.

                        Equations
                        Instances For
                          source
                          def Complexity.DepthThreeLowerBound.TapeConvolutionStep.resultStore (σ : TapeStore) (j : ℕ) (out : List Bool) :
                          TapeStore

                          Tape-store contents at the result stage of the convolution step routine.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            theorem Complexity.DepthThreeLowerBound.TapeConvolutionStep.runs_step (σ : TapeStore) (pa sa pb sb pc sc : List Bool) (a b old : Bool) (hi : σ TapeRegister.indexA = List.replicate pa.length true) (hj : σ TapeRegister.indexB = List.replicate pb.length true) (hk : σ TapeRegister.indexC = []) (hs : σ TapeRegister.scratchA = []) (ha : σ TapeRegister.hashBits = pa ++ a :: sa) (hb : σ TapeRegister.accumBits = pb ++ b :: sb) (hc : σ TapeRegister.productBits = pc ++ old :: sc) (hlen : pc.length = pa.length + pb.length) :
                            RunsIn program.step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (resultStore σ pb.length (pc ++ (old ^^ a && b) :: sc)))) (8 * pa.length + 16 * pb.length + 37)
                            source
                            @[simp]
                            theorem Complexity.DepthThreeLowerBound.TapeConvolutionStep.program_done (h : TapeHeads) :
                            program done h = none