Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeHornerExtract

Unrestricted depth-three lower bound: tape horner extract #

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

    Control states of the horner extract routine.

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

      Transition function of the horner extract routine.

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

        Initial control state of the horner extract routine.

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

          Terminal control state of the horner extract routine.

          Equations
          Instances For
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeHornerExtract.program_done (h : TapeHeads) :
            program done h = none
            source
            theorem Complexity.DepthThreeLowerBound.TapeHornerExtract.runs_extract (σ : TapeStore) («prefix» block suffix : List Bool) (r : ℕ) (hsource : σ TapeRegister.coeffBits = «prefix» ++ block ++ suffix) (hcursor : σ TapeRegister.loop3 = List.replicate («prefix».length + r) true) (hdegree : σ TapeRegister.ringDegree = List.replicate r true) (hblock : block.length = r) (hcount : σ TapeRegister.loop4 = []) (hdest : σ 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.scratchB block))) (r * (2 * «prefix».length + r + 19) + 8)