theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.carrier_logRatio_range {D p : ℕ} (hp : 2 ≤ p) (hDp : 2 * p ≤ D) : 1 < Real.log ↑D / Real.log ↑p ∧ Real.log ↑D / Real.log ↑p ≤ Real.log ↑D / Real.log 2

The logarithmic coordinate of a natural carrier lies in the source range needed in (14.13).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_13_pointwise_of_log_coordinates (H : Section13HatLayers) {N : ℕ} (hN : 1 ≤ N) {D d Δ s x ℓ : ℝ} (hℓ : 0 < ℓ) (hs : 1 < s) (hd : 1 < d) (_hΔ : 0 < Δ) (hlogD : Real.log D = ℓ * s) (hlogx : Real.log x = ℓ * (s - 1)) (hT : 0 ≤ H.T (ErrorSign.ofDepth N).opposite (s - 1)) : Claim14_13PointwisePremise H N D d Δ s x

The real-variable algebra and monotonicity immediately preceding source (14.13). The two logarithm identities say log D = s log p and log x = (s-1) log p; they are kept abstract here so the natural carrier specialization below does not hide the source calculation.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_13_pointwise_carrier (H : Section13HatLayers) {N D p : ℕ} {d Δ : ℝ} (hN : 1 ≤ N) (hp : 2 ≤ p) (hDp : 2 * p ≤ D) (hd : 1 < d) (hΔ : 0 < Δ) (hT : 0 ≤ H.T (ErrorSign.ofDepth (N - 1)) (Real.log ↑D / Real.log ↑p - 1)) : Claim14_13PointwisePremise H N (↑D) d Δ (Real.log ↑D / Real.log ↑p) (↑D / ↑p)

Source (14.13), internalized for a natural carrier prime/cutoff p before any natural-ceiling displacement is introduced.