High-order support of the actual small-weight density boundaries

For the source parameters L = D^ε, u = D^(ε²), a failed cubic test L ≤ (∏ s) q³ involving small primes forces 1 < ε (|s| + 3). The finite boundary kernels are therefore sums over these high layers only. This localizes the explicit errors; it does not estimate their total size.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.small_cubic_failure_card (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) {q : ℕ} {s : Finset ℕ} (hq : q ∈ geometricSmallPrimes P D ε) (hs : s ⊆ geometricSmallPrimes P D ε) (hfail : D ^ ε ≤ ↑(s.prod id) * ↑q ^ 3) : 1 < ε * (↑s.card + 3)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSmallBoundary_highLayer (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) {q : ℕ} {s : Finset ℕ} (hq : q ∈ geometricSmallPrimes P D ε) (hs : s ⊆ geometricSmallPrimes P D ε) (hb : LowerBoundary (D ^ ε) q s) : ¬Even s.card ∧ 1 < ε * (↑s.card + 3)

Lower boundaries have odd tail length and start beyond 1/ε - 3.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSmallBoundary_highLayer (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) {q : ℕ} {s : Finset ℕ} (hq : q ∈ geometricSmallPrimes P D ε) (hs : s ⊆ geometricSmallPrimes P D ε) (hb : UpperBoundary (D ^ ε) q s) : Even s.card ∧ 1 < ε * (↑s.card + 3)

Upper boundaries have even tail length and start beyond 1/ε - 3.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerBoundaryDensity_eq_highLayers (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (g : ℕ → ℝ) {q : ℕ} {B : Finset ℕ} (hq : q ∈ geometricSmallPrimes P D ε) (hB : B ⊆ geometricSmallPrimes P D ε) : lowerBoundaryDensity (D ^ ε) g q B = ∑ s ∈ B.powerset with ¬Even s.card ∧ 1 < ε * (↑s.card + 3), if LowerBoundary (D ^ ε) q s then ∏ p ∈ s, g p else 0

A finite source-aligned restriction of the same lower boundary kernel.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperBoundaryDensity_eq_highLayers (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (g : ℕ → ℝ) {q : ℕ} {B : Finset ℕ} (hq : q ∈ geometricSmallPrimes P D ε) (hB : B ⊆ geometricSmallPrimes P D ε) : upperBoundaryDensity (D ^ ε) g q B = ∑ s ∈ B.powerset with Even s.card ∧ 1 < ε * (↑s.card + 3), if UpperBoundary (D ^ ε) q s then ∏ p ∈ s, g p else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.lowerSmallBoundary_card_seven (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) {q : ℕ} {s : Finset ℕ} (hq : q ∈ geometricSmallPrimes P D ε) (hs : s ⊆ geometricSmallPrimes P D ε) (hb : LowerBoundary (D ^ ε) q s) : 7 ≤ s.card

In the Li--Liu parameter range a lower boundary needs at least seven tail primes (and the new least prime); the upper boundary needs six.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.upperSmallBoundary_card_six (P : Finset ℕ) {D ε : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) {q : ℕ} {s : Finset ℕ} (hq : q ∈ geometricSmallPrimes P D ε) (hs : s ⊆ geometricSmallPrimes P D ε) (hb : UpperBoundary (D ^ ε) q s) : 6 ≤ s.card