Lemma 14.3 / Claim 14.5 comparison: internal quantitative bridge

This file keeps the Proposition 13.1(ii) lower estimate independent of every Claim-14.5 assertion. It also records explicitly the loss caused by replacing the real power cutoff by its natural ceiling.

theorem MathlibNt.SieveTheory.claim145_natCeil_rpow_le {D : ℕ} {s : ℝ} (hD : 2 ≤ D) (hs : 2 ≤ s) : ⌈↑D ^ (1 / s)⌉₊ ≤ D

For D ≥ 2 and s ≥ 2, the natural ceiling of D^(1/s) is still at most D. Thus the ceiling does not force the Lemma-14.1 logarithmic parameter to be evaluated beyond D.

theorem MathlibNt.SieveTheory.suzukiSourceL_mono {x y K : ℝ} (hx : 1 < x) (hxy : x ≤ y) : suzukiSourceL x K ≤ suzukiSourceL y K

Monotonicity of the explicit Lemma-14.1 source parameter on the range where both inner logarithms are positive.

theorem MathlibNt.SieveTheory.suzukiSourceL_natCeil_rpow_le {D : ℕ} {s K : ℝ} (hD : 2 ≤ D) (hs : 2 ≤ s) : suzukiSourceL (↑⌈↑D ^ (1 / s)⌉₊) K ≤ suzukiSourceL (↑D) K

The actual ceiling cutoff has no larger Lemma-14.1 logarithmic parameter than the unrounded ambient cutoff D. This is the ceiling-sensitive estimate needed before any asymptotic comparison.

theorem MathlibNt.SieveTheory.claim14_5Scale_lower_of_proposition131ii (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N : ℕ} {D d Δ σ K C M s : ℝ} (hD : 1 < D) (hσ : 0 < σ) (hs : 0 < s) (hM : M ≤ s) (hprop : ∀ (sign : SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) (t : ℝ), M ≤ t → SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiLowerProfile C t ≤ H.T sign t) : SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5VProduct S D * (Real.exp √K / (Real.log D * σ)) * ((1 + s ^ d / Real.log D) ^ s * s * SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiLowerProfile C s) * Real.log D ^ (-Δ) ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N D d Δ σ K s

The Proposition-13.1(ii) lower profile gives a literal lower bound for the Claim-14.5 scale. This step is uniform in the parity/depth N; the only use of N is to select one of the two signs covered by the source theorem.

theorem MathlibNt.SieveTheory.suzukiLemma14_3_le_claim145Scale_of_scalar_at (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N D : ℕ} {d Δ σ K C M C145 s : ℝ} (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hD : 2 ≤ D) (hσ : 0 < σ) (hs : 2 ≤ s) (hM : M ≤ s) (hKpos : 0 < K) (hC145 : 0 ≤ C145) (hprop : ∀ (sign : SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) (t : ℝ), M ≤ t → SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiLowerProfile C t ≤ H.T sign t) (hsourceLarge : Real.exp 1 * suzukiSourceL (↑D) K ≤ s - 2) (hscalar : Real.exp (suzukiSourceL (↑D) K + (s - 2) * (1 + Real.log (suzukiSourceL (↑D) K) - Real.log (s - 2))) ≤ C145 * (SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5VProduct S ↑D * (Real.exp √K / (Real.log ↑D * σ)) * ((1 + s ^ d / Real.log ↑D) ^ s * s * SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiLowerProfile C s) * Real.log ↑D ^ (-Δ))) : suzukiActualT S N D ⌈↑D ^ (1 / s)⌉₊ ≤ C145 * SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N (↑D) d Δ σ K s

Two-parameter Case-B closure of Lemma 14.3. Here σ is Suzuki's (log D)^(1/d) log log (27D) (and remains in the denominator of (14.6)), whereas s is an arbitrary coordinate with s ≥ σ. The former endpoint lemma identified these parameters and therefore did not state the full Case-B range.

theorem MathlibNt.SieveTheory.suzukiLemma14_3_le_claim145Scale_of_scalar (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N D : ℕ} {d Δ σ K C M C145 : ℝ} (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hD : 2 ≤ D) (hσ : 2 ≤ σ) (hM : M ≤ σ) (hKpos : 0 < K) (hC145 : 0 ≤ C145) (hprop : ∀ (sign : SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) (t : ℝ), M ≤ t → SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiLowerProfile C t ≤ H.T sign t) (hsourceLarge : Real.exp 1 * suzukiSourceL (↑D) K ≤ σ - 2) (hscalar : Real.exp (suzukiSourceL (↑D) K + (σ - 2) * (1 + Real.log (suzukiSourceL (↑D) K) - Real.log (σ - 2))) ≤ C145 * (SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5VProduct S ↑D * (Real.exp √K / (Real.log ↑D * σ)) * ((1 + σ ^ d / Real.log ↑D) ^ σ * σ * SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiLowerProfile C σ) * Real.log ↑D ^ (-Δ))) : suzukiActualT S N D ⌈↑D ^ (1 / σ)⌉₊ ≤ C145 * SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N (↑D) d Δ σ K σ

Pointwise closure of Lemma 14.3 against the explicit Proposition-13.1(ii) lower profile. The final numerical premise is stated entirely in elementary real functions and contains neither Claim14_5Bound, claim14_5Scale, nor the discrete object. It is the scalar large-logarithm inequality to be discharged by the eventual asymptotic calculation.

theorem MathlibNt.SieveTheory.suzukiLemma14_3_le_claim145Scale_uniformN_of_scalar (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {D : ℕ} {d Δ σ K C M C145 : ℝ} (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hD : 2 ≤ D) (hσ : 2 ≤ σ) (hM : M ≤ σ) (hKpos : 0 < K) (hC145 : 0 ≤ C145) (hprop : ∀ (sign : SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) (t : ℝ), M ≤ t → SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiLowerProfile C t ≤ H.T sign t) (hsourceLarge : Real.exp 1 * suzukiSourceL (↑D) K ≤ σ - 2) (hscalar : Real.exp (suzukiSourceL (↑D) K + (σ - 2) * (1 + Real.log (suzukiSourceL (↑D) K) - Real.log (σ - 2))) ≤ C145 * (SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5VProduct S ↑D * (Real.exp √K / (Real.log ↑D * σ)) * ((1 + σ ^ d / Real.log ↑D) ^ σ * σ * SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiLowerProfile C σ) * Real.log ↑D ^ (-Δ))) (N : ℕ) : suzukiActualT S N D ⌈↑D ^ (1 / σ)⌉₊ ≤ C145 * SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N (↑D) d Δ σ K σ

The same comparison with the quantifier over the discrete depth moved after all analytic data. In particular one scalar estimate and one Proposition 13.1(ii) pair of signwise bounds work for every N.

Shared scalar comparisons for the endpoint and all-coordinate estimates

theorem MathlibNt.SieveTheory.claim14_5VProduct_lower_of_localProduct {S : BoundingSieve} {D K : ℝ} (hD : 2 ≤ D) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) : 1 ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5VProduct S D * (Real.log D / Real.log 2 * (1 + K / Real.log 2))

The dimension-one local-product contract gives the needed lower edge for Claim 14.5's finite Euler product.

theorem MathlibNt.SieveTheory.claim145_caseB_scalar_exponent_comparison {x q L s b C Q : ℝ} (hx : 0 < x) (_hq : 0 < q) (hL : 1 ≤ L) (hs : 4 ≤ s) (hQ : 0 < Q) (hqlog : q = Real.log x) (habsorb : L + 2 * Real.log s + 3 * q + |Real.log Q| ≤ s) (hgap : Real.log L + Real.log (Real.log (3 * s)) + C + 2 + Real.log 2 ≤ Real.log b) : Real.exp (L + (s - 2) * (1 + Real.log L - Real.log (s - 2))) ≤ Q / x ^ 3 * Real.exp (s * Real.log b - s * Real.log s - s * Real.log (Real.log (3 * s)) - C * s)

The scalar comparison in the literal Case-B variables. Unlike the endpoint specialization above, the harmless terms are absorbed directly at the actual coordinate s; this is what permits every s ≥ sourceSigma D d.

theorem MathlibNt.SieveTheory.claim145_scalar_exponent_comparison {x q L s b C Q : ℝ} (hx : 0 < x) (hq : 0 < q) (hL : 1 ≤ L) (hs : 4 ≤ s) (hQ : 0 < Q) (hqlog : q = Real.log x) (hLsq : L ≤ q ^ 2) (hlogs : Real.log s ≤ 3 * q) (habsorb : q ^ 2 + 9 * q + |Real.log Q| ≤ s) (hgap : Real.log L + Real.log (Real.log (3 * s)) + C + 2 + Real.log 2 ≤ Real.log b) : Real.exp (L + (s - 2) * (1 + Real.log L - Real.log (s - 2))) ≤ Q / x ^ 3 * Real.exp (s * Real.log b - s * Real.log s - s * Real.log (Real.log (3 * s)) - C * s)

Elementary logarithmic comparison used after all moving quantities have been bounded. It keeps the decisive negative -s log s term on both sides.