Claim 14.5: source Case-A / Case-B interface

This is the source branch dispatcher, not the later Lemma-14.4 Case-I/Case-II split. Its public disjunction is literally

log D ≤ C1 * K^Θ ∨ sourceSigma D d ≤ s.

Every branch contract below returns the actual discrete Claim-14.5 inequality. In particular, the open low-s scalar target and the high-s logarithmic-gain lemma are not accepted as substitutes for a closed Case-A branch.

def MathlibNt.SieveTheory.ActualClaim145BoundAt (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (N D : ℕ) (d Δ K s C145 : ℝ) : Prop

Claim 14.5 for the actual discrete parity sum and the literal natural ceiling cutoff attached to the coordinate s.

Equations

• MathlibNt.SieveTheory.ActualClaim145BoundAt S H N D d Δ K s C145 = (MathlibNt.SieveTheory.suzukiActualT S N D ⌈↑D ^ (1 / s)⌉₊ ≤ C145 * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N (↑D) d Δ (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) K s)

theorem MathlibNt.SieveTheory.claim14_5Scale_nonneg_on_source_domain (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N D : ℕ} {d Δ K s : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hD : 2 ≤ D) (hs : 2 ≤ s) : 0 ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N (↑D) d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) K s

The Claim-14.5 scale is nonnegative on its source domain. This permits branch constants to be enlarged without hiding any analytic premise.

theorem MathlibNt.SieveTheory.ActualClaim145BoundAt.mono_constant (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N D : ℕ} {d Δ K s C C' : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hD : 2 ≤ D) (hs : 2 ≤ s) (hCC' : C ≤ C') (h : ActualClaim145BoundAt S H N D d Δ K s C) : ActualClaim145BoundAt S H N D d Δ K s C'

Enlarging the multiplicative constant preserves the actual Claim bound.

def MathlibNt.SieveTheory.Claim145CaseABoundedKClosed (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (d Δ C1 Θ K0 CA : ℝ) : Prop

The bounded-K piece suppressed by the paper's implicit-constant notation. The constant is chosen before K,N,D,s; hence this is genuinely uniform on 2 ≤ K ≤ K0, rather than a pointwise compactness assertion.

Equations

• MathlibNt.SieveTheory.Claim145CaseABoundedKClosed S H d Δ C1 Θ K0 CA = ∀ (K : ℝ) (N D : ℕ) (s : ℝ), 2 ≤ K → K ≤ K0 → MathlibNt.SieveTheory.SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → 2 ≤ s → Real.log ↑D ≤ C1 * K ^ Θ → MathlibNt.SieveTheory.ActualClaim145BoundAt S H N D d Δ K s CA

def MathlibNt.SieveTheory.Claim145CaseALargeKLowSClosed (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (d Δ C1 Θ K0 CA : ℝ) : Prop

Large-K, low-coordinate half of source Case A. This contract is closed only when it returns the final actual bound, not merely the frozen big-O scalar target from C2Claim145CaseALowS.

Equations

• MathlibNt.SieveTheory.Claim145CaseALargeKLowSClosed S H d Δ C1 Θ K0 CA = ∀ (K : ℝ) (N D : ℕ) (s : ℝ), K0 ≤ K → MathlibNt.SieveTheory.SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → 2 ≤ s → s ≤ √K / Real.log K → Real.log ↑D ≤ C1 * K ^ Θ → MathlibNt.SieveTheory.ActualClaim145BoundAt S H N D d Δ K s CA

def MathlibNt.SieveTheory.Claim145CaseALargeKHighSClosed (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (d Δ C1 Θ K0 CA : ℝ) : Prop

Large-K, high-coordinate half of source Case A. The logarithmic-gain lemmas are upstream ingredients; this contract demands their completed composition with Lemma 14.3 and Proposition 13.1(ii).

Equations

• MathlibNt.SieveTheory.Claim145CaseALargeKHighSClosed S H d Δ C1 Θ K0 CA = ∀ (K : ℝ) (N D : ℕ) (s : ℝ), K0 ≤ K → MathlibNt.SieveTheory.SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → 2 ≤ s → √K / Real.log K ≤ s → Real.log ↑D ≤ C1 * K ^ Θ → MathlibNt.SieveTheory.ActualClaim145BoundAt S H N D d Δ K s CA

theorem MathlibNt.SieveTheory.claim145_caseA_closed_of_boundedK_lowS_highS (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ C1 Θ K0 CA : ℝ} (hbounded : Claim145CaseABoundedKClosed S H d Δ C1 Θ K0 CA) (hlow : Claim145CaseALargeKLowSClosed S H d Δ C1 Θ K0 CA) (hhigh : Claim145CaseALargeKHighSClosed S H d Δ C1 Θ K0 CA) (K : ℝ) (N D : ℕ) (s : ℝ) : 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → 2 ≤ s → Real.log ↑D ≤ C1 * K ^ Θ → ActualClaim145BoundAt S H N D d Δ K s CA

Honest assembly of source Case A, including the bounded-K range.

def MathlibNt.SieveTheory.Claim145CaseBClosed (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (d Δ Θ C1min CB : ℝ) : Prop

Source Case B. CB and C1min are fixed before C1; this makes the paper's assertion that the Case-B implicit constant is independent of C1 visible in the quantifier order. C1min ≤ C1 records that the source first chooses C1 sufficiently large.

Equations

• MathlibNt.SieveTheory.Claim145CaseBClosed S H d Δ Θ C1min CB = ∀ (C1 K : ℝ) (N D : ℕ) (s : ℝ), C1min ≤ C1 → 2 ≤ K → MathlibNt.SieveTheory.SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → 2 ≤ s → C1 * K ^ Θ < Real.log ↑D → MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ≤ s → MathlibNt.SieveTheory.ActualClaim145BoundAt S H N D d Δ K s CB

theorem MathlibNt.SieveTheory.claim145_actual_of_source_disjunction (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ C1 Θ C1min CA CB K s : ℝ} {N D : ℕ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hC1 : C1min ≤ C1) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hD : 2 ≤ D) (hs : 2 ≤ s) (hA : ∀ (K : ℝ) (N D : ℕ) (s : ℝ), 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → 2 ≤ s → Real.log ↑D ≤ C1 * K ^ Θ → ActualClaim145BoundAt S H N D d Δ K s CA) (hB : Claim145CaseBClosed S H d Δ Θ C1min CB) (hregime : Real.log ↑D ≤ C1 * K ^ Θ ∨ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ≤ s) : ActualClaim145BoundAt S H N D d Δ K s (max CA CB)

Complete source-disjunction assembler. Case A may have a C1-dependent constant CA; Case B uses a constant CB selected independently of C1. The final public constant is their maximum.

theorem MathlibNt.SieveTheory.claim145_actual_of_closed_source_branches (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ C1 Θ K0 C1min CA CB K s : ℝ} {N D : ℕ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hC1 : C1min ≤ C1) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hD : 2 ≤ D) (hs : 2 ≤ s) (hbounded : Claim145CaseABoundedKClosed S H d Δ C1 Θ K0 CA) (hlow : Claim145CaseALargeKLowSClosed S H d Δ C1 Θ K0 CA) (hhigh : Claim145CaseALargeKHighSClosed S H d Δ C1 Θ K0 CA) (hB : Claim145CaseBClosed S H d Δ Θ C1min CB) (hregime : Real.log ↑D ≤ C1 * K ^ Θ ∨ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ≤ s) : ActualClaim145BoundAt S H N D d Δ K s (max CA CB)

End-to-end branch assembly. This theorem accepts exactly three completed Case-A leaves (bounded K, large-K low s, and large-K high s) plus the completed Case-B leaf, and returns the literal source disjunction. None of the four inputs may be replaced by a scalar target, logarithmic gain, or endpoint- only theorem.