theorem MathlibNt.SieveTheory.lowerRosserBoundaryLayerMass_eq_zero_of_card_lt (S : BoundingSieve) (n D z : ℕ) (hcard : (SwitchingPrinciple.suzukiSupportedBelow S z).card < n) : lowerRosserBoundaryLayerMass S n D z = 0

A boundary layer longer than the finite prime support below z vanishes. Each recursive step chooses a strictly smaller prime, so it strictly decreases that support.

theorem MathlibNt.SieveTheory.lowerRosserEvenBoundaryLayerMass_eq_zero_of_support_card_lt (S : BoundingSieve) (k D z : ℕ) (hcard : (SwitchingPrinciple.suzukiSupportedBelow S z).card < 2 * (k + 1)) : lowerRosserEvenBoundaryLayerMass S k D z = 0

In particular, every even layer whose depth exceeds the finite support cardinality is zero.

theorem MathlibNt.SieveTheory.suzukiActualT_twice_support_card_succ_eq_all_even_boundary_layers (S : BoundingSieve) (D z : ℕ) : suzukiActualT S (2 * ((SwitchingPrinciple.suzukiSupportedBelow S z).card + 1)) D z = ∑ k ∈ Finset.range ((SwitchingPrinciple.suzukiSupportedBelow S z).card + 1), lowerRosserEvenBoundaryLayerMass S k D z

The concrete cutoff card + 1 already contains every nonzero even layer.

theorem MathlibNt.SieveTheory.suzukiActualT_even_stable_of_support_card_lt (S : BoundingSieve) (D z m : ℕ) (hm : (SwitchingPrinciple.suzukiSupportedBelow S z).card < m) : suzukiActualT S (2 * m) D z = suzukiActualT S (2 * ((SwitchingPrinciple.suzukiSupportedBelow S z).card + 1)) D z

Increasing the even truncation beyond card + 1 adds only zero layers.