Documentation

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

A constant-rate numerical schedule for block recursion #

The entropy budget decreases by a factor of four at each executed level. Every internal condenser uses rate parameter three. Its actual output half-width is the next block width, including all sparse-field rounding. The initial width is supplied separately so the initial compression can use its own rate and input length.

These total numerical definitions do not by themselves assert the entropy inequalities, seed bound, or polynomial-time complexity of a recursive run.

source
def Algebraic.Cutwidth.Extractor.recursiveBlockEntropy (h Q i : ℕ) :
ℕ

Entropy retained at level i of a depth-h schedule with leaf reserve Q.

Equations
Instances For
    source
    def Algebraic.Cutwidth.Extractor.recursiveBlockWidth (initial h Q E : ℕ) :
    ℕ → ℕ

    Actual block widths after successive rate-three condensations and equal splits.

    Equations
    Instances For
      source
      def Algebraic.Cutwidth.Extractor.recursiveBlockSeedWidth (initial h Q E i : ℕ) :
      ℕ

      Bit width of the fresh field seed at an internal level.

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

        A fixed leaf reserve large enough for the later explicit budget estimates.

        Equations
        Instances For