Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeCopyAdd

Unrestricted depth-three lower bound: tape copy add #

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

Control states of the copy add routine.

Equations
Instances For
    source
    def Complexity.DepthThreeLowerBound.TapeCopyAdd.program (src scratch dst : TapeRegister) :
    TapeMultiProgram State

    Transition function of the copy add routine.

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

      Initial control state of the copy add routine.

      Equations
      Instances For
        source
        def Complexity.DepthThreeLowerBound.TapeCopyAdd.done :
        State

        Terminal control state of the copy add routine.

        Equations
        Instances For
          source
          @[simp]
          theorem Complexity.DepthThreeLowerBound.TapeCopyAdd.program_done (src scratch dst : TapeRegister) (h : TapeHeads) :
          program src scratch dst done h = none
          source
          theorem Complexity.DepthThreeLowerBound.TapeCopyAdd.runs_add {src scratch dst : TapeRegister} (hsc : src ≠ scratch) (hcd : scratch ≠ dst) (σ : TapeStore) (n m : ℕ) (hn : σ src = List.replicate n true) (hm : σ dst = List.replicate m true) (hc : σ scratch = []) :
          RunsIn (program src scratch dst).step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (Function.update σ dst (List.replicate (m + n) true)))) (10 * n + 8)