Uniform unary construction of all selected condenser dimensions

Polynomial-time unary inputs give polynomial-time unary budgets, exponents, field widths, extension degrees, and coordinate counts. The half-degree 3^s is certified directly for use by the runtime modulus generator.

Only rounded powers base^(clog base target) are constructed. The proof uses the existing bounded-power and logarithm algorithms in Classes.P.Unary; it does not enumerate the field or construct the numbers 2^b and 2^r. These certificates are independent of positivity assumptions and cover the total natural-number definitions.

theorem Algebraic.Cutwidth.Extractor.explicitCondenserBudget_unaryFn {n k e : List Bool → ℕ} (hn : Complexity.UnaryFn n) (hk : Complexity.UnaryFn k) (he : Complexity.UnaryFn e) : Complexity.UnaryFn fun (z : List Bool) => explicitCondenserBudget (n z) (k z) (e z)

The logarithmic slack budget can be written in unary in polynomial time.

theorem Algebraic.Cutwidth.Extractor.sparseFieldExponent_unaryFn {u T : List Bool → ℕ} (hu : Complexity.UnaryFn u) (hT : Complexity.UnaryFn T) : Complexity.UnaryFn fun (z : List Bool) => sparseFieldExponent (u z) (T z)

The exponent selecting a sparse field is polynomial-time in its inputs.

theorem Algebraic.Cutwidth.Extractor.sparseFieldHalfDegree_unaryFn {u T : List Bool → ℕ} (hu : Complexity.UnaryFn u) (hT : Complexity.UnaryFn T) : Complexity.UnaryFn fun (z : List Bool) => 3 ^ sparseFieldExponent (u z) (T z)

The actual unary half-degree uses bounded power rounding, rather than enumeration.

theorem Algebraic.Cutwidth.Extractor.sparseFieldBits_unaryFn {u T : List Bool → ℕ} (hu : Complexity.UnaryFn u) (hT : Complexity.UnaryFn T) : Complexity.UnaryFn fun (z : List Bool) => sparseFieldBits (u z) (T z)

The full base-field bit width is polynomial-time in unary.

theorem Algebraic.Cutwidth.Extractor.sparsePowerBits_unaryFn {u T : List Bool → ℕ} (hu : Complexity.UnaryFn u) (hT : Complexity.UnaryFn T) : Complexity.UnaryFn fun (z : List Bool) => sparsePowerBits (u z) (T z)

The modular squaring stride is polynomial-time in unary.

theorem Algebraic.Cutwidth.Extractor.condenserCoordinates_unaryFn {k r : List Bool → ℕ} (hk : Complexity.UnaryFn k) (hr : Complexity.UnaryFn r) : Complexity.UnaryFn fun (z : List Bool) => condenserCoordinates (k z) (r z)

Ceiling division computes the unary coordinate count uniformly.

theorem Algebraic.Cutwidth.Extractor.explicitCondenserExtensionExponent_unaryFn {n k e u : List Bool → ℕ} (hn : Complexity.UnaryFn n) (hk : Complexity.UnaryFn k) (he : Complexity.UnaryFn e) (hu : Complexity.UnaryFn u) : Complexity.UnaryFn fun (z : List Bool) => explicitCondenserExtensionExponent (n z) (k z) (e z) (u z)

The selected extension exponent is polynomial-time in all four unary inputs.

theorem Algebraic.Cutwidth.Extractor.explicitCondenserExtensionDegree_unaryFn {n k e u : List Bool → ℕ} (hn : Complexity.UnaryFn n) (hk : Complexity.UnaryFn k) (he : Complexity.UnaryFn e) (hu : Complexity.UnaryFn u) : Complexity.UnaryFn fun (z : List Bool) => explicitCondenserExtensionDegree (n z) (k z) (e z) (u z)

The extension degree itself is polynomial-time by bounded power rounding.