Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeInputBlocks

Unrestricted depth-three lower bound: tape input blocks #

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

Control states for the prepare stage of the input blocks routine.

Equations
Instances For
    source
    def Complexity.DepthThreeLowerBound.TapeInputBlocks.prepareProgram (R : TapeInputBlockLoop.Registers) :
    TapeMultiProgram PrepareState

    Transition function for the prepare stage of the input blocks routine.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.DepthThreeLowerBound.TapeInputBlocks.prepareStart :
      PrepareState

      Initial control state of the prepare stage of the input blocks routine.

      Equations
      Instances For
        source
        def Complexity.DepthThreeLowerBound.TapeInputBlocks.prepareDone :
        PrepareState

        Terminal control state of the prepare stage of the input blocks routine.

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

          Control states of the input blocks routine.

          Equations
          Instances For
            source
            def Complexity.DepthThreeLowerBound.TapeInputBlocks.program (R : TapeInputBlockLoop.Registers) :
            TapeMultiProgram State

            Transition function of the input blocks routine.

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

              Initial control state of the input blocks routine.

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

                Terminal control state of the input blocks routine.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem Complexity.DepthThreeLowerBound.TapeInputBlocks.prepare_done (R : TapeInputBlockLoop.Registers) (h : TapeHeads) :
                  prepareProgram R prepareDone h = none
                  source
                  @[simp]
                  theorem Complexity.DepthThreeLowerBound.TapeInputBlocks.program_done (R : TapeInputBlockLoop.Registers) (h : TapeHeads) :
                  program R done h = none
                  source
                  theorem Complexity.DepthThreeLowerBound.TapeInputBlocks.runs_prepare (R : TapeInputBlockLoop.Registers) (σ : TapeStore) (offset len : ℕ) (hi : σ (TapeInputBlockLoop.index R) = List.replicate offset true) (hc : σ (TapeInputBlockLoop.count R) = List.replicate len true) (hs : σ (TapeInputBlockLoop.scratch R) = []) :
                  RunsIn (prepareProgram R).step (TapeMultiProgram.cfg prepareStart (storeTapes σ)) (TapeMultiProgram.cfg prepareDone (storeTapes (Function.update σ (TapeInputBlockLoop.index R) (List.replicate (offset + len) true)))) (10 * len + 8)
                  source
                  theorem Complexity.DepthThreeLowerBound.TapeInputBlocks.blockStore_prepared (R : TapeInputBlockLoop.Registers) (σ : TapeStore) (offset len : ℕ) (acc : List Bool) (hc : σ (TapeInputBlockLoop.count R) = List.replicate len true) (hd : σ (TapeInputBlockLoop.destination R) = acc) :
                  TapeInputBlockLoop.blockStore R σ (offset + len) len acc = Function.update σ (TapeInputBlockLoop.index R) (List.replicate (offset + len) true)
                  source
                  theorem Complexity.DepthThreeLowerBound.TapeInputBlocks.blockStore_finished (R : TapeInputBlockLoop.Registers) (σ : TapeStore) (offset : ℕ) (bits : List Bool) (hi : σ (TapeInputBlockLoop.index R) = List.replicate offset true) :
                  TapeInputBlockLoop.blockStore R σ offset 0 bits = Function.update (Function.update σ (TapeInputBlockLoop.count R) []) (TapeInputBlockLoop.destination R) bits
                  source
                  theorem Complexity.DepthThreeLowerBound.TapeInputBlocks.runs_extract (R : TapeInputBlockLoop.Registers) (σ : TapeStore) («prefix» block suffix acc : List Bool) (hinput : σ (TapeInputBlockLoop.source R) = «prefix» ++ block ++ suffix) (hi : σ (TapeInputBlockLoop.index R) = List.replicate «prefix».length true) (hc : σ (TapeInputBlockLoop.count R) = List.replicate block.length true) (hs : σ (TapeInputBlockLoop.scratch R) = []) (hd : σ (TapeInputBlockLoop.destination R) = acc) :
                  RunsIn (program R).step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (Function.update (Function.update σ (TapeInputBlockLoop.count R) []) (TapeInputBlockLoop.destination R) (block ++ acc)))) (block.length * (2 * «prefix».length + block.length + 27) + 12)
                  source
                  def Complexity.DepthThreeLowerBound.TapeInputBlocks.outputRegister :
                  InputBlockKind → TapeRegister

                  The destination register for the selected kind of input block.

                  Equations
                  Instances For
                    source
                    def Complexity.DepthThreeLowerBound.TapeInputBlocks.canonicalRegisters (kind : InputBlockKind) :
                    TapeInputBlockLoop.Registers

                    Allocate input and temporary registers for decoding the selected block.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[simp]
                      theorem Complexity.DepthThreeLowerBound.TapeInputBlocks.canonical_source (kind : InputBlockKind) :
                      TapeInputBlockLoop.source (canonicalRegisters kind) = TapeRegister.input
                      source
                      @[simp]
                      theorem Complexity.DepthThreeLowerBound.TapeInputBlocks.canonical_index (kind : InputBlockKind) :
                      TapeInputBlockLoop.index (canonicalRegisters kind) = TapeRegister.temp0
                      source
                      @[simp]
                      theorem Complexity.DepthThreeLowerBound.TapeInputBlocks.canonical_count (kind : InputBlockKind) :
                      TapeInputBlockLoop.count (canonicalRegisters kind) = TapeRegister.temp1
                      source
                      @[simp]
                      theorem Complexity.DepthThreeLowerBound.TapeInputBlocks.canonical_scratch (kind : InputBlockKind) :
                      TapeInputBlockLoop.scratch (canonicalRegisters kind) = TapeRegister.temp2
                      source
                      @[simp]
                      theorem Complexity.DepthThreeLowerBound.TapeInputBlocks.canonical_destination (kind : InputBlockKind) :
                      TapeInputBlockLoop.destination (canonicalRegisters kind) = outputRegister kind
                      source
                      def Complexity.DepthThreeLowerBound.TapeInputBlocks.canonicalProgram (kind : InputBlockKind) :
                      TapeMultiProgram State

                      Transition function for the canonical stage of the input blocks routine.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        @[simp]
                        theorem Complexity.DepthThreeLowerBound.TapeInputBlocks.canonical_done (kind : InputBlockKind) (h : TapeHeads) :
                        canonicalProgram kind done h = none
                        source
                        theorem Complexity.DepthThreeLowerBound.TapeInputBlocks.canonical_cost_le {w : List Bool} (hfit : InputFits w) (kind : InputBlockKind) :
                        inputBlockLength w.length kind * (2 * inputBlockOffset w.length kind + inputBlockLength w.length kind + 27) + 12 ≤ w.length * (3 * w.length + 27) + 12
                        source
                        theorem Complexity.DepthThreeLowerBound.TapeInputBlocks.runs_canonical_block (kind : InputBlockKind) (σ : TapeStore) (w : List Bool) (hfit : InputFits w) (hw : σ TapeRegister.input = w) (hi : σ TapeRegister.temp0 = List.replicate (inputBlockOffset w.length kind) true) (hc : σ TapeRegister.temp1 = List.replicate (inputBlockLength w.length kind) true) (hs : σ TapeRegister.temp2 = []) (hd : σ (outputRegister kind) = []) :
                        RunsIn (canonicalProgram kind).step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (Function.update (Function.update σ TapeRegister.temp1 []) (outputRegister kind) (inputBlockData w kind)))) (inputBlockLength w.length kind * (2 * inputBlockOffset w.length kind + inputBlockLength w.length kind + 27) + 12)
                        source
                        theorem Complexity.DepthThreeLowerBound.TapeInputBlocks.runs_data (σ : TapeStore) (w : List Bool) (hfit : InputFits w) (hw : σ TapeRegister.input = w) (hi : σ TapeRegister.temp0 = []) (hc : σ TapeRegister.temp1 = List.replicate (dataDimension w.length) true) (hs : σ TapeRegister.temp2 = []) (hd : σ TapeRegister.dataBits = []) :
                        RunsIn (canonicalProgram InputBlockKind.data).step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (Function.update (Function.update σ TapeRegister.temp1 []) TapeRegister.dataBits (inputBlockData w InputBlockKind.data)))) (dataDimension w.length * (dataDimension w.length + 27) + 12)
                        source
                        theorem Complexity.DepthThreeLowerBound.TapeInputBlocks.runs_hash (σ : TapeStore) (w : List Bool) (hfit : InputFits w) (hw : σ TapeRegister.input = w) (hi : σ TapeRegister.temp0 = List.replicate (hashOffset (dataDimension w.length)) true) (hc : σ TapeRegister.temp1 = List.replicate (hashBlockLength (dataDimension w.length)) true) (hs : σ TapeRegister.temp2 = []) (hd : σ TapeRegister.keyBits = []) :
                        RunsIn (canonicalProgram InputBlockKind.hash).step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (Function.update (Function.update σ TapeRegister.temp1 []) TapeRegister.keyBits (inputBlockData w InputBlockKind.hash)))) (hashBlockLength (dataDimension w.length) * (2 * hashOffset (dataDimension w.length) + hashBlockLength (dataDimension w.length) + 27) + 12)
                        source
                        theorem Complexity.DepthThreeLowerBound.TapeInputBlocks.runs_polynomial (σ : TapeStore) (w : List Bool) (hfit : InputFits w) (hw : σ TapeRegister.input = w) (hi : σ TapeRegister.temp0 = List.replicate (polynomialOffset (dataDimension w.length)) true) (hc : σ TapeRegister.temp1 = List.replicate (hashDimension (dataDimension w.length)) true) (hs : σ TapeRegister.temp2 = []) (hd : σ TapeRegister.polyBits = []) :
                        RunsIn (canonicalProgram InputBlockKind.polynomial).step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (Function.update (Function.update σ TapeRegister.temp1 []) TapeRegister.polyBits (inputBlockData w InputBlockKind.polynomial)))) (hashDimension (dataDimension w.length) * (2 * polynomialOffset (dataDimension w.length) + hashDimension (dataDimension w.length) + 27) + 12)
                        source
                        theorem Complexity.DepthThreeLowerBound.TapeInputBlocks.runs_coefficients (σ : TapeStore) (w : List Bool) (hfit : InputFits w) (hw : σ TapeRegister.input = w) (hi : σ TapeRegister.temp0 = List.replicate (coefficientsOffset (dataDimension w.length)) true) (hc : σ TapeRegister.temp1 = List.replicate (independenceOrder (dataDimension w.length) * hashDimension (dataDimension w.length)) true) (hs : σ TapeRegister.temp2 = []) (hd : σ TapeRegister.coeffBits = []) :
                        RunsIn (canonicalProgram InputBlockKind.coefficients).step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (Function.update (Function.update σ TapeRegister.temp1 []) TapeRegister.coeffBits (inputBlockData w InputBlockKind.coefficients)))) (independenceOrder (dataDimension w.length) * hashDimension (dataDimension w.length) * (2 * coefficientsOffset (dataDimension w.length) + independenceOrder (dataDimension w.length) * hashDimension (dataDimension w.length) + 27) + 12)