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

The genuine depth-two lower-Rosser boundary mass, written with the largest stored prime p first and the external terminal prime q second. The factor sourceDiscreteEuler S q is the product of all Euler factors below q; it is exactly the factor acquired when the density recurrence reaches terminal q.

Equations

• MathlibNt.SieveTheory.lowerRosserDepthTwoSourceMass S D z = ∑ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p * ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S p with p < D ∧ D ≤ p * q ^ 3, S.nu q * MathlibNt.SieveTheory.sourceDiscreteEuler S q

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

In the legal even depth-two range z² ≤ D, Suzuki's actual source layer is exactly the singleton lower-Rosser boundary carrier. Outside this range the predicates are not equivalent: the lower carrier has p < D, whereas the source recursion has the divided-level terminal test.

theorem MathlibNt.SieveTheory.lowerRosserSetDensitySum_eq_euler_sub_boundaryAccum (S : BoundingSieve) {D z : ℕ} (qs : List ℕ) (hcarrier : qs.toFinset = SwitchingPrinciple.suzukiSupportedBelow S z) (hprime : ∀ q ∈ qs, Nat.Prime q) (hD : ∀ q ∈ qs, q < D) (hordered : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) qs) (hD1 : 1 < D) : LinearSieve.lowerRosserSetDensitySum (⇑S.nu) D (SwitchingPrinciple.suzukiSupportedBelow S z) = sourceDiscreteEuler S z - LinearSieve.lowerRosserBoundaryAccum (⇑S.nu) D ∅ qs

Iterating the one-prime recurrence expands the lower density as the full Euler product minus an explicit recursively weighted sum of odd cubic boundary layers. The list is increasing, so its head is the least prime inserted last.

noncomputable def MathlibNt.SieveTheory.lowerRosserDeepBoundaryTail (S : BoundingSieve) (D z : ℕ) (qs : List ℕ) : ℝ

The deep discrepancy on an ordered prime carrier. Unlike the old opaque Euler - density - V₂ difference, this is the explicit all-boundary accumulator with the concrete depth-two source carrier removed.

Equations

• MathlibNt.SieveTheory.lowerRosserDeepBoundaryTail S D z qs = MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryAccum (⇑S.nu) D ∅ qs - MathlibNt.SieveTheory.lowerRosserDepthTwoSourceMass S D z

theorem MathlibNt.SieveTheory.lowerRosserDepthTwoSourceMass_nonneg (S : BoundingSieve) (D z : ℕ) : 0 ≤ lowerRosserDepthTwoSourceMass S D z

The genuine depth-two source mass is nonnegative.

theorem MathlibNt.SieveTheory.lowerRosserDeepBoundaryTail_bounds (S : BoundingSieve) {D z : ℕ} (qs : List ℕ) (hfold : List.foldr insert ∅ qs = SwitchingPrinciple.suzukiSupportedBelow S z) : -lowerRosserDepthTwoSourceMass S D z ≤ lowerRosserDeepBoundaryTail S D z qs ∧ lowerRosserDeepBoundaryTail S D z qs ≤ LinearSieve.lowerRosserBoundaryAccum (⇑S.nu) D ∅ qs

The explicit deep tail has a quantitative one-sided enclosure: it is at most the total boundary loss and at least minus the depth-two source mass.

theorem MathlibNt.SieveTheory.lowerRosserSetDensitySum_lower_of_boundaryAccum_le (S : BoundingSieve) {D z : ℕ} (qs : List ℕ) (hcarrier : qs.toFinset = SwitchingPrinciple.suzukiSupportedBelow S z) (hprime : ∀ q ∈ qs, Nat.Prime q) (hD : ∀ q ∈ qs, q < D) (hordered : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) qs) (hD1 : 1 < D) {B : ℝ} (hB : LinearSieve.lowerRosserBoundaryAccum (⇑S.nu) D ∅ qs ≤ B) : sourceDiscreteEuler S z - B ≤ LinearSieve.lowerRosserSetDensitySum (⇑S.nu) D (SwitchingPrinciple.suzukiSupportedBelow S z)

A JR-ready lower estimate with no absolute value: any explicit upper bound for the recursive boundary accumulator immediately gives a lower density bound.

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

The concrete discrepancy left after transporting the genuine depth-two source layer into the full lower-Rosser density. It includes every deeper boundary layer and any out-of-range carrier discrepancy; it is data, not an abstract proposition.

Equations

• MathlibNt.SieveTheory.lowerRosserDensityDiscrepancy S D z = MathlibNt.SieveTheory.sourceDiscreteEuler S z - MathlibNt.SieveTheory.LinearSieve.lowerRosserSetDensitySum (⇑S.nu) D (MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z) - MathlibNt.SieveTheory.suzukiActualT S 2 D z

theorem MathlibNt.SieveTheory.lowerRosserDensityDiscrepancy_eq_deepBoundaryTail (S : BoundingSieve) {D z : ℕ} (qs : List ℕ) (hcarrier : qs.toFinset = SwitchingPrinciple.suzukiSupportedBelow S z) (hprime : ∀ q ∈ qs, Nat.Prime q) (hD : ∀ q ∈ qs, q < D) (hordered : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) qs) (hD1 : 1 < D) (hzD : z ^ 2 ≤ D) : lowerRosserDensityDiscrepancy S D z = lowerRosserDeepBoundaryTail S D z qs

On any ordered enumeration of the supported primes, the source-to-density discrepancy is exactly the explicit deeper boundary tail.

theorem MathlibNt.SieveTheory.lowerRosserSetDensitySum_eq_euler_sub_suzukiActualT_two_sub_discrepancy (S : BoundingSieve) (D z : ℕ) : LinearSieve.lowerRosserSetDensitySum (⇑S.nu) D (SwitchingPrinciple.suzukiSupportedBelow S z) = sourceDiscreteEuler S z - suzukiActualT S 2 D z - lowerRosserDensityDiscrepancy S D z

Exact source-to-density decomposition. In particular, replacing the boundary carrier by suzukiActualT without this discrepancy is unjustified.

theorem MathlibNt.SieveTheory.lowerRosserSetDensitySum_lower_transport_two (S : BoundingSieve) (D z : ℕ) : sourceDiscreteEuler S z - suzukiActualT S 2 D z - |lowerRosserDensityDiscrepancy S D z| ≤ LinearSieve.lowerRosserSetDensitySum (⇑S.nu) D (SwitchingPrinciple.suzukiSupportedBelow S z)

Unconditional honest lower transport: the unknown deeper/discrepant tail is paid for by its absolute value rather than silently set to zero.

theorem MathlibNt.SieveTheory.lowerRosserSetDensitySum_lower_transport_depthTwoCarrier (S : BoundingSieve) {D z : ℕ} (hzD : z ^ 2 ≤ D) : sourceDiscreteEuler S z - lowerRosserDepthTwoSourceMass S D z - |lowerRosserDensityDiscrepancy S D z| ≤ LinearSieve.lowerRosserSetDensitySum (⇑S.nu) D (SwitchingPrinciple.suzukiSupportedBelow S z)

In the legal even depth-two range, the preceding inequality visibly uses the real lower-boundary carrier, not a falsely identified predicate.