Quantitative Case-II rounded-bracket gap

The existing contraction proof spends only 5/32 of the source tangent gap: the integral-transport excess costs 1/32 and the four endpoint terms cost 4/32. Thus the rounded bracket retains 27/32 of (1-Δ)/sourceSigma D d. In particular the true proved scale is 1/σ, stronger than the requested 1/(loglog D * σ) scale.

theorem MathlibNt.SieveTheory.exists_caseIIConcreteRoundedRelativeBracket_gap_threshold (N : ℕ) (K C d Δ : ℝ) (hF0 : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3) (hF1 : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) 2) (hK : 0 ≤ K) (hC : 0 ≤ C) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (D : ℝ), D0 ≤ D → 27 * (1 - Δ) / (32 * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) ≤ 1 - caseIIConcreteRoundedRelativeBracket N D d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) C K

Quantitative strengthening of exists_caseIIConcreteRoundedRelativeBracket_lt_one_threshold.

theorem MathlibNt.SieveTheory.exists_caseIIConcreteRoundedRelativeBracket_gap_threshold_scaleFree (N : ℕ) (K d Δ : ℝ) (hF0 : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3) (hF1 : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) 2) (hK : 0 ≤ K) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (D C : ℝ), D0 ≤ D → 27 * (1 - Δ) / (32 * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) ≤ 1 - caseIIConcreteRoundedRelativeBracket N D d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) C K

Scale-free form of the quantitative gap: one threshold works for every choice of the outer constant C.

theorem MathlibNt.SieveTheory.claim145_endpoint_absorbed_by_caseII_gap {VD Vz expK Eσ Es L logD σ C C145 Δ gap : ℝ} (hVD : 0 ≤ VD) (hV : VD ≤ Vz) (hexp : 0 ≤ expK) (hEσ : 0 ≤ Eσ) (hE : Eσ ≤ Es) (hL : 0 ≤ L) (hlog : 0 < logD) (hσ : 0 < σ) (hΔ1 : Δ ≤ 1) (hC145 : 0 ≤ C145) (hC : 0 ≤ C) (hgap : 27 * (1 - Δ) / (32 * σ) ≤ gap) (hconstant : C145 ≤ 27 * C * (1 - Δ) * logD / 32) : C145 * (VD * (expK / (logD * σ)) * Eσ * L) ≤ Vz * (C * expK * Es * L) * gap

Pure algebraic endpoint absorption. After V(D) ≤ V(z) and Claim 14.6(i) provide E(D,σ) ≤ E(D,s), the quantitative gap cancels the source 1/σ; the remaining Claim-14.5 factor 1/log D is absorbed by hconstant.

theorem MathlibNt.SieveTheory.exists_claim145_gap_constant_threshold {C C145 Δ : ℝ} (hC : 0 < C) (hΔ1 : Δ < 1) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (D : ℝ), D0 ≤ D → C145 ≤ 27 * C * (1 - Δ) * Real.log D / 32

The sole remaining scalar requirement in endpoint absorption is eventual and independent of s; positivity of the target constant C is essential.