Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeRemainder

Unrestricted depth-three lower bound: tape remainder #

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

Control states of the remainder routine.

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

    Transition function of the remainder routine.

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

      Initial control state of the remainder routine.

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

        Terminal control state of the remainder routine.

        Equations
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeRemainder.cost (r : ℕ) :
          ℕ

          Transition budget for the remainder routine.

          Equations
          Instances For
            source
            theorem Complexity.DepthThreeLowerBound.TapeRemainder.cost_le (r : ℕ) :
            cost r ≤ 100 * (r + 1) ^ 3
            source
            theorem Complexity.DepthThreeLowerBound.TapeRemainder.input_frame (σ : TapeStore) (c : List Bool) (r : ℕ) (hOut : σ TapeRegister.productBits = c) :
            Function.update σ TapeRegister.loop0 (List.replicate r true) = TapeRemainderOuter.frame σ r c
            source
            theorem Complexity.DepthThreeLowerBound.TapeRemainder.output_frame (σ : TapeStore) (out : List Bool) (hLoop0 : σ TapeRegister.loop0 = []) :
            TapeRemainderOuter.frame σ 0 out = Function.update σ TapeRegister.productBits out
            source
            theorem Complexity.DepthThreeLowerBound.TapeRemainder.runs_remainder (σ : TapeStore) (p c : List Bool) (hP : σ TapeRegister.polyBits = p) (hOut : σ TapeRegister.productBits = c) (hDegree : σ TapeRegister.ringDegree = List.replicate p.length true) (hWidth : c.length = 2 * p.length) (hLoop0 : σ TapeRegister.loop0 = []) (hLoop1 : σ TapeRegister.loop1 = []) (hA : σ TapeRegister.indexA = []) (hB : σ TapeRegister.indexB = []) (hC : σ TapeRegister.indexC = []) (hScratch : σ TapeRegister.scratchA = []) :
            RunsIn program.step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (Function.update σ TapeRegister.productBits (reduceByUpdates p p.length c)))) (cost p.length)
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeRemainder.program_done (h : TapeHeads) :
            program done h = none