Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeInitialization

Unrestricted depth-three lower bound: tape initialization #

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

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

source
inductive Complexity.DepthThreeLowerBound.InitState :
Type

Control states for the init stage of the initialization routine.

Instances For
    source
    @[instance_reducible]
    instance Complexity.DepthThreeLowerBound.instDecidableEqInitState :
    DecidableEq InitState
    Equations
    source
    @[instance_reducible]
    instance Complexity.DepthThreeLowerBound.instInhabitedInitState :
    Inhabited InitState
    Equations
    source
    @[instance_reducible]
    instance Complexity.DepthThreeLowerBound.instFintypeInitState :
    Fintype InitState
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def Complexity.DepthThreeLowerBound.initActive (r : TapeRegister) :
    Prop

    The input and input-length registers that move during initialization.

    Equations
    Instances For
      source
      @[instance_reducible]
      instance Complexity.DepthThreeLowerBound.instDecidableInitActive (r : TapeRegister) :
      Decidable (initActive r)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Complexity.DepthThreeLowerBound.initializationCode :
      TapeMultiProgram InitState

      Transition function for the initialization stage of the initialization routine.

      Equations
      Instances For
        source
        def Complexity.DepthThreeLowerBound.rawInputTapes (bits : List Bool) :
        TapeTapes

        The raw encoded input on its designated tape, with all others blank.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Complexity.DepthThreeLowerBound.initializedTapes (bits : List Bool) :
          TapeTapes

          Boundary-marked input, its unary length, and empty workspace tapes.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.initializedTapes_input (bits : List Bool) :
            initializedTapes bits TapeRegister.input = wordTape bits
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.initializedTapes_length (bits : List Bool) :
            initializedTapes bits TapeRegister.length = wordTape (List.replicate bits.length true)
            source
            theorem Complexity.DepthThreeLowerBound.initializedTapes_other (bits : List Bool) (r : TapeRegister) (hi : r ≠ TapeRegister.input) (hl : r ≠ TapeRegister.length) :
            initializedTapes bits r = wordTape []
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.initializedTapes_head (bits : List Bool) (r : TapeRegister) :
            (initializedTapes bits r).head = cleanAtom TapeAtom.home
            source
            def Complexity.DepthThreeLowerBound.initHomeTapes (bits : List Bool) :
            TapeTapes

            The intermediate tapes after writing their left boundary markers.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Complexity.DepthThreeLowerBound.initScanTapes (left right : List Bool) :
              TapeTapes

              The tapes while scanning input bits and accumulating the unary length.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Complexity.DepthThreeLowerBound.initRewindTapes (left right : List Bool) :
                TapeTapes

                The tapes while returning input and length heads to their left markers.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem Complexity.DepthThreeLowerBound.initialization_runs (bits : List Bool) :
                  RunsIn initializationCode.step { q := InitState.start, tapes := rawInputTapes bits } { q := InitState.done, tapes := initializedTapes bits } (2 * bits.length + 6)
                  source
                  @[simp]
                  theorem Complexity.DepthThreeLowerBound.initialization_done (T : TapeTapes) :
                  initializationCode.step { q := InitState.done, tapes := T } = none
                  source
                  def Complexity.DepthThreeLowerBound.initializationMachine :
                  FiniteMultiTapeMachine

                  The bundled finite multitape input-initialization machine.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem Complexity.DepthThreeLowerBound.initializationMachine_init (bits : List Bool) :
                    initializationMachine.init bits = { q := InitState.start, tapes := rawInputTapes bits }
                    source
                    theorem Complexity.DepthThreeLowerBound.initializationMachine_halts (bits : List Bool) :
                    MultiTapeHaltsIn initializationMachine bits true (2 * bits.length + 6)