Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeHornerBody

Unrestricted depth-three lower bound: tape horner body #

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

Control states for the product stage of the horner body routine.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Complexity.DepthThreeLowerBound.TapeHornerBody.WorkState :
    Type

    Control states for the work stage of the horner body routine.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Complexity.DepthThreeLowerBound.TapeHornerBody.State :
      Type

      Control states of the horner body routine.

      Equations
      Instances For
        source
        def Complexity.DepthThreeLowerBound.TapeHornerBody.product :
        TapeMultiProgram ProductState

        Extract the next coefficient block and multiply the Horner accumulator.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeHornerBody.work :
          TapeMultiProgram WorkState

          Compose the main computational stages of the routine.

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

            Transition function of the horner body routine.

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

              Initial control state of the horner body routine.

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

                Terminal control state of the horner body routine.

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

                  Transition budget for the horner body routine.

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem Complexity.DepthThreeLowerBound.TapeHornerBody.program_done (h : TapeHeads) :
                    program done h = none
                    source
                    theorem Complexity.DepthThreeLowerBound.TapeHornerBody.runs_body (σ : TapeStore) (p h a «prefix» b suffix : List Bool) (r : ℕ) (hW : TapeHornerMultiply.Workspace σ r) (hP : σ TapeRegister.polyBits = p) (hH : σ TapeRegister.hashBits = h) (hA : σ TapeRegister.accumBits = a) (hp : p.length = r) (hh : h.length = r) (ha : a.length = r) (hb : b.length = r) (hsource : σ TapeRegister.coeffBits = «prefix» ++ b ++ suffix) (hcursor : σ TapeRegister.loop3 = List.replicate («prefix».length + r) true) (hcount : σ TapeRegister.loop4 = []) (hbuffer : σ TapeRegister.scratchB = []) :
                    RunsIn program.step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (Function.update (Function.update σ TapeRegister.loop3 (List.replicate «prefix».length true)) TapeRegister.accumBits (hornerStep r p h b a)))) (cost r «prefix».length)