Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeOutput

Unrestricted depth-three lower bound: tape output #

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

Control states of the output routine.

Equations
Instances For
    source
    def Complexity.DepthThreeLowerBound.TapeOutput.haltProgram :
    TapeMultiProgram Bool

    Transition function for the halt stage of the output routine.

    Equations
    Instances For
      source
      def Complexity.DepthThreeLowerBound.TapeOutput.acceptFlag :
      TapeArray.State → Bool

      Read the Boolean verdict from the terminal control state of the output routine.

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

        Transition function of the output routine.

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

          Initial control state of the output routine.

          Equations
          Instances For
            source
            def Complexity.DepthThreeLowerBound.TapeOutput.done (answer : Bool) :
            State

            Terminal control state of the output routine.

            Equations
            Instances For
              source
              @[simp]
              theorem Complexity.DepthThreeLowerBound.TapeOutput.program_done (answer : Bool) (h : TapeHeads) :
              program (done answer) h = none
              source
              theorem Complexity.DepthThreeLowerBound.TapeOutput.runs_output (σ : TapeStore) (b : Bool) (tail : List Bool) (hi : σ TapeRegister.indexA = []) (ha : σ TapeRegister.accumBits = b :: tail) :
              RunsIn program.step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg (done !b) (storeTapes σ)) 5