noncomputable def MathlibNt.SieveTheory.sourceDiscreteEuler (S : BoundingSieve) (z : ℕ) : ℝ

The finite Euler product V(z) on the supported prime carrier.

Equations

• MathlibNt.SieveTheory.sourceDiscreteEuler S z = ∏ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z, (1 - S.nu p)

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

Suzuki's discrete V_n(D,z), with complete-chain source index n.

At n=1 this is exactly the one-prime terminal shell p < D ∧ D ≤ p^3. For n+2, peeling the largest source prime gives the source recurrence with level D/p, encoded exactly on naturals by D ⌈/⌉ p. Index zero is deliberately zero: it is not a source layer.

Equations

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

@[simp]

theorem MathlibNt.SieveTheory.section14ExtendedV_zero (S : BoundingSieve) (D z : ℕ) : section14ExtendedV S 0 D z = 0

@[simp]

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

theorem MathlibNt.SieveTheory.section14ExtendedV_succ_of_pos (S : BoundingSieve) {n : ℕ} (hn : 0 < n) (D z : ℕ) : section14ExtendedV S (n + 1) D z = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p * section14ExtendedV S n (D ⌈/⌉ p) p

Exact one-prime source recurrence, valid for every positive predecessor index. No positivity or analytic hypothesis is used.

theorem MathlibNt.SieveTheory.section14ExtendedV_one_eq_zero_of_cube_le (S : BoundingSieve) {D z : ℕ} (hzD : z ^ 3 ≤ D) : section14ExtendedV S 1 D z = 0

Exact support boundary for the exceptional source layer V₁. This is the finite form used in Suzuki's Case I when s ≥ β+1 and β=2: z^3 ≤ D.

def MathlibNt.SieveTheory.sourceParityIndices (N : ℕ) : Finset ℕ

Source-selected indices 1 ≤ n ≤ N, n ≡ N (mod 2).

Equations

• MathlibNt.SieveTheory.sourceParityIndices N = {n ∈ Finset.Icc 1 N | n % 2 = N % 2}

def MathlibNt.SieveTheory.sourceParityTailIndices (N : ℕ) : Finset ℕ

The positive-index tail, used to separate the exceptional V₁ term.

Equations

• MathlibNt.SieveTheory.sourceParityTailIndices N = {n ∈ Finset.Icc 2 N | n % 2 = N % 2}

noncomputable def MathlibNt.SieveTheory.section14ExtendedT (S : BoundingSieve) (N D z : ℕ) : ℝ

The finite discrete parity sum T_N(D,z).

Equations

• MathlibNt.SieveTheory.section14ExtendedT S N D z = ∑ n ∈ MathlibNt.SieveTheory.sourceParityIndices N, MathlibNt.SieveTheory.section14ExtendedV S n D z

@[simp]

theorem MathlibNt.SieveTheory.section14ExtendedT_zero (S : BoundingSieve) (D z : ℕ) : section14ExtendedT S 0 D z = 0

theorem MathlibNt.SieveTheory.section14ExtendedT_recurrence_of_even (S : BoundingSieve) {N D z : ℕ} (hN : Even N) (hN2 : 2 ≤ N) : section14ExtendedT S N D z = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p * section14ExtendedT S (N - 1) (D ⌈/⌉ p) p

Exact parity recurrence for even source cutoff N. Since every selected index is at least two, no terminal boundary term occurs.

theorem MathlibNt.SieveTheory.section14ExtendedT_eq_one_add_recurrence_of_odd (S : BoundingSieve) {N D z : ℕ} (hN : Odd N) (hN1 : 1 ≤ N) : section14ExtendedT S N D z = section14ExtendedV S 1 D z + ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p * section14ExtendedT S (N - 1) (D ⌈/⌉ p) p

For odd N, the only obstruction to the same recurrence is the source base layer V₁; all higher selected layers reindex exactly.

theorem MathlibNt.SieveTheory.section14ExtendedT_recurrence (S : BoundingSieve) {N D z : ℕ} (hN2 : 2 ≤ N) (hboundary : Odd N → section14ExtendedV S 1 D z = 0) : section14ExtendedT S N D z = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p * section14ExtendedT S (N - 1) (D ⌈/⌉ p) p

Suzuki Case-I exact recurrence. For even N it is unconditional; for odd N, the precise boundary hypothesis is the vanishing of V₁(D,z).

theorem MathlibNt.SieveTheory.section14ExtendedT_recurrence_of_cube_le (S : BoundingSieve) {N D z : ℕ} (hN2 : 2 ≤ N) (hzD : z ^ 3 ≤ D) : section14ExtendedT S N D z = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p * section14ExtendedT S (N - 1) (D ⌈/⌉ p) p

The concrete Case-I boundary z^3 ≤ D kills V₁, hence yields the exact recurrence for both parities.

noncomputable def MathlibNt.SieveTheory.sourceDiscreteLowerBoundaryV (S : BoundingSieve) (n D z : ℕ) : ℝ

The normalized lower V_n(D,z)/V(z) written directly on the production lower-boundary chain carrier. The terminal prime q is external to l, so the complete source index is imposed by l.length + 1 = n.

Equations

• MathlibNt.SieveTheory.sourceDiscreteLowerBoundaryV S n D z = ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z, S.nu q * MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSuffixRatio S z q * ∑ l ∈ MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryChainsAtSourceIndex D q ({p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z | q < p}) n, (List.map (⇑S.nu) l).prod

theorem MathlibNt.SieveTheory.section14ExtendedV_two_eq_recursiveCarrier (S : BoundingSieve) (D z : ℕ) : section14ExtendedV S 2 D z = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p * ∑ q ∈ SwitchingPrinciple.suzukiSupportedBelow S p with q < D ⌈/⌉ p ∧ D ⌈/⌉ p ≤ q ^ 3, S.nu q * sourceDiscreteEuler S q

The recursive source layer at index two, fully expanded. This is the strongest unconditional comparison datum with the lower boundary carrier: its inner terminal shell is tested at the divided level D ⌈/⌉ p.

theorem MathlibNt.SieveTheory.sourceDiscreteLowerBoundaryV_two_eq_chainCarrier (S : BoundingSieve) (D z : ℕ) : sourceDiscreteLowerBoundaryV S 2 D z = ∑ q ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu q * SwitchingPrinciple.suzukiSuffixRatio S z q * ∑ p ∈ {p ∈ SwitchingPrinciple.suzukiSupportedBelow S z | q < p} with p < D ∧ D ≤ p * q ^ 3, S.nu p

The chain-based lower slice at index two, fully expanded. In contrast to section14ExtendedV_two_eq_recursiveCarrier, the stored prime is tested by p < D, while the terminal prime q occurs only in the cubic crossing test D ≤ p*q^3. Thus the two definitions do not have the same base carrier.

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

The base carriers are genuinely different, already on prime-shaped data: with stored prime p = 5, terminal prime q = 2, and level D = 9, the chain predicate holds but the recursive divided-level predicate does not.

theorem MathlibNt.SieveTheory.sourceDiscreteLowerBoundaryV_eq_zero_of_odd (S : BoundingSieve) {n D z : ℕ} (hn : Odd n) : sourceDiscreteLowerBoundaryV S n D z = 0

A lower-boundary source slice is supported only at even complete-chain indices.

theorem MathlibNt.SieveTheory.sourceDiscreteLowerBoundaryV_even_eq_normalizedLayer (S : BoundingSieve) (D z k : ℕ) : sourceDiscreteLowerBoundaryV S (2 * k + 2) D z = lowerSuzukiNormalizedLayer S D 0 z k

Exact identification of the direct source-index slice with the existing production lower layer at source index 2*k+2.

theorem MathlibNt.SieveTheory.sourceDiscrete_lower_boundary_index (S : BoundingSieve) (D z k q : ℕ) : lowerSuzukiDiscreteKernel S D z k q = ∑ l ∈ LinearSieve.lowerRosserBoundaryChainsAtSourceIndex D q ({p ∈ SwitchingPrinciple.suzukiSupportedBelow S z | q < p}) (2 * k + 2), (List.map (⇑S.nu) l).prod

Existing lower Rosser preterminal chains carry the exact complete-chain source index: odd stored length 2k+1, plus the external terminal prime, is 2k+2. This is the non-proxy bridge used by the lower discrete layer.

theorem MathlibNt.SieveTheory.sourceDiscrete_lower_boundary_even {D q n : ℕ} {P : Finset ℕ} {l : List ℕ} (hl : l ∈ LinearSieve.lowerRosserBoundaryChainsAtSourceIndex D q P n) : Even n

Every chain in the lower slice has even complete source index.