Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeProductLength

Unrestricted depth-three lower bound: tape product length #

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

Control states of the product length routine.

Equations
Instances For
    source
    def Complexity.DepthThreeLowerBound.TapeProductLength.program :
    TapeMultiProgram State

    Transition function of the product length routine.

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

      Initial control state of the product length routine.

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

        Terminal control state of the product length routine.

        Equations
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeProductLength.outputStore (σ : TapeStore) (n m : ℕ) :
          TapeStore

          Tape-store contents at the output stage of the product length routine.

          Equations
          Instances For
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeProductLength.outputStore_destination (σ : TapeStore) (n m : ℕ) :
            outputStore σ n m 30 = List.replicate (n * m) true
            source
            theorem Complexity.DepthThreeLowerBound.TapeProductLength.outputStore_other (σ : TapeStore) (n m : ℕ) (r : TapeRegister) (hr : r ≠ 30) :
            outputStore σ n m r = σ r
            source
            def Complexity.DepthThreeLowerBound.TapeProductLength.cost (n m : ℕ) :
            ℕ

            Transition budget for the product length routine.

            Equations
            Instances For
              source
              theorem Complexity.DepthThreeLowerBound.TapeProductLength.runs_product (σ : TapeStore) (n m : ℕ) (h4 : σ 4 = List.replicate n true) (h3 : σ 3 = List.replicate m true) (h5 : σ 5 = []) (h6 : σ 6 = []) (h30 : σ 30 = []) :
              RunsIn program.step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (outputStore σ n m))) (cost n m)
              source
              @[simp]
              theorem Complexity.DepthThreeLowerBound.TapeProductLength.program_done (h : TapeHeads) :
              program done h = none