theorem MathlibNt.SieveTheory.claim145_sourceSigma_allS_internal_of_scalar (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ K C145 D₀ C M : ℝ} (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hK : 0 < K) (hC145 : 0 < C145) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hM3 : 3 ≤ M) (hprop : ∀ (sign : SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) (t : ℝ), M ≤ t → SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiLowerProfile C t ≤ H.T sign t) (hD₀ : 1 < D₀) (hscalar : ∀ (D : ℕ) (s : ℝ), D₀ ≤ ↑D → SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ≤ s → 0 < SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ∧ M ≤ s ∧ Real.exp 1 * suzukiSourceL (↑D) K ≤ s - 2 ∧ Real.exp (suzukiSourceL (↑D) K + (s - 2) * (1 + Real.log (suzukiSourceL (↑D) K) - Real.log (s - 2))) ≤ C145 * (SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5VProduct S ↑D * (Real.exp √K / (Real.log ↑D * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)) * ((1 + s ^ d / Real.log ↑D) ^ s * s * SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiLowerProfile C s) * Real.log ↑D ^ (-Δ))) (D N : ℕ) (s : ℝ) : D₀ ≤ ↑D → SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ≤ s → suzukiActualT S N D ⌈↑D ^ (1 / s)⌉₊ ≤ C145 * SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N (↑D) d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) K s

Literal all-s Case-B interface. The source scalar inequalities are kept elementary: they mention neither the discrete tail nor claim14_5Scale. This separates the actual Lemma-14.3/(14.6) closure from the remaining uniform calculus estimate.

theorem MathlibNt.SieveTheory.claim145_sourceSigma_allS_internal (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ K C145 : ℝ} (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hK : 0 < K) (hC145 : 0 < C145) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D N : ℕ) (s : ℝ), D₀ ≤ ↑D → SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ≤ s → suzukiActualT S N D ⌈↑D ^ (1 / s)⌉₊ ≤ C145 * SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N (↑D) d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) K s

Source-faithful Claim 14.5, Case B, on the complete half-line s ≥ sourceSigma D d. The common threshold is chosen before D, N, and s; no support-vanishing or endpoint specialization is used.

theorem MathlibNt.SieveTheory.claim145_sourceSigma_endpoint_internal (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ K C145 : ℝ} (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hK : 0 < K) (hC145 : 0 < C145) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D N : ℕ), D₀ ≤ ↑D → suzukiActualT S N D ⌈↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)⌉₊ ≤ C145 * SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N (↑D) d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) K (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)

Source-faithful Claim 14.5 at Suzuki's moving sourceSigma endpoint. One threshold is chosen before both natural parameters D and N, and the endpoint is the literal natural ceiling.

theorem MathlibNt.SieveTheory.exists_claim145_sourceSigma_allS_internal (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ K : ℝ} (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hK : 0 < K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ∃ (C145 : ℝ), 0 < C145 ∧ ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D N : ℕ) (s : ℝ), D₀ ≤ ↑D → SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ≤ s → suzukiActualT S N D ⌈↑D ^ (1 / s)⌉₊ ≤ C145 * SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N (↑D) d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) K s

Quantifier-closed full Case-B form, with the positive Claim-14.5 constant chosen before the common threshold and all three varying parameters.

theorem MathlibNt.SieveTheory.exists_claim145_sourceSigma_endpoint_internal (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ K : ℝ} (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hK : 0 < K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ∃ (C145 : ℝ), 0 < C145 ∧ ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D N : ℕ), D₀ ≤ ↑D → suzukiActualT S N D ⌈↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)⌉₊ ≤ C145 * SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N (↑D) d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) K (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)

Quantifier-closed endpoint form: choose the positive Claim-14.5 constant before the common threshold and before both natural parameters.