Case I, (14.23): source-faithful remainder interface

The paper does not replace the two Lemma-8.7 endpoints by an arbitrary fixed quotient. Claim 14.6(ii) licenses Lemma 8.7, Claim 14.6(iii) supplies the main contraction, and the two remaining endpoint terms retain the literal coefficient 3 * (κ + 1) * K^2, hence 6 * K^2 in the production specialization κ = 1.

The paper's subsequent estimates contain σ^3 log (e σ). Consequently the already accepted σ^2 scalar decay is necessary normalization data but is not, by itself, the source estimate. The predicates below freeze the exact additional source inequalities without choosing numerical constants hidden by the paper's O notation.

noncomputable def MathlibNt.SieveTheory.caseI1423RemainderUnit (B D σ : ℝ) : ℝ

Exact normalized unit used by every side remainder in (14.23).

Equations

• MathlibNt.SieveTheory.caseI1423RemainderUnit B D σ = B / (Real.log (Real.log D) * σ)

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

The literal Σ₁₁ Lemma-8.7 endpoint at τ=s, κ=1, β=2.

Equations

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

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

The literal Σ₁₂ Lemma-8.7 endpoint at τ=s, κ=1. This is definitionally the existing endpoint after cancelling s/s.

Equations

• MathlibNt.SieveTheory.caseI1423Sigma12Endpoint S H N D z C K d Δ s σ = C * Real.exp √K * MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑z * Real.log ↑D ^ (-Δ) * (6 * K ^ 2 * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD H (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite (↑D) d Δ s / Real.log (↑D ^ (1 / σ)))

def MathlibNt.SieveTheory.CaseI1423Sigma11SourceScalar (K d Δ : ℝ) : Prop

Exact source scalar left in the Σ₁₁ endpoint calculation on p.87. The existential coefficient is the honest interpretation of ≪; it is fixed before D and works eventually.

Equations

• MathlibNt.SieveTheory.CaseI1423Sigma11SourceScalar K d Δ = ∃ (A : ℝ), 0 ≤ A ∧ ∀ᶠ (D : ℝ) in Filter.atTop, K ^ 2 * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d ^ 3 * Real.log (Real.exp 1 * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) * Real.log (Real.log D) / Real.log D ^ (1 - Δ) ≤ A

def MathlibNt.SieveTheory.CaseI1423Sigma12SourceScalar (K d Δ : ℝ) : Prop

Exact source scalar left in the Σ₁₂ endpoint calculation on p.93. It is deliberately not weakened to a fixed signed-layer quotient.

Equations

• MathlibNt.SieveTheory.CaseI1423Sigma12SourceScalar K d Δ = ∃ (A : ℝ), 0 ≤ A ∧ ∀ᶠ (D : ℝ) in Filter.atTop, K ^ 2 * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d ^ 3 * Real.log (Real.exp 1 * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) * Real.log (Real.log D) / Real.log D ^ (1 - Δ) ≤ A

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

Uniform Claim-14.6 source contract actually consumed before (14.19). One threshold is chosen before the sign and the moving coordinate. Part (ii) is the monotonicity input to Lemma 8.7; part (iii) is the strict integral bound which creates the main multiplier in (14.23).

Equations

• MathlibNt.SieveTheory.CaseI1423Claim146iiiiiSource H d Δ = ∃ (D₀ : ℝ), ∀ (D : ℝ), D₀ ≤ D → have σ := MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d; (∀ (sign : MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign), AntitoneOn (fun (t : ℝ) => MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD H sign.opposite D d Δ t * t) (Set.Ioc (2 + sign.epsilon) σ)) ∧ ∀ (sign : MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) (s : ℝ), 2 + sign.epsilon ≤ s → s ≤ σ → ∫ (t : ℝ) in s..σ, MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD H sign.opposite D d Δ t < (1 - 1 / σ) ^ (1 - Δ) * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lambda H sign D d 0 s

def MathlibNt.SieveTheory.CaseI1423EndpointSourceBounds : Prop

A numerical O-coefficient package for the two endpoint estimates. The constants are selected before D; this is the uniformity needed in (14.23). The hypotheses are the exact inequalities obtained after applying Claim 14.6(ii) to Lemma 8.7 and then estimating the displayed endpoints on pp.87 and 93.

Equations

• MathlibNt.SieveTheory.CaseI1423EndpointSourceBounds = ∀ (S : BoundingSieve) (H : MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (N : ℕ) (C K d Δ s : ℝ), ∃ (A11 : ℝ) (A12 : ℝ), 0 ≤ A11 ∧ 0 ≤ A12 ∧ ∀ᶠ (D : ℕ) in Filter.atTop, have σ := MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d; have z := ⌈↑D ^ (1 / s)⌉₊; have B := MathlibNt.SieveTheory.sigma12InheritedBudget S H N D z C K d Δ s; MathlibNt.SieveTheory.caseI1423Sigma11Endpoint S N D z K s σ ≤ A11 * MathlibNt.SieveTheory.caseI1423RemainderUnit B (↑D) σ ∧ MathlibNt.SieveTheory.caseI1423Sigma12Endpoint S H N D z C K d Δ s σ ≤ A12 * MathlibNt.SieveTheory.caseI1423RemainderUnit B (↑D) σ

theorem MathlibNt.SieveTheory.caseI1423_sigma11_sigma12_endpoints_add {R11 R12 A11 A12 B D σ : ℝ} (h11 : R11 ≤ A11 * caseI1423RemainderUnit B D σ) (h12 : R12 ≤ A12 * caseI1423RemainderUnit B D σ) : R11 + R12 ≤ (A11 + A12) * caseI1423RemainderUnit B D σ

Exact finite algebra behind the endpoint part of (14.23): the two source remainders combine with coefficient A11 + A12, with no generic quotient and no absorption premise.

theorem MathlibNt.SieveTheory.caseI1423_endpointSourceBounds_combined (hsrc : CaseI1423EndpointSourceBounds) (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (N : ℕ) (C K d Δ s : ℝ) : ∃ (A : ℝ), 0 ≤ A ∧ ∀ᶠ (D : ℕ) in Filter.atTop, have σ := SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d; have z := ⌈↑D ^ (1 / s)⌉₊; have B := sigma12InheritedBudget S H N D z C K d Δ s; caseI1423Sigma11Endpoint S N D z K s σ + caseI1423Sigma12Endpoint S H N D z C K d Δ s σ ≤ A * caseI1423RemainderUnit B (↑D) σ

Eventual endpoint combination with all source quantifiers in their required order. In particular A11,A12 are independent of D.