Lemma 14.4 Case II: exact final dispatcher boundary

The accepted double-rounded endpoint starts at 2 ≤ N; for odd depths this is the range 3 ≤ N. The source-native base theorem instead gives the depth-one bound with local remainder 9 K / (s log D). This file records the exact common same-C eventual conclusion and proves that these two disjoint producers are sufficient. It also names the first producer still absent from the accepted chain: absorption of the depth-one local remainder into the same C envelope.

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

The natural-ceiling Lemma-14.4 estimate at one parameter value. The constant C occurs literally in the conclusion and is therefore shared by the base and odd-successor branches.

Equations

• MathlibNt.SieveTheory.Lemma144CaseIISameCAt S H N D d Δ C K s = (∑ n ∈ Finset.Icc 1 N with n % 2 = N % 2, MathlibNt.SieveTheory.suzukiSourceV S n D ⌈↑D ^ (1 / s)⌉₊ ≤ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / s)⌉₊ * (MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N s + C * Real.exp √K * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s * Real.log ↑D ^ (-Δ)))

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

Eventual source-parameter form of the same-C Case-II conclusion. The moving analytic endpoint used by the successor proof is literally sourceSigma D d; it is exposed here so the producer cannot silently revert to a fixed σ.

Equations

• MathlibNt.SieveTheory.Lemma144CaseIISameCEventuallyAtSourceSigma S H N d Δ C K s = ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℕ), D₀ ≤ ↑D → have σ := MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d; 3 ≤ σ ∧ MathlibNt.SieveTheory.Lemma144CaseIISameCAt S H N D d Δ C K s

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

Exact missing base producer. lemma14_4_base_one_natCeil proves only the antecedent displayed here. Closing this implication eventually is precisely the required absorption of 9 K/(s log D) into the same C error envelope; no endpoint, recurrence, or main-sum estimate is hidden in the signature.

Equations

• MathlibNt.SieveTheory.Lemma144CaseIIBaseOneSameCProducer S H d Δ C K s = ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℕ), D₀ ≤ ↑D → have z := ⌈↑D ^ (1 / s)⌉₊; 3 ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ∧ (MathlibNt.SieveTheory.suzukiSourceV S 1 D z ≤ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑z * (MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 1 s + 9 * K / (s * Real.log ↑D)) → MathlibNt.SieveTheory.Lemma144CaseIISameCAt S H 1 D d Δ C K s)

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

The accepted Case-II endpoint must ultimately export this restricted producer. Restricting it to 3 ≤ N exactly matches its premise 2 ≤ N on odd natural depths and avoids demanding a false depth-one instance.

Equations

• MathlibNt.SieveTheory.Lemma144CaseIIOddSuccessorSameCProducer S H d Δ C K s = ∀ (N : ℕ), Odd N → 3 ≤ N → MathlibNt.SieveTheory.Lemma144CaseIISameCEventuallyAtSourceSigma S H N d Δ C K s

theorem MathlibNt.SieveTheory.lemma14_4_caseII_sameC_eventually_at_sourceSigma_of_base_successor {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} {N : ℕ} {d Δ C K s : ℝ} (hD : ∀ᶠ (D : ℕ) in Filter.atTop, 1 < ↑D) (hdom : s ∈ SuzukiFiniteContinuousLayers.suzukiParityDomainOne 2 N) (hs3 : s ≤ 3) (hroot2 : ∀ᶠ (D : ℕ) in Filter.atTop, 2 ≤ ↑D ^ (1 / s)) (hK : 0 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hbase : Lemma144CaseIIBaseOneSameCProducer S H d Δ C K s) (hsuccessor : Lemma144CaseIIOddSuccessorSameCProducer S H d Δ C K s) (hN : Odd N) : Lemma144CaseIISameCEventuallyAtSourceSigma S H N d Δ C K s

Complete Case-II logical assembly. Both branches use the identical fixed C, and both thresholds precede the natural source parameter D.