Suzuki (14.10): finite assembly of the pointwise induction hypothesis

This file isolates exactly the finite step which turns the pointwise induction hypothesis for T_{N-1}(⌈D/p⌉,p) into Σ₁ ≤ Σ₁₁ + Σ₁₂. The recursive natural argument always uses ceiling division. The cutoff and continuous-layer coordinates are displayed explicitly as real powers/logarithms. No endpoint estimate for either resulting sum is assumed.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (support : Finset ℕ) (D : ℕ) (σ τ : ℝ) : Finset ℕ

The finite prime carrier in the range D^(1/σ) ≤ p < D^(1/τ). The casts make the real-power cutoffs explicit.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier support D σ τ = {p ∈ support | ↑D ^ (1 / σ) ≤ ↑p ∧ ↑p < ↑D ^ (1 / τ)}

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate (D p : ℕ) : ℝ

The continuous coordinate at the inherited depth in (14.10).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p = Real.log ↑D / Real.log ↑p - 1

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate (D p : ℕ) : ℝ

The coordinate obtained by applying the induction theorem literally at the natural recursive argument D ⌈/⌉ p.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p = Real.log ↑(D ⌈/⌉ p) / Real.log ↑p

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.coordinatePerturbation (D p : ℕ) : ℝ

The (nonnegative) coordinate displacement caused by natural ceiling division.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.coordinatePerturbation D p = MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p - MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.ceilDiv_mul_bounds {D p : ℕ} (hp : 0 < p) : D ≤ D ⌈/⌉ p * p ∧ D ⌈/⌉ p * p ≤ D + p - 1

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate_eq_log_div (D p : ℕ) (hD : 0 < D) (hp : 2 ≤ p) : inheritedCoordinate D p = Real.log (↑D / ↑p) / Real.log ↑p

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.coordinate_bounds {D p : ℕ} (hp : 2 ≤ p) (hDp : 2 * p ≤ D) : inheritedCoordinate D p ≤ recursiveCoordinate D p ∧ recursiveCoordinate D p ≤ inheritedCoordinate D p + Real.log (3 / 2) / Real.log ↑p

Exact direction and a uniform explicit size bound for the ceiling perturbation. The hypothesis 2 * p ≤ D is the natural-number form of the range condition 2 ≤ D / p.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.coordinate_bounds_sharp {D p : ℕ} (hp : 2 ≤ p) (hDp : 2 * p ≤ D) : inheritedCoordinate D p ≤ recursiveCoordinate D p ∧ recursiveCoordinate D p ≤ inheritedCoordinate D p + Real.log (1 + (↑p - 1) / ↑D) / Real.log ↑p

Sharper, D,p-dependent version of the upper bound. The coarse 3/2 bound above follows from (p-1)/D < 1/2; this version retains the full natural ceiling error.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.coordinatePerturbation_bounds {D p : ℕ} (hp : 2 ≤ p) (hDp : 2 * p ≤ D) : 0 ≤ coordinatePerturbation D p ∧ coordinatePerturbation D p ≤ Real.log (3 / 2) / Real.log ↑p

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.coordinatePerturbation_bounds_sharp {D p : ℕ} (hp : 2 ≤ p) (hDp : 2 * p ≤ D) : 0 ≤ coordinatePerturbation D p ∧ coordinatePerturbation D p ≤ Real.log (1 + (↑p - 1) / ↑D) / Real.log ↑p

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate_eq_inherited_add_perturbation (D p : ℕ) : recursiveCoordinate D p = inheritedCoordinate D p + coordinatePerturbation D p

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.finiteSourceLayer_recursive_le_inherited {β : ℝ} (hβ : 1 < β) (N D p : ℕ) (hp : 2 ≤ p) (hDp : 2 * p ≤ D) (hx : inheritedCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β N) (hy : recursiveCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β N) : SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N (recursiveCoordinate D p) ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N (inheritedCoordinate D p)

Proposition 9.3 has exactly the useful direction: since ceiling division increases the coordinate, antitonicity makes the literal recursive main term no larger than the source coordinate main term.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedErrorPerturbation (E : ℕ → ℕ → ℝ → ℝ) (n D p : ℕ) : ℝ

The error displacement is kept as an explicit additive term. No monotonicity of E is built into the induction contract.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedErrorPerturbation E n D p = E n (D ⌈/⌉ p) (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p) - E n (D ⌈/⌉ p) (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.error_at_recursive_eq_inherited_add_perturbation (E : ℕ → ℕ → ℝ → ℝ) (n D p : ℕ) : E n (D ⌈/⌉ p) (recursiveCoordinate D p) = E n (D ⌈/⌉ p) (inheritedCoordinate D p) + inheritedErrorPerturbation E n D p

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.error_recursive_le_inherited_of_antitoneOn (E : ℕ → ℕ → ℝ → ℝ) (n D p : ℕ) (hp : 2 ≤ p) (hDp : 2 * p ≤ D) (S : Set ℝ) (hx : inheritedCoordinate D p ∈ S) (hy : recursiveCoordinate D p ∈ S) (hanti : AntitoneOn (E n (D ⌈/⌉ p)) S) : E n (D ⌈/⌉ p) (recursiveCoordinate D p) ≤ E n (D ⌈/⌉ p) (inheritedCoordinate D p)

To discard the error perturbation one needs antitonicity, in the same direction as for the finite source layer. In particular this is the required extra input when E is instantiated by errorEnvelope; its Section-13 layer field is arbitrary, so the direction is not a consequence of that definition.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.ceilDiv_log_rpow_neg_le_div_log_rpow_neg {D p : ℕ} {Δ : ℝ} (hp : 2 ≤ p) (hDp : 2 * p ≤ D) (hΔ : 0 ≤ Δ) : Real.log ↑(D ⌈/⌉ p) ^ (-Δ) ≤ Real.log (↑D / ↑p) ^ (-Δ)

The logarithmic loss at the literal ceiling quotient is no larger than the source logarithmic loss at D / p. Positivity is recorded explicitly: the assumption 2 * p ≤ D puts both logarithm arguments in (1,∞), while 0 ≤ Δ makes the exponent -Δ nonpositive.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.errorEnvelope_antitone_cutoff (H : SuzukiLemma144KappaOne.Section13HatLayers) (n : ℕ) {X Y d s : ℝ} (hX : 1 < X) (hXY : X ≤ Y) (hs : 0 ≤ s) (hT : 0 ≤ H.T (SuzukiLemma144KappaOne.ErrorSign.ofDepth n) s) : SuzukiLemma144KappaOne.errorEnvelope H n Y d s ≤ SuzukiLemma144KappaOne.errorEnvelope H n X d s

For a fixed nonnegative source coordinate, the explicit error envelope is antitone in its cutoff argument. This is the cutoff-coordinate comparison needed because ⌈D/p⌉ ≥ D/p.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.naturalCeil_error_le_claim14_13 (H : SuzukiLemma144KappaOne.Section13HatLayers) {N D p : ℕ} {d Δ : ℝ} (hp : 2 ≤ p) (hDp : 2 * p ≤ D) (hΔ : 0 ≤ Δ) (S : Set ℝ) (hinherited : inheritedCoordinate D p ∈ S) (hrecursive : recursiveCoordinate D p ∈ S) (hanti : AntitoneOn (SuzukiLemma144KappaOne.errorEnvelope H (N - 1) (↑(D ⌈/⌉ p)) d) S) (hT : 0 ≤ H.T (SuzukiLemma144KappaOne.ErrorSign.ofDepth (N - 1)) (inheritedCoordinate D p)) (h1413 : SuzukiLemma144KappaOne.Claim14_13PointwisePremise H N (↑D) d Δ (Real.log ↑D / Real.log ↑p) (↑D / ↑p)) : SuzukiLemma144KappaOne.errorEnvelope H (N - 1) (↑(D ⌈/⌉ p)) d (recursiveCoordinate D p) * Real.log ↑(D ⌈/⌉ p) ^ (-Δ) ≤ Real.log ↑D ^ (-Δ) * SuzukiLemma144KappaOne.qD H (SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite (↑D) d Δ (Real.log ↑D / Real.log ↑p)

Pointwise closure of the two ceiling discrepancies against source (14.13).

hanti removes the displacement from the literal recursive coordinate to the source coordinate. hcutoff is the separate monotonicity comparison in the cutoff argument of errorEnvelope, from ⌈D/p⌉ down to the source cutoff D/p. The preceding lemma then enlarges only the logarithmic factor. Thus the final hypothesis is exactly the existing source-level Claim14_13PointwisePremise, with every positivity/domain input visible.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.naturalCeil_error_normalized_le_qD (H : SuzukiLemma144KappaOne.Section13HatLayers) {N D p : ℕ} {d Δ : ℝ} (hp : 2 ≤ p) (hDp : 2 * p ≤ D) (hΔ : 0 ≤ Δ) (S : Set ℝ) (hinherited : inheritedCoordinate D p ∈ S) (hrecursive : recursiveCoordinate D p ∈ S) (hanti : AntitoneOn (SuzukiLemma144KappaOne.errorEnvelope H (N - 1) (↑(D ⌈/⌉ p)) d) S) (hT : 0 ≤ H.T (SuzukiLemma144KappaOne.ErrorSign.ofDepth (N - 1)) (inheritedCoordinate D p)) (h1413 : SuzukiLemma144KappaOne.Claim14_13PointwisePremise H N (↑D) d Δ (Real.log ↑D / Real.log ↑p) (↑D / ↑p)) : Real.log ↑D ^ Δ * (SuzukiLemma144KappaOne.errorEnvelope H (N - 1) (↑(D ⌈/⌉ p)) d (recursiveCoordinate D p) * Real.log ↑(D ⌈/⌉ p) ^ (-Δ)) ≤ SuzukiLemma144KappaOne.qD H (SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite (↑D) d Δ (Real.log ↑D / Real.log ↑p)

The normalized form of naturalCeil_error_le_claim14_13. Its conclusion is exactly a R(log D / log p) ≤ qD(..., log D / log p) premise of the shape consumed by sigma12_middle_le_qD_lemma8_7: the global (log D)^{-Δ} has been cancelled, but the literal induction factor at ⌈D/p⌉ remains visible inside R.

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.NaturalCeilPointwiseInductionContract (support : Finset ℕ) (T : ℕ → ℕ → ℕ → ℝ) (V : ℕ → ℝ) (E : ℕ → ℕ → ℝ → ℝ) (β C K Δ : ℝ) (N D : ℕ) (σ τ : ℝ) : Prop

The induction theorem applied literally at the natural recursive argument. Unlike PointwiseInductionContract, this contract does not silently replace log ⌈D/p⌉ / log p by log D / log p - 1.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.NaturalCeilPointwiseInductionContract support T V E β C K Δ N D σ τ = ∀ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier support D σ τ, T (N - 1) (D ⌈/⌉ p) p ≤ V p * (MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p) + C * Real.exp √K * E (N - 1) (D ⌈/⌉ p) (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p) * Real.log ↑(D ⌈/⌉ p) ^ (-Δ))

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.PerturbedPointwiseInductionContract (support : Finset ℕ) (T : ℕ → ℕ → ℕ → ℝ) (V : ℕ → ℝ) (E : ℕ → ℕ → ℝ → ℝ) (β C K Δ : ℝ) (N D : ℕ) (σ τ : ℝ) : Prop

Maximal unconditional bridge after using antitonicity only for the finite source layer. The error is evaluated at the inherited coordinate plus the explicit displacement inheritedErrorPerturbation; it is not hidden in the induction hypothesis.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.PerturbedPointwiseInductionContract support T V E β C K Δ N D σ τ = ∀ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier support D σ τ, T (N - 1) (D ⌈/⌉ p) p ≤ V p * (MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p) + C * Real.exp √K * (E (N - 1) (D ⌈/⌉ p) (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p) + MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedErrorPerturbation E (N - 1) D p) * Real.log ↑(D ⌈/⌉ p) ^ (-Δ))

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.naturalCeilContract_to_perturbed (support : Finset ℕ) (T : ℕ → ℕ → ℕ → ℝ) (V : ℕ → ℝ) (E : ℕ → ℕ → ℝ → ℝ) (β C K Δ : ℝ) (N D : ℕ) (σ τ : ℝ) (hV : ∀ p ∈ sigmaOneCarrier support D σ τ, 0 ≤ V p) (hSource : ∀ p ∈ sigmaOneCarrier support D σ τ, SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (recursiveCoordinate D p) ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (inheritedCoordinate D p)) (hIH : NaturalCeilPointwiseInductionContract support T V E β C K Δ N D σ τ) : PerturbedPointwiseInductionContract support T V E β C K Δ N D σ τ

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.PointwiseInductionContract (support : Finset ℕ) (T : ℕ → ℕ → ℕ → ℝ) (V : ℕ → ℝ) (E : ℕ → ℕ → ℝ → ℝ) (β C K Δ : ℝ) (N D : ℕ) (σ τ : ℝ) : Prop

Narrow pointwise induction contract used in (14.10).

The discrete recursive argument is D ⌈/⌉ p (natural ceiling division), while both occurrences of the continuous coordinate are exactly log D / log p - 1.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.PointwiseInductionContract support T V E β C K Δ N D σ τ = ∀ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier support D σ τ, T (N - 1) (D ⌈/⌉ p) p ≤ V p * (MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p) + C * Real.exp √K * E (N - 1) (D ⌈/⌉ p) (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p) * Real.log ↑(D ⌈/⌉ p) ^ (-Δ))

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.naturalCeilContract_to_sourceCoordinate (support : Finset ℕ) (T : ℕ → ℕ → ℕ → ℝ) (V : ℕ → ℝ) (E : ℕ → ℕ → ℝ → ℝ) (β C K Δ : ℝ) (N D : ℕ) (σ τ : ℝ) (hV : ∀ p ∈ sigmaOneCarrier support D σ τ, 0 ≤ V p) (hC : 0 ≤ C) (hlog : ∀ p ∈ sigmaOneCarrier support D σ τ, 0 ≤ Real.log ↑(D ⌈/⌉ p)) (hSource : ∀ p ∈ sigmaOneCarrier support D σ τ, SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (recursiveCoordinate D p) ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (inheritedCoordinate D p)) (hError : ∀ p ∈ sigmaOneCarrier support D σ τ, E (N - 1) (D ⌈/⌉ p) (recursiveCoordinate D p) ≤ E (N - 1) (D ⌈/⌉ p) (inheritedCoordinate D p)) (hIH : NaturalCeilPointwiseInductionContract support T V E β C K Δ N D σ τ) : PointwiseInductionContract support T V E β C K Δ N D σ τ

Full closure criterion. The finite source layer and the error envelope must both be antitone across the ceiling displacement (or otherwise satisfy the two displayed pointwise inequalities). Without hError, only naturalCeilContract_to_perturbed is available.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOne (support : Finset ℕ) (omega : ℕ → ℝ) (T : ℕ → ℕ → ℕ → ℝ) (N D : ℕ) (σ τ : ℝ) : ℝ

Suzuki's Σ₁, restricted to the finite range in (14.10).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOne support omega T N D σ τ = ∑ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier support D σ τ, omega p * T (N - 1) (D ⌈/⌉ p) p

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaEleven (support : Finset ℕ) (omega V : ℕ → ℝ) (Vz β : ℝ) (N D : ℕ) (σ τ : ℝ) : ℝ

The main-term sum Σ₁₁ in (14.10), with the normalization V(p)/V(z) displayed rather than cancelled.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaEleven support omega V Vz β N D σ τ = Vz * ∑ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier support D σ τ, omega p * V p / Vz * MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaTwelve (support : Finset ℕ) (omega V : ℕ → ℝ) (E : ℕ → ℕ → ℝ → ℝ) (Vz C K Δ : ℝ) (N D : ℕ) (σ τ : ℝ) : ℝ

The inherited-error sum Σ₁₂ in (14.10).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaTwelve support omega V E Vz C K Δ N D σ τ = C * Real.exp √K * Vz * ∑ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier support D σ τ, omega p * V p / Vz * E (N - 1) (D ⌈/⌉ p) (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p) * Real.log ↑(D ⌈/⌉ p) ^ (-Δ)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.equation14_10_finset_assembly (support : Finset ℕ) (omega V : ℕ → ℝ) (T : ℕ → ℕ → ℕ → ℝ) (E : ℕ → ℕ → ℝ → ℝ) (Vz β C K Δ : ℝ) (N D : ℕ) (σ τ : ℝ) (hVz : Vz ≠ 0) (homega : ∀ p ∈ sigmaOneCarrier support D σ τ, 0 ≤ omega p) (hIH : PointwiseInductionContract support T V E β C K Δ N D σ τ) : sigmaOne support omega T N D σ τ ≤ sigmaEleven support omega V Vz β N D σ τ + sigmaTwelve support omega V E Vz C K Δ N D σ τ

Equation (14.10), as a pure finite assembly theorem. It uses only the pointwise induction contract, nonnegativity of the outer weights, and the nonvanishing of the normalizing Euler product. In particular it does not assume or prove either endpoint bound for Σ₁₁ or Σ₁₂.