Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeCancel

Unrestricted depth-three lower bound: tape cancel #

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

Control states for the read stage of the cancel routine.

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

    Control states for the clear stage of the cancel routine.

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

      Control states of the cancel routine.

      Equations
      Instances For
        source
        def Complexity.DepthThreeLowerBound.TapeCancel.readProgram :
        TapeMultiProgram ReadState

        Transition function for the read stage of the cancel routine.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeCancel.clearProgram :
          TapeMultiProgram ClearState

          Transition function for the clear stage of the cancel routine.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Complexity.DepthThreeLowerBound.TapeCancel.haltProgram :
            TapeMultiProgram Unit

            Transition function for the halt stage of the cancel routine.

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

              Transition function of the cancel routine.

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

                Initial control state of the cancel routine.

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

                  Terminal control state of the cancel routine.

                  Equations
                  Instances For
                    source
                    def Complexity.DepthThreeLowerBound.TapeCancel.resultStore (σ : TapeStore) (r s : ℕ) (out : List Bool) :
                    TapeStore

                    Tape-store contents at the result stage of the cancel routine.

                    Equations
                    Instances For
                      source
                      def Complexity.DepthThreeLowerBound.TapeCancel.cost (s r : ℕ) :
                      ℕ

                      Transition budget for the cancel routine.

                      Equations
                      Instances For
                        source
                        theorem Complexity.DepthThreeLowerBound.TapeCancel.set_eq_split (xs : List Bool) (i : ℕ) (hi : i < xs.length) (b : Bool) :
                        xs.set i b = List.take i xs ++ b :: List.drop (i + 1) xs
                        source
                        theorem Complexity.DepthThreeLowerBound.TapeCancel.clear_at (σ : TapeStore) (i : ℕ) (hi : σ TapeRegister.indexC = List.replicate i true) (hib : i < (σ TapeRegister.productBits).length) :
                        RunsIn (TapeArray.code TapeRegister.indexC TapeRegister.productBits fun (x : Bool) => false).step (TapeMultiProgram.cfg TapeArray.State.start (storeTapes σ)) (TapeMultiProgram.cfg (TapeArray.State.done ((σ TapeRegister.productBits).getD i false)) (storeTapes (Function.update σ TapeRegister.productBits ((σ TapeRegister.productBits).set i false)))) (2 * i + 4)
                        source
                        theorem Complexity.DepthThreeLowerBound.TapeCancel.update_output (σ : TapeStore) (r s : ℕ) (out out' : List Bool) :
                        Function.update (resultStore σ r s out) TapeRegister.productBits out' = resultStore σ r s out'
                        source
                        theorem Complexity.DepthThreeLowerBound.TapeCancel.runs_cancel (σ : TapeStore) (p c : List Bool) (s : ℕ) (hP : σ TapeRegister.polyBits = p) (hOut : σ TapeRegister.productBits = c) (hLoop : σ TapeRegister.loop1 = List.replicate p.length true) (hA : σ TapeRegister.indexA = []) (hB : σ TapeRegister.indexB = List.replicate (s + p.length) true) (hC : σ TapeRegister.indexC = List.replicate s true) (hbound : s + p.length < c.length) :
                        RunsIn program.step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (resultStore σ p.length s (cancelByUpdates p c s)))) (cost s p.length)
                        source
                        @[simp]
                        theorem Complexity.DepthThreeLowerBound.TapeCancel.program_done (h : TapeHeads) :
                        program done h = none