theorem MathlibNt.SieveTheory.evenEndpoint_carrier_scale (S : BoundingSieve) {D Dmin : ℕ} {σ : ℝ} (_hDmin : 2 ≤ Dmin) (hD : Dmin ^ 2 ≤ D) : SwitchingPrinciple.SuzukiLemma144Equation1410.CarrierQuotientThresholdGeometry S.prodPrimes.primeFactors D Dmin σ 2

theorem MathlibNt.SieveTheory.evenEndpoint_pointwiseContract_of_movingIH_sourceLargeConsumer (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 : Lemma144MovingDomainGlobalDepthAt 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

Actual strict endpoint carriers allow the moving predecessor IH to be instantiated without the illegal formal coordinate 1.

Closed-left-endpoint source control used by the even Case-I producer.

theorem MathlibNt.SieveTheory.lemma132_finiteSourceLayer_evenEndpoint_uniform_sourceLargeConsumer {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ∃ (L : ℝ), 1 ≤ L ∧ ∀ (M : ℕ), Even M → 2 ≤ M → SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (M - 1) 1 ≤ L * H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth M).opposite 1

The uniform Lemma-13.2 finite-layer estimate extends to the closed odd predecessor endpoint by one-sided continuity.

def MathlibNt.SieveTheory.CaseI1423EvenEndpointSourceBoundsSourceScalar (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ : ℝ) : Prop

Source-bound interface for the two endpoint remainders at even depth.

Equations

• MathlibNt.SieveTheory.CaseI1423EvenEndpointSourceBoundsSourceScalar S H C K d Δ = ∃ (A11 : ℝ) (A12 : ℝ), 0 ≤ A11 ∧ 0 ≤ A12 ∧ ∀ (D M : ℕ), 3 ≤ D → K ^ 2 * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ^ 3 * Real.log (Real.exp 1 * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) * Real.log (Real.log ↑D) / Real.log ↑D ^ (1 - Δ) ≤ 1 → Even M → 2 ≤ M → 2 ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → have σ := MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d; have z := ⌈↑D ^ (1 / 2)⌉₊; have B := MathlibNt.SieveTheory.sigma12InheritedBudget S H M D z C K d Δ 2; MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑z * (6 * K ^ 2 * MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (M - 1) 1 / Real.log (↑D ^ (1 / σ))) ≤ A11 * MathlibNt.SieveTheory.caseI1423RemainderUnit B (↑D) σ ∧ MathlibNt.SieveTheory.caseI1423Sigma12Endpoint S H M D z C K d Δ 2 σ ≤ A12 * MathlibNt.SieveTheory.caseI1423RemainderUnit B (↑D) σ

The proof below reuses the source-normalization algebra of (14.23); only its finite-layer input is replaced by the closed endpoint lemma above.

theorem MathlibNt.SieveTheory.caseI1423EndpointSourceBounds_evenEndpoint_explicit (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ L R : ℝ) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hC : 0 < C) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (_hd : 7 / (1 - Δ) < d) (hL : 1 ≤ L) (hfinite : ∀ (M : ℕ), Even M → 2 ≤ M → SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (M - 1) 1 ≤ L * H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth M).opposite 1) (hR : 1 ≤ R) (hratio : ∀ (sign : SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) (s σ : ℝ), 2 ≤ s → s ≤ σ → SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiiReverseRatio H sign s ≤ R * (σ * Real.log (Real.exp 1 * σ))) (D M : ℕ) : 3 ≤ D → K ^ 2 * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ^ 3 * Real.log (Real.exp 1 * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) * Real.log (Real.log ↑D) / Real.log ↑D ^ (1 - Δ) ≤ 1 → Even M → 2 ≤ M → 2 ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → have σ := SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d; have z := ⌈↑D ^ (1 / 2)⌉₊; have B := sigma12InheritedBudget S H M D z C K d Δ 2; SwitchingPrinciple.suzukiVProduct S ↑z * (6 * K ^ 2 * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (M - 1) 1 / Real.log (↑D ^ (1 / σ))) ≤ 6 * L * R / (C * Real.exp √K) * caseI1423RemainderUnit B (↑D) σ ∧ caseI1423Sigma12Endpoint S H M D z C K d Δ 2 σ ≤ 12 * R * caseI1423RemainderUnit B (↑D) σ

Closed-endpoint source bounds with the source-uniform constants exposed. This strengthened form is used by the pointwise source-large producer to choose its coefficient cutoff before the later common constant and K.

theorem MathlibNt.SieveTheory.caseI1423EndpointSourceBounds_evenEndpoint_of_sourceScalar (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ : ℝ) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hC : 0 < C) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) : CaseI1423EvenEndpointSourceBoundsSourceScalar S H C K d Δ

Closed-endpoint analogue of caseI1423EndpointSourceBoundsFinal.

theorem MathlibNt.SieveTheory.lemma14_4_caseI_evenEndpoint_sameC_successor_of_sourceScalar (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {Dmin : ℕ} {C C145 K d Δ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hC : 0 < C) (hC145 : 0 < C145) (hDmin : 2 ≤ Dmin) : ∀ᶠ (D : ℕ) in Filter.atTop, ∀ (M : ℕ), Even M → 2 ≤ M → 2 ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → K ^ 2 * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ^ 3 * Real.log (Real.exp 1 * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) * Real.log (Real.log ↑D) / Real.log ↑D ^ (1 - Δ) ≤ 1 → Lemma144MovingDomainGlobalDepthAt S H C K d Δ (M - 1) Dmin → suzukiActualT S M D ⌈↑D ^ (1 / 2)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / 2)⌉₊ * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 M 2 + sigma12InheritedBudget S H M D ⌈↑D ^ (1 / 2)⌉₊ C K d Δ 2

Even s=2 Case-I successor with the same error constant and moving IH.

theorem MathlibNt.SieveTheory.exists_lemma14_4_caseI_evenEndpoint_sameC_sourceLargeLog (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΘ : 0 < Θ) (hmargin : Δ + 2 / Θ < 1) (hd : 7 / (1 - (Δ + 2 / Θ)) < d) : ∃ (C1min : ℝ), 1 ≤ C1min ∧ ∀ (C1 C C145 K : ℝ) (Dmin : ℕ), C1min ≤ C1 → 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 0 < C → 0 < C145 → 2 ≤ Dmin → ∀ᶠ (D : ℕ) in Filter.atTop, ∀ (M : ℕ), Even M → 2 ≤ M → 2 ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → C1 * K ^ Θ < Real.log ↑D → Lemma144MovingDomainGlobalDepthAt S H C K d Δ (M - 1) Dmin → suzukiActualT S M D ⌈↑D ^ (1 / 2)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / 2)⌉₊ * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 M 2 + sigma12InheritedBudget S H M D ⌈↑D ^ (1 / 2)⌉₊ C K d Δ 2

Source-large-log even endpoint. C1min is selected before all later C1,C,C145,K,Dmin,D,M; the scalar endpoint input is discharged pointwise from C1*K^Theta < log D.