theorem MathlibNt.SieveTheory.finiteSourceLayer_one_eq_lowStrip {s : ℝ} (hs3 : s ≤ 3) : SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 1 s = (3 - s) / s

At depth one the finite continuous source layer is the literal initial function (3-s)/s throughout the low strip.

theorem MathlibNt.SieveTheory.section13Hat_plus_initial_lowStrip {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) {s : ℝ} (hs : 0 < s) (hs3 : s ≤ 3) : H.Tplus s = 1 / s ^ 2

The Section 13 plus-hat initial condition at β=2, written in the normalization occurring in the depth-one error envelope.

theorem MathlibNt.SieveTheory.one_div_le_errorEnvelope_one_lowStrip {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) {D d s : ℝ} (hD : 1 < D) (hs : 0 < s) (hs3 : s ≤ 3) : 1 / s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H 1 D d s

On the low strip the exact hat initial value gives the uniform lower bound 1/s for the depth-one production error envelope.

theorem MathlibNt.SieveTheory.exists_baseOne_localError_sameC_threshold {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) {d Δ C K : ℝ} (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hC : 0 < C) (hK : 2 ≤ K) : ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∀ (s : ℝ), 1 < s → s ≤ 3 → 9 * K / (s * Real.log D) ≤ C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H 1 D d s * Real.log D ^ (-Δ)

A completely explicit eventual comparison of the local depth-one remainder with the same fixed C error budget. The threshold is chosen before s, so this is uniform on 1 < s ≤ 3.

theorem MathlibNt.SieveTheory.suzukiVProduct_nonneg (S : BoundingSieve) (x : ℝ) : 0 ≤ SwitchingPrinciple.suzukiVProduct S x

The Euler product multiplying both base-one brackets is nonnegative.

theorem MathlibNt.SieveTheory.two_le_rpow_inv_lowStrip {D s : ℝ} (hD : 0 < D) (hlog3 : 3 ≤ Real.log D) (hs : 1 < s) (hs3 : s ≤ 3) : 2 ≤ D ^ (1 / s)

log D ≥ 3 is a uniform root threshold for every 1 < s ≤ 3.

theorem MathlibNt.SieveTheory.lemma14_4_caseII_base_one_sameC_uniform {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) {d Δ C K : ℝ} (hd : 0 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hC : 0 < C) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) : ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℕ), D₀ ≤ ↑D → 3 ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ∧ ∀ (s : ℝ), 1 < s → s ≤ 3 → Lemma144CaseIISameCAt S H 1 D d Δ C K s

Actual Case-II N=1 closure with one fixed C. A single threshold is chosen before the low-strip parameter s; it simultaneously enforces the source value 3 ≤ sourceSigma D d, the natural-ceiling base geometry, and the uniform absorption of 9K/(s log D).

theorem MathlibNt.SieveTheory.lemma14_4_caseII_base_one_sameC_producer {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) {d Δ C K s : ℝ} (hd : 0 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hC : 0 < C) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hs : 1 < s) (hs3 : s ≤ 3) : Lemma144CaseIIBaseOneSameCProducer S H d Δ C K s

The exact producer requested by the Case-II dispatcher, now discharged from source data. It is a specialization of the stronger threshold-before-s uniform theorem above and therefore uses the identical constant C.