Lemma 14.4: the even Σ₁₁ endpoint

At even depth M, the predecessor depth M-1 is odd. Its source domain is open at 1, but the κ=1 layers are regular on the closed envelope. We use that closed-envelope regularity only to run Lemma 8.7 and the finite recursion at the endpoint. The prime carrier itself is strict, so no prime coordinate is added.

theorem MathlibNt.SieveTheory.finiteSourceLayer_continuousOn_closedDomain {β : ℝ} (hβ : 1 < β) (N : ℕ) : ContinuousOn (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N) (SuzukiFiniteContinuousLayers.KappaOneModel.closedDomain β N)

Finite source layers are continuous on the closed parity domain for beta > 1.

theorem MathlibNt.SieveTheory.sigma11_finiteSourceLayer_lemma8_7_even_endpoint {S : BoundingSieve} {D z v w σ K : ℝ} {M : ℕ} (hM : Even M) (hM2 : 2 ≤ M) (hσ : 2 ≤ σ) (hD : 1 < D) (hz2 : 2 ≤ z) (hv2 : 2 ≤ v) (hw2 : 2 ≤ w) (hwv : w ≤ v) (hvz : v ≤ z) (hz : z = D ^ (1 / 2)) (hv : v = D ^ (1 / 2)) (hw : w = D ^ (1 / σ)) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) : (SwitchingPrinciple.suzukiLemmaEightSevenPrimeSum S D w v z fun (t : ℝ) => SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (M - 1) (t - 1)) ≤ (1 / 2 * ∫ (t : ℝ) in 2..σ, SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (M - 1) (t - 1)) + 6 * K ^ 2 * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (M - 1) 1 / Real.log w

Lemma 8.7 at s=τ=2, using closed-envelope regularity at the one formal boundary point. Its prime sum remains on the original strict carrier.

theorem MathlibNt.SieveTheory.Sigma11FiniteLayerMajorization_even_endpoint {M : ℕ} (hM : Even M) (hM2 : 2 ≤ M) {σ : ℝ} (hσ : 2 ≤ σ) : 1 / 2 * ∫ (t : ℝ) in 2..σ, SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (M - 1) (t - 1) ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 M 2

The finite (9.2) majorization remains valid when the odd predecessor is used at its closed left endpoint.

theorem MathlibNt.SieveTheory.caseI_evenEndpointSigma11Edge (S : BoundingSieve) {M D : ℕ} {K σ : ℝ} (hM : Even M) (hM2 : 2 ≤ M) (hσ : 2 ≤ σ) (hD : 1 < ↑D) (hroot2 : 2 ≤ ↑D ^ (1 / 2)) (hw2 : 2 ≤ ↑D ^ (1 / σ)) (hwroot : ↑D ^ (1 / σ) ≤ ↑D ^ (1 / 2)) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) : CaseIEvenEndpointSigma11Edge S M D K σ

Production closure of the even Case-I Σ₁₁ endpoint, with no predecessor open-domain hypothesis.