One deterministic condense-then-split level #
Apply a supplied condenser to every current block with the same fresh seed,
then split its pair outputs into consecutive half-blocks. The map specifies
only this deterministic operation; retaining prior seeds and sampling the
fresh seed are handled by retainedSeedStep in the statistical theorem.
def
Algebraic.Cutwidth.Extractor.condenseSplitMap
{α : Type u_1}
{β : Type u_2}
{Fresh : Type u_3}
(C : α → Fresh → β × β)
(t : ℕ)
(x : Fin t → α)
(y : Fresh)
:
Condense all blocks with one seed, then place each pair's two outputs consecutively.
Equations
- Algebraic.Cutwidth.Extractor.condenseSplitMap C t x y = (Algebraic.Cutwidth.Extractor.splitBlockEquiv β t) fun (i : Fin t) => C (x i) y