theorem MathlibNt.SieveTheory.caseI1423EndpointSourceBounds_sharp_of_source (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 : ∀ (N : ℕ) (s : ℝ), 2 ≤ N → 2 ≤ s → s - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1) → SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) (s - 1) ≤ L * ((s - 1) * H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite (s - 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 N : ℕ) (s : ℝ) : 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 → 2 ≤ N → 2 ≤ s → s - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1) → s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → have σ := SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d; have z := ⌈↑D ^ (1 / s)⌉₊; have B := sigma12InheritedBudget S H N D z C K d Δ s; caseI1423Sigma11Endpoint S N D z K s σ ≤ 6 * L * R / (C * Real.exp √K) * caseI1423RemainderUnit B (↑D) σ ∧ caseI1423Sigma12Endpoint S H N D z C K d Δ s σ ≤ 12 * R * caseI1423RemainderUnit B (↑D) σ

Sharp pointwise endpoint bounds with the two explicit coefficients exposed.

theorem MathlibNt.SieveTheory.exists_lemma14_4_caseI_final_producer_sourceLargeLog_pointwise_uniform_in_S (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hsrc : SuzukiClaim145SourceParameters d Δ Θ) : ∃ (C1min : ℝ) (CB : ℝ), 1 ≤ C1min ∧ 0 < CB ∧ ∀ (S : BoundingSieve) (C1 C K : ℝ) (M D : ℕ) (s : ℝ), C1min ≤ C1 → max 3 CB ≤ C → 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ M → s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 M → s - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (M - 1) → 2 ≤ s → 2 + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth M).epsilon ≤ s → C1 * K ^ Θ < Real.log ↑D → s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → H.betaHat + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth M).epsilon < s → Lemma144MovingDomainGlobalDepthAt S H C K d Δ (M - 1) 2 → suzukiActualT S M D ⌈↑D ^ (1 / s)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / s)⌉₊ * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 M s + sigma12InheritedBudget S H M D ⌈↑D ^ (1 / s)⌉₊ C K d Δ s

Production strict Case-I pointwise producer, uniform in the bounding sieve. The cutoff constants precede S,C1,C,K,M,D,s; the predecessor induction threshold is literally 2.

theorem MathlibNt.SieveTheory.exists_lemma14_4_caseI_final_producer_sourceLargeLog_pointwise (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hsrc : SuzukiClaim145SourceParameters d Δ Θ) : ∃ (C1min : ℝ) (CB : ℝ), 1 ≤ C1min ∧ 0 < CB ∧ ∀ (C1 C K : ℝ) (M D : ℕ) (s : ℝ), C1min ≤ C1 → max 3 CB ≤ C → 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ M → s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 M → s - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (M - 1) → 2 ≤ s → 2 + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth M).epsilon ≤ s → C1 * K ^ Θ < Real.log ↑D → s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → H.betaHat + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth M).epsilon < s → Lemma144MovingDomainGlobalDepthAt S H C K d Δ (M - 1) 2 → suzukiActualT S M D ⌈↑D ^ (1 / s)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / s)⌉₊ * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 M s + sigma12InheritedBudget S H M D ⌈↑D ^ (1 / s)⌉₊ C K d Δ s

Compatibility specialization of the producer uniform in S.