Case II, odd depth at least three: the remaining same-C normalization

The accepted rounded source chain ends with a relative bracket and an additive recursive endpoint term B₀ N D. The target Lemma144CaseIISameCAt contains neither that endpoint term nor a larger constant. The exact missing comparison is therefore the absorption of B₀ N D by the strict bracket gap 1 - caseIIConcreteRoundedRelativeBracket ....

The definitions below keep the large-D cutoff before s, and permit the cutoff to depend on the fixed finite depth N. The final theorem proves that this comparison, together with the accepted rounded-relative output, is exactly sufficient to construct Lemma144CaseIIOddSuccessorSameCProducer.

def MathlibNt.SieveTheory.Lemma144CaseIIOddRoundedRelativeProducer (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (B₀ : ℕ → ℕ → ℝ) (d Δ C K : ℝ) : Prop

Exact output shape of the accepted rounded Case-II source assembly, with a threshold uniform in s ∈ (1,3] (but allowed to depend on the fixed depth).

Equations

• MathlibNt.SieveTheory.Lemma144CaseIIOddRoundedRelativeProducer S H B₀ d Δ C K = ∀ (N : ℕ), Odd N → 3 ≤ N → ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℕ), D₀ ≤ ↑D → ∀ (s : ℝ), 1 < s → s ≤ 3 → 3 ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ∧ MathlibNt.SieveTheory.caseIISourceBracket✝ N (↑D) d Δ C K < 1 ∧ have z := ⌈↑D ^ (1 / s)⌉₊; ∑ n ∈ Finset.Icc 1 N with n % 2 = N % 2, MathlibNt.SieveTheory.suzukiSourceV S n D z ≤ B₀ N D + MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑z * (MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N s + MathlibNt.SieveTheory.caseIISameCScale✝ H N (↑D) d Δ C K s * MathlibNt.SieveTheory.caseIISourceBracket✝ N (↑D) d Δ C K)

def MathlibNt.SieveTheory.Lemma144CaseIIOddEndpointGapNormalization (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (B₀ : ℕ → ℕ → ℝ) (d Δ C K : ℝ) : Prop

Earliest missing normalization after the accepted rounded-relative assembly. It does not assume the desired successor inequality: it compares only the recursive endpoint term with the unused strict-bracket margin.

Equations

• MathlibNt.SieveTheory.Lemma144CaseIIOddEndpointGapNormalization S H B₀ d Δ C K = ∀ (N : ℕ), Odd N → 3 ≤ N → ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℕ), D₀ ≤ ↑D → ∀ (s : ℝ), 1 < s → s ≤ 3 → have z := ⌈↑D ^ (1 / s)⌉₊; B₀ N D ≤ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑z * (MathlibNt.SieveTheory.caseIISameCScale✝ H N (↑D) d Δ C K s * (1 - MathlibNt.SieveTheory.caseIISourceBracket✝ N (↑D) d Δ C K))

theorem MathlibNt.SieveTheory.caseII_sameC_of_relative_and_endpoint_gap {sourceSum V B₀ finiteLayer scale bracket : ℝ} (hB₀ : B₀ ≤ V * (scale * (1 - bracket))) (hrelative : sourceSum ≤ B₀ + V * (finiteLayer + scale * bracket)) : sourceSum ≤ V * (finiteLayer + scale)

Terminal algebra: the endpoint-gap comparison removes B₀ without changing C.

theorem MathlibNt.SieveTheory.lemma14_4_caseII_odd_successor_sameC_producer_of_endpoint_gap {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} {B₀ : ℕ → ℕ → ℝ} {d Δ C K s : ℝ} (hrelative : Lemma144CaseIIOddRoundedRelativeProducer S H B₀ d Δ C K) (hnormalize : Lemma144CaseIIOddEndpointGapNormalization S H B₀ d Δ C K) (hs1 : 1 < s) (hs3 : s ≤ 3) : Lemma144CaseIIOddSuccessorSameCProducer S H d Δ C K s

A uniform-in-s rounded-relative producer plus the exact endpoint-gap normalization constructs the actual dispatcher producer. The threshold may still depend on the fixed finite odd depth N, which is all the producer interface requires.