Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Extractor.Strong.Block.Recursion.NearHalving.Parameters.Explicit.Defs

Rounded parameters for a near-halving ordinary extractor #

At target output length b, use source width 8*b, subtract three ceiling logarithms and fifteen from its binary logarithm to choose the depth, and round the reserve upward to obtain at least b output bits. The size guard makes the depth subtraction exact. These are total natural-number definitions; their useful finite inequalities and eventual validity are separate results.

source
def Algebraic.Cutwidth.Extractor.gammaBlockLog (b : ℕ) :
ℕ

Ceiling logarithm controlling the selected seed budget.

Equations
Instances For
    source
    def Algebraic.Cutwidth.Extractor.gammaBlockDepth (b : ℕ) :
    ℕ

    Leave a cubic logarithmic output quantum below the target width.

    Equations
    Instances For
      source
      def Algebraic.Cutwidth.Extractor.gammaBlockErrorExponent (b : ℕ) :
      ℕ

      The local error exponent paying for final error one quarter.

      Equations
      Instances For
        source
        def Algebraic.Cutwidth.Extractor.gammaBlockOutputQuantum (b : ℕ) :
        ℕ

        Number of output bits contributed by one unit of the leaf reserve.

        Equations
        Instances For
          source
          def Algebraic.Cutwidth.Extractor.gammaBlockReserve (b : ℕ) :
          ℕ

          Round the leaf reserve upward so the complete output covers b bits.

          Equations
          Instances For
            source
            def Algebraic.Cutwidth.Extractor.gammaBlockLeafLength (b : ℕ) :
            ℕ

            The common final output length of every leaf extractor.

            Equations
            Instances For
              source
              def Algebraic.Cutwidth.Extractor.gammaBlockInputEntropy (b : ℕ) :
              ℕ

              The actual input entropy threshold in bits for the rounded schedule.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Algebraic.Cutwidth.Extractor.GammaBlockSizeGuard (b : ℕ) :
                Prop

                The logarithmic depth subtraction does not truncate at zero.

                Equations
                Instances For