Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Extractor.Strong.Block.Recursion.Scheduled.State.Parameters.Defs

Total runtime parameters for the numerical block schedule #

The source length determines its ceiling binary logarithm. The requested depth is clipped to that logarithm before selecting the local error exponent, leaf reserve, and initial entropy. Initial rate-one compression determines the actual starting width. The encoded initializer uses the standard numerical state codec; every definition is total on natural inputs.

source
def Algebraic.Cutwidth.Extractor.scheduledBlockInputLog (n : ℕ) :
ℕ

The input logarithm used by the total numerical initializer.

Equations
Instances For
    source
    def Algebraic.Cutwidth.Extractor.scheduledBlockDepth (n requested : ℕ) :
    ℕ

    Clip the requested depth to the source-length logarithm.

    Equations
    Instances For
      source
      def Algebraic.Cutwidth.Extractor.scheduledBlockErrorExponent (n requested e : ℕ) :
      ℕ

      Local error exponent paying for the clipped number of levels.

      Equations
      Instances For
        source
        def Algebraic.Cutwidth.Extractor.scheduledBlockLeafReserve (n requested e : ℕ) :
        ℕ

        The finite leaf reserve selected from the input logarithm and local error.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Algebraic.Cutwidth.Extractor.scheduledBlockInitialEntropy (n requested e : ℕ) :
          ℕ

          Initial entropy for the clipped-depth schedule.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Algebraic.Cutwidth.Extractor.scheduledBlockRuntimeInitialWidth (n requested e : ℕ) :
            ℕ

            Actual initial compressed width for the total runtime parameter choice.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Algebraic.Cutwidth.Extractor.scheduledBlockStateInit (n requested e : ℕ) :
              List Bool

              Initialize the encoded numerical state from runtime source length, depth, and error.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For