Case I, (14.23): endpoint source bounds

The published predicate CaseI1423EndpointSourceBounds omits the source hypotheses (and even quantifies over C = 0), so it is not a valid unconditional statement. This file proves the source-faithful version used in Case I. The source bounds are imported from their proved production producers. In particular, neither endpoint inequality is assumed in this module.

def MathlibNt.SieveTheory.CaseI1423EndpointSourceBoundsSourceLargeLog (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ : ℝ) : Prop

Honest endpoint-source statement with a D threshold uniform in N and s. Both constants and the eventual threshold precede the pointwise Case-I source-window hypotheses.

Equations

• MathlibNt.SieveTheory.CaseI1423EndpointSourceBoundsSourceLargeLog S H C K d Δ = ∃ (A11 : ℝ) (A12 : ℝ), 0 ≤ A11 ∧ 0 ≤ A12 ∧ ∀ (D N : ℕ) (s : ℝ), 3 ≤ D → 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 - Δ) ≤ 1 → 2 ≤ N → 2 ≤ s → s - 1 ∈ MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1) → s ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → 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.caseI1423EndpointSourceBounds_of_sourceScalar (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ : ℝ) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hC : 0 < C) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (_hd : 7 / (1 - Δ) < d) : CaseI1423EndpointSourceBoundsSourceLargeLog S H C K d Δ

Closure of the two endpoint source bounds.

theorem MathlibNt.SieveTheory.exists_caseI1423EndpointSourceBounds_sourceLargeLog_uniform (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hΔ0 : 0 < Δ) (hΘ : 0 < Θ) (hmargin : Δ + 2 / Θ < 1) (hd : 7 / (1 - (Δ + 2 / Θ)) < d) : ∃ (C1min : ℝ), 1 ≤ C1min ∧ ∀ (C1 C K : ℝ), C1min ≤ C1 → 0 < C → 2 ≤ K → ∃ (A11 : ℝ) (A12 : ℝ), 0 ≤ A11 ∧ 0 ≤ A12 ∧ ∀ (N D : ℕ) (s : ℝ), 3 ≤ D → C1 * K ^ Θ < Real.log ↑D → 2 ≤ N → 2 ≤ s → s - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1) → s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → 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 σ ≤ A11 * caseI1423RemainderUnit B (↑D) σ ∧ caseI1423Sigma12Endpoint S H N D z C K d Δ s σ ≤ A12 * caseI1423RemainderUnit B (↑D) σ

Source-large-log endpoint API. The cutoff is selected before C, K, N, D, and s; the only large-parameter hypothesis is the literal Case-I source inequality.