Source-faithful moving assembly of Claim 14.6(iii)

The source splits at the fixed point M + 2. The compact head is controlled by Lemma 13.3/(14.2), whereas the moving tail is controlled by the large-s DDE argument. Proposition 13.1(iii) is used only to make the endpoint value at M + 2 be O(M⁻²) relative to every starting value in the compact range.

Section13HatContract contains only qualitative convergence weightedHat → 0; it has no quantitative rate from which this M⁻² estimate can be selected. Accordingly the first definition below is the minimal extra DDE-tail interface. It is not Claim 14.6(iii), and it is independent of D, d, Δ, sourceSigma, and the qD integral.

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Proposition131TailDecayContract (H : Section13HatLayers) : Prop

Minimal quantitative consequence of Proposition 13.1(iii) needed in the moving proof. The source gives the stronger (M log (eM))⁻² decay; only its weaker C M⁻² consequence, together with the monotone comparison back to every 3 ≤ s ≤ M, is retained here.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Proposition131TailDecayContract H = ∃ (C : ℝ), 0 ≤ C ∧ ∀ (sign : MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) (M s : ℝ), 4 ≤ M → 2 + sign.epsilon ≤ s → s ≤ M → MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.weightedHat H sign (M + 2) ≤ C / M ^ 2 * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.weightedHat H sign s

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.FixedCompactPerturbationContract (d M : ℝ) : Prop

The fixed-compact perturbation factors tend uniformly to one. This tiny interface records only the factor 2 needed to transfer Proposition 13.1(iii) from weightedHat to lambda; it is elementary and separate from the DDE.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.FixedCompactPerturbationContract d M = ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∀ (sign : MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) (s : ℝ), 2 + sign.epsilon ≤ s → s ≤ M → MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.perturbation D d 0 (M + 2) ≤ 2 * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.perturbation D d 0 s

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Lemma133WeightedHeadContract (H : Section13HatLayers) (d Δ gap M : ℝ) : Prop

Source Lemma 13.3/(14.2), after the fixed compact prefactors have been absorbed. The positive first-order saving is deliberately gap/(4M); here gap = Δ₀-Δ, correcting the reversed sign in the last two displays on printed p. 92. This is a head estimate, not the final moving claim.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Lemma133WeightedHeadContract H d Δ gap M = ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∀ (sign : MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) (s : ℝ), 2 + sign.epsilon ≤ s → s ≤ M → ∫ (t : ℝ) in s..M + 2, MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD H sign.opposite D d Δ t ≤ (1 - 1 / MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) ^ (1 - Δ) * (1 - gap / (4 * M)) * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lambda H sign D d 0 s

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.MovingDDEWeightedTailContract (H : Section13HatLayers) (d Δ M : ℝ) : Prop

The already established large-s differential/DDE tail, uniform up to the actual moving source cutoff. Its left endpoint is fixed before D is chosen.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.MovingDDEWeightedTailContract H d Δ M = ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → M + 2 ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d ∧ (∀ (sign : MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) (s : ℝ), M ≤ s → s ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d → ∫ (t : ℝ) in s..MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d, MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD H sign.opposite D d Δ t < (1 - 1 / MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) ^ (1 - Δ) * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lambda H sign D d 0 s) ∧ ∀ (sign : MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign), ∀ s ≤ M, ∫ (t : ℝ) in s..MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d, MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD H sign.opposite D d Δ t = (∫ (t : ℝ) in s..M + 2, MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD H sign.opposite D d Δ t) + ∫ (t : ℝ) in M + 2..MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d, MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD H sign.opposite D d Δ t

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim146iiiFixedM (C gap : ℝ) : ℝ

A fixed cutoff chosen solely from the Proposition-13.1 constant and the positive source gap. The 16 leaves twice the margin actually needed below.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim146iiiFixedM C gap = max 4 (16 * C / gap + 1)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim146iiiFixedM_margin {C gap : ℝ} (hC : 0 ≤ C) (hgap : 0 < gap) : have M := claim146iiiFixedM C gap; 4 ≤ M ∧ 2 * C / M ^ 2 < gap / (4 * M)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.tendsto_source_weight (gap : ℝ) : Filter.Tendsto (fun (σ : ℝ) => (1 - 1 / σ) ^ gap) Filter.atTop (nhds 1)

The source weight tends to one for every fixed real exponent.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lambda_pos_of_source_range {H : Section13HatLayers} (hH : Section13HatContract H 2) (sign : ErrorSign) {D d s : ℝ} (hD : 1 < D) (hs : 2 + sign.epsilon ≤ s) : 0 < lambda H sign D d 0 s

The perturbed layer is positive throughout the parity-dependent source range.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lambda_fixed_endpoint_decay {H : Section13HatLayers} {d C M D s : ℝ} (sign : ErrorSign) (hM : 4 ≤ M) (hD : 1 < D) (hs : 2 + sign.epsilon ≤ s) (h131 : weightedHat H sign (M + 2) ≤ C / M ^ 2 * weightedHat H sign s) (hpert : perturbation D d 0 (M + 2) ≤ 2 * perturbation D d 0 s) (hpos : ∀ (sign : ErrorSign) (t : ℝ), 0 < t → 0 < H.T sign t) : lambda H sign D d 0 (M + 2) ≤ 2 * C / M ^ 2 * lambda H sign D d 0 s

Proposition 13.1(iii), plus the harmless fixed-compact perturbation bound, turns the DDE tail endpoint into the required O(M⁻²) multiple of the value at any compact-range starting point.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.moving_claim14_6_iii_of_source_contracts {H : Section13HatLayers} (hH : Section13HatContract H 2) {d Δ gap : ℝ} (_hΔ : Δ < 1) (hgap : 0 < gap) (h131 : Proposition131TailDecayContract H) (hpertAll : ∀ (C : ℝ), 0 ≤ C → FixedCompactPerturbationContract d (claim146iiiFixedM C gap)) (hheadAll : ∀ (C : ℝ), 0 ≤ C → Lemma133WeightedHeadContract H d Δ gap (claim146iiiFixedM C gap)) (htailAll : ∀ (C : ℝ), 0 ≤ C → MovingDDEWeightedTailContract H d Δ (claim146iiiFixedM C gap)) : ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∀ (sign : ErrorSign) (s : ℝ), 2 + sign.epsilon ≤ s → s ≤ sourceSigma D d → ∫ (t : ℝ) in s..sourceSigma D d, qD H sign.opposite D d Δ t < (1 - 1 / sourceSigma D d) ^ (1 - Δ) * lambda H sign D d 0 s

Source-faithful head+tail assembly of moving Claim 14.6(iii).

The cutoff is fixed as M = max 4 (16 C / gap + 1) before any D threshold is chosen. Consequently the tail coefficient 2C/M² is strictly smaller than the head saving gap/(4M). The theorem does not package its own conclusion as a premise: its four inputs are respectively Proposition 13.1 quantitative decay, elementary compact perturbation, Lemma 13.3 weighted head, and the large-range DDE tail.