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

The exact uniform-in-S production interface still owed by complete Claim 14.5. Its constants are selected from the source data before the bounding sieve, local-product constant, depth, discrete parameter, and coordinate.

Equations

• MathlibNt.SieveTheory.Claim145SourceCompleteUniformInS H d Δ Θ = ∃ (C1min : ℝ) (CB : ℝ), 0 < C1min ∧ 0 < CB ∧ ∀ (C1 : ℝ), C1min ≤ C1 → ∃ (C145 : ℝ), 0 < C145 ∧ ∀ (S : BoundingSieve) (K : ℝ) (N D : ℕ) (s : ℝ), 2 ≤ K → MathlibNt.SieveTheory.SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → 2 ≤ s → Real.log ↑D ≤ C1 * K ^ Θ ∨ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ≤ s → MathlibNt.SieveTheory.ActualClaim145BoundAt S H N D d Δ K s C145

theorem MathlibNt.SieveTheory.claim145_odd_lowStrip_smallLog_actual_uniform_in_S (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ C1 Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hC1 : 0 ≤ C1) (hΘ : 0 < Θ) (hd : 0 < d) (hsource : 2 / d < 1 / Θ) (hΔ0 : 0 ≤ Δ) (hΔ1 : Δ ≤ 1) : ∃ (C145 : ℝ), 0 ≤ C145 ∧ ∀ (S : BoundingSieve) (K : ℝ) (N D : ℕ) (s : ℝ), 2 ≤ K → Odd N → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → 1 < s → s ≤ 2 → Real.log ↑D ≤ C1 * K ^ Θ → ActualClaim145BoundAt S H N D d Δ K s C145

Suzuki's omitted odd strip can be extended with one coefficient selected before S. This is deliberately separate from complete Claim 14.5: the latter has the printed domain 2 ≤ s, while this extension has 1 < s ≤ 2.

theorem MathlibNt.SieveTheory.exists_lemma14_4_literal_allDepth_with_lowStrip_extension_uniform_in_S (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hsrc : SuzukiClaim145SourceParameters d Δ Θ) (hclaimUniform : Claim145SourceCompleteUniformInS H d Δ Θ) : ∃ (C1min : ℝ), 0 < C1min ∧ ∀ (C1 : ℝ), C1min ≤ C1 → ∃ (C145 : ℝ) (Clow : ℝ) (C : ℝ), 0 < C145 ∧ 0 ≤ Clow ∧ 3 ≤ C ∧ ∀ (S : BoundingSieve) (K : ℝ), 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → ∀ (N : ℕ), 1 ≤ N → Lemma144MovingDomainNatCeilAt S H C K d Δ N 2

Literal all-depth, cutoff-two Lemma 14.4 uniformly in the bounding sieve.

The source order is encoded in the conclusion: source data → C1min → C1 → C145, Clow, C → S,K,N,D,s. The printed Claim-14.5 region (2 ≤ s) and its complement are preserved. On odd successor depths the non-source-large low strip 1 < s < 2 is routed to the explicit extension above; no false 2 ≤ s is manufactured. The remaining source-large complement is split into Case II (s ≤ 3), the even endpoint s = 2, and strict Case I. The induction threshold is literally 2; there is no Dmin induction or eventual quantifier.

The sole premise is the exact complete Claim-14.5 uniform-in-S producer.

theorem MathlibNt.SieveTheory.exists_lemma14_4_literal_allDepth_with_lowStrip_extension_uniform_in_S_of_source (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hsrc : SuzukiClaim145SourceParameters d Δ Θ) : ∃ (C1min : ℝ), 0 < C1min ∧ ∀ (C1 : ℝ), C1min ≤ C1 → ∃ (C145 : ℝ) (Clow : ℝ) (C : ℝ), 0 < C145 ∧ 0 ≤ Clow ∧ 3 ≤ C ∧ ∀ (S : BoundingSieve) (K : ℝ), 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → ∀ (N : ℕ), 1 ≤ N → Lemma144MovingDomainNatCeilAt S H C K d Δ N 2

Historical compatibility name for the uniform cutoff-two, moving-range, natural-ceiling specialization of Suzuki Lemma 14.4. Despite literal in the identifier, the conclusion is restricted to x ≤ sourceSigma D d; it is not the full printed all-s ∈ I_N statement. The Claim 14.5 producer is constructed internally from the source parameter packet.

theorem MathlibNt.SieveTheory.exists_lemma14_4_movingRange_rounded_allDepth_uniform_in_S_of_source (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hsrc : SuzukiClaim145SourceParameters d Δ Θ) : ∃ (C1min : ℝ), 0 < C1min ∧ ∀ (C1 : ℝ), C1min ≤ C1 → ∃ (C145 : ℝ) (Clow : ℝ) (C : ℝ), 0 < C145 ∧ 0 ≤ Clow ∧ 3 ≤ C ∧ ∀ (S : BoundingSieve) (K : ℝ), 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → ∀ (N : ℕ), 1 ≤ N → Lemma144MovingDomainNatCeilAt S H C K d Δ N 2

Scope-faithful public name for the theorem above: all depths, but only the moving range x ≤ sourceSigma D d and the rounded natural cutoff.