Lemma 14.4, Case I: the same-constant scalar absorption edge

The three displayed side terms in the current Case-I API are the Claim-14.5 Σ₀ budget, the Lemma-8.7 endpoint in Σ₁₁, and the Lemma-8.7 endpoint in Σ₁₂. Suzuki's (14.23) reduces their sum to a fixed multiple of

B / (log (log D) * sourceSigma D d),

where B is the inherited same-C budget. The theorem below proves, rather than assumes, that every such fixed source-order side term is eventually paid for by the canonical midpoint gap from Claim 14.6(iii).

noncomputable def MathlibNt.SieveTheory.caseISigma11EndpointRemainder (S : BoundingSieve) (N D z : ℕ) (K β s τ σ : ℝ) : ℝ

The exact Σ₁₁ endpoint term displayed by the internal Lemma-8.7 bound.

Equations

• MathlibNt.SieveTheory.caseISigma11EndpointRemainder S N D z K β s τ σ = MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑z * (6 * K ^ 2 * MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (τ - 1) / Real.log (↑D ^ (1 / σ)) * (τ / s))

noncomputable def MathlibNt.SieveTheory.caseIExplicitSideBudget (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (N D z : ℕ) (C C145 K β d Δ s τ σ : ℝ) : ℝ

The literal sum of all explicit Case-I side budgets currently exposed by Σ₀, Σ₁₁, and Σ₁₂. No absorption inequality is a field of this object.

Equations

• MathlibNt.SieveTheory.caseIExplicitSideBudget S H N D z C C145 K β d Δ s τ σ = MathlibNt.SieveTheory.suzukiSigmaZeroClaim145Budget S H N D z d Δ σ K C145 + MathlibNt.SieveTheory.caseISigma11EndpointRemainder S N D z K β s τ σ + MathlibNt.SieveTheory.sigma12EndpointRemainder S H N D z C K d Δ s σ

noncomputable def MathlibNt.SieveTheory.caseISourceOrderCoefficient (A D d : ℝ) : ℝ

The source-order coefficient in Suzuki (14.23).

Equations

• MathlibNt.SieveTheory.caseISourceOrderCoefficient A D d = A / (Real.log (Real.log D) * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d)

theorem MathlibNt.SieveTheory.caseI_rpow_contraction_gap {Δ σ : ℝ} (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hσ : 1 < σ) : (1 - Δ) / σ ≤ 1 - (1 - 1 / σ) ^ (1 - Δ)

Bernoulli/weighted-AM--GM lower bound for the Claim-14.6 contraction gap.

theorem MathlibNt.SieveTheory.caseI_midpoint_gap_lower {Δ σ : ℝ} (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hσ : 1 < σ) : ∃ (q : Lemma144StrictFactor), q.ρ = (1 + sigma12ContractionMultiplier σ Δ) / 2 ∧ (1 - Δ) / (2 * σ) ≤ 1 - q.ρ

The canonical midpoint strict factor leaves at least half of the elementary Claim-14.6 gap.

theorem MathlibNt.SieveTheory.eventually_caseISourceOrderCoefficient_le_sameC_gap {A d Δ : ℝ} (_hA : 0 ≤ A) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) : ∀ᶠ (D : ℝ) in Filter.atTop, ∃ (q : Lemma144StrictFactor), q.ρ = (1 + sigma12ContractionMultiplier (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) Δ) / 2 ∧ caseISourceOrderCoefficient A D d ≤ 1 - q.ρ

Every fixed source-order side coefficient is eventually absorbed by the same-C midpoint gap. This is the complete scalar step in (14.23); its proof uses the literal sourceSigma and the growth of log (log D).

theorem MathlibNt.SieveTheory.eventually_caseISourceOrderBudget_le_sameC_gap {A B d Δ : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) : ∀ᶠ (D : ℝ) in Filter.atTop, ∃ (q : Lemma144StrictFactor), q.ρ = (1 + sigma12ContractionMultiplier (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) Δ) / 2 ∧ caseISourceOrderCoefficient A D d * B ≤ (1 - q.ρ) * B

Budget-valued form of the scalar theorem. The side term is the proved source-order majorant, not an assumed absorption inequality.

theorem MathlibNt.SieveTheory.eventually_caseI_allExplicitRemainderCoefficient_le_sameC_gap {A145 K d Δ : ℝ} (hA145 : 0 ≤ A145) (hK : 0 < K) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) : ∀ᶠ (D : ℝ) in Filter.atTop, ∃ (q : Lemma144StrictFactor), q.ρ = (1 + sigma12ContractionMultiplier (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) Δ) / 2 ∧ caseISourceOrderCoefficient (A145 + 12 * K ^ 2) D d ≤ 1 - q.ρ

Case-I's three displayed remainder families have one Claim-14.5 constant and two Lemma-8.7 endpoint constants 6 K². For fixed positive K, their combined source-order coefficient is therefore eventually inside the same-C gap. The theorem is scalar: it makes no assumption of the desired absorption inequality.

def MathlibNt.SieveTheory.Lemma144CaseIExplicitRemaindersSourceOrder : Prop

Earliest remaining non-scalar edge. It says that the literal sum of the three explicit API budgets has Suzuki's source order. This is deliberately a frozen proposition (not an axiom and not a premise of the scalar absorption theorems): the reachable production cone contains no theorem simultaneously normalising the Claim-14.5 Σ₀ sum and the two Lemma-8.7 endpoints to the inherited errorEnvelope budget.

Equations

• MathlibNt.SieveTheory.Lemma144CaseIExplicitRemaindersSourceOrder = ∀ (S : BoundingSieve) (H : MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (N : ℕ) (C C145 K β d Δ s τ : ℝ), ∃ (A : ℝ), 0 ≤ A ∧ ∀ᶠ (D : ℕ) in Filter.atTop, have σ := MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d; have z := ⌈↑D ^ (1 / s)⌉₊; MathlibNt.SieveTheory.caseIExplicitSideBudget S H N D z C C145 K β d Δ s τ σ ≤ MathlibNt.SieveTheory.caseISourceOrderCoefficient A (↑D) d * MathlibNt.SieveTheory.sigma12InheritedBudget S H N D z C K d Δ s