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.