Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeFill

Unrestricted depth-three lower bound: tape fill #

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

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

source
def Complexity.DepthThreeLowerBound.TapeFill.pushProgram (r : TapeRegister) (b : Bool) :
TapeMultiProgram TapeUnary.IncState

Transition function for the push stage of the fill routine.

Equations
Instances For
    source
    theorem Complexity.DepthThreeLowerBound.TapeFill.runs_push (r : TapeRegister) (b : Bool) (T : TapeTapes) (bits : List Bool) (hT : T r = wordTape bits) :
    RunsIn (pushProgram r b).step (TapeMultiProgram.cfg TapeUnary.IncState.start T) (TapeMultiProgram.cfg TapeUnary.IncState.done (Function.update T r (wordTape (b :: bits)))) 2
    source
    @[reducible, inline]
    abbrev Complexity.DepthThreeLowerBound.TapeFill.FillState :
    Type

    Control states for the fill stage of the fill routine.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.DepthThreeLowerBound.TapeFill.fillProgram (counter destination : TapeRegister) (b : Bool) :
      TapeMultiProgram FillState

      Transition function for the fill stage of the fill routine.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Complexity.DepthThreeLowerBound.TapeFill.fillStart :
        FillState

        Initial control state of the fill stage of the fill routine.

        Equations
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeFill.fillDone :
          FillState

          Terminal control state of the fill stage of the fill routine.

          Equations
          Instances For
            source
            theorem Complexity.DepthThreeLowerBound.TapeFill.runs_fill {counter destination : TapeRegister} (hne : counter ≠ destination) (b : Bool) (T : TapeTapes) (n : ℕ) (bits : List Bool) :
            RunsIn (fillProgram counter destination b).step (TapeMultiProgram.cfg fillStart (TapeCopy.onPair counter destination T (TapeUnary.counterTape n) (wordTape bits))) (TapeMultiProgram.cfg fillDone (TapeCopy.onPair counter destination T (TapeUnary.counterTape 0) (wordTape (List.replicate n b ++ bits)))) (8 * n + 3)
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeFill.fill_done (counter destination : TapeRegister) (b : Bool) (h : TapeHeads) :
            fillProgram counter destination b fillDone h = none