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

The depth-four lower-Rosser boundary mass: three stored decreasing primes, followed by the terminal least prime. The two displayed inequalities are exactly the active even-prefix test and terminal odd-boundary crossing.

Equations

• MathlibNt.SieveTheory.lowerRosserDepthFourSourceMass S D z = ∑ p₀ ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p₀ * ∑ p₁ ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S p₀ with p₀ * p₁ ^ 3 < D, S.nu p₁ * ∑ p₂ ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S p₁, S.nu p₂ * ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S p₂ with D ≤ p₀ * p₁ * p₂ * q ^ 3, S.nu q * MathlibNt.SieveTheory.sourceDiscreteEuler S q

theorem MathlibNt.SieveTheory.suzukiSourceV_odd_succ_eq_upper_only (S : BoundingSieve) {n D z : ℕ} (hn : 0 < n) (hodd : Odd (n + 1)) : suzukiSourceV S (n + 1) D z = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z with p ^ 3 < D, S.nu p * suzukiSourceV S n (D ⌈/⌉ p) p

At every odd outer depth, the source lower cutoff is redundant: whenever it fails, the remaining even layer vanishes. The odd cubic upper cutoff is the only active outer condition.

theorem MathlibNt.SieveTheory.suzukiSourceV_four_eq_lowerRosserDepthFourSourceMass (S : BoundingSieve) (D z : ℕ) : suzukiSourceV S 4 D z = lowerRosserDepthFourSourceMass S D z

Suzuki's complete even layer V₄ is exactly the depth-four lower-Rosser boundary mass. The proof follows the exact recurrence: even source lower cutoffs vanish, the depth-three lower cutoff is killed by the residual V₂, and the remaining divided inequalities clear to the prefix and terminal tests.

theorem MathlibNt.SieveTheory.suzukiActualT_four_eq_two_add_lowerRosserDepthFourSourceMass (S : BoundingSieve) (D z : ℕ) : suzukiActualT S 4 D z = suzukiSourceV S 2 D z + lowerRosserDepthFourSourceMass S D z

The finite even Suzuki aggregate truncated at depth four is the depth-two layer plus the newly identified lower-Rosser depth-four boundary mass. This is the explicit depth-four truncation of the general even-layer correspondence.

theorem MathlibNt.SieveTheory.suzukiEvenParitySum_four_eq_two_add_lowerRosserDepthFourSourceMass (S : BoundingSieve) (D z : ℕ) : ∑ n ∈ suzukiActualParityCarrier 4, suzukiSourceV S n D z = suzukiSourceV S 2 D z + lowerRosserDepthFourSourceMass S D z

Equivalently, the literal finite parity sum at truncation depth four splits into its depth-two layer and the lower-Rosser depth-four boundary mass.

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

The depth-six lower-Rosser boundary mass. Its two interior tests occur at the odd prefixes, followed by the terminal boundary crossing.

Equations

• MathlibNt.SieveTheory.lowerRosserDepthSixSourceMass S D z = ∑ p₀ ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p₀ * ∑ p₁ ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S p₀ with p₀ * p₁ ^ 3 < D, S.nu p₁ * ∑ p₂ ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S p₁, S.nu p₂ * ∑ p₃ ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S p₂ with p₀ * p₁ * p₂ * p₃ ^ 3 < D, S.nu p₃ * ∑ p₄ ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S p₃, S.nu p₄ * ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S p₄ with D ≤ p₀ * p₁ * p₂ * p₃ * p₄ * q ^ 3, S.nu q * MathlibNt.SieveTheory.sourceDiscreteEuler S q

theorem MathlibNt.SieveTheory.suzukiSourceV_six_eq_lowerRosserDepthSixSourceMass (S : BoundingSieve) (D z : ℕ) : suzukiSourceV S 6 D z = lowerRosserDepthSixSourceMass S D z

Suzuki's complete even layer V₆ is exactly the depth-six lower-Rosser boundary mass. This is the next case of the alternating odd-prefix pattern.

theorem MathlibNt.SieveTheory.suzukiActualT_six_eq_four_add_lowerRosserDepthSixSourceMass (S : BoundingSieve) (D z : ℕ) : suzukiActualT S 6 D z = suzukiActualT S 4 D z + lowerRosserDepthSixSourceMass S D z

The finite even Suzuki aggregate truncated at depth six is its depth-four aggregate plus the newly identified depth-six boundary mass.

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

The boundary layer at arbitrary recursion depth. Depth one is the terminal odd crossing. Every later odd layer records the active cubic upper test, while every even layer only extends the decreasing prime chain. Thus a layer carries exactly the alternating-prefix invariant visible at depths four and six.

Equations

• MathlibNt.SieveTheory.lowerRosserBoundaryLayerMass S 0 x✝¹ x✝ = 0
• MathlibNt.SieveTheory.lowerRosserBoundaryLayerMass S 1 x✝¹ x✝ = ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S x✝ with x✝¹ ≤ q ^ 3, S.nu q * MathlibNt.SieveTheory.sourceDiscreteEuler S q
• MathlibNt.SieveTheory.lowerRosserBoundaryLayerMass S n.succ.succ x✝¹ x✝ = ∑ p ∈ if Odd (n + 2) then {p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S x✝ | p ^ 3 < x✝¹} else MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S x✝, S.nu p * MathlibNt.SieveTheory.lowerRosserBoundaryLayerMass S (n + 1) (x✝¹ ⌈/⌉ p) p

theorem MathlibNt.SieveTheory.suzukiSourceV_eq_lowerRosserBoundaryLayerMass (S : BoundingSieve) (n D z : ℕ) (hn : 0 < n) : suzukiSourceV S n D z = lowerRosserBoundaryLayerMass S n D z

General Suzuki/lower-Rosser layer correspondence. The inductive invariant is that the current divided level is retained literally; odd outer depths add p³ < D, even outer depths add no test, and depth one closes with D ≤ q³.

noncomputable def MathlibNt.SieveTheory.lowerRosserEvenBoundaryLayerMass (S : BoundingSieve) (m D z : ℕ) : ℝ

The m-th (one-indexed mathematically, zero-indexed here) even boundary layer has Suzuki depth 2(m+1).

Equations

• MathlibNt.SieveTheory.lowerRosserEvenBoundaryLayerMass S m D z = MathlibNt.SieveTheory.lowerRosserBoundaryLayerMass S (2 * (m + 1)) D z

theorem MathlibNt.SieveTheory.suzukiSourceV_even_eq_lowerRosserEvenBoundaryLayerMass (S : BoundingSieve) (m D z : ℕ) : suzukiSourceV S (2 * (m + 1)) D z = lowerRosserEvenBoundaryLayerMass S m D z

Every positive even Suzuki layer is the corresponding lower-Rosser boundary layer.

theorem MathlibNt.SieveTheory.lowerRosserBoundaryLayerMass_four_eq_depthFour (S : BoundingSieve) (D z : ℕ) : lowerRosserBoundaryLayerMass S 4 D z = lowerRosserDepthFourSourceMass S D z

The general layer specializes to the previously expanded depth-four mass.

theorem MathlibNt.SieveTheory.lowerRosserBoundaryLayerMass_six_eq_depthSix (S : BoundingSieve) (D z : ℕ) : lowerRosserBoundaryLayerMass S 6 D z = lowerRosserDepthSixSourceMass S D z

The general layer specializes to the previously expanded depth-six mass.

theorem MathlibNt.SieveTheory.suzukiActualT_even_eq_sum_lowerRosserEvenBoundaryLayerMass (S : BoundingSieve) (m D z : ℕ) : suzukiActualT S (2 * m) D z = ∑ k ∈ Finset.range m, lowerRosserEvenBoundaryLayerMass S k D z

At arbitrary even truncation, suzukiActualT is exactly the finite sum of all lower-Rosser boundary layers through depth 2m.

noncomputable def MathlibNt.SieveTheory.lowerRosserBoundaryAfterEvenDepth (S : BoundingSieve) (D z : ℕ) (P : Finset ℕ) (qs : List ℕ) (m : ℕ) : ℝ

The part of the full one-prime lower-Rosser boundary accumulator not yet represented by the even layers through depth 2m. This definition keeps the remaining combinatorial issue explicit rather than identifying it silently.

Equations

• MathlibNt.SieveTheory.lowerRosserBoundaryAfterEvenDepth S D z P qs m = MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryAccum (⇑S.nu) D P qs - ∑ k ∈ Finset.range m, MathlibNt.SieveTheory.lowerRosserEvenBoundaryLayerMass S k D z

theorem MathlibNt.SieveTheory.lowerRosserBoundaryAccum_eq_suzukiActualT_even_add_remainder (S : BoundingSieve) (D z : ℕ) (P : Finset ℕ) (qs : List ℕ) (m : ℕ) : LinearSieve.lowerRosserBoundaryAccum (⇑S.nu) D P qs = suzukiActualT S (2 * m) D z + lowerRosserBoundaryAfterEvenDepth S D z P qs m

Exact connection between the finite Suzuki even-layer sum and the existing lowerRosserBoundaryAccum: the latter is the truncation plus its explicit post-depth remainder.

theorem MathlibNt.SieveTheory.suzukiActualT_even_eq_lowerRosserBoundaryAccum_iff (S : BoundingSieve) (D z : ℕ) (P : Finset ℕ) (qs : List ℕ) (m : ℕ) : suzukiActualT S (2 * m) D z = LinearSieve.lowerRosserBoundaryAccum (⇑S.nu) D P qs ↔ lowerRosserBoundaryAfterEvenDepth S D z P qs m = 0

Consequently, identifying the finite Suzuki truncation with the complete boundary accumulator is exactly the assertion that the explicit remainder vanishes.