theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayerNumerator_eq_sourceRecursion_of_two_le (β s : ℝ) {n : ℕ} (hn : 2 ≤ n) : suzukiLayerNumerator 1 β n s = ∫ (t : ℝ) in recursionLower β s n..β + ↑n, suzukiLayer 1 β (n - 1) (t - 1)

Every source layer of index at least two is its normalized predecessor integral.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer_continuousOn_parityDomain {β : ℝ} (hβ : 1 < β) (N : ℕ) : ContinuousOn (finiteSourceLayer 1 β N) (KappaOneModel.parityDomain β N)

Proposition 9.3, κ=1: the finite source layer is continuous on its exact Suzuki parity domain.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer_nonneg_on_parityDomain {β : ℝ} (hβ : 1 < β) (N : ℕ) {s : ℝ} (hs : s ∈ KappaOneModel.parityDomain β N) : 0 ≤ finiteSourceLayer 1 β N s

Proposition 9.3, κ=1: finite source layers are nonnegative on their exact Suzuki parity domains.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer_weighted_antitoneOn_parityDomain {β : ℝ} (hβ : 1 < β) (N : ℕ) : AntitoneOn (fun (s : ℝ) => s * finiteSourceLayer 1 β N s) (KappaOneModel.parityDomain β N)

Proposition 9.3, κ=1: the source-weighted finite layer is antitone on the exact parity domain.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer_antitoneOn_parityDomain {β : ℝ} (hβ : 1 < β) (N : ℕ) : AntitoneOn (finiteSourceLayer 1 β N) (KappaOneModel.parityDomain β N)

Proposition 9.3, κ=1: the finite source layer itself is antitone on the exact parity domain.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer_eq_zero_of_le (β : ℝ) (N : ℕ) {s : ℝ} (hs : β + ↑N ≤ s) : finiteSourceLayer 1 β N s = 0

Support vanishing: after the largest source endpoint every summand, hence its finite parity sum, is zero. No parity-domain hypothesis is needed.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer_add_two (β : ℝ) (N : ℕ) (s : ℝ) : finiteSourceLayer 1 β (N + 2) s = finiteSourceLayer 1 β N s + suzukiLayer 1 β (N + 2) s

Finite parity step identity: increasing the source cutoff by two preserves its parity and adds exactly the new terminal source layer.