Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeHornerPrepare

Unrestricted depth-three lower bound: tape horner prepare #

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

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

source
structure Complexity.DepthThreeLowerBound.TapeHornerPrepare.Clean (σ : TapeStore) :
Prop

Register allocation for the horner prepare routine.

Instances For
    source
    @[reducible, inline]
    abbrev Complexity.DepthThreeLowerBound.TapeHornerPrepare.ZeroState :
    Type

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

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

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

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

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

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

          Control states of the horner prepare routine.

          Equations
          Instances For
            source
            def Complexity.DepthThreeLowerBound.TapeHornerPrepare.zeroProgram :
            TapeMultiProgram ZeroState

            Transition function for the zero stage of the horner prepare routine.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Complexity.DepthThreeLowerBound.TapeHornerPrepare.countProgram :
              TapeMultiProgram CountState

              Transition function for the count stage of the horner prepare routine.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Complexity.DepthThreeLowerBound.TapeHornerPrepare.cursorProgram :
                TapeMultiProgram CursorState

                Transition function for the cursor stage of the horner prepare routine.

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

                  Transition function of the horner prepare routine.

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

                    Initial control state of the horner prepare routine.

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

                      Terminal control state of the horner prepare routine.

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

                        Transition budget for the horner prepare routine.

                        Equations
                        Instances For
                          source
                          @[simp]
                          theorem Complexity.DepthThreeLowerBound.TapeHornerPrepare.program_done (h : TapeHeads) :
                          program done h = none
                          source
                          theorem Complexity.DepthThreeLowerBound.TapeHornerPrepare.runs_zero (σ : TapeStore) (r : ℕ) (hr : σ TapeRegister.ringDegree = List.replicate r true) (hs : σ TapeRegister.scratchA = []) (ha : σ TapeRegister.accumBits = []) :
                          RunsIn zeroProgram.step (TapeMultiProgram.cfg (Sum.inl TapeCopy.State.start) (storeTapes σ)) (TapeMultiProgram.cfg (Sum.inr TapeFill.fillDone) (storeTapes (Function.update σ TapeRegister.accumBits (List.replicate r false)))) (10 * r + 8)
                          source
                          theorem Complexity.DepthThreeLowerBound.TapeHornerPrepare.runs_prepare (σ : TapeStore) (r t : ℕ) (hW : TapeHornerMultiply.Workspace σ r) (hC : Clean σ) (ht : σ TapeRegister.coeffCount = List.replicate t true) :
                          RunsIn program.step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (TapeHornerLoop.frame σ t (t * r) (List.replicate r false)))) (cost r t)