theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13AdjointPlus_window_lower {s t : ℝ} (hs : 4 ≤ s) (ht : t ∈ Set.Icc (s - 1) s) : section13AdjointPlus s ≤ section13AdjointPlus (t + 1)

On the window [s-1,s], the explicit positive adjoint has weight at least its current weight. This is the order input that turns pairing-zero into the local premise of Suzuki's Lemma 10.22.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_lemma1022_local_premise {H : Section13HatLayers} (hH : Section13HatSourceContract H) : ∀ᶠ (s : ℝ) in Filter.atTop, (s + 1) * section13Qhat H s ≥ ∫ (t : ℝ) in s - 1..s, section13Qhat H t

The Lemma-10.22 local lower inequality is a theorem of Qhat, not an extra premise. Pairing-zero says that the adjoint-weighted window integral is s q(s) Qhat(s); positivity of Qhat and monotonicity of the explicit quadratic adjoint remove the weight.