theorem MathlibNt.SieveTheory.suzukiSourceV_eq_recurrence_of_supported_cube (S : BoundingSieve) {n D z : ℕ} (hn : 2 ≤ n) (hcube : Odd n → ∀ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, p ^ 3 < D) : suzukiSourceV S n D z = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p * suzukiSourceV S (n - 1) (D ⌈/⌉ p) p

A source layer can be extended from its literal outer carrier to every supported outer prime when the odd cubic cutoff is known pointwise. Terms failing the lower cutoff vanish by source support, so no global z^n ≤ D condition is needed.

theorem MathlibNt.SieveTheory.sourceParityIndices_odd_eq_insert_image_pred {N : ℕ} (hN : Odd N) : sourceParityIndices N = insert 1 (Finset.image (fun (m : ℕ) => m + 1) (sourceParityIndices (N - 1)))

For odd N, the selected source indices are the base index one together with successors of all predecessor-parity indices.

theorem MathlibNt.SieveTheory.suzukiSourceParitySum_recurrence_of_odd_of_supported_cube (S : BoundingSieve) {N D z : ℕ} (hN : Odd N) (hcube : ∀ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, p ^ 3 < D) : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D z = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p * ∑ m ∈ sourceParityIndices (N - 1), suzukiSourceV S m (D ⌈/⌉ p) p

Direct source-faithful parity recurrence at an odd endpoint. It expands suzukiSourceV itself and retains source layers on the right; it never passes through section14ExtendedT.

theorem MathlibNt.SieveTheory.sourceParityIndices_even_eq_image_pred {N : ℕ} (hN : Even N) (hN2 : 2 ≤ N) : sourceParityIndices N = Finset.image (fun (m : ℕ) => m + 1) (sourceParityIndices (N - 1))

At an even endpoint there is no exceptional base index: every selected source index is the successor of a uniquely selected predecessor index.

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

Direct source-faithful parity recurrence at an even endpoint. All selected layers have even index, so neither the odd cubic side condition nor a base layer condition is needed.

theorem MathlibNt.SieveTheory.suzukiSourceParitySum_recurrence (S : BoundingSieve) {N D z : ℕ} (hN2 : 2 ≤ N) (hbase : Odd N → suzukiSourceV S 1 D z = 0) (hcube : ∀ n ∈ sourceParityIndices N, 2 ≤ n → Odd n → ∀ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, p ^ 3 < D) : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D z = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p * ∑ m ∈ sourceParityIndices (N - 1), suzukiSourceV S m (D ⌈/⌉ p) p

The exact Case-I recurrence for either parity. hbase is required only when the parity domain contains the exceptional source layer V₁; hcube is required only for odd non-base layers. Thus even endpoints carry no artificial cubic or base hypothesis.

noncomputable def MathlibNt.SieveTheory.caseITau (D s : ℝ) : ℝ

The source-reviewed Case-I value τ = max(s, (1 - log 2 / log D)⁻¹).

Equations

• MathlibNt.SieveTheory.caseITau D s = max s (1 - Real.log 2 / Real.log D)⁻¹

structure MathlibNt.SieveTheory.CaseIThreeRangeDomain (D z : ℕ) (σ s : ℝ) : Prop

Exact real cutoff data used in the three-range Case-I split. Besides the ordering needed for a partition, this records the source identity D^(1/τ) = min(z,D/2) rather than replacing real cutoffs by rounded naturals.

• sigmaCut_le_tauCut : ↑D ^ (1 / σ) ≤ ↑D ^ (1 / caseITau (↑D) s)
• tauCut_eq_min : ↑D ^ (1 / caseITau (↑D) s) = min (↑z) (↑D / 2)

theorem MathlibNt.SieveTheory.sum_supported_eq_caseI_three_ranges (S : BoundingSieve) {D z : ℕ} {σ s : ℝ} (hdom : CaseIThreeRangeDomain D z σ s) (f : ℕ → ℝ) : ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, f p = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z with ↑p < ↑D ^ (1 / σ), f p + ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z with ↑D ^ (1 / σ) ≤ ↑p ∧ ↑p < ↑D ^ (1 / caseITau (↑D) s), f p + ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z with ↑D ^ (1 / caseITau (↑D) s) ≤ ↑p, f p

Any sum on the supported natural-prime carrier splits exactly into the three source ranges Σ₀, Σ₁, Σ₂. The inequalities are predicates in ℝ; no floor/ceiling surrogate is introduced.

theorem MathlibNt.SieveTheory.suzukiSourceParitySum_recurrence_three_ranges (S : BoundingSieve) {N D z : ℕ} {σ s : ℝ} (hN2 : 2 ≤ N) (hbase : Odd N → suzukiSourceV S 1 D z = 0) (hcube : ∀ n ∈ sourceParityIndices N, 2 ≤ n → Odd n → ∀ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, p ^ 3 < D) (hdom : CaseIThreeRangeDomain D z σ s) : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D z = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z with ↑p < ↑D ^ (1 / σ), S.nu p * ∑ m ∈ sourceParityIndices (N - 1), suzukiSourceV S m (D ⌈/⌉ p) p + ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z with ↑D ^ (1 / σ) ≤ ↑p ∧ ↑p < ↑D ^ (1 / caseITau (↑D) s), S.nu p * ∑ m ∈ sourceParityIndices (N - 1), suzukiSourceV S m (D ⌈/⌉ p) p + ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z with ↑D ^ (1 / caseITau (↑D) s) ≤ ↑p, S.nu p * ∑ m ∈ sourceParityIndices (N - 1), suzukiSourceV S m (D ⌈/⌉ p) p

Source-faithful Case-I recurrence followed by the exact Σ₀+Σ₁+Σ₂ partition at the real cutoffs from pages 85--86.