Unary computation of the paired condenser half-width

The coordinate count and sparse field half-degree already have uniform unary certificates. Their product computes the exact half-width.

theorem Algebraic.Cutwidth.Extractor.Internal.explicitCondenserHalfWidth_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) => explicitCondenserHalfWidth (n z) (k z) (e z) (u z)