Uniform Case-II endpoint coefficients

The Case-II source carrier does not eventually vanish with the odd depth. The uniform estimate instead comes from Suzuki Lemma 13.2: specialize (13.13) at the fixed endpoint coordinates 3 and 2, then dominate the depth sign by the maximum of the two fixed hat-layer values.

theorem MathlibNt.SieveTheory.caseII_endpoint_source_layers_uniform {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ∃ (L3 : ℝ) (L2 : ℝ), 0 ≤ L3 ∧ 0 ≤ L2 ∧ ∀ (N : ℕ), Odd N → 3 ≤ N → SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3 ≤ L3 ∧ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) 2 ≤ L2

Uniform-in-depth bounds for the two finite source layers occurring in the Case-II algebraic endpoint coefficient.

theorem MathlibNt.SieveTheory.caseII_algebraic_endpoint_coefficients_uniform {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {K : ℝ} (hK : 0 ≤ K) : ∃ (A0 : ℝ) (A1 : ℝ), 0 ≤ A0 ∧ 0 ≤ A1 ∧ ∀ (N : ℕ), Odd N → 3 ≤ N → caseIIAlgebraicEndpointCoeffA0 N K ≤ A0 ∧ caseIIAlgebraicEndpointCoeffA1 N K ≤ A1

For fixed source data and fixed K ≥ 0, both Case-II algebraic endpoint coefficients admit nonnegative bounds independent of the odd depth N.