Uniform unary construction of the paired condenser half-width

The actual half-width is polynomial-time in all four unary parameters. Its coordinate count and sparse field half-degree use the certified bounded arithmetic of Condenser.Parameters.Explicit.Unary. The guarantee covers every natural input, including zero parameters.

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

Uniformly compute the exact half-width, including sparse-field rounding.