The complete near-halving extractor as a bit program

After the requested number of block steps, apply one shared one-shot extractor to every leaf. Both final field seeds are sliced at their exact widths, so bits following the complete seed word are ignored. The separate iteration count permits a zero-step fallback in total parameter generators. All string operations are total, including on short or malformed inputs.

def Algebraic.Cutwidth.Extractor.nearHalvingBlockFinish (E ell : ℕ) (state : NearHalvingBlockRunState) : List Bool

Extract every current leaf using the exact final condenser and hash seed words.

Equations

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

def Algebraic.Cutwidth.Extractor.nearHalvingBlockFinishEval (z : List Bool) : List Bool

Parse an encoded runtime state and unary leaf length, then extract all current blocks.

Equations

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

def Algebraic.Cutwidth.Extractor.nearHalvingBlockExtractorBits (N h Q E ell count : ℕ) (source seeds : List Bool) : List Bool

Execute the requested block levels and finish with the shared leaf extractor.

Equations

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