Finite-prefix closure of Suzuki Proposition 11.8 at κ = 1

This module independently closes the source-pairing route through genuine finite prefixes. The finite weighted DDE is integrated on the two smooth pieces around s = 3; the terminal layer is then removed by dominated convergence, and the finite pairings converge to the genuine source pairing.

theorem MathlibNt.SieveTheory.tendsto_suzukiProposition118SourceQPrefix {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (s : ℝ) : Filter.Tendsto (fun (m : ℕ) => suzukiProposition118SourceQPrefix m s) Filter.atTop (nhds (suzukiProposition118SourceQ s))

At every fixed point, the genuine finite source prefixes converge to the actual source Q.

theorem MathlibNt.SieveTheory.continuousOn_suzukiProposition118SourceQPrefix_Ici (m : ℕ) : ContinuousOn (suzukiProposition118SourceQPrefix m) (Set.Ici 2)

Every finite source prefix is continuous on the closed series range.

theorem MathlibNt.SieveTheory.suzukiProposition118SourceQPrefix_nonneg_le {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (m : ℕ) {s : ℝ} (hs : 2 ≤ s) : 0 ≤ suzukiProposition118SourceQPrefix m s ∧ suzukiProposition118SourceQPrefix m s ≤ suzukiProposition118SourceQ s

On the series range the finite prefix is nonnegative and lies below the actual source series.

theorem MathlibNt.SieveTheory.tendsto_suzukiProposition118SourceQPrefix_pairing {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {y : ℝ} (hy : 3 ≤ y) : Filter.Tendsto (fun (m : ℕ) => SwitchingPrinciple.SuzukiLemma144KappaOne.section10SignedPairing 1 (suzukiProposition118SourceQPrefix m) suzukiProposition118KappaOneSourceAdjoint y) Filter.atTop (nhds (suzukiProposition118SourceQPairing y))

For every fixed pairing coordinate y ≥ 3, finite-prefix pairings converge pointwise to the genuine source pairing. The moving integral is passed to the limit on its compact window by domination from the source/hat comparison.