Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Extractor.Condenser.Parameters.Sparse.Defs

Sparse binary field sizes and condenser coordinates #

The field bit length is rounded up to 2 * 3^s. Choosing the powering bit length after this rounding preserves the target output rate 1 + 1/u. These are total natural-number parameters; their useful bounds assume positive budgets. No field representation or running time is defined here.

source
def Algebraic.Cutwidth.Extractor.sparseFieldExponent (u T : ℕ) :
ℕ

The exponent selecting the first sparse field bit length above (u+1)*T.

Equations
Instances For
    source
    def Algebraic.Cutwidth.Extractor.sparseFieldBits (u T : ℕ) :
    ℕ

    A binary field bit length on the grid 2 * 3^s.

    Equations
    Instances For
      source
      def Algebraic.Cutwidth.Extractor.sparsePowerBits (u T : ℕ) :
      ℕ

      The powering exponent leaves T bits of slack below the field bit length.

      Equations
      Instances For
        source
        def Algebraic.Cutwidth.Extractor.condenserCoordinates (k r : ℕ) :
        ℕ

        The number of coordinates needed to carry k entropy bits at r bits each. At r = 0, natural-number division makes this total definition equal to zero.

        Equations
        Instances For