Chen--Suzuki floor/ceiling coordinate bridge

This module contains the parameter arithmetic only. It is deliberately independent of the sieve implementation, so the eventual estimates do not rely on a finite scan.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.chenLevel (N : ℕ) (ε : ℝ) : ℕ

Chen's natural level D = floor(N^(1/2-epsilon))+1.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.chenLevel N ε = ⌊↑N ^ (1 / 2 - ε)⌋₊ + 1

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.chenS (ε : ℝ) : ℝ

Chen's upper Suzuki coordinate.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.chenS ε = 5 - 10 * ε

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.chenZ (N : ℕ) (ε : ℝ) : ℕ

The natural cutoff associated to Chen's upper Suzuki coordinate.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.chenZ N ε = ⌈↑(MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.chenLevel N ε) ^ (1 / MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.chenS ε)⌉₊

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lt_cast_floor_add_one (x : ℝ) : x < ↑(⌊x⌋₊ + 1)

Adding one after taking the natural floor strictly dominates the original real number.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.chen_exponent_div_s {ε : ℝ} (hε : ε < 1 / 2) : (1 / 2 - ε) * (1 / chenS ε) = 1 / 10

The identity behind Chen's exponent choice: (1/2-epsilon)/(5-10 epsilon)=1/10.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.chen_lt_tenth_rpow_imp_lt_chenZ {N p : ℕ} {ε : ℝ} (hN : 1 ≤ N) (_hε0 : 0 ≤ ε) (hε : ε < 1 / 10) (hp : ↑p < ↑N ^ (1 / 10)) : p < chenZ N ε

Exact, scan-free floor/rpow/ceiling bridge. Every natural below Chen's N^(1/10) cutoff is strictly below the Suzuki natural cutoff z.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.mem_filter_lt_chenZ_of_lt_tenth_rpow {N p : ℕ} {ε : ℝ} (P : Finset ℕ) (hN : 1 ≤ N) (hε0 : 0 ≤ ε) (hε : ε < 1 / 10) (hpP : p ∈ P) (hp : ↑p < ↑N ^ (1 / 10)) : p ∈ {q ∈ P | q < chenZ N ε}

The same bridge packaged as membership in an arbitrary supported carrier. This is the precise shape needed when P is the production prime-factor carrier.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.chenSigmaThreshold : ℝ

A convenient explicit threshold for the fixed Claim-14.5 choice d=16.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.chenSigmaThreshold = Real.exp (max (5 ^ 16) (Real.exp 1))

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.chenS_le_sourceSigma_sixteen {D ε : ℝ} (hε0 : 0 ≤ ε) (hD : chenSigmaThreshold ≤ D) : chenS ε ≤ sourceSigma D 16

Above the explicit threshold, the fixed Claim-14.5 coordinate d=16 dominates every Chen s=5-10 epsilon with nonnegative epsilon.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.exists_chen_floor_level_sourceSigma_gate : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → ∀ (ε : ℝ), 0 ≤ ε → ε < 1 / 10 → chenS ε ≤ sourceSigma (↑(chenLevel N ε)) 16

Eventual Chen-to-Suzuki coordinate gate, with a concrete natural threshold and the source-valid fixed choice d=16 (for example 16 > 7/(1-1/2)).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sixteen_claim14_5_admissible : 7 / (1 - 1 / 2) < 16

The fixed value used above satisfies Claim 14.5's source inequality at Delta=1/2.