theorem MathlibNt.SieveTheory.LiuWeight.liuPanActualError_one (κ : ℝ) (N : ℕ) (B : ℝ) : liuPanActualError κ N B 1 = |liuMainPanCoprimeIntervalSum (liuLogarithmicIntegral κ) N (liuPanSourceIntervalLower N B) (liuPanSourceIntervalUpper N) 1 0 (liuWeight N (liuSourceZ10 N) (liuSourceY3 N))|

q=1 retains the canonical residue 0 in the actual maximum.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanActualError_zero (κ : ℝ) (N : ℕ) (B : ℝ) : liuPanActualError κ N B 0 = 0 ∧ ↑(ArithmeticFunction.moebius 0) ^ 2 = 0

q=0 vanishes both in the source residue maximum and in the weight.

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanUnweightedTheorem2Specialization.to_canonicalCoprimeTheorem (h : LiuPanUnweightedTheorem2Specialization) : LiuPanCanonicalCoprimeTheorem

Genuine original consumer, with precisely the single unweighted analytic input.