Even Case-I source-large pointwise producer #
This is the no-post-K endpoint producer at s = 2. The induction threshold is
literally Dmin = 2. Every source-fixed cutoff is selected before C1,C,K,M,D
and is paid pointwise by C1 * K ^ Θ < log D. The only exponent assumptions
are the formal SuzukiClaim145SourceParameters packet.
theorem
MathlibNt.SieveTheory.exists_lemma14_4_caseI_evenEndpoint_sourceLargeLog_pointwise_uniform_in_S
(H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers)
{d Δ Θ : ℝ}
(hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H)
(hsrc : SuzukiClaim145SourceParameters d Δ Θ)
:
∃ (C1min : ℝ) (CB : ℝ),
1 ≤ C1min ∧ 0 < CB ∧ ∀ (S : BoundingSieve) (C1 C K : ℝ) (M D : ℕ),
C1min ≤ C1 →
max 3 CB ≤ C →
2 ≤ K →
SwitchingPrinciple.HasDimensionOneLocalProductBound S K →
Even M →
2 ≤ M →
C1 * K ^ Θ < Real.log ↑D →
Lemma144MovingDomainGlobalDepthAt S H C K d Δ (M - 1) 2 →
suzukiActualT S M D ⌈↑D ^ (1 / 2)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / 2)⌉₊ * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 M 2 + sigma12InheritedBudget S H M D ⌈↑D ^ (1 / 2)⌉₊ C K d Δ 2
Even s=2 Case-I pointwise producer with fixed induction threshold 2.
There is no eventual quantifier after K; the source separator pays the finite
geometry, source-coordinate, error-transport, Claim-14.6, and Σ₁₂ cutoffs.
theorem
MathlibNt.SieveTheory.exists_lemma14_4_caseI_evenEndpoint_sourceLargeLog_pointwise
(S : BoundingSieve)
(H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers)
{d Δ Θ : ℝ}
(hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H)
(hsrc : SuzukiClaim145SourceParameters d Δ Θ)
:
∃ (C1min : ℝ) (CB : ℝ),
1 ≤ C1min ∧ 0 < CB ∧ ∀ (C1 C K : ℝ) (M D : ℕ),
C1min ≤ C1 →
max 3 CB ≤ C →
2 ≤ K →
SwitchingPrinciple.HasDimensionOneLocalProductBound S K →
Even M →
2 ≤ M →
C1 * K ^ Θ < Real.log ↑D →
Lemma144MovingDomainGlobalDepthAt S H C K d Δ (M - 1) 2 →
suzukiActualT S M D ⌈↑D ^ (1 / 2)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / 2)⌉₊ * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 M 2 + sigma12InheritedBudget S H M D ⌈↑D ^ (1 / 2)⌉₊ C K d Δ 2
Compatibility specialization of the producer uniform in the bounding sieve.