Documentation

MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiSourceRoundedGeometryPacket

source
structure MathlibNt.SieveTheory.SourceRoundedGeometryPacket (S : BoundingSieve) (D y z : ℕ) (d s : ℝ) :
Prop

Every size and cutoff-geometry premise used by the double-rounded Case-II endpoint, after substituting Suzuki's moving source cutoff. The extra fields hyceil, hyrzr, and hzr2 make explicit the three immediate geometric facts that consumers otherwise have to reconstruct from the displayed premises.

Instances For
    source
    theorem MathlibNt.SieveTheory.natCeil_cuberoot_cubeBracket (D : ℕ) (hD : 0 < D) :
    have y := ⌈↑D ^ (1 / 3)⌉₊; (y - 1) ^ 3 < D ∧ D ≤ y ^ 3

    The natural ceiling of the real cube root satisfies the strict lower and weak upper cubic bracket. This is the direction needed to manufacture the rounded natural cutoff, rather than consume a pre-existing bracket.

    source
    theorem MathlibNt.SieveTheory.exists_sourceSigma_doubleRounded_geometry_threshold (d : ℝ) (hd : 1 < d) :
    ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (S : BoundingSieve) (D : ℕ), D0 ≤ ↑D → ∀ (s : ℝ), 1 < s → s ≤ 3 → SourceRoundedGeometryPacket S D ⌈↑D ^ (1 / 3)⌉₊ ⌈↑D ^ (1 / s)⌉₊ d s

    A single threshold, depending only on d, supplies all moving source-sigma, logarithmic-size, and double-rounded cutoff geometry uniformly in the sieve, in the natural parameter D, and in every 1 < s ≤ 3.

    The cutoffs are fixed in the conclusion as y = ceil(D^(1/3)) and z = ceil(D^(1/s)); thus no perfect-power equality is assumed and no size premise remains for downstream induction/source consumers.