Explicit finite parameters for the advice chain

The advice length, target error exponent, requested output length, and left source length determine a common scale. The local error exponent pays the checked factor-four error recurrence. The common source entropy reserve also serves as the right-source length. Its capacity in the left source is a separate condition, not a property of this total parameter chooser.

def Algebraic.Cutwidth.Extractor.adviceErrorExponent (a target : ℕ) : ℕ

Local error exponent for a advice steps and final error 2^(-target).

Equations

• Algebraic.Cutwidth.Extractor.adviceErrorExponent a target = target + 2 * a + Nat.clog 2 (a + 1) + 10

def Algebraic.Cutwidth.Extractor.adviceScale (n a target out : ℕ) : ℕ

Common scale controlling the source lengths and all fixed-depth extractor calls.

Equations

• Algebraic.Cutwidth.Extractor.adviceScale n a target out = 1024 * (a + target + out + Nat.clog 2 (n + 1) + 256)

def Algebraic.Cutwidth.Extractor.adviceSourceEntropy (n a target out : ℕ) : ℕ

Equal source entropy reserve, also used as the right-source length.

Equations

• Algebraic.Cutwidth.Extractor.adviceSourceEntropy n a target out = 2 ^ 150 * (a + 1) * Algebraic.Cutwidth.Extractor.adviceScale n a target out