The Case-I recursive coordinate lies below the quotient source endpoint

This is a genuine moving-carrier estimate. It uses both power inequalities in sigmaOneCarrier; in particular, it does not replace the carrier by an asymptotically empty fixed finite support.

theorem MathlibNt.SieveTheory.recursiveCoordinate_le_quotient_sourceSigma {d : ℝ} (hd : 1 < d) {D p : ℕ} (hD : Real.exp (MathlibNt.SieveTheory.sourceRatioStart✝ d) ^ 2 ≤ ↑D) (hp : Nat.Prime p) {s : ℝ} (hs : 2 ≤ s) (hlower : ↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ ↑p) (hupper : ↑p < ↑D ^ (1 / s)) : SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑(D ⌈/⌉ p)) d

Pointwise form, independent of any finite support.

theorem MathlibNt.SieveTheory.eventually_recursiveCoordinate_le_quotient_sourceSigma_uniform {d : ℝ} (hd : 1 < d) : ∀ᶠ (D : ℕ) in Filter.atTop, ∀ (S : BoundingSieve) (s : ℝ), 2 ≤ s → ∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier S.prodPrimes.primeFactors D (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) s, SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑(D ⌈/⌉ p)) d

Uniform Case-I carrier actualization with the threshold chosen before any sieve. The proof and cutoff depend only on d.

theorem MathlibNt.SieveTheory.eventually_recursiveCoordinate_le_quotient_sourceSigma (S : BoundingSieve) {d : ℝ} (hd : 1 < d) : ∀ᶠ (D : ℕ) in Filter.atTop, ∀ (s : ℝ), 2 ≤ s → ∀ p ∈ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier S.prodPrimes.primeFactors D (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) s, SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑(D ⌈/⌉ p)) d

Compatibility wrapper for the original sieve-first API.