Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeParameterSearch

Unrestricted depth-three lower bound: tape parameter search #

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

Control states for the cube stage of the parameter search routine.

Equations
Instances For
    source
    def Complexity.DepthThreeLowerBound.TapeParameterSearch.cubeProgram (R : TapePowerSearch.Registers) :
    TapeMultiProgram CubeState

    Transition function for the cube stage of the parameter search routine.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.DepthThreeLowerBound.TapeParameterSearch.cubeStart :
      CubeState

      Initial control state of the cube stage of the parameter search routine.

      Equations
      Instances For
        source
        def Complexity.DepthThreeLowerBound.TapeParameterSearch.cubeDone :
        CubeState

        Terminal control state of the cube stage of the parameter search routine.

        Equations
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeParameterSearch.cubeCost (d : ℕ) :
          ℕ

          Transition budget for the parameter search routine at its cube stage.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem Complexity.DepthThreeLowerBound.TapeParameterSearch.runs_cube (R : TapePowerSearch.Registers) (σ : TapeStore) (d : ℕ) (ho : σ (R 0) = []) (hs : σ (R 2) = []) (hd : σ (R 3) = []) (ht : σ (R 4) = List.replicate (d ^ 2) true) :
            RunsIn (cubeProgram R).step (TapeMultiProgram.cfg cubeStart (storeTapes (TapePowerSearch.candidateStore R σ 0))) (TapeMultiProgram.cfg cubeDone (storeTapes (TapePowerSearch.candidateStore R σ (hashDimension d)))) (cubeCost d)
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeParameterSearch.cube_done (R : TapePowerSearch.Registers) (h : TapeHeads) :
            cubeProgram R cubeDone h = none
            source
            @[reducible, inline]
            abbrev Complexity.DepthThreeLowerBound.TapeParameterSearch.DecreaseState :
            Type

            Control states for the decrease stage of the parameter search routine.

            Equations
            Instances For
              source
              def Complexity.DepthThreeLowerBound.TapeParameterSearch.decreaseProgram (R : TapePowerSearch.Registers) :
              TapeMultiProgram DecreaseState

              Transition function for the decrease stage of the parameter search routine.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Complexity.DepthThreeLowerBound.TapeParameterSearch.decreaseStart :
                DecreaseState

                Initial control state of the decrease stage of the parameter search routine.

                Equations
                Instances For
                  source
                  def Complexity.DepthThreeLowerBound.TapeParameterSearch.decreaseDone :
                  DecreaseState

                  Terminal control state of the decrease stage of the parameter search routine.

                  Equations
                  Instances For
                    source
                    theorem Complexity.DepthThreeLowerBound.TapeParameterSearch.runs_decrease (R : TapePowerSearch.Registers) (σ : TapeStore) (c : ℕ) :
                    RunsIn (decreaseProgram R).step (TapeMultiProgram.cfg decreaseStart (storeTapes (TapePowerSearch.candidateStore R σ (c + 2)))) (TapeMultiProgram.cfg decreaseDone (storeTapes (TapePowerSearch.candidateStore R σ c))) 9
                    source
                    @[reducible, inline]
                    abbrev Complexity.DepthThreeLowerBound.TapeParameterSearch.CleanupState :
                    Type

                    Control states for the cleanup stage of the parameter search routine.

                    Equations
                    Instances For
                      source
                      def Complexity.DepthThreeLowerBound.TapeParameterSearch.cleanupProgram (R : TapePowerSearch.Registers) :
                      TapeMultiProgram CleanupState

                      Transition function for the cleanup stage of the parameter search routine.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def Complexity.DepthThreeLowerBound.TapeParameterSearch.cleanupStart :
                        CleanupState

                        Initial control state of the cleanup stage of the parameter search routine.

                        Equations
                        Instances For
                          source
                          def Complexity.DepthThreeLowerBound.TapeParameterSearch.cleanupDone :
                          CleanupState

                          Terminal control state of the cleanup stage of the parameter search routine.

                          Equations
                          Instances For
                            source
                            theorem Complexity.DepthThreeLowerBound.TapeParameterSearch.runs_cleanup (R : TapePowerSearch.Registers) (σ : TapeStore) (c : ℕ) (ho : σ (R 0) = []) (hd : σ (R 3) = []) :
                            RunsIn (cleanupProgram R).step (TapeMultiProgram.cfg cleanupStart (storeTapes (TapePowerCompare.outputStore 6 (R 0) (R 3) (TapePowerSearch.candidateStore R σ (c + 2)) (c + 2)))) (TapeMultiProgram.cfg cleanupDone (storeTapes (TapePowerSearch.candidateStore R σ c))) (2 * (c + 2) ^ 6 + 5 + 1 + 9)
                            source
                            @[reducible, inline]
                            abbrev Complexity.DepthThreeLowerBound.TapeParameterSearch.SixthState :
                            Type

                            Control states for the sixth stage of the parameter search routine.

                            Equations
                            Instances For
                              source
                              def Complexity.DepthThreeLowerBound.TapeParameterSearch.sixthProgram (R : TapePowerSearch.Registers) :
                              TapeMultiProgram SixthState

                              Transition function for the sixth stage of the parameter search routine.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                def Complexity.DepthThreeLowerBound.TapeParameterSearch.sixthStart :
                                SixthState

                                Initial control state of the sixth stage of the parameter search routine.

                                Equations
                                Instances For
                                  source
                                  def Complexity.DepthThreeLowerBound.TapeParameterSearch.sixthDone :
                                  SixthState

                                  Terminal control state of the sixth stage of the parameter search routine.

                                  Equations
                                  Instances For
                                    source
                                    def Complexity.DepthThreeLowerBound.TapeParameterSearch.sixthCost (d : ℕ) :
                                    ℕ

                                    Transition budget for the parameter search routine at its sixth stage.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      source
                                      theorem Complexity.DepthThreeLowerBound.TapeParameterSearch.runs_sixth (R : TapePowerSearch.Registers) (σ : TapeStore) (d : ℕ) (ho : σ (R 0) = []) (hs : σ (R 2) = []) (hd : σ (R 3) = []) (ht : σ (R 4) = List.replicate d true) :
                                      RunsIn (sixthProgram R).step (TapeMultiProgram.cfg sixthStart (storeTapes (TapePowerSearch.candidateStore R σ 0))) (TapeMultiProgram.cfg sixthDone (storeTapes (TapePowerSearch.candidateStore R σ (independenceOrder d)))) (sixthCost d)
                                      source
                                      @[simp]
                                      theorem Complexity.DepthThreeLowerBound.TapeParameterSearch.sixth_done (R : TapePowerSearch.Registers) (h : TapeHeads) :
                                      sixthProgram R sixthDone h = none