theorem MathlibNt.SieveTheory.suzukiSigmaZero_eq_actualT_sourceSigma_strict (S : BoundingSieve) {N D z : ℕ} {d : ℝ} (hN : 2 ≤ N) (hz : ↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ ↑z) (hOddCarrier : Odd N → ∀ p < ⌈↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)⌉₊, p ^ 3 < D) : suzukiSigmaZero S N D z (↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)) = suzukiActualT S N D ⌈↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)⌉₊

The strict source carrier at the single sourceSigma endpoint recombines Σ₀ into the actual parity sum. The natural ceiling is retained literally; only primes strictly below it are used in the odd cubic side condition.

theorem MathlibNt.SieveTheory.suzukiSigmaZero_eq_actualT_sourceSigma_even (S : BoundingSieve) {N D z : ℕ} {d : ℝ} (hN : 2 ≤ N) (hEven : Even N) (hz : ↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ ↑z) : suzukiSigmaZero S N D z (↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)) = suzukiActualT S N D ⌈↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)⌉₊

At even depth the odd side condition is vacuous, so the same exact source recurrence holds without a cubic-ceiling surrogate.

theorem MathlibNt.SieveTheory.claim145_caseB_sigmaZero_uniform_strict_in_S (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ Θ : ℝ} (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hTheta : 1 ≤ Θ) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ∃ (C1min : ℝ) (CB : ℝ), 0 < C1min ∧ 0 < CB ∧ ∀ (S : BoundingSieve) (C1 C K : ℝ) (N D z : ℕ), C1min ≤ C1 → CB ≤ C → 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → C1 * K ^ Θ < Real.log ↑D → 2 ≤ N → ↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ ↑z → suzukiSigmaZero S N D z (↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)) ≤ CB / C * (C * SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N (↑D) d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) K (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d))

Source-large, non-eventual Σ₀ closure, with all Case-B constants selected uniformly before the varying bounding sieve S, then before C1, the common constant C, K, depth and D. The displayed relative coefficient is exactly CB / C; allowing C ≥ CB makes it at most one.

theorem MathlibNt.SieveTheory.claim145_caseB_sigmaZero_uniform_strict (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ Θ : ℝ} (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hTheta : 1 ≤ Θ) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ∃ (C1min : ℝ) (CB : ℝ), 0 < C1min ∧ 0 < CB ∧ ∀ (C1 C K : ℝ) (N D z : ℕ), C1min ≤ C1 → CB ≤ C → 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → C1 * K ^ Θ < Real.log ↑D → 2 ≤ N → ↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ ↑z → suzukiSigmaZero S N D z (↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)) ≤ CB / C * (C * SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N (↑D) d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) K (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d))

Compatibility specialization of the strict uniform-in-S Case-B closure.

theorem MathlibNt.SieveTheory.claim145_caseB_sigmaZero_uniform_even_in_S (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ Θ : ℝ} (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hTheta : 1 ≤ Θ) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ∃ (C1min : ℝ) (CB : ℝ), 0 < C1min ∧ 0 < CB ∧ ∀ (S : BoundingSieve) (C1 C K : ℝ) (N D z : ℕ), C1min ≤ C1 → CB ≤ C → 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → C1 * K ^ Θ < Real.log ↑D → Even N → 2 ≤ N → ↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ ↑z → suzukiSigmaZero S N D z (↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)) ≤ CB / C * (C * SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N (↑D) d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) K (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d))

Even-depth specialization, still uniform in the varying bounding sieve.

theorem MathlibNt.SieveTheory.claim145_caseB_sigmaZero_uniform_even (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ Θ : ℝ} (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hTheta : 1 ≤ Θ) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ∃ (C1min : ℝ) (CB : ℝ), 0 < C1min ∧ 0 < CB ∧ ∀ (C1 C K : ℝ) (N D z : ℕ), C1min ≤ C1 → CB ≤ C → 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → C1 * K ^ Θ < Real.log ↑D → Even N → 2 ≤ N → ↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ ↑z → suzukiSigmaZero S N D z (↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)) ≤ CB / C * (C * SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N (↑D) d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) K (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d))

Compatibility specialization of the even uniform-in-S Case-B closure.