theorem MathlibNt.SieveTheory.LiuWeight.LiuPanUnweightedTheorem2Specialization.to_corollary230 (hPan : LiuPanUnweightedTheorem2Specialization) : LiuPanWangDingCorollary230

Modern Cauchy weight payment for Pan's actual unweighted convolution specialization. The only analytic premise is hPan; κ and B are unchanged. Nine logarithms pay 9^ω/q and two pay the proved actual pointwise envelope.