A block schedule that retains nearly half the entropy at each split

The rate parameter depends on the total depth. Each next width is the actual paired condenser half-width, including sparse rounding. The entropy gap pays for both the field width and the splitting error. The initial block has the supplied width, with no preliminary compression. One final seed pair is shared by all leaves and counted once.

These total numerical definitions assert no splitting guarantee, asymptotic parameter choice, or runtime bound. Their finite bounds are proved separately.

def Algebraic.Cutwidth.Extractor.nearHalvingBlockRate (h : ℕ) : ℕ

Rate parameter shared by all condensers at a fixed recursion depth.

Equations

• Algebraic.Cutwidth.Extractor.nearHalvingBlockRate h = 16 * (h + 1)

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

Entropy at level i, including the reserve lost in each remaining split.

Equations

• Algebraic.Cutwidth.Extractor.nearHalvingBlockEntropy h Q i = 2 ^ (h - i) * (8 * h + 8 + (h - i)) * Q

def Algebraic.Cutwidth.Extractor.nearHalvingBlockWidth (N h Q E : ℕ) : ℕ → ℕ

Actual rounded block widths after successive condensations and equal splits.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.Cutwidth.Extractor.nearHalvingBlockWidth N h Q E 0 = N

def Algebraic.Cutwidth.Extractor.nearHalvingBlockSeedWidth (N h Q E i : ℕ) : ℕ

Bit width of the field seed used at one internal level.

Equations

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

def Algebraic.Cutwidth.Extractor.nearHalvingBlockLeafLength (h Q : ℕ) : ℕ

Number of bits extracted from each final block.

Equations

• Algebraic.Cutwidth.Extractor.nearHalvingBlockLeafLength h Q = (8 * h + 7) * Q

def Algebraic.Cutwidth.Extractor.nearHalvingBlockOutputBits (h Q : ℕ) : ℕ

Number of bits in all final output blocks together.

Equations

• Algebraic.Cutwidth.Extractor.nearHalvingBlockOutputBits h Q = 2 ^ h * Algebraic.Cutwidth.Extractor.nearHalvingBlockLeafLength h Q

def Algebraic.Cutwidth.Extractor.nearHalvingBlockSeedBits (N h Q E : ℕ) : ℕ

Total width of internal field seeds and the final pair shared by all leaves.

Equations

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