theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier_filter_lt_eq (support : Finset ℕ) {D z : ℕ} {σ τ : ℝ} (hvz : ↑D ^ (1 / τ) ≤ ↑z) : sigmaOneCarrier ({p ∈ support | p < z}) D σ τ = sigmaOneCarrier support D σ τ

Restricting a support to primes below z does not change the middle carrier when its upper cutoff is at most z.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaTwelve_filter_lt_eq (support : Finset ℕ) (omega V : ℕ → ℝ) (E : ℕ → ℕ → ℝ → ℝ) (Vz C K Δ : ℝ) (N D z : ℕ) (σ τ : ℝ) (hvz : ↑D ^ (1 / τ) ≤ ↑z) : sigmaTwelve ({p ∈ support | p < z}) omega V E Vz C K Δ N D σ τ = sigmaTwelve support omega V E Vz C K Δ N D σ τ

sigmaTwelve is exactly unchanged when its full support is replaced by that support cut off below z, provided the middle upper cutoff lies below z. This is equality, not merely monotonicity.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier_supportedBelow_eq_full (S : BoundingSieve) {D z : ℕ} {σ τ : ℝ} (hvz : ↑D ^ (1 / τ) ≤ ↑z) : sigmaOneCarrier ({p ∈ S.prodPrimes.primeFactors | p < z}) D σ τ = sigmaOneCarrier S.prodPrimes.primeFactors D σ τ

Bounding-sieve specialization: this is the exact carrier represented by suzukiSupportedBelow S z after unfolding that definition.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaTwelve_supportedBelow_eq_full (S : BoundingSieve) (V : ℕ → ℝ) (E : ℕ → ℕ → ℝ → ℝ) (Vz C K Δ : ℝ) (N D z : ℕ) (σ τ : ℝ) (hvz : ↑D ^ (1 / τ) ≤ ↑z) : sigmaTwelve ({p ∈ S.prodPrimes.primeFactors | p < z}) (⇑S.nu) V E Vz C K Δ N D σ τ = sigmaTwelve S.prodPrimes.primeFactors (⇑S.nu) V E Vz C K Δ N D σ τ

Exact supported/full sigmaTwelve equality for a bounding sieve. The left support is definitionally the finite set used by suzukiSupportedBelow.