Total string evaluation of the advice chain

The loop retains both original sources, unary parameters, remaining advice, and the current right state. A step consumes the first remaining advice bit; after exhaustion it leaves the state unchanged. The initial right state is zero-completed to its full width. The final depth-twenty-four call uses its seed-width prefix and the original left source.

The evaluator input is pair (pair x y) (pair scale (pair error advice)). The numerical parameters are lengths of their words. All operations are total, including malformed pairings and invalid numerical parameters.

structure Algebraic.Cutwidth.Extractor.AdviceRunState : Type

Every part of the advice-loop state, including the original source words.

• x : List Bool

  The original left source.

• y : List Bool

  The original right source.

• scale : ℕ

  The common scale.

• error : ℕ

  The common error exponent.

• remaining : List Bool

  Advice not yet consumed.

• q : List Bool

  The current right state.

def Algebraic.Cutwidth.Extractor.adviceInitialWord (L : ℕ) (y : List Bool) : List Bool

The right-source prefix, padded with false bits to the full state width.

Equations

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

def Algebraic.Cutwidth.Extractor.adviceRunInitial (L e : ℕ) (x y advice : List Bool) : AdviceRunState

Initialize the loop with its full immutable input and remaining advice.

Equations

• Algebraic.Cutwidth.Extractor.adviceRunInitial L e x y advice = { x := x, y := y, scale := L, error := e, remaining := advice, q := Algebraic.Cutwidth.Extractor.adviceInitialWord L y }

def Algebraic.Cutwidth.Extractor.adviceRunStep (state : AdviceRunState) : AdviceRunState

Consume the next advice bit, leaving the state fixed once the advice is empty.

Equations

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

def Algebraic.Cutwidth.Extractor.adviceRun (L e : ℕ) (x y advice : List Bool) (count : ℕ) : AdviceRunState

Run exactly the requested number of advice transitions.

Equations

• Algebraic.Cutwidth.Extractor.adviceRun L e x y advice count = Algebraic.Cutwidth.Extractor.adviceRunStep^[count] (Algebraic.Cutwidth.Extractor.adviceRunInitial L e x y advice)

def Algebraic.Cutwidth.Extractor.encodeAdviceRunState (state : AdviceRunState) : List Bool

Encode the full state, including the immutable source words and parameters.

Equations

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

def Algebraic.Cutwidth.Extractor.decodeAdviceRunState (z : List Bool) : AdviceRunState

Total projections decode all parts of a state word.

Equations

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

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

A single encoded transition, total on arbitrary words.

Equations

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

def Algebraic.Cutwidth.Extractor.adviceCorrelationBreakerRuntime (L e : ℕ) (x y advice : List Bool) : List Bool

Execute the advice chain, then extract from the original left source.

Equations

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

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

A single evaluator with unary scale/error words and arbitrary source/advice words.

Equations

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