Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeConvolutionRow

Unrestricted depth-three lower bound: tape convolution row #

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

Control states of the convolution row routine.

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

    Transition function of the convolution row routine.

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

      Initial control state of the convolution row routine.

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

        Terminal control state of the convolution row routine.

        Equations
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeConvolutionRow.frame (σ : TapeStore) (remaining column : ℕ) (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.TapeConvolutionRow.frame_counter (σ : TapeStore) (n j : ℕ) (out : List Bool) :
            frame σ n j out TapeRegister.loop1 = List.replicate n true
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeConvolutionRow.frame_index (σ : TapeStore) (n j : ℕ) (out : List Bool) :
            frame σ n j out TapeRegister.indexB = List.replicate j true
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeConvolutionRow.frame_output (σ : TapeStore) (n j : ℕ) (out : List Bool) :
            frame σ n j out TapeRegister.productBits = out
            source
            theorem Complexity.DepthThreeLowerBound.TapeConvolutionRow.update_counter (σ : TapeStore) (n n' j : ℕ) (out : List Bool) :
            Function.update (frame σ n j out) TapeRegister.loop1 (List.replicate n' true) = frame σ n' j out
            source
            theorem Complexity.DepthThreeLowerBound.TapeConvolutionRow.resultStore_frame (σ : TapeStore) (n j : ℕ) (out out' : List Bool) :
            TapeConvolutionStep.resultStore (frame σ n j out) j out' = frame σ n (j + 1) out'
            source
            theorem Complexity.DepthThreeLowerBound.TapeConvolutionRow.runs_step (σ : TapeStore) (i j : ℕ) (hi : σ TapeRegister.indexA = List.replicate i true) (hj : σ TapeRegister.indexB = List.replicate j true) (hk : σ TapeRegister.indexC = []) (hs : σ TapeRegister.scratchA = []) (ha : i < (σ TapeRegister.hashBits).length) (hb : j < (σ TapeRegister.accumBits).length) (hc : i + j < (σ TapeRegister.productBits).length) :
            RunsIn TapeConvolutionStep.program.step (TapeMultiProgram.cfg TapeConvolutionStep.start (storeTapes σ)) (TapeMultiProgram.cfg TapeConvolutionStep.done (storeTapes (TapeConvolutionStep.resultStore σ j (xorListAt (σ TapeRegister.productBits) (i + j) ((σ TapeRegister.hashBits).getD i false && (σ TapeRegister.accumBits).getD j false))))) (8 * i + 16 * j + 37)
            source
            theorem Complexity.DepthThreeLowerBound.TapeConvolutionRow.runs_row (σ : TapeStore) (a b : List Bool) (i j n : ℕ) (out : List Bool) (hA : σ TapeRegister.hashBits = a) (hB : σ TapeRegister.accumBits = b) (hI : σ TapeRegister.indexA = List.replicate i true) (hK : σ TapeRegister.indexC = []) (hS : σ TapeRegister.scratchA = []) (hi : i < a.length) (hj : j + n ≤ b.length) (hsize : a.length + b.length ≤ out.length) :
            RunsIn program.step (TapeMultiProgram.cfg start (storeTapes (frame σ n j out))) (TapeMultiProgram.cfg done (storeTapes (frame σ 0 (j + n) (convolutionUpdateRow a b i (List.range' j n) out)))) (n * (8 * a.length + 16 * b.length + 43) + 3)
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeConvolutionRow.program_done (h : TapeHeads) :
            program done h = none