Runtime block payloads and seed consumption

Each state stores the current width and entropy, the block count, the concatenated block payload, and the unused seed suffix. One step uses the next field-width prefix as the shared condenser seed, splits every output into its consecutive halves, and discards exactly that seed prefix.

The numerical error exponent is fixed workspace in the string encoding. All programs are total, including on short seed words or malformed pairing encodings. Agreement with the statistical map uses canonical seed words; polynomial-time iteration additionally needs the proved state-size bounds.

structure Algebraic.Cutwidth.Extractor.ScheduledBlockRunState : Type

Runtime data at a level of the scheduled block recursion.

• dimensions : ℕ × ℕ

  Current block width and entropy threshold, in bits.

• count : ℕ

  Number of consecutive equal-width blocks.

• payload : List Bool

  Concatenation of the current block words.

• seeds : List Bool

  Seed bits not yet consumed by an earlier stage.

def Algebraic.Cutwidth.Extractor.scheduledBlockRunStep (E : ℕ) (state : ScheduledBlockRunState) : ScheduledBlockRunState

Condense every block using one fresh seed prefix, then advance the state.

Equations

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

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

Encode numerical workspace, block count, payload, and unused seed suffix.

Equations

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

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

One total step of the runtime payload loop on paired bit strings.

Equations

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

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

The initial condenser consumes the first seed and produces one compressed block.

Equations

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

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

Run the actual initial condenser and all requested internal block levels.

Equations

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