Matched Boolean seed and output widths for the scheduled extractor

The source and the padded seed are Boolean vectors. The actual scheduled bit program receives precisely its prescribed seed prefix, with false completion if the supplied budget is too small. Its output is read in flat block order. Thus every parameter choice has a total deterministic meaning, including zero widths; statistical guarantees use separate finite bounds.

def Algebraic.Cutwidth.Extractor.matchedBlockSeedBits (L : ℕ) : ℕ

The common padded seed width for recursion depths at most sixty-four.

Equations

• Algebraic.Cutwidth.Extractor.matchedBlockSeedBits L = 2 ^ 24 * L

def Algebraic.Cutwidth.Extractor.matchedBlockOutputBits (h L : ℕ) : ℕ

The exact flattened output width at the chosen recursion depth.

Equations

• Algebraic.Cutwidth.Extractor.matchedBlockOutputBits h L = 2 ^ h * L

def Algebraic.Cutwidth.Extractor.matchedBlockExtractor (n h L e : ℕ) (x : Fin n → Bool) (seed : Fin (matchedBlockSeedBits L) → Bool) (j : Fin (matchedBlockOutputBits h L)) : Bool

Run the actual scheduled program at the common seed and output widths.

Equations

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