Unary computation of the explicit parameter formulas

The two variable powers occur immediately after ceiling logarithms. The UnaryFn.pow_clog rule bounds those rounded powers by a polynomial in their targets. All remaining operations are unary arithmetic and ceiling logarithms.

theorem Algebraic.Cutwidth.Extractor.Internal.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)

theorem Algebraic.Cutwidth.Extractor.Internal.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)

theorem Algebraic.Cutwidth.Extractor.Internal.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)

theorem Algebraic.Cutwidth.Extractor.Internal.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)

theorem Algebraic.Cutwidth.Extractor.Internal.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)

theorem Algebraic.Cutwidth.Extractor.Internal.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)

theorem Algebraic.Cutwidth.Extractor.Internal.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)

theorem Algebraic.Cutwidth.Extractor.Internal.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)