theorem
MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.carrier_logRatio_range
{D p : ℕ}
(hp : 2 ≤ p)
(hDp : 2 * p ≤ D)
:
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.