The complete scheduled extractor as a bit program

Run the initial condenser and the internal block loop, then use the final two shared field seeds for one-shot extraction on every leaf. The complete seed word is consumed in stage order without copying any seed per block.

The total runtime wrapper derives the source length, clips the requested depth to its ceiling logarithm, and generates the error and entropy parameters. Its paired interface accepts only source, seed word, requested depth, and requested error exponent; all numerical parameters are generated by the same program.

def Algebraic.Cutwidth.Extractor.scheduledBlockFinish (E ell : ℕ) (state : ScheduledBlockRunState) : List Bool

Finish every leaf using the final pair of shared field seeds.

Equations

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

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

Decode an encoded runtime state and unary output length, then extract every leaf.

Equations

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

def Algebraic.Cutwidth.Extractor.scheduledBlockExtractorBits (n h Q E ell : ℕ) (source seeds : List Bool) : List Bool

Evaluate the specified extractor using one flat seed word.

Equations

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

def Algebraic.Cutwidth.Extractor.scheduledBlockExtractorRuntime (requested e : ℕ) (source seeds : List Bool) : List Bool

Generate a valid finite schedule from the source length and the requested depth and error.

Equations

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

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

Codec: pair (pair source seeds) (pair unaryRequestedDepth unaryError).

Equations

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