Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeSearchBody

Unrestricted depth-three lower bound: tape search body #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/TapeSearchBody.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

source
def Complexity.DepthThreeLowerBound.TapeSearchBody.amount (two : Bool) :
ℕ

The search increment: one or two according to the supplied flag.

Equations
Instances For
    source
    def Complexity.DepthThreeLowerBound.TapeSearchBody.incrementCost (two : Bool) :
    ℕ

    Transition budget for the search body routine at its increment stage.

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

      Control states for the increment stage of the search body routine.

      Equations
      Instances For
        source
        def Complexity.DepthThreeLowerBound.TapeSearchBody.tailProgram (two : Bool) (candidate : TapeRegister) :
        TapeMultiProgram TapeUnary.IncState

        Transition function for the tail stage of the search body routine.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeSearchBody.incrementProgram (two : Bool) (candidate : TapeRegister) :
          TapeMultiProgram IncrementState

          Transition function for the increment stage of the search body routine.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Complexity.DepthThreeLowerBound.TapeSearchBody.incrementStart :
            IncrementState

            Initial control state of the increment stage of the search body routine.

            Equations
            Instances For
              source
              def Complexity.DepthThreeLowerBound.TapeSearchBody.incrementDone (two : Bool) :
              IncrementState

              Terminal control state of the increment stage of the search body routine.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem Complexity.DepthThreeLowerBound.TapeSearchBody.runs_increment (two : Bool) (r : TapeRegister) (σ : TapeStore) (c : ℕ) (hc : σ r = List.replicate c true) :
                RunsIn (incrementProgram two r).step (TapeMultiProgram.cfg incrementStart (storeTapes σ)) (TapeMultiProgram.cfg (incrementDone two) (storeTapes (Function.update σ r (List.replicate (c + amount two) true)))) (incrementCost two)
                source
                @[simp]
                theorem Complexity.DepthThreeLowerBound.TapeSearchBody.increment_done (two : Bool) (r : TapeRegister) (h : TapeHeads) :
                incrementProgram two r (incrementDone two) h = none
                source
                @[reducible, inline]
                abbrev Complexity.DepthThreeLowerBound.TapeSearchBody.State :
                Type

                Control states of the search body routine.

                Equations
                Instances For
                  source
                  def Complexity.DepthThreeLowerBound.TapeSearchBody.program (k : ℕ) (two : Bool) (outer destination candidate : TapeRegister) :
                  TapeMultiProgram State

                  Transition function of the search body routine.

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

                    Initial control state of the search body routine.

                    Equations
                    Instances For
                      source
                      def Complexity.DepthThreeLowerBound.TapeSearchBody.done (two : Bool) :
                      State

                      Terminal control state of the search body routine.

                      Equations
                      Instances For
                        source
                        def Complexity.DepthThreeLowerBound.TapeSearchBody.cost (k : ℕ) (two : Bool) (c : ℕ) :
                        ℕ

                        Transition budget for the search body routine.

                        Equations
                        Instances For
                          source
                          theorem Complexity.DepthThreeLowerBound.TapeSearchBody.runs_body (k : ℕ) (two : Bool) (outer destination candidate : TapeRegister) (σ : TapeStore) (c : ℕ) (ho : σ outer = []) (hd : σ destination = []) (hc : σ candidate = List.replicate c true) :
                          RunsIn (program k two outer destination candidate).step (TapeMultiProgram.cfg start (storeTapes (TapePowerCompare.outputStore k outer destination σ c))) (TapeMultiProgram.cfg (done two) (storeTapes (Function.update σ candidate (List.replicate (c + amount two) true)))) (cost k two c)
                          source
                          @[simp]
                          theorem Complexity.DepthThreeLowerBound.TapeSearchBody.program_done (k : ℕ) (two : Bool) (outer destination candidate : TapeRegister) (h : TapeHeads) :
                          program k two outer destination candidate (done two) h = none