theorem MathlibNt.SieveTheory.caseI_endpoint_sigma11_normalization (K σ logσ logD logLog Δ : ℝ) (hlog : 0 < logD) (hll : 0 < logLog) (hσ : 0 < σ) (hscalar : K ^ 2 * σ ^ 3 * logσ * logLog ≤ logD ^ (1 - Δ)) (hpowe : logD ^ (-Δ) * logD = logD ^ (1 - Δ)) : K ^ 2 * σ ^ 2 * logσ / logD ≤ logD ^ (-Δ) / (logLog * σ)

Normalize the Case-I sigma-eleven scalar factor using the sigma-cubed bound.