theorem MathlibNt.SieveTheory.LiuWeight.principalError_eq_liuPanActualPrincipalRaw (N A₁ A₂ q : ℕ) : AnalyticNumberTheory.LargeSieve.PanPrincipal.principalError N A₁ A₂ q = liuPanActualPrincipalRaw (liuLogarithmicIntegral (2 / Real.log 2)) N A₁ A₂ q (liuWeight N (liuSourceZ10 N) (liuSourceY3 N))

Exact identity of the two independently constructed actual principal remainders.

theorem MathlibNt.SieveTheory.LiuWeight.liuWeight_intervalMaxL_le_nonprincipal_with_paid_principal (s : ℝ) (hs : 0 < s) : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ (q A₁ A₂ : ℕ), 1 ≤ q → ↑q ≤ √↑N → ↑A₂ ≤ ↑N ^ (2 / 3) → liuMainPanCoprimeIntervalMaxL (liuLogarithmicIntegral (2 / Real.log 2)) N A₁ A₂ q (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) ≤ (liuPanActualNonprincipalMass N A₁ A₂ q (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) + C * ↑N / Real.log ↑N ^ s) / ↑q.totient

The actual same-modulus nonprincipal mass is the only term left unpaid. The principal remainder has an unconditional uniform logarithmic bound.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanActualError_le_nonprincipal_with_paid_principal (s : ℝ) (hs : 0 < s) : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ∀ (B : ℝ) (q : ℕ), 1 ≤ q → ↑q ≤ √↑N → liuPanActualError (2 / Real.log 2) N B q ≤ (liuPanActualNonprincipalMass N (liuPanSourceIntervalLower N B) (liuPanSourceIntervalUpper N) q (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) + C * ↑N / Real.log ↑N ^ s) / ↑q.totient

Actual Pan consumer window, with the normalization fixed before s. No hypothesis asserting either a PNT estimate or a principal remainder estimate remains.