Proposition 11.8: decay of the genuine source Q and pairing at infinity

This file never identifies the source series with the Section-13 hat solution. Instead it applies the production finite-depth domination from Lemma 13.2 to finite odd/even source partial sums, passes to their genuine tsum limits, and only then invokes the hat contract's (T5) decay.

theorem MathlibNt.SieveTheory.suzukiProposition118SourceParitySeries_le_hat {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (s : ℝ), 2 ≤ s → suzukiProposition118SourceTPlus s ≤ C * s * H.T SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.plus s ∧ suzukiProposition118SourceTMinus s ≤ C * s * H.T SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.minus s

The finite-depth source/hat comparison survives the two parity tsum limits. This is domination, not an identification of source and hat layers.

theorem MathlibNt.SieveTheory.suzukiProposition118SourceQ_nonneg_and_le_hat {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (s : ℝ), 2 ≤ s → 0 ≤ suzukiProposition118SourceQ s ∧ suzukiProposition118SourceQ s ≤ C * s * (H.T SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.plus s + H.T SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.minus s)

On its series range, the genuine source Q=T⁺+T⁻ is nonnegative and is bounded by the sum of the two Section-13 hat majorants.

theorem MathlibNt.SieveTheory.suzukiProposition118SourceQ_eventually_le_mul_exp {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ∃ (D : ℝ), 0 ≤ D ∧ ∀ᶠ (s : ℝ) in Filter.atTop, 0 ≤ suzukiProposition118SourceQ s ∧ suzukiProposition118SourceQ s ≤ D * s * Real.exp (-s)

Quantitative eventual decay of the genuine source. The extra factor s comes from the finite source/hat comparison and is retained explicitly.

theorem MathlibNt.SieveTheory.suzukiProposition118SourceQ_weighted_eventual_bound {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ∃ (D : ℝ), 0 ≤ D ∧ ∀ᶠ (s : ℝ) in Filter.atTop, 0 ≤ s ^ 2 * suzukiProposition118SourceQ s ∧ s ^ 2 * suzukiProposition118SourceQ s ≤ D * (s ^ 3 * Real.exp (-s))

The weighted genuine source has the explicit eventual majorant D s³ e⁻ˢ.

theorem MathlibNt.SieveTheory.tendsto_suzukiProposition118SourceQ_weighted_zero {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : Filter.Tendsto (fun (s : ℝ) => s ^ 2 * suzukiProposition118SourceQ s) Filter.atTop (nhds 0)

Consequently s² Q(s) → 0 for the genuine source Q.

theorem MathlibNt.SieveTheory.tendsto_suzukiProposition118SourceQ_pairing_integral_zero {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : Filter.Tendsto (fun (s : ℝ) => ∫ (t : ℝ) in s - 1..s, suzukiProposition118KappaOneSourceAdjoint (t + 1) * suzukiProposition118SourceQ t) Filter.atTop (nhds 0)

The moving-window integral in the source pairing tends to zero. Its control uses nonnegativity and the same genuine-source exponential majorant.

theorem MathlibNt.SieveTheory.tendsto_suzukiProposition118SourceQ_pairing_point_zero {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : Filter.Tendsto (fun (s : ℝ) => s * suzukiProposition118KappaOneSourceAdjoint s * suzukiProposition118SourceQ s) Filter.atTop (nhds 0)

The point term in the source pairing tends to zero by weighted source decay and the linear source adjoint.

theorem MathlibNt.SieveTheory.tendsto_suzukiProposition118SourceQPairing_zero {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : Filter.Tendsto suzukiProposition118SourceQPairing Filter.atTop (nhds 0)

The genuine Proposition-11.8 source pairing tends to zero at infinity.