def MathlibNt.SieveTheory.SuzukiSourceCubeCut (S : BoundingSieve) (D y z : ℕ) : Prop

A natural-number formulation of the source cutoff y = D^(1/3) on the finite prime support relevant below z. It records the exact strict-cutoff statement used in Suzuki Case II, without imposing either incompatible rounded cube inequality on y.

Equations

• MathlibNt.SieveTheory.SuzukiSourceCubeCut S D y z = ∀ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z, p < y ↔ p ^ 3 < D

theorem MathlibNt.SieveTheory.suzukiSourceCubeCut_of_ceilingCube (S : BoundingSieve) {D y z : ℕ} (hyLower : (y - 1) ^ 3 < D) (hyUpper : D ≤ y ^ 3) : SuzukiSourceCubeCut S D y z

The standard natural encoding of Suzuki's real cutoff D^(1/3) implies its exact strict membership rule. Thus y is the ceiling cube root: the last integer below the real cutoff is y-1.

theorem MathlibNt.SieveTheory.suzukiSourceV_one_eq_zero_of_cubeCut (S : BoundingSieve) {D y z : ℕ} (hyz : y ≤ z) (hcut : SuzukiSourceCubeCut S D y z) : suzukiSourceV S 1 D y = 0

The source base layer vanishes below the cubic cutoff.

theorem MathlibNt.SieveTheory.suzukiSourceV_eq_of_cubeCut_of_odd (S : BoundingSieve) {n D y z : ℕ} (hn2 : 2 ≤ n) (hn : Odd n) (hyz : y ≤ z) (hcut : SuzukiSourceCubeCut S D y z) : suzukiSourceV S n D z = suzukiSourceV S n D y

Every odd source layer of index at least three is unchanged when its outer cutoff is enlarged from the cubic cutoff y to z. This is immediate from Suzuki's literal odd-index carrier p^3 < D; no global hypothesis z^n ≤ D is involved.

theorem MathlibNt.SieveTheory.suzukiSourceParitySum_caseII_cut (S : BoundingSieve) {N D y z : ℕ} (hN : Odd N) (hyz : y ≤ z) (hcut : SuzukiSourceCubeCut S D y z) : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D z = ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D y + suzukiSourceV S 1 D z

Source-faithful Case-II cutoff identity (Suzuki (14.24), at β = 2).

The selected indices are odd. The n=1 layer vanishes at the natural cubic cutoff, while every selected n≥3 layer has Suzuki's own outer carrier p^3<D, hence is already supported below y. In particular this proof does not pass through section14ExtendedV and does not assume the false-for-N>3 global bridge z^N ≤ D.

theorem MathlibNt.SieveTheory.suzukiSourceParitySum_caseII_cut_of_ceilingCube (S : BoundingSieve) {N D y z : ℕ} (hN : Odd N) (hyz : y ≤ z) (hyLower : (y - 1) ^ 3 < D) (hyUpper : D ≤ y ^ 3) : ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D z = ∑ n ∈ sourceParityIndices N, suzukiSourceV S n D y + suzukiSourceV S 1 D z

(14.24) with the natural hypotheses expressing y = D^(1/3) for strict integer prime cutoffs.