theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.fixedGap_rpow_margin {gap M : ℝ} (hgap0 : 0 < gap) (hgap1 : gap < 1) (hM : 4 ≤ M) : (1 - 1 / (M + 2)) ^ (gap / 2) < 1 - gap / (4 * M)

A fixed positive gap gives a strict power saving beyond the head-budget margin.