def MathlibNt.SieveTheory.suzukiSourceOuterCarrier (n D z : ℕ) (P : Finset ℕ) : Finset ℕ

Exact integral outer carrier in Suzuki Lemma 7.1 for beta = 2.

n is the complete source index. D <= p^(n+2) is y_n <= p; for odd n, p^3 < D is the extra upper cutoff in z_n = min(z,D^(1/3)).

Equations

• MathlibNt.SieveTheory.suzukiSourceOuterCarrier n D z P = {p ∈ {p ∈ P | p < z} | D ≤ p ^ (n + 2) ∧ (Odd n → p ^ 3 < D)}

noncomputable def MathlibNt.SieveTheory.suzukiSourceV (S : BoundingSieve) : ℕ → ℕ → ℕ → ℝ

A total, source-faithful beta=2 recursion. Unlike the old section14ExtendedV, the base does not invent p < D, and every successor keeps Suzuki's y_n and (odd-index) z_n cutoffs.

Equations

• MathlibNt.SieveTheory.suzukiSourceV S 0 x✝¹ x✝ = 0
• MathlibNt.SieveTheory.suzukiSourceV S 1 x✝¹ x✝ = ∑ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S x✝ with x✝¹ ≤ p ^ 3, S.nu p * MathlibNt.SieveTheory.sourceDiscreteEuler S p
• MathlibNt.SieveTheory.suzukiSourceV S n.succ.succ x✝¹ x✝ = ∑ p ∈ MathlibNt.SieveTheory.suzukiSourceOuterCarrier (n + 2) x✝¹ x✝ S.prodPrimes.primeFactors, S.nu p * MathlibNt.SieveTheory.suzukiSourceV S (n + 1) (x✝¹ ⌈/⌉ p) p

@[simp]

theorem MathlibNt.SieveTheory.suzukiSourceV_one (S : BoundingSieve) (D z : ℕ) : suzukiSourceV S 1 D z = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z with D ≤ p ^ 3, S.nu p * sourceDiscreteEuler S p

theorem MathlibNt.SieveTheory.suzukiSourceV_succ_of_pos (S : BoundingSieve) {n : ℕ} (hn : 0 < n) (D z : ℕ) : suzukiSourceV S (n + 1) D z = ∑ p ∈ suzukiSourceOuterCarrier (n + 1) D z S.prodPrimes.primeFactors, S.nu p * suzukiSourceV S n (D ⌈/⌉ p) p

Correct total recurrence: the outer source carrier cannot be erased without the Section 14 domain/support hypotheses.

theorem MathlibNt.SieveTheory.suzukiSourceV_two_eq (S : BoundingSieve) (D z : ℕ) : suzukiSourceV S 2 D z = ∑ p ∈ suzukiSourceOuterCarrier 2 D z S.prodPrimes.primeFactors, S.nu p * ∑ q ∈ SwitchingPrinciple.suzukiSupportedBelow S p with D ⌈/⌉ p ≤ q ^ 3, S.nu q * sourceDiscreteEuler S q

The corrected index-two carrier before simplification. It has no invented q < ceil(D/p) condition.

theorem MathlibNt.SieveTheory.section14Extended_n2_rejects_source_chain : 9 ≤ 5 * 2 ^ 3 ∧ ¬(2 < 9 ⌈/⌉ 5 ∧ 9 ⌈/⌉ 5 ≤ 2 ^ 3)

At n=2 Suzuki's literal terminal test accepts (D,p,q)=(9,5,2), while the Section 14 extended recursive totalization rejects it because it additionally asks q<D/p.

theorem MathlibNt.SieveTheory.lower_boundary_n2_accepts_source_chain : 5 < 9 ∧ 9 ≤ 5 * 2 ^ 3

The production lower-boundary singleton accepts the same source chain: its active-prefix clause is p<D, not the Section 14 extended recursive p*q<D.

theorem MathlibNt.SieveTheory.lower_boundary_n2_prefix_redundant {D z p : ℕ} (hp2 : 2 ≤ p) (hpz : p < z) (hzD : z ^ 2 ≤ D) : p < D

In Suzuki's even parity domain (z^2 <= D), the lower boundary's apparent extra n=2 prefix p<D is automatic.

theorem MathlibNt.SieveTheory.section14Extended_n2_iff_source_in_even_domain {D z p q : ℕ} (hp : 0 < p) (hq : q < p) (hpz : p < z) (hzD : z ^ 2 ≤ D) : q < D ⌈/⌉ p ∧ D ⌈/⌉ p ≤ q ^ 3 ↔ D ≤ p * q ^ 3

In the same domain, the old divided-level predicate and Suzuki's literal n=2 terminal condition agree. Thus the mismatch is outside the theorem's legal domain, not a missing lower-chain prefix.