Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeConvolve

Unrestricted depth-three lower bound: tape convolve #

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

Control states for the work stage of the convolve routine.

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

    Control states of the convolve routine.

    Equations
    Instances For
      source
      def Complexity.DepthThreeLowerBound.TapeConvolve.work :
      TapeMultiProgram WorkState

      Compose the main computational stages of the routine.

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

        Transition function of the convolve routine.

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

          Initial control state of the convolve routine.

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

            Terminal control state of the convolve routine.

            Equations
            Instances For
              source
              def Complexity.DepthThreeLowerBound.TapeConvolve.cost (r : ℕ) :
              ℕ

              Transition budget for the convolve routine.

              Equations
              Instances For
                source
                theorem Complexity.DepthThreeLowerBound.TapeConvolve.runs_convolve (σ : TapeStore) (a b : List Bool) (r : ℕ) (hA : σ TapeRegister.hashBits = a) (hB : σ TapeRegister.accumBits = b) (hlenA : a.length = r) (hlenB : b.length = r) (hCount : σ TapeRegister.ringDegree = List.replicate r true) (hL0 : σ TapeRegister.loop0 = []) (hL1 : σ TapeRegister.loop1 = []) (hI : σ TapeRegister.indexA = []) (hJ : σ TapeRegister.indexB = []) (hK : σ TapeRegister.indexC = []) (hS : σ TapeRegister.scratchA = []) (hOut : σ TapeRegister.productBits = []) :
                RunsIn program.step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (Function.update σ TapeRegister.productBits (convolveBitLists a b)))) (cost r)
                source
                @[simp]
                theorem Complexity.DepthThreeLowerBound.TapeConvolve.program_done (h : TapeHeads) :
                program done h = none