Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeHorner

Unrestricted depth-three lower bound: tape horner #

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

Control states of the horner routine.

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

    Transition function of the horner routine.

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

      Initial control state of the horner routine.

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

        Terminal control state of the horner routine.

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

          Transition budget for the horner routine.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeHorner.program_done (h : TapeHeads) :
            program done h = none
            source
            theorem Complexity.DepthThreeLowerBound.TapeHorner.cost_le (r t : ℕ) :
            cost r t ≤ 1000 * (r + t + 1) ^ 4
            source
            theorem Complexity.DepthThreeLowerBound.TapeHorner.runs_horner (σ : TapeStore) (p h : List Bool) (blocks : List (List Bool)) (r : ℕ) (hW : TapeHornerMultiply.Workspace σ r) (hC : TapeHornerPrepare.Clean σ) (hP : σ TapeRegister.polyBits = p) (hH : σ TapeRegister.hashBits = h) (hB : σ TapeRegister.coeffBits = blocks.flatten) (hT : σ TapeRegister.coeffCount = List.replicate blocks.length true) (hp : p.length = r) (hh : h.length = r) (hblocks : ∀ b ∈ blocks, b.length = r) :
            RunsIn program.step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (Function.update σ TapeRegister.accumBits (hornerBitLists r p h blocks)))) (cost r blocks.length)