Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeHornerLoop

Unrestricted depth-three lower bound: tape horner loop #

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

Control states of the horner loop routine.

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

    Transition function of the horner loop routine.

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

      Initial control state of the horner loop routine.

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

        Terminal control state of the horner loop routine.

        Equations
        Instances For
          source
          @[simp]
          theorem Complexity.DepthThreeLowerBound.TapeHornerLoop.program_done (h : TapeHeads) :
          program done h = none
          source
          def Complexity.DepthThreeLowerBound.TapeHornerLoop.frame (σ : TapeStore) (remaining offset : ℕ) (a : List Bool) :
          TapeStore

          Tape-store invariant recording the loop counters and current output.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeHornerLoop.frame_count (σ : TapeStore) (k j : ℕ) (a : List Bool) :
            frame σ k j a TapeRegister.loop2 = List.replicate k true
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeHornerLoop.frame_cursor (σ : TapeStore) (k j : ℕ) (a : List Bool) :
            frame σ k j a TapeRegister.loop3 = List.replicate j true
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeHornerLoop.frame_accum (σ : TapeStore) (k j : ℕ) (a : List Bool) :
            frame σ k j a TapeRegister.accumBits = a
            source
            theorem Complexity.DepthThreeLowerBound.TapeHornerLoop.frame_workspace (σ : TapeStore) (k j r : ℕ) (a : List Bool) (hW : TapeHornerMultiply.Workspace σ r) :
            TapeHornerMultiply.Workspace (frame σ k j a) r
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeHornerLoop.update_frame_count (σ : TapeStore) (k k' j : ℕ) (a : List Bool) :
            Function.update (frame σ k j a) TapeRegister.loop2 (List.replicate k' true) = frame σ k' j a
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeHornerLoop.update_frame_cursor (σ : TapeStore) (k j j' : ℕ) (a : List Bool) :
            Function.update (frame σ k j a) TapeRegister.loop3 (List.replicate j' true) = frame σ k j' a
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeHornerLoop.update_frame_accum (σ : TapeStore) (k j : ℕ) (a b : List Bool) :
            Function.update (frame σ k j a) TapeRegister.accumBits b = frame σ k j b
            source
            theorem Complexity.DepthThreeLowerBound.TapeHornerLoop.body_cost_mono (r m n : ℕ) (hmn : m ≤ n) :
            TapeHornerBody.cost r m ≤ TapeHornerBody.cost r n
            source
            theorem Complexity.DepthThreeLowerBound.TapeHornerLoop.runs_loop (σ : TapeStore) (p h : List Bool) (bs : List (List Bool)) (suffix a : List Bool) (r N : ℕ) (hW : TapeHornerMultiply.Workspace σ r) (hP : σ TapeRegister.polyBits = p) (hH : σ TapeRegister.hashBits = h) (hp : p.length = r) (hh : h.length = r) (ha : a.length = r) (hblocks : ∀ b ∈ bs, b.length = r) (hsource : σ TapeRegister.coeffBits = bs.flatten ++ suffix) (hN : bs.flatten.length ≤ N) (hcount : σ TapeRegister.loop4 = []) (hbuffer : σ TapeRegister.scratchB = []) :
            RunsIn program.step (TapeMultiProgram.cfg start (storeTapes (frame σ bs.length bs.flatten.length a))) (TapeMultiProgram.cfg done (storeTapes (frame σ 0 0 (hornerFrom r p h bs a)))) (bs.length * (TapeHornerBody.cost r N + 6) + 3)