noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13AdjointPlus (s : ℝ) : ℝ

The κ=1 positive-sign standard adjoint.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13AdjointPlus s = s ^ 2 - 2 * s + 1 / 2

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13AdjointMinus (_s : ℝ) : ℝ

The κ=1 negative-sign standard adjoint.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13AdjointMinus _s = 1

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13AdjointPlus_dde (s : ℝ) : HasDerivAt (fun (u : ℝ) => u * section13AdjointPlus u) (2 * section13AdjointPlus s + section13AdjointPlus (s + 1)) s

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13AdjointMinus_dde (s : ℝ) : HasDerivAt (fun (u : ℝ) => u * section13AdjointMinus u) (2 * section13AdjointMinus s - section13AdjointMinus (s + 1)) s

structure MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract (H : Section13HatLayers) extends MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2 : Prop

Source-faithful Section 13 hat package at κ = 1. The inherited contract contains (T1)--(T4) and the weak weighted limit formerly used for tails; the extra field is precisely the original exponential-decay assertion (T5). Pairing-zero is deliberately a theorem below, not a field of this contract.

• betaHat_eq : H.betaHat = 2
• beta_gt_one : 1 < 2
• continuous (sign : ErrorSign) : ContinuousOn (H.T sign) (Set.Ioi 0)
• positive (sign : ErrorSign) (s : ℝ) : 0 < s → 0 < H.T sign s
• initial_plus (s : ℝ) : 0 < s → s ≤ 2 + 1 → weightedHat H ErrorSign.plus s = 2 - 1
• initial_minus (s : ℝ) : 0 < s → s ≤ 2 → weightedHat H ErrorSign.minus s = 2
• dde (sign : ErrorSign) (s : ℝ) : 2 + sign.epsilon < s → HasDerivAt (weightedHat H sign) (-s * H.T sign.opposite (s - 1)) s
• weighted_tendsto_zero (sign : ErrorSign) : Filter.Tendsto (weightedHat H sign) Filter.atTop (nhds 0)
• t5 : Section13HatExponentialDecay H

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13AdjointPlus_eventual_bounds : (∀ᶠ (s : ℝ) in Filter.atTop, |section13AdjointPlus s| ≤ 4 * s ^ 2) ∧ ∀ᶠ (s : ℝ) in Filter.atTop, ∀ t ∈ Set.uIoc (s - 1) s, |section13AdjointPlus (t + 1)| ≤ 4 * s ^ 2

The explicit polynomial adjoint q₊ has quadratic growth, both at the current point and uniformly over the moving unit window.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13AdjointMinus_eventual_bounds : (∀ᶠ (s : ℝ) in Filter.atTop, |section13AdjointMinus s| ≤ 1 * s ^ 2) ∧ ∀ᶠ (s : ℝ) in Filter.atTop, ∀ t ∈ Set.uIoc (s - 1) s, |section13AdjointMinus (t + 1)| ≤ 1 * s ^ 2

The constant adjoint q₋ = 1 satisfies the corresponding moving-window bounds with constant one.

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

Signwise source (T5) passes to the symmetric Q̂ combination.

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

Signwise source (T5) also passes to the antisymmetric P̂ combination.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10SignedPairing_tendsto_zero_of_exp_bound {R q : ℝ → ℝ} {b C K : ℝ} (hb : |b| ≤ 1) (hC : 0 ≤ C) (hK : 0 ≤ K) (hR : ∀ᶠ (s : ℝ) in Filter.atTop, |R s| ≤ C * Real.exp (-s)) (hq : ∀ᶠ (s : ℝ) in Filter.atTop, |q s| ≤ K * s ^ 2) (hqwin : ∀ᶠ (s : ℝ) in Filter.atTop, ∀ t ∈ Set.uIoc (s - 1) s, |q (t + 1)| ≤ K * s ^ 2) : Filter.Tendsto (section10SignedPairing b R q) Filter.atTop (nhds 0)

Exponential decay of the DDE solution and quadratic growth of its adjoint force the full moving-window pairing to tend to zero.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10SignedPairing_eq_of_dde_on_section13_range {b x y : ℝ} {R q : ℝ → ℝ} (hxy : x ≤ y) (hx : 3 < x) (hRcont : ContinuousOn R (Set.Ioi 0)) (hqcont : Continuous q) (hR : ∀ (s : ℝ), 3 < s → HasDerivAt R (-(2 * R s + b * R (s - 1)) / s) s) (hq : ∀ (s : ℝ), 0 < s → HasDerivAt (fun (u : ℝ) => u * q u) (2 * q s + b * q (s + 1)) s) : section10SignedPairing b R q y = section10SignedPairing b R q x

Constancy on the legal Section-13 range, obtained from the DDE without requiring a fictitious global continuity field.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_pairing_tendsto_zero {H : Section13HatLayers} (hH : Section13HatSourceContract H) : Filter.Tendsto (section10SignedPairing 1 (section13Qhat H) section13AdjointPlus) Filter.atTop (nhds 0)

The Q̂,q₊ pairing tends to zero by source (T5).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Phat_pairing_tendsto_zero {H : Section13HatLayers} (hH : Section13HatSourceContract H) : Filter.Tendsto (section10SignedPairing (-1) (section13Phat H) section13AdjointMinus) Filter.atTop (nhds 0)

The P̂,q₋ pairing tends to zero by source (T5).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_pairing_zero {H : Section13HatLayers} (hH : Section13HatSourceContract H) {s : ℝ} (hs : 3 < s) : section10SignedPairing 1 (section13Qhat H) section13AdjointPlus s = 0

Source (13.8), Q̂ branch: constancy plus (T5) gives pairing zero at every legal parameter, rather than assuming it in a bridge record.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Phat_pairing_zero {H : Section13HatLayers} (hH : Section13HatSourceContract H) {s : ℝ} (hs : 3 < s) : section10SignedPairing (-1) (section13Phat H) section13AdjointMinus s = 0

Source (13.8), P̂ branch: pairing zero for every legal parameter.