Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeHashClean

Unrestricted depth-three lower bound: tape hash clean #

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

Control states of the hash clean routine.

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

    Transition function of the hash clean routine.

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

      Initial control state of the hash clean routine.

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

        Terminal control state of the hash clean routine.

        Equations
        Instances For
          source
          theorem Complexity.DepthThreeLowerBound.TapeHashClean.cost_le (d r : ℕ) :
          200 * (d + r + 1) ^ 3 + 1 + (2 * r + 5) ≤ 210 * (d + r + 1) ^ 3
          source
          theorem Complexity.DepthThreeLowerBound.TapeHashClean.runs_wordHash (σ : TapeStore) {d r : ℕ} (u : BitWord (d + r - 1)) (x : BitWord d) (hd : σ TapeRegister.dataLength = List.replicate d true) (hr : σ TapeRegister.ringDegree = List.replicate r true) (ha : σ TapeRegister.indexA = []) (hb : σ TapeRegister.indexB = []) (hc : σ TapeRegister.indexC = []) (hs : σ TapeRegister.scratchA = []) (hh : σ TapeRegister.hashBits = []) (hkey : σ TapeRegister.keyBits = List.ofFn u) (hdata : σ TapeRegister.dataBits = List.ofFn x) :
          RunsIn program.step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (Function.update σ TapeRegister.hashBits (List.ofFn (wordHash u x))))) (210 * (d + r + 1) ^ 3)
          source
          @[simp]
          theorem Complexity.DepthThreeLowerBound.TapeHashClean.program_done (h : TapeHeads) :
          program done h = none