Lemma 14.4, even Case-I endpoint

This file closes the discrete recurrence and the moving-domain pointwise-IH part of the exceptional endpoint s = 2. It also records the first analytic statement that is not exported by the current Case-I successor API. In particular, no estimate for suzukiActualT S M D ... is postulated.

def MathlibNt.SieveTheory.Lemma144EvenEndpointMovingIH (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ : ℝ) (n Dmin : ℕ) : Prop

The predecessor assertion needed at the actual quotient coordinates.

Equations

• MathlibNt.SieveTheory.Lemma144EvenEndpointMovingIH S H C K d Δ n Dmin = ∀ (D z : ℕ), Dmin ≤ D → 2 ≤ D → 2 ≤ z → ∀ x ∈ MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 n, x ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → ↑D ^ (1 / x) = ↑z → MathlibNt.SieveTheory.suzukiActualT S n D z ≤ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑z * (MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 n x + C * Real.exp √K * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H n (↑D) d x * Real.log ↑D ^ (-Δ))

theorem MathlibNt.SieveTheory.evenEndpoint_pointwiseInductionContract_of_movingIH (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ : ℝ) (M D Dmin : ℕ) (hDmin : 2 ≤ Dmin) (hM : Even M) (hM2 : 2 ≤ M) (hD : 4 ≤ D) (hscale : SwitchingPrinciple.SuzukiLemma144Equation1410.CarrierQuotientThresholdGeometry (SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / 2)⌉₊) D Dmin (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) 2) (hrecursiveSigma : ∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / 2)⌉₊) D (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) 2, SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑(D ⌈/⌉ p)) d) (hError : ∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / 2)⌉₊) D (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) 2, SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (M - 1) (↑(D ⌈/⌉ p)) d (SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p) ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (M - 1) (↑(D ⌈/⌉ p)) d (SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)) (hC : 0 ≤ C) (hIH : Lemma144EvenEndpointMovingIH S H C K d Δ (M - 1) Dmin) : SwitchingPrinciple.SuzukiLemma144Equation1410.PointwiseInductionContract (SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / 2)⌉₊) (suzukiActualT S) (fun (p : ℕ) => SwitchingPrinciple.suzukiVProduct S ↑p) (fun (n D' : ℕ) (x : ℝ) => SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H n (↑D') d x) 2 C K Δ M D (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) 2

The moving predecessor IH instantiates at every actual endpoint carrier coordinate. The illegal formal point 2-1=1 never occurs.

theorem MathlibNt.SieveTheory.evenEndpoint_recurrence_and_pointwise (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ : ℝ) (M D Dmin : ℕ) (hDmin : 2 ≤ Dmin) (hM : Even M) (hM2 : 2 ≤ M) (hD : 4 ≤ D) (hscale : SwitchingPrinciple.SuzukiLemma144Equation1410.CarrierQuotientThresholdGeometry (SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / 2)⌉₊) D Dmin (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) 2) (hrecursiveSigma : ∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / 2)⌉₊) D (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) 2, SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑(D ⌈/⌉ p)) d) (hError : ∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / 2)⌉₊) D (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) 2, SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (M - 1) (↑(D ⌈/⌉ p)) d (SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p) ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (M - 1) (↑(D ⌈/⌉ p)) d (SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)) (hC : 0 ≤ C) (hIH : Lemma144EvenEndpointMovingIH S H C K d Δ (M - 1) Dmin) : suzukiActualT S M D ⌈↑D ^ (1 / 2)⌉₊ = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / 2)⌉₊, S.nu p * suzukiActualT S (M - 1) (D ⌈/⌉ p) p ∧ SwitchingPrinciple.SuzukiLemma144Equation1410.PointwiseInductionContract (SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / 2)⌉₊) (suzukiActualT S) (fun (p : ℕ) => SwitchingPrinciple.suzukiVProduct S ↑p) (fun (n D' : ℕ) (x : ℝ) => SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H n (↑D') d x) 2 C K Δ M D (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) 2

Exact endpoint recurrence together with its fully instantiated pointwise IH.

def MathlibNt.SieveTheory.CaseIEvenEndpointSigma11Edge (S : BoundingSieve) (M D : ℕ) (K σ : ℝ) : Prop

The exact first missing analytic edge. Existing Σ₁₁ production requires 2-1 ∈ parityDomain 2 (M-1), which is false for even M; the carrier packet above is insufficient because the current Lemma-8.7 API asks for the formal closed lower endpoint rather than only the actual strict prime coordinates.

Equations

• MathlibNt.SieveTheory.CaseIEvenEndpointSigma11Edge S M D K σ = (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaEleven (MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / 2)⌉₊) (⇑S.nu) (fun (p : ℕ) => MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑p) (MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / 2)⌉₊) 2 M D σ 2 ≤ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / 2)⌉₊ * MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 M 2 + MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / 2)⌉₊ * (6 * K ^ 2 * MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (M - 1) 1 / Real.log (↑D ^ (1 / σ))))