theorem MathlibNt.SieveTheory.caseITau_eq_s_of_beta_le {β D s : ℝ} (hβ : 1 < β) (hβs : β ≤ s) (hDcorr : 1 / β ≤ 1 - Real.log 2 / Real.log D) : caseITau D s = s

For Case I, the finite-D correction in τ is inactive once its reciprocal denominator is at least 1/β.

theorem MathlibNt.SieveTheory.caseITau_eq_s_of_log_threshold {β D s : ℝ} (hβ : 1 < β) (hβs : β ≤ s) (hD : 1 < D) (hDlarge : β * Real.log 2 ≤ (β - 1) * Real.log D) : caseITau D s = s

A logarithmic threshold stated directly in D implies the correction condition above. This is the source-relevant explicit large-D form.

theorem MathlibNt.SieveTheory.caseITau_eq_s_of_claim14_5CaseI {β D s σ : ℝ} {N : ℕ} (hβ : 1 < β) (hcaseI : SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5CaseI β N s σ) (hD : 1 < D) (hDlarge : β * Real.log 2 ≤ (β - 1) * Real.log D) : caseITau D s = s

Exact Case-I wrapper: β + ε_N ≤ s supplies β ≤ s, so the explicit logarithmic threshold forces τ=s.

theorem MathlibNt.SieveTheory.caseI_tauCut_eq_z_of_power_coordinate {D z : ℕ} {s : ℝ} (hτ : caseITau (↑D) s = s) (hz : ↑D ^ (1 / s) = ↑z) : ↑D ^ (1 / caseITau (↑D) s) = ↑z

Once τ=s, the Case-I power coordinate identifies the upper split cutoff with the source cutoff z.

theorem MathlibNt.SieveTheory.caseI_sigma2_filter_eq_empty (S : BoundingSieve) {D z : ℕ} {s : ℝ} (hτ : caseITau (↑D) s = s) (hz : ↑D ^ (1 / s) = ↑z) : {p ∈ SwitchingPrinciple.suzukiSupportedBelow S z | ↑D ^ (1 / caseITau (↑D) s) ≤ ↑p} = ∅

The Σ₂ carrier in the exact three-range decomposition is empty in Case I.

theorem MathlibNt.SieveTheory.caseI_sigma2_sum_eq_zero (S : BoundingSieve) {D z : ℕ} {s : ℝ} (hτ : caseITau (↑D) s = s) (hz : ↑D ^ (1 / s) = ↑z) (f : ℕ → ℝ) : ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z with ↑D ^ (1 / caseITau (↑D) s) ≤ ↑p, f p = 0

Consequently every Σ₂ sum in the source recurrence vanishes.

theorem MathlibNt.SieveTheory.caseI_sigma0_eq_sigma_endpoint (S : BoundingSieve) {D z : ℕ} {σ s : ℝ} (hdom : CaseIThreeRangeDomain D z σ s) (hτ : caseITau (↑D) s = s) (hz : ↑D ^ (1 / s) = ↑z) (f : ℕ → ℝ) : ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z with ↑p < ↑D ^ (1 / σ), f p = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / σ)⌉₊, f p

In a CaseIThreeRangeDomain, Σ₀ is literally the endpoint sum whose strict cutoff is D^(1/σ).

theorem MathlibNt.SieveTheory.claim14_5_sigma_endpoint_regime {β D σ C1 K ΘK : ℝ} (hβσ : β ≤ σ) : SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5Regime β D σ C1 K ΘK σ

The endpoint parameter s'=σ lies in Claim 14.5's already-closed regime by the second alternative σ ≤ s'; no induction hypothesis is involved.

theorem MathlibNt.SieveTheory.claim14_5_sigma_endpoint_regime_of_caseI {β D s σ C1 K ΘK : ℝ} {N : ℕ} (hcaseI : SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5CaseI β N s σ) : SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5Regime β D σ C1 K ΘK σ

Case I itself supplies the lower endpoint condition needed at s'=σ.

theorem MathlibNt.SieveTheory.caseI_sigma0_le_of_claim14_5_sigma_endpoint (S : BoundingSieve) {D z N : ℕ} {σ s β C1 K ΘK B : ℝ} (hdom : CaseIThreeRangeDomain D z σ s) (hτ : caseITau (↑D) s = s) (hz : ↑D ^ (1 / s) = ↑z) (hcaseI : SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5CaseI β N s σ) (f : ℕ → ℝ) (hendpoint : SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5Regime β (↑D) σ C1 K ΘK σ → ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / σ)⌉₊, f p ≤ B) : ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z with ↑p < ↑D ^ (1 / σ), f p ≤ B

Package the Σ₀ transport through the already-closed s'=σ regime of Claim 14.5. The endpoint provider is explicitly keyed by Claim14_5Regime, rather than by an induction hypothesis at the current s.

theorem MathlibNt.SieveTheory.suzukiSourceParitySum_recurrence_caseI_two_ranges (S : BoundingSieve) {N D z : ℕ} {σ s : ℝ} (hN2 : 2 ≤ N) (hbase : Odd N → suzukiSourceV S 1 D z = 0) (hcube : ∀ n ∈ sourceParityIndices N, 2 ≤ n → Odd n → ∀ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, p ^ 3 < D) (hdom : CaseIThreeRangeDomain D z σ s) (hτ : caseITau (↑D) s = s) (hz : ↑D ^ (1 / s) = ↑z) : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D z = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z with ↑p < ↑D ^ (1 / σ), S.nu p * ∑ m ∈ sourceParityIndices (N - 1), suzukiSourceV S m (D ⌈/⌉ p) p + ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z with ↑D ^ (1 / σ) ≤ ↑p ∧ ↑p < ↑D ^ (1 / caseITau (↑D) s), S.nu p * ∑ m ∈ sourceParityIndices (N - 1), suzukiSourceV S m (D ⌈/⌉ p) p

The current source-faithful recurrence with Case-I Σ₂ deleted.