String programs for the concrete look-ahead and advice-bit step

The look-ahead runtime encodes its two outputs with Complexity.pair. The step uses the matched extractor runtime at fixed depths twenty-four and sixty-four, always retaining the original source words. Each component has total behavior on arbitrary strings and parameters; agreement with the fixed-width definitions uses the explicit common-scale guard.

The single-input codec is pair (pair x (pair y q)) (pair scale (pair error bit)). The numerical parameters are unary lengths and the advice bit is the first bit of its word, defaulting to false for an empty word.

def Algebraic.Cutwidth.Extractor.FlipFlopSizeGuard (n m L e : ℕ) : Prop

Shared scale sufficient for all three kinds of extractor call in one step.

Equations

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

def Algebraic.Cutwidth.Extractor.flipFlopLookAheadRuntime (L e : ℕ) (x q : List Bool) : List Bool

Encode the two look-ahead outputs from the actual string programs.

Equations

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

def Algebraic.Cutwidth.Extractor.flipFlopStepRuntime (L e : ℕ) (x y q : List Bool) (b : Bool) : List Bool

Execute one advice-bit step, using the original y at both refreshes.

Equations

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

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

One total evaluator for all lengths, shared scales, errors, and advice bits.

Equations

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