theorem MathlibNt.SieveTheory.suzukiSourceV_eq_zero_of_pow_le (S : BoundingSieve) {n D z : ℕ} (hn : 1 ≤ n) (hzD : z ^ (n + 2) ≤ D) : suzukiSourceV S n D z = 0

General upper support of the source-faithful layer.

theorem MathlibNt.SieveTheory.suzukiSourceV_inner_eq_zero_of_outer_lower_fails (S : BoundingSieve) {n D p : ℕ} (hn : 1 ≤ n) (hp : 0 < p) (hfail : ¬D ≤ p ^ (n + 3)) : suzukiSourceV S n (D ⌈/⌉ p) p = 0

If the Lemma 7.1 lower outer cutoff fails, the recursively remaining layer vanishes.

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

Legal-domain recurrence: the source carrier may be extended to every supported p < z. The odd-index upper cutoff is automatic from z^3 ≤ D; the omitted lower-cutoff terms vanish by the preceding support lemma.

theorem MathlibNt.SieveTheory.suzukiSourceV_two_eq_extended_recurrence (S : BoundingSieve) (D z : ℕ) : suzukiSourceV S 2 D z = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p * suzukiSourceV S 1 (D ⌈/⌉ p) p

Index two: no parity-domain hypothesis is needed.

theorem MathlibNt.SieveTheory.suzukiSourceV_three_eq_extended_recurrence (S : BoundingSieve) {D z : ℕ} (hzD : z ^ 3 ≤ D) : suzukiSourceV S 3 D z = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p * suzukiSourceV S 2 (D ⌈/⌉ p) p

Index three: z^3 ≤ D is exactly the legal odd-domain assumption making Suzuki's extra outer upper cutoff automatic.

theorem MathlibNt.SieveTheory.suzukiSourceV_eq_section14ExtendedV_of_pow_le (S : BoundingSieve) (n D z : ℕ) (hzD : z ^ n ≤ D) : suzukiSourceV S n D z = section14ExtendedV S n D z

Exact induction invariant for the full bridge: at layer n, z^n ≤ D propagates to p^(n-1) ≤ ceil(D/p) for every supported outer prime p < z. This simultaneously makes every odd source upper cutoff automatic.

theorem MathlibNt.SieveTheory.suzukiSourceV_two_eq_section14ExtendedV (S : BoundingSieve) {D z : ℕ} (hzD : z ^ 2 ≤ D) : suzukiSourceV S 2 D z = section14ExtendedV S 2 D z

Index two closes under the exact even legal-domain hypothesis.

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

Index three closes under the exact odd legal-domain hypothesis.

theorem MathlibNt.SieveTheory.suzukiSourceParitySum_eq_section14ExtendedT_of_pow_le (S : BoundingSieve) (N D z : ℕ) (hzD : z ^ N ≤ D) : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D z = section14ExtendedT S N D z

Consequently the source-faithful parity sum agrees with the renamed §14 extended sum on the uniform legal domain z^N ≤ D.