A runtime payload loop for the near-halving schedule

The state stores the actual block width, remaining depth and its power of two, block count, concatenated payload, and unused seed suffix. Each step consumes one shared field seed and applies the variable-rate block condenser. The initial payload is the unchanged source word. A separate iteration count allows a zero-step run without any splitting budget.

The encoded step is total on arbitrary strings and computes no exponential. The initializer's power of two must have an explicit uniform unary certificate when proving polynomial-time iteration. Numerical and complete state-size bounds are supplied separately; canonical seed semantics is another layer.

structure Algebraic.Cutwidth.Extractor.NearHalvingBlockRunState : Type

Runtime workspace for the near-halving block loop.

• width : ℕ

  Width of one current block.

• remaining : ℕ

  Number of scheduled levels remaining.

• remainingPower : ℕ

  Stored power of two of the remaining depth, updated by division.

• count : ℕ

  Number of consecutive blocks in the payload.

• payload : List Bool

  Concatenated current block words.

• seeds : List Bool

  Seed suffix not yet consumed by this run.

def Algebraic.Cutwidth.Extractor.nearHalvingBlockRunStep (h Q E : ℕ) (state : NearHalvingBlockRunState) : NearHalvingBlockRunState

Apply the actual shared-seed condenser to every block and advance the workspace.

Equations

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

def Algebraic.Cutwidth.Extractor.encodeNearHalvingBlockRun (h Q E : ℕ) (state : NearHalvingBlockRunState) : List Bool

Encode runtime workspace, static parameters, payload, and unused seed suffix.

Equations

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

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

One total encoded payload-loop step, with all numeric operands decoded in unary.

Equations

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

def Algebraic.Cutwidth.Extractor.nearHalvingBlockRunInitial (N h : ℕ) (source seeds : List Bool) : NearHalvingBlockRunState

Identity initialization keeps the source and every seed bit unchanged.

Equations

• Algebraic.Cutwidth.Extractor.nearHalvingBlockRunInitial N h source seeds = { width := N, remaining := h, remainingPower := 2 ^ h, count := 1, payload := source, seeds := seeds }

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

Execute any requested number of payload steps from the identity initialization.

Equations

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