A computer-assisted sharp diagonal Hlawka inequality for real exponents p ≥ 21

We give a computer-assisted proof that, for every real p ≥ 21, the dimension-independent sharp Hlawka constant of complex ℓ_p is the maximum of an explicit one-parameter ratio on the cyclic triple (-t,1,1), (1,-t,1), (1,1,-t), 1/2 ≤ t ≤ 2. The new finite calculation covers 21 ≤ p ≤ 32; the range p ≥ 32 uses a previously accepted Prove2Me theorem. The improvement uses norm caps, clipped pair-coordinate tails, and linear coordinate-sum constraints on a convex averaging domain, together with a sharper residual Hessian estimate. Rational linear-programming dual witnesses and interval certificates cover real exponent intervals, rather than sampled exponents. The finite obligations pass both Arb and a standard-library dyadic rational implementation. We give the analytic reduction, certificate specification, and reproduction instructions. An accompanying Lean formalization of the original uniform complex least-constant goal is verified on Prove2Me with no open dependencies, reusing the accepted p ≥ 32 tail. Independent analytic review remains pending, and no optimality of the exponent threshold 21 is asserted.