Uniform exponent margins for the existing C.2 split

Reuse the existing factor exponents, including the S = 1 branch. These are scalar payment lemmas, not an assertion of the distribution estimate. Actual coefficient, carrier and local-frequency estimates are separate.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2_direct_secondary_exponent_margin {ν ε : ℝ} (hε : 0 ≤ ε) (hεν : ε ≤ ν) (hν : ν ≤ 1 / 10) : ν + 3 * c2RExponent ν ε / 4 + 3 * c2SExponent ν ε / 2 - 1 / 2 ≤ -(3 * ε / 4)

The secondary normalized exponent fits the existing split uniformly.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2_direct_normalized_margins {ν ε L : ℝ} (hε : 0 ≤ ε) (hεν : ε ≤ ν) (hν : ν ≤ 1 / 10) (hL : L ≤ ε / 4) : c2RExponent ν ε + c2SExponent ν ε / 2 - 1 / 2 + L ≤ -(ε / 2) ∧ 5 * ν / 4 + 7 * c2RExponent ν ε / 4 + 2 * c2SExponent ν ε - 1 + L ≤ -(ε / 2) ∧ ν + 3 * c2RExponent ν ε / 4 + 3 * c2SExponent ν ε / 2 - 1 / 2 + L ≤ -(ε / 2)

A common loss allowance, without changing the already used R/S split.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.c2_direct_loss_allowance {ε C : ℝ} (hε : 0 < ε) (hC : 0 ≤ C) : ∃ (η : ℝ), 0 < η ∧ η < ε ∧ C * η ≤ ε / 4

Choose an internal exponent after a fixed loss multiplier, before data.