The total amplified-sampler program

Gamma reads the outer and candidate words and produces the seed for the growing-depth matched program on the original source word. Take the desired output prefix, completing it by false bits. Both component programs retain their total behavior on malformed inputs and invalid parameter choices. The paired evaluator reads three words and two unary widths.

def Algebraic.Cutwidth.Extractor.amplifiedMatchedSamplerRuntime (L d : ℕ) (source outer candidate : List Bool) : List Bool

Run both actual component programs and produce exactly d output bits.

Equations

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

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

Codec: pair (pair source (pair outer candidate)) (pair scale outputWidth), unary widths.

Equations

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