Case-II odd recursive endpoint: exact remaining scaling bridge

The accepted source-σ Claim 14.5 controls the recombined recursive endpoint at the scale

C145 * V(D) * exp(sqrt K) / (log D * sourceSigma D d) * E_N(D, sourceSigma D d) * (log D)^(-Δ).

The same-C endpoint-gap normalization instead requires this to fit below

V(⌈D^(1/s)⌉) * C * exp(sqrt K) * E_N(D,s) * (log D)^(-Δ) * (1 - caseIIConcreteRoundedRelativeBracket ...).

The theorem below consumes Claim 14.5 and isolates exactly that comparison. In particular, a bare proof that the bracket is < 1 supplies only positivity of the last factor and does not supply the quantitative lower bound needed to compare the two displayed scales uniformly in s.

noncomputable def MathlibNt.SieveTheory.caseIIOddClaim145Endpoint (S : BoundingSieve) (d : ℝ) (N D : ℕ) : ℝ

The literal endpoint to which the accepted source-σ Claim 14.5 applies.

Equations

• MathlibNt.SieveTheory.caseIIOddClaim145Endpoint S d N D = MathlibNt.SieveTheory.suzukiActualT S N D ⌈↑D ^ (1 / MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)⌉₊

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

The exact, expanded scale comparison still needed after applying the accepted source-σ Claim 14.5. The threshold is before s, as required by the odd endpoint normalization.

Equations

• MathlibNt.SieveTheory.Lemma144CaseIIOddClaim145ScalingBridge S H d Δ C K C145 = ∀ (N : ℕ), Odd N → 3 ≤ N → ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℕ), D₀ ≤ ↑D → ∀ (s : ℝ), 1 < s → s ≤ 3 → C145 * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N (↑D) d Δ (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) K (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / s)⌉₊ * (C * Real.exp √K * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s * Real.log ↑D ^ (-Δ) * (1 - MathlibNt.SieveTheory.caseIIConcreteRoundedRelativeBracket N (↑D) d Δ (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) C K))

theorem MathlibNt.SieveTheory.strict_bracket_lt_one_does_not_force_endpoint_absorption {endpoint budget : ℝ} (he : 0 < endpoint) (hb : 0 < budget) : ∃ bracket < 1, ¬endpoint ≤ budget * (1 - bracket)

A strict bracket inequality alone is quantitatively insufficient for endpoint absorption: even with positive endpoint and budget scales there are brackets strictly below one whose gap is too small.

theorem MathlibNt.SieveTheory.lemma144_caseII_odd_endpoint_gap_of_claim145_scaling_bridge (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ C K C145 : ℝ} (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hK : 0 < K) (hC145 : 0 < C145) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hscale : Lemma144CaseIIOddClaim145ScalingBridge S H d Δ C K C145) : Lemma144CaseIIOddEndpointGapNormalization S H (caseIIOddClaim145Endpoint S d) d Δ C K

Claim 14.5 closes the recursive endpoint-gap normalization exactly when the remaining scale bridge is supplied. No enlargement of the target constant C occurs.