Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeProductTerm

Unrestricted depth-three lower bound: tape product term #

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

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

source
theorem Complexity.DepthThreeLowerBound.TapeProductTerm.onPair_eq_self {src dst : TapeRegister} {T : TapeTapes} {S D : Turing.Tape TapeSymbol} (hS : T src = S) (hD : T dst = D) :
TapeCopy.onPair src dst T S D = T
source
theorem Complexity.DepthThreeLowerBound.TapeProductTerm.read_at {index array : TapeRegister} (hne : index ≠ array) (T : TapeTapes) («prefix» suffix : List Bool) (b : Bool) (hi : T index = TapeUnary.counterTape «prefix».length) (ha : T array = wordTape («prefix» ++ b :: suffix)) :
RunsIn (TapeArray.code index array id).step (TapeMultiProgram.cfg TapeArray.State.start T) (TapeMultiProgram.cfg (TapeArray.State.done b) T) (2 * «prefix».length + 4)
source
theorem Complexity.DepthThreeLowerBound.TapeProductTerm.modify_at {index array : TapeRegister} (hne : index ≠ array) (f : Bool → Bool) (T : TapeTapes) («prefix» suffix : List Bool) (b : Bool) (hi : T index = TapeUnary.counterTape «prefix».length) (ha : T array = wordTape («prefix» ++ b :: suffix)) :
RunsIn (TapeArray.code index array f).step (TapeMultiProgram.cfg TapeArray.State.start T) (TapeMultiProgram.cfg (TapeArray.State.done b) (Function.update T array (wordTape («prefix» ++ f b :: suffix)))) (2 * «prefix».length + 4)
source
def Complexity.DepthThreeLowerBound.TapeProductTerm.carryCode {F : Type uDepth1} {Q : Type uDepth2} (P : F → TapeMultiProgram Q) :
TapeMultiProgram (F × Q)

Transition function for the carry stage of the product term routine.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Complexity.DepthThreeLowerBound.TapeProductTerm.carry_runs {F : Type uDepth3} {Q : Type uDepth4} (P : F → TapeMultiProgram Q) (flag : F) {q q' : Q} {T U : TapeTapes} {n : ℕ} (h : RunsIn (P flag).step (TapeMultiProgram.cfg q T) (TapeMultiProgram.cfg q' U) n) :
    RunsIn (carryCode P).step (TapeMultiProgram.cfg (flag, q) T) (TapeMultiProgram.cfg (flag, q') U) n
    source
    def Complexity.DepthThreeLowerBound.TapeProductTerm.readFlag :
    TapeArray.State → Bool

    Read the bit returned by the array access routine.

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

      Control states for the read stage of the product term routine.

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

        Control states of the product term routine.

        Equations
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeProductTerm.readProgram (i a j b : TapeRegister) :
          TapeMultiProgram ReadState

          Transition function for the read stage of the product term routine.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Complexity.DepthThreeLowerBound.TapeProductTerm.termFlags :
            ReadState → Bool × Bool

            Read the pair of bits used to compute a convolution term.

            Equations
            Instances For
              source
              def Complexity.DepthThreeLowerBound.TapeProductTerm.updateProgram (k c : TapeRegister) :
              TapeMultiProgram ((Bool × Bool) × TapeArray.State)

              Transition function for the update stage of the product term routine.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Complexity.DepthThreeLowerBound.TapeProductTerm.program (i a j b k c : TapeRegister) :
                TapeMultiProgram State

                Transition function of the product term routine.

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

                  Initial control state of the product term routine.

                  Equations
                  Instances For
                    source
                    def Complexity.DepthThreeLowerBound.TapeProductTerm.done (a b old : Bool) :
                    State

                    Terminal control state of the product term routine.

                    Equations
                    Instances For
                      source
                      theorem Complexity.DepthThreeLowerBound.TapeProductTerm.runs_product_term (i a j b k c : TapeRegister) (hia : i ≠ a) (hjb : j ≠ b) (hkc : k ≠ c) (T : TapeTapes) (pa sa pb sb pc sc : List Bool) (va vb old : Bool) (hi : T i = TapeUnary.counterTape pa.length) (ha : T a = wordTape (pa ++ va :: sa)) (hj : T j = TapeUnary.counterTape pb.length) (hb : T b = wordTape (pb ++ vb :: sb)) (hk : T k = TapeUnary.counterTape pc.length) (hc : T c = wordTape (pc ++ old :: sc)) :
                      RunsIn (program i a j b k c).step (TapeMultiProgram.cfg start T) (TapeMultiProgram.cfg (done va vb old) (Function.update T c (wordTape (pc ++ (old ^^ va && vb) :: sc)))) (2 * (pa.length + pb.length + pc.length) + 14)
                      source
                      @[simp]
                      theorem Complexity.DepthThreeLowerBound.TapeProductTerm.program_done (i a j b k c : TapeRegister) (va vb old : Bool) (h : TapeHeads) :
                      program i a j b k c (done va vb old) h = none