structure MathlibNt.SieveTheory.Claim145SourceParameterPacket (Δ₀ Δ d Θ : ℝ) : Prop

The parameter inequalities chosen on Suzuki p.81, equations (14.3) and (14.4). Keeping them together prevents later consumers from silently assuming extra size conditions on Θ.

• delta0_le_one : Δ₀ ≤ 1
• delta_nonneg : 0 ≤ Δ
• d_pos : 0 < d
• theta_pos : 0 < Θ
• equation14_3 : 2 / d < 1 / Θ
• equation14_4 : 2 / Θ + 3 / d < Δ₀ - Δ

theorem MathlibNt.SieveTheory.Claim145SourceParameterPacket.two_lt_theta {Δ₀ Δ d Θ : ℝ} (h : Claim145SourceParameterPacket Δ₀ Δ d Θ) : 2 < Θ

Equation (14.4), together with the source range Δ₀ ≤ 1 and Δ ≥ 0, forces the auxiliary exponent to exceed two. In particular the 1 ≤ Θ condition used by the uniform Case-B logarithmic bookkeeping is not an added hypothesis.

theorem MathlibNt.SieveTheory.Claim145SourceParameterPacket.one_le_theta {Δ₀ Δ d Θ : ℝ} (h : Claim145SourceParameterPacket Δ₀ Δ d Θ) : 1 ≤ Θ

theorem MathlibNt.SieveTheory.Claim145SourceParameterPacket.highS_gap {Δ₀ Δ d Θ : ℝ} (h : Claim145SourceParameterPacket Δ₀ Δ d Θ) : 0 < d - 2 * Θ

The same packet supplies the positive high-coordinate exponent gap.

structure MathlibNt.SieveTheory.SuzukiClaim145SourceParameters (d Δ Θ : ℝ) : Prop

Exact specialized source packet on Suzuki p.81 for κ = κ̂ = 1, where Δ₀ = 1.

• hDelta_pos : 0 < Δ
• hDelta_lt : Δ < 1
• h14_1 : 7 / (1 - Δ) < d
• hTheta_pos : 0 < Θ
• h14_3 : 2 / d < 1 / Θ
• h14_4 : 2 / Θ + 3 / d < 1 - Δ

theorem MathlibNt.SieveTheory.SuzukiClaim145SourceParameters.d_pos {d Δ Θ : ℝ} (h : SuzukiClaim145SourceParameters d Δ Θ) : 0 < d

theorem MathlibNt.SieveTheory.SuzukiClaim145SourceParameters.two_lt_theta {d Δ Θ : ℝ} (h : SuzukiClaim145SourceParameters d Δ Θ) : 2 < Θ

theorem MathlibNt.SieveTheory.SuzukiClaim145SourceParameters.one_le_theta {d Δ Θ : ℝ} (h : SuzukiClaim145SourceParameters d Δ Θ) : 1 ≤ Θ

theorem MathlibNt.SieveTheory.SuzukiClaim145SourceParameters.toGeneric {d Δ Θ : ℝ} (h : SuzukiClaim145SourceParameters d Δ Θ) : Claim145SourceParameterPacket 1 Δ d Θ