theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.eventually_all_depth_suzuki_error_half (H : Section13HatLayers) {β C K s : ℝ} (hH : Section13HatContract H β) (hC : 0 ≤ C) (hs : 0 < s) (ρ : ℝ) (hρ : 0 < ρ) : ∀ᶠ (D : ℝ) in Filter.atTop, ∀ (depth : ℕ), 0 ≤ C * Real.exp √K * errorEnvelope H depth D 16 s * Real.log D ^ (-(1 / 2)) ∧ C * Real.exp √K * errorEnvelope H depth D 16 s * Real.log D ^ (-(1 / 2)) < ρ

At the legal source choice Δ = 1/2, the Suzuki error is absorbed uniformly in the recursion depth. This uses the literal errorEnvelope: depth only chooses one of the two Section-13 hat layers.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.tendsto_chenLevel_atTop {ε : ℝ} (hε : ε < 1 / 10) : Filter.Tendsto (fun (N : ℕ) => ↑(chenLevel N ε)) Filter.atTop Filter.atTop

Chen's floor level tends to infinity for every ε < 1/2. The proof keeps the floor explicit and uses the fixed lower exponent 2/5 in the Chen range.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.chen_half_parameters_admissible {ε : ℝ} (hε0 : 0 ≤ ε) (hε : ε < 1 / 10) : 0 < 1 / 2 ∧ 1 / 2 < 1 ∧ 7 / (1 - 1 / 2) < 16 ∧ 0 < chenS ε ∧ chenS ε ≤ 5

The fixed choices used in the production theorem are simultaneously legal: Δ = Θ = 1/2, d = 16, and Chen's s = 5 - 10ε stays positive.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.chen_eventually_all_depth_suzuki_error_absorption (H : Section13HatLayers) {β C K ε : ℝ} (hH : Section13HatContract H β) (hC : 0 ≤ C) (hε0 : 0 ≤ ε) (hε : ε < 1 / 10) (ρ : ℝ) (hρ : 0 < ρ) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → ∀ (depth : ℕ), C * Real.exp √K * errorEnvelope H depth (↑(chenLevel N ε)) 16 (chenS ε) * Real.log ↑(chenLevel N ε) ^ (-(1 / 2)) < ρ

Production Chen-parameter absorption, uniform in all depths. In particular, the depth may grow with the supported prime carrier. No uniform comparison proposition is assumed: parity is eliminated directly from the literal Section-13 errorEnvelope.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.chen_eventually_adaptive_depth_suzuki_error_absorption (H : Section13HatLayers) {β C K ε : ℝ} (hH : Section13HatContract H β) (hC : 0 ≤ C) (hε0 : 0 ≤ ε) (hε : ε < 1 / 10) (Nadapt : ℕ → ℕ) (ρ : ℝ) (hρ : 0 < ρ) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → C * Real.exp √K * errorEnvelope H (Nadapt N) (↑(chenLevel N ε)) 16 (chenS ε) * Real.log ↑(chenLevel N ε) ^ (-(1 / 2)) < ρ

Adaptive-depth corollary: Nadapt is completely arbitrary and hence may track the growing finite carrier.