Runtime numerical states for scheduled block recursion

The evolving state consists of the current block width and entropy threshold. A transition computes the actual next condenser half-width and divides the threshold by four. The local error exponent is fixed workspace.

The string codec is pair (pair unaryWidth unaryEntropy) unaryError. Its step is total and uses the standard total pairing projections on malformed inputs. Certificates for complete iteration require bounds on every intermediate state.

def Algebraic.Cutwidth.Extractor.scheduledBlockStateStep (E : ℕ) (state : ℕ × ℕ) : ℕ × ℕ

Update the two runtime numerical parameters of one rate-three level.

Equations

• Algebraic.Cutwidth.Extractor.scheduledBlockStateStep E state = (Algebraic.Cutwidth.Extractor.explicitCondenserHalfWidth state.1 state.2 E 3, state.2 / 4)

def Algebraic.Cutwidth.Extractor.encodeScheduledBlockState (E : ℕ) (state : ℕ × ℕ) : List Bool

Encode the evolving width and entropy together with the fixed local error exponent.

Equations

• Algebraic.Cutwidth.Extractor.encodeScheduledBlockState E state = Complexity.pair (Complexity.pair (List.replicate state.1 true) (List.replicate state.2 true)) (List.replicate E true)

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

One total uniform step on the nested unary state codec.

Equations

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