Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeRemainderSetup

Unrestricted depth-three lower bound: tape remainder setup #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/TapeRemainderSetup.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.TapeRemainderSetup.preparedStore (σ : TapeStore) (r s : ℕ) :
TapeStore

Tape-store contents at the prepared stage of the remainder setup routine.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Complexity.DepthThreeLowerBound.TapeRemainderSetup.clearIndices (σ : TapeStore) :
    TapeStore

    Clear the three index registers in the tape store.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem Complexity.DepthThreeLowerBound.TapeRemainderSetup.preparedStore_indexB (σ : TapeStore) (r s : ℕ) :
      preparedStore σ r s TapeRegister.indexB = List.replicate (s + r) true
      source
      @[simp]
      theorem Complexity.DepthThreeLowerBound.TapeRemainderSetup.preparedStore_indexC (σ : TapeStore) (r s : ℕ) :
      preparedStore σ r s TapeRegister.indexC = List.replicate s true
      source
      @[simp]
      theorem Complexity.DepthThreeLowerBound.TapeRemainderSetup.preparedStore_loop1 (σ : TapeStore) (r s : ℕ) :
      preparedStore σ r s TapeRegister.loop1 = List.replicate r true
      source
      theorem Complexity.DepthThreeLowerBound.TapeRemainderSetup.preparedStore_other (σ : TapeStore) (r s : ℕ) (q : TapeRegister) (hB : q ≠ TapeRegister.indexB) (hC : q ≠ TapeRegister.indexC) (hL : q ≠ TapeRegister.loop1) :
      preparedStore σ r s q = σ q
      source
      @[simp]
      theorem Complexity.DepthThreeLowerBound.TapeRemainderSetup.clearIndices_indexA (σ : TapeStore) :
      clearIndices σ TapeRegister.indexA = []
      source
      @[simp]
      theorem Complexity.DepthThreeLowerBound.TapeRemainderSetup.clearIndices_indexB (σ : TapeStore) :
      clearIndices σ TapeRegister.indexB = []
      source
      @[simp]
      theorem Complexity.DepthThreeLowerBound.TapeRemainderSetup.clearIndices_indexC (σ : TapeStore) :
      clearIndices σ TapeRegister.indexC = []
      source
      theorem Complexity.DepthThreeLowerBound.TapeRemainderSetup.clearIndices_other (σ : TapeStore) (q : TapeRegister) (hA : q ≠ TapeRegister.indexA) (hB : q ≠ TapeRegister.indexB) (hC : q ≠ TapeRegister.indexC) :
      clearIndices σ q = σ q
      source
      @[reducible, inline]
      abbrev Complexity.DepthThreeLowerBound.TapeRemainderSetup.SetupState :
      Type

      Control states for the setup stage of the remainder setup routine.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Complexity.DepthThreeLowerBound.TapeRemainderSetup.setupProgram :
        TapeMultiProgram SetupState

        Transition function for the setup stage of the remainder setup routine.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeRemainderSetup.setupStart :
          SetupState

          Initial control state of the setup stage of the remainder setup routine.

          Equations
          Instances For
            source
            def Complexity.DepthThreeLowerBound.TapeRemainderSetup.setupDone :
            SetupState

            Terminal control state of the setup stage of the remainder setup routine.

            Equations
            Instances For
              source
              @[simp]
              theorem Complexity.DepthThreeLowerBound.TapeRemainderSetup.setupProgram_done (h : TapeHeads) :
              setupProgram setupDone h = none
              source
              theorem Complexity.DepthThreeLowerBound.TapeRemainderSetup.runs_setup (σ : TapeStore) (r s : ℕ) (hLoop0 : σ TapeRegister.loop0 = List.replicate s true) (hDegree : σ TapeRegister.ringDegree = List.replicate r true) (hLoop1 : σ TapeRegister.loop1 = []) (_hA : σ TapeRegister.indexA = []) (hB : σ TapeRegister.indexB = []) (hC : σ TapeRegister.indexC = []) (hScratch : σ TapeRegister.scratchA = []) :
              RunsIn setupProgram.step (TapeMultiProgram.cfg setupStart (storeTapes σ)) (TapeMultiProgram.cfg setupDone (storeTapes (preparedStore σ r s))) (4 * s + 12 * r + 23)
              source
              @[reducible, inline]
              abbrev Complexity.DepthThreeLowerBound.TapeRemainderSetup.CleanupState :
              Type

              Control states for the cleanup stage of the remainder setup routine.

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

                Transition function for the cleanup stage of the remainder setup routine.

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

                  Initial control state of the cleanup stage of the remainder setup routine.

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

                    Terminal control state of the cleanup stage of the remainder setup routine.

                    Equations
                    Instances For
                      source
                      @[simp]
                      theorem Complexity.DepthThreeLowerBound.TapeRemainderSetup.cleanupProgram_done (h : TapeHeads) :
                      cleanupProgram cleanupDone h = none
                      source
                      theorem Complexity.DepthThreeLowerBound.TapeRemainderSetup.runs_cleanup (σ : TapeStore) (r s : ℕ) (hA : σ TapeRegister.indexA = List.replicate r true) (hB : σ TapeRegister.indexB = List.replicate (s + r) true) (hC : σ TapeRegister.indexC = List.replicate (s + r) true) :
                      RunsIn cleanupProgram.step (TapeMultiProgram.cfg cleanupStart (storeTapes σ)) (TapeMultiProgram.cfg cleanupDone (storeTapes (clearIndices σ))) (4 * s + 6 * r + 17)