theorem MathlibNt.SieveTheory.exists_claim145_source_complete_uniform_in_S (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {Δ₀ Δ d Θ : ℝ} (hparam : Claim145SourceParameterPacket Δ₀ Δ d Θ) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ∃ (C1min : ℝ) (CB : ℝ), 0 < C1min ∧ 0 < CB ∧ ∀ (C1 : ℝ), C1min ≤ C1 → ∃ (C145 : ℝ), 0 < C145 ∧ ∀ (S : BoundingSieve) (K : ℝ) (N D : ℕ) (s : ℝ), 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → 2 ≤ s → Real.log ↑D ≤ C1 * K ^ Θ ∨ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ≤ s → ActualClaim145BoundAt S H N D d Δ K s C145

Fully inhabited Suzuki Claim 14.5 with its final constants chosen before a varying bounding sieve, as required by the source dependence in Lemma 14.4.

theorem MathlibNt.SieveTheory.exists_claim145_source_complete (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {Δ₀ Δ d Θ : ℝ} (hparam : Claim145SourceParameterPacket Δ₀ Δ d Θ) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ∃ (C1min : ℝ) (CB : ℝ), 0 < C1min ∧ 0 < CB ∧ ∀ (C1 : ℝ), C1min ≤ C1 → ∃ (C145 : ℝ), 0 < C145 ∧ ∀ (K : ℝ) (N D : ℕ) (s : ℝ), 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → 2 ≤ s → Real.log ↑D ≤ C1 * K ^ Θ ∨ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ≤ s → ActualClaim145BoundAt S H N D d Δ K s C145

Fully inhabited Suzuki Claim 14.5 with the source order of constants. C1min and the Case-B constant are chosen before the varying C1; after a legal C1 is fixed, the common Claim-14.5 constant is chosen before K,N,D,s.