theorem MathlibNt.SieveTheory.LiuWeight.liuPanUnweightedTheorem2Sum_le_closed (κ : ℝ) (N : ℕ) (B : ℝ) : liuPanUnweightedTheorem2Sum κ N B ≤ ∑ q ∈ Finset.Icc 1 (panModulusCutoff N B), liuPanActualError κ N B q

The strict ceil carrier is only enlarged to the closed floor carrier; the q=0 term vanishes separately. There is no false carrier equality.

theorem MathlibNt.SieveTheory.LiuWeight.pan_log_sq_payment (N : ℕ) (A K : ℝ) (hK : 0 ≤ K) (hlog : 1 ≤ Real.log ↑N) : K * ↑N / Real.log ↑N ^ (A + 2) * (1 + Real.log ↑N) ^ 2 ≤ 4 * K * ↑N / Real.log ↑N ^ A

Two logarithms pay a reciprocal-totient cofactor (or principal-modulus) sum.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanUnweightedTheorem2Specialization_proved : LiuPanUnweightedTheorem2Specialization

Actual unweighted distribution at the fixed principal normalization. All low, high, cofactor and principal estimates are consumed internally.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanWangDingCorollary230_proved : LiuPanWangDingCorollary230

Existing finite modern weight payment applied to the actual proved source.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanCanonicalCoprimeTheorem_proved : LiuPanCanonicalCoprimeTheorem

Existing source/normalization transport, with no distribution hypothesis.