Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeHornerTake

Unrestricted depth-three lower bound: tape horner take #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/TapeHornerTake.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

source
def Complexity.DepthThreeLowerBound.TapeHornerTake.registers :
TapeInputBlockLoop.Registers

The register allocation used by this block-transfer routine.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[reducible, inline]
    abbrev Complexity.DepthThreeLowerBound.TapeHornerTake.PrepareState :
    Type

    Control states for the prepare stage of the horner take routine.

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

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

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

        Control states of the horner take routine.

        Equations
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeHornerTake.prepare :
          TapeMultiProgram PrepareState

          Clear the accumulator and copy the modulus degree into the block counter.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Complexity.DepthThreeLowerBound.TapeHornerTake.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.TapeHornerTake.program :
              TapeMultiProgram State

              Transition function of the horner take routine.

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

                Initial control state of the horner take routine.

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

                  Terminal control state of the horner take routine.

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem Complexity.DepthThreeLowerBound.TapeHornerTake.program_done (h : TapeHeads) :
                    program done h = none
                    source
                    theorem Complexity.DepthThreeLowerBound.TapeHornerTake.runs_take (σ : TapeStore) (a c : List Bool) (r : ℕ) (hacc : σ TapeRegister.accumBits = a) (hprod : σ TapeRegister.productBits = c) (hlenA : a.length = r) (hlenC : c.length = 2 * r) (hdegree : σ TapeRegister.ringDegree = List.replicate r true) (hcount : σ TapeRegister.loop1 = []) (hindex : σ TapeRegister.indexA = []) (hscratch : σ TapeRegister.scratchA = []) :
                    RunsIn program.step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (Function.update (Function.update σ TapeRegister.accumBits (List.take r c)) TapeRegister.productBits []))) (r * (r + 27) + 8 * r + 29)