A total runtime for the rounded Gamma parameters

All numerical parameters come from the target width. The block loop executes the selected depth when the size guard holds and zero steps otherwise. The runtime returns the requested output prefix on the guarded branch, and an all-false word of the same width on the other branch.

The paired evaluator infers its target width as the source-word length divided by eight. Pair decoding and source lengths not divisible by eight remain total. Statistical correctness on canonical words is a separate layer.

@[instance_reducible]

def Algebraic.Cutwidth.Extractor.instDecidableGammaBlockSizeGuard (b : ℕ) : Decidable (GammaBlockSizeGuard b)

The runtime decides its size guard by the explicit inequality of natural logarithms.

Equations

• Algebraic.Cutwidth.Extractor.instDecidableGammaBlockSizeGuard b = { decide := (3 * Nat.clog 2 (Algebraic.Cutwidth.Extractor.gammaBlockLog b + 1) + 15).ble (Nat.log 2 b), reflects_decide := ⋯ }

def Algebraic.Cutwidth.Extractor.gammaBlockExtractorRuntime (b : ℕ) (source seeds : List Bool) : List Bool

Generate all parameters, run only the guarded number of levels, and emit exactly b bits.

Equations

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

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

Codec: pair source seeds; the target width is the source length divided by eight.

Equations

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