Lemma 14.4, Case I: the even lower endpoint s = 2

When the successor depth M is even, the formal predecessor endpoint 1 is not in the open odd parity domain. It is nevertheless not an index of the actual finite recurrence: every summand has p < D^(1/2), hence its inherited coordinate log D / log p - 1 is strictly larger than 1.

Thus the endpoint is a strict-carrier boundary phenomenon. The actual natural-ceiling recurrence remains exact, and both coordinates used by the induction hypothesis lie in the predecessor parity domain. No estimate for the desired Lemma-14.4 conclusion is assumed below.

theorem MathlibNt.SieveTheory.lemma144_caseI_even_endpoint_odd_carrier {M D z : ℕ} (hM : Even M) : Odd M → ∀ p < z, p ^ 3 < D

At even depth the odd source-cutoff premise of the exact recurrence is vacuous. Therefore suzukiActualT_caseI_recurrence_strict applies at the literal natural ceiling without any (generally false) ceiling-square claim.

theorem MathlibNt.SieveTheory.lemma144_caseI_even_endpoint_inherited_domain (S : BoundingSieve) {M D z : ℕ} (hM : Even M) (hM2 : 2 ≤ M) (hD : 4 ≤ D) (hz : z = ⌈↑D ^ (1 / 2)⌉₊) (p : ℕ) : p ∈ SwitchingPrinciple.suzukiSupportedBelow S z → SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (M - 1)

Every actual recurrence index at the even endpoint has inherited coordinate strictly inside the predecessor's open odd parity domain. This is the strict inequality which the formal endpoint 2 - 1 = 1 itself lacks.

theorem MathlibNt.SieveTheory.lemma144_caseI_even_endpoint_source_packet (S : BoundingSieve) {M D z : ℕ} (hM : Even M) (hM2 : 2 ≤ M) (hD : 4 ≤ D) (hz : z = ⌈↑D ^ (1 / 2)⌉₊) (p : ℕ) : p ∈ SwitchingPrinciple.suzukiSupportedBelow S z → SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (M - 1) ∧ SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (M - 1) ∧ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (M - 1) (SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p) ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (M - 1) (SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)

The ceiling-recursive coordinate is also legal, and Proposition 9.3 gives exactly the finite-source-layer comparison needed by the pointwise IH. This uniform packet uses only actual recurrence indices; it has no hypothesis that 1 belongs to the predecessor parity domain.