Corrected-sign compact-head margin

For κ = 1 we take Δ₀ = 1 and θ = (Δ₀ - Δ) / 2 = (1 - Δ) / 2. Thus the positive exponent is Δ₀ - Δ, not the reversed (and negative) printed sign Δ - Δ₀.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.compactHeadTheta (Δ : ℝ) : ℝ

The corrected positive half-gap exponent for the κ = 1 compact head.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.compactHeadTheta Δ = (1 - Δ) / 2

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.compactHeadCoefficient (Δ M : ℝ) : ℝ

The coefficient at the fixed splitting point M corresponding to the half-gap exponent.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.compactHeadCoefficient Δ M = (1 - 1 / M) ^ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.compactHeadTheta Δ

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.compactHeadMargin (Δ M : ℝ) : ℝ

The explicit coefficient margin between the half-gap coefficient and the full source exponent Δ₀ - Δ = 1 - Δ.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.compactHeadMargin Δ M = MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.compactHeadCoefficient Δ M - (1 - 1 / M) ^ (1 - Δ)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.corrected_deltaGap_pos {Δ : ℝ} (hΔ : Δ < 1) : 0 < 1 - Δ

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.compactHeadTheta_pos {Δ : ℝ} (hΔ : Δ < 1) : 0 < compactHeadTheta Δ

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.compactHeadMargin_pos {Δ M : ℝ} (hΔ : Δ < 1) (hM : 1 < M) : 0 < compactHeadMargin Δ M

The corrected sign gives a genuinely positive, completely explicit margin at every fixed M > 1.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.compactHead_weightedTail_strict {H : Section13HatLayers} (hH : Section13HatContract H 2) (sign : ErrorSign) {Δ M : ℝ} (hΔ : Δ < 1) (hM : 3 ≤ M) : ∫ (t : ℝ) in 3..M, ((t - 1) / t) ^ compactHeadTheta Δ * hatTailIntegrand H sign t < weightedHat H sign 3

Direct Lemma-13.3 witness with the corrected positive exponent. This is the strict compactness input behind the quantitative margin.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.eventually_compactHead_le_coefficient_sub_margin {H : Section13HatLayers} (hH : Section13HatContract H 2) (sign : ErrorSign) {d Δ M : ℝ} (hd : 0 ≤ d) (hΔ : Δ < 1) (hM : 3 ≤ M) : 0 < compactHeadMargin Δ M ∧ ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∫ (t : ℝ) in 3..M, qD H sign.opposite D d Δ t ≤ (compactHeadCoefficient Δ M - compactHeadMargin Δ M) * lambda H sign D d 0 3

Explicit positive-margin form of the fixed compact head. The established DDE/FTC compact-head estimate actually has the stronger coefficient (1 - 1/M)^(1-Δ). Rewriting that coefficient as compactHeadCoefficient - compactHeadMargin exposes a fixed positive amount which is available for absorbing the moving tail.

The threshold is fixed after M; no fixed-endpoint theorem is diagonalized at a moving source cutoff.