Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeHashOuter

Unrestricted depth-three lower bound: tape hash outer #

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

Control states of the hash outer routine.

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

    Transition function of the hash outer routine.

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

      Initial control state of the hash outer routine.

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

        Terminal control state of the hash outer routine.

        Equations
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeHashOuter.progressStore (σ : TapeStore) (i : ℕ) :
          TapeStore

          Tape-store contents at the progress stage of the hash outer routine.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem Complexity.DepthThreeLowerBound.TapeHashOuter.progress_zero (σ : TapeStore) (hc : σ TapeRegister.indexC = []) :
            progressStore σ 0 = σ
            source
            theorem Complexity.DepthThreeLowerBound.TapeHashOuter.progress_step (σ : TapeStore) (i d : ℕ) (hd : (σ TapeRegister.dataBits).length = d) :
            TapeHashRow.resultStore (progressStore σ i) i d = Function.update (progressStore σ (i + 1)) TapeRegister.indexC (List.replicate i true)
            source
            theorem Complexity.DepthThreeLowerBound.TapeHashOuter.row_cost_le (i d r : ℕ) (hi : i ≤ r) :
            d * (4 * i + 8 * d + 29) + 4 * i + 8 * d + 25 ≤ 64 * (d + r + 1) ^ 2
            source
            theorem Complexity.DepthThreeLowerBound.TapeHashOuter.runs_outer (σ : TapeStore) (d r : ℕ) (hd : σ TapeRegister.dataLength = List.replicate d true) (hr : σ TapeRegister.ringDegree = List.replicate r true) (ha : σ TapeRegister.indexA = []) (hb : σ TapeRegister.indexB = []) (hc : σ TapeRegister.indexC = []) (hkey : (σ TapeRegister.keyBits).length = d + r - 1) (hdata : (σ TapeRegister.dataBits).length = d) (hout : (σ TapeRegister.hashBits).length = r) :
            RunsIn program.step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (progressStore σ r))) (r * (64 * (d + r + 1) ^ 2 + 4 * r + 12) + (4 * r + 8))
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeHashOuter.program_done (h : TapeHeads) :
            program done h = none