Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeReadPush

Unrestricted depth-three lower bound: tape read push #

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

Control states of the read push routine.

Equations
Instances For
    source
    def Complexity.DepthThreeLowerBound.TapeReadPush.program (index source destination : TapeRegister) :
    TapeMultiProgram State

    Transition function of the read push routine.

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

      Initial control state of the read push routine.

      Equations
      Instances For
        source
        def Complexity.DepthThreeLowerBound.TapeReadPush.done (b : Bool) :
        State

        Terminal control state of the read push routine.

        Equations
        Instances For
          source
          theorem Complexity.DepthThreeLowerBound.TapeReadPush.runs_read_push {index source : TapeRegister} (hne : index ≠ source) (destination : TapeRegister) (T : TapeTapes) («prefix» suffix acc : List Bool) (b : Bool) (hi : T index = TapeUnary.counterTape «prefix».length) (hs : T source = wordTape («prefix» ++ b :: suffix)) (hd : T destination = wordTape acc) :
          RunsIn (program index source destination).step (TapeMultiProgram.cfg start T) (TapeMultiProgram.cfg (done b) (Function.update T destination (wordTape (b :: acc)))) (2 * «prefix».length + 7)
          source
          @[simp]
          theorem Complexity.DepthThreeLowerBound.TapeReadPush.program_done (index source destination : TapeRegister) (b : Bool) (h : TapeHeads) :
          program index source destination (done b) h = none
          source
          theorem Complexity.DepthThreeLowerBound.TapeReadPush.runs_store {index source : TapeRegister} (hne : index ≠ source) (destination : TapeRegister) (σ : TapeStore) («prefix» suffix : List Bool) (b : Bool) (hi : σ index = List.replicate «prefix».length true) (hs : σ source = «prefix» ++ b :: suffix) :
          RunsIn (program index source destination).step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg (done b) (storeTapes (Function.update σ destination (b :: σ destination)))) (2 * «prefix».length + 7)