Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeForLoop

Unrestricted depth-three lower bound: tape for loop #

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

Control states for the body stage of the for loop routine.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Complexity.DepthThreeLowerBound.TapeForLoop.State (Q : Type uDepth2) :
    Type uDepth2

    Control states of the for loop routine.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.DepthThreeLowerBound.TapeForLoop.bodyProgram {Q : Type uDepth3} (r : TapeRegister) (P : TapeMultiProgram Q) :
      TapeMultiProgram (BodyState Q)

      Transition function for the body stage of the for loop routine.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Complexity.DepthThreeLowerBound.TapeForLoop.bodyStart {Q : Type uDepth4} (q : Q) :
        BodyState Q

        Initial control state of the body stage of the for loop routine.

        Equations
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeForLoop.bodyDone {Q : Type uDepth5} :
          BodyState Q

          Terminal control state of the body stage of the for loop routine.

          Equations
          Instances For
            source
            def Complexity.DepthThreeLowerBound.TapeForLoop.again :
            TapeUnaryCompare.State → Bool

            Continue the counted loop exactly when its index is less than its bound.

            Equations
            Instances For
              source
              def Complexity.DepthThreeLowerBound.TapeForLoop.program {Q : Type uDepth6} (r s : TapeRegister) (P : TapeMultiProgram Q) (qStart : Q) :
              TapeMultiProgram (State Q)

              Transition function of the for loop routine.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Complexity.DepthThreeLowerBound.TapeForLoop.start {Q : Type uDepth7} :
                State Q

                Initial control state of the for loop routine.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Complexity.DepthThreeLowerBound.TapeForLoop.done {Q : Type uDepth8} :
                  State Q

                  Terminal control state of the for loop routine.

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem Complexity.DepthThreeLowerBound.TapeForLoop.body_done {Q : Type uDepth9} (r : TapeRegister) (P : TapeMultiProgram Q) (h : TapeHeads) :
                    bodyProgram r P bodyDone h = none
                    source
                    @[simp]
                    theorem Complexity.DepthThreeLowerBound.TapeForLoop.program_done {Q : Type uDepth10} (r s : TapeRegister) (P : TapeMultiProgram Q) (qStart : Q) (h : TapeHeads) :
                    program r s P qStart done h = none
                    source
                    theorem Complexity.DepthThreeLowerBound.TapeForLoop.runs_body {Q : Type uDepth11} (r : TapeRegister) (P : TapeMultiProgram Q) (qStart qDone : Q) (T U : TapeTapes) (j B : ℕ) (hU : U r = TapeUnary.counterTape (j + 1)) (hbody : RunsIn P.step (TapeMultiProgram.cfg qStart T) (TapeMultiProgram.cfg qDone (Function.update U r (TapeUnary.counterTape j))) B) (hhalt : P qDone (TapeMultiProgram.heads (Function.update U r (TapeUnary.counterTape j))) = none) :
                    RunsIn (bodyProgram r P).step (TapeMultiProgram.cfg (bodyStart qStart) T) (TapeMultiProgram.cfg bodyDone U) (B + 3)
                    source
                    theorem Complexity.DepthThreeLowerBound.TapeForLoop.runs_iteration {Q : Type uDepth12} {r s : TapeRegister} (hrs : r ≠ s) (P : TapeMultiProgram Q) (qStart qDone : Q) (T U : TapeTapes) (j n B : ℕ) (hj : j < n) (hR : T r = TapeUnary.counterTape j) (hS : T s = TapeUnary.counterTape n) (hU : U r = TapeUnary.counterTape (j + 1)) (hbody : RunsIn P.step (TapeMultiProgram.cfg qStart T) (TapeMultiProgram.cfg qDone (Function.update U r (TapeUnary.counterTape j))) B) (hhalt : P qDone (TapeMultiProgram.heads (Function.update U r (TapeUnary.counterTape j))) = none) :
                    RunsIn (program r s P qStart).step (TapeMultiProgram.cfg start T) (TapeMultiProgram.cfg start U) (B + 4 * j + 12)
                    source
                    theorem Complexity.DepthThreeLowerBound.TapeForLoop.runs_exit {Q : Type uDepth13} {r s : TapeRegister} (hrs : r ≠ s) (P : TapeMultiProgram Q) (qStart : Q) (T : TapeTapes) (n : ℕ) (hR : T r = TapeUnary.counterTape n) (hS : T s = TapeUnary.counterTape n) :
                    RunsIn (program r s P qStart).step (TapeMultiProgram.cfg start T) (TapeMultiProgram.cfg done T) (4 * n + 8)
                    source
                    theorem Complexity.DepthThreeLowerBound.TapeForLoop.runs {Q : Type uDepth14} {r s : TapeRegister} (hrs : r ≠ s) (P : TapeMultiProgram Q) (qStart qDone : Q) (σ : ℕ → TapeTapes) (n B : ℕ) (hindex : ∀ j ≤ n, σ j r = TapeUnary.counterTape j) (hbound : ∀ j ≤ n, σ j s = TapeUnary.counterTape n) (hbody : ∀ j < n, RunsIn P.step (TapeMultiProgram.cfg qStart (σ j)) (TapeMultiProgram.cfg qDone (Function.update (σ (j + 1)) r (TapeUnary.counterTape j))) B) (hhalt : ∀ (h : TapeHeads), P qDone h = none) (i : ℕ) (hi : i ≤ n) :
                    RunsIn (program r s P qStart).step (TapeMultiProgram.cfg start (σ i)) (TapeMultiProgram.cfg done (σ n)) ((n - i) * (B + 4 * n + 12) + (4 * n + 8))
                    source
                    theorem Complexity.DepthThreeLowerBound.TapeForLoop.runs_zero {Q : Type uDepth15} {r s : TapeRegister} (hrs : r ≠ s) (P : TapeMultiProgram Q) (qStart qDone : Q) (σ : ℕ → TapeTapes) (n B : ℕ) (hindex : ∀ j ≤ n, σ j r = TapeUnary.counterTape j) (hbound : ∀ j ≤ n, σ j s = TapeUnary.counterTape n) (hbody : ∀ j < n, RunsIn P.step (TapeMultiProgram.cfg qStart (σ j)) (TapeMultiProgram.cfg qDone (Function.update (σ (j + 1)) r (TapeUnary.counterTape j))) B) (hhalt : ∀ (h : TapeHeads), P qDone h = none) :
                    RunsIn (program r s P qStart).step (TapeMultiProgram.cfg start (σ 0)) (TapeMultiProgram.cfg done (σ n)) (n * (B + 4 * n + 12) + (4 * n + 8))