Claim 14.5: closed source assembly boundary

This module first combines the three genuine Case-A producers. It then records an end-to-end source theorem whose Case-B argument is the exact uniform-in-C1 closed producer required by the paper. In particular, the eventual-in-D claim145_sourceSigma_allS_internal theorem is not silently promoted to this stronger quantifier order.

theorem MathlibNt.SieveTheory.exists_claim145_caseA_closed_uniform_in_S (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ C1 Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd2 : 2 < d) (hC1 : 0 < C1) (hΘ : 0 < Θ) (hsource : 2 / d < 1 / Θ) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hgap : 0 < d - 2 * Θ) : ∃ (K0 : ℝ) (CA : ℝ), 2 ≤ K0 ∧ 0 < CA ∧ ∀ (S : BoundingSieve), Claim145CaseABoundedKClosed S H d Δ C1 Θ K0 CA ∧ Claim145CaseALargeKLowSClosed S H d Δ C1 Θ K0 CA ∧ Claim145CaseALargeKHighSClosed S H d Δ C1 Θ K0 CA

The three Case-A branches with thresholds and coefficient selected before any bounding sieve.

theorem MathlibNt.SieveTheory.exists_claim145_caseA_closed (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ C1 Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd2 : 2 < d) (hC1 : 0 < C1) (hΘ : 0 < Θ) (hsource : 2 / d < 1 / Θ) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hgap : 0 < d - 2 * Θ) : ∃ (K0 : ℝ) (CA : ℝ), 2 ≤ K0 ∧ 0 < CA ∧ Claim145CaseABoundedKClosed S H d Δ C1 Θ K0 CA ∧ Claim145CaseALargeKLowSClosed S H d Δ C1 Θ K0 CA ∧ Claim145CaseALargeKHighSClosed S H d Δ C1 Θ K0 CA

The three production Case-A leaves give one threshold and one positive constant. The bounded range is closed only after the two large-K thresholds have been fixed, so its finite-range constant has the correct dependence.

theorem MathlibNt.SieveTheory.claim145_source_actual_of_uniform_caseB_uniform_in_S (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ C1 Θ C1min CB : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd2 : 2 < d) (hC1pos : 0 < C1) (hΘ : 0 < Θ) (hsource : 2 / d < 1 / Θ) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hgap : 0 < d - 2 * Θ) (hC1 : C1min ≤ C1) (hB : ∀ (S : BoundingSieve), Claim145CaseBClosed S H d Δ Θ C1min CB) : ∃ (C145 : ℝ), 0 < C145 ∧ ∀ (S : BoundingSieve) (K : ℝ) (N D : ℕ) (s : ℝ), 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → 2 ≤ s → Real.log ↑D ≤ C1 * K ^ Θ ∨ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ≤ s → ActualClaim145BoundAt S H N D d Δ K s C145

Complete source Claim 14.5 uniformly in the varying bounding sieve.

theorem MathlibNt.SieveTheory.claim145_source_actual_of_uniform_caseB (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ C1 Θ C1min CB : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd2 : 2 < d) (hC1pos : 0 < C1) (hΘ : 0 < Θ) (hsource : 2 / d < 1 / Θ) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hgap : 0 < d - 2 * Θ) (hC1 : C1min ≤ C1) (hB : Claim145CaseBClosed S H d Δ Θ C1min CB) : ∃ (C145 : ℝ), 0 < C145 ∧ ∀ (K : ℝ) (N D : ℕ) (s : ℝ), 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → 2 ≤ s → Real.log ↑D ≤ C1 * K ^ Θ ∨ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ≤ s → ActualClaim145BoundAt S H N D d Δ K s C145

Complete source Claim 14.5 after supplying a genuine Case-B producer with CB and C1min chosen before the varying C1. The source disjunction is kept literal. Crucially, the final constant is chosen before K,N,D,s.

theorem MathlibNt.SieveTheory.claim145_source_claim14_5Bound_of_uniform_caseB (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ C1 Θ C1min CB : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd2 : 2 < d) (hC1pos : 0 < C1) (hΘ : 0 < Θ) (hsource : 2 / d < 1 / Θ) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hgap : 0 < d - 2 * Θ) (hC1 : C1min ≤ C1) (hB : Claim145CaseBClosed S H d Δ Θ C1min CB) : ∃ (C145 : ℝ), 0 < C145 ∧ ∀ (K : ℝ) (N D : ℕ) (s : ℝ), 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → 2 ≤ s → Real.log ↑D ≤ C1 * K ^ Θ ∨ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ≤ s → SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5Bound (fun (m : ℕ) (D' z' : ℝ) => suzukiActualT S m ⌈D'⌉₊ ⌈z'⌉₊) S H N (↑D) (↑⌈↑D ^ (1 / s)⌉₊) d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) K s C145

Public Claim14_5Bound spelling of the complete source result, retaining the same constant-before-variables quantifier order.

theorem MathlibNt.SieveTheory.claim145_actual_to_caseI_endpoint_provider (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N D : ℕ} {d Δ C1 Θ K C145 : ℝ} (hN2 : 2 ≤ N) (hOddBoundary : Odd N → ⌈↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)⌉₊ ^ 3 ≤ D) (hclaim : SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5Regime 2 (↑D) (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) C1 K Θ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) → ActualClaim145BoundAt S H N D d Δ K (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) C145) : SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5Regime 2 (↑D) (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) C1 K Θ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) → ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)⌉₊, S.nu p * ∑ m ∈ sourceParityIndices (N - 1), suzukiSourceV S m (D ⌈/⌉ p) p ≤ C145 * SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N (↑D) d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) K (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)

Direct Claim-14.5 endpoint provider for the hEndpoint argument of caseI_total_le_sigma0_add_sigma11_add_sigma12. This is the source induction interface: the exact recurrence identifies the endpoint prime sum with suzukiActualT; no Dmin or hybrid finite-quotient split is introduced.