Uniform cutoffs for the common Lemma-14.4 scale

Claim 14.5 is chosen after the source small-parameter constant C1, whereas Lemma 14.4 subsequently enlarges its error constant to

C = max 3 (A * C145).

The old eventual Case-I and Case-II APIs accepted both C and C145, which made their generated witnesses look as though they had to be paid by C1 after C145 was known. The two lemmas below expose the cancellations already present in the production gap arguments. Their eventual threshold is selected before C145 and C.

noncomputable def MathlibNt.SieveTheory.lemma144CommonScale (A C145 : ℝ) : ℝ

The common normalization used after Claim 14.5.

Equations

• MathlibNt.SieveTheory.lemma144CommonScale A C145 = max 3 (A * C145)

theorem MathlibNt.SieveTheory.lemma144CommonScale_bounds {A C145 : ℝ} : 3 ≤ lemma144CommonScale A C145 ∧ A * C145 ≤ lemma144CommonScale A C145

Both elementary lower bounds supplied by the common normalization.

theorem MathlibNt.SieveTheory.eventually_caseISourceOrderCoefficient_commonScale_uniform {A B E d Δ : ℝ} (hA : 0 < A) (hB : 0 ≤ B) (hE : 0 ≤ E) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) : ∀ᶠ (D : ℝ) in Filter.atTop, ∀ (C145 C : ℝ), 0 ≤ C145 → C = lemma144CommonScale A C145 → ∃ (q : Lemma144StrictFactor), q.ρ = (1 + sigma12ContractionMultiplier (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) Δ) / 2 ∧ caseISourceOrderCoefficient (C145 / C + B / C + E) D d ≤ 1 - q.ρ

In Case I every occurrence of the two late constants is through a scale ratio. Consequently one cutoff works for all C145 ≥ 0 after imposing C = max 3 (A*C145). B/C represents the normalized Σ₁₁ coefficient and E the already scale-free endpoint coefficient; in production these are the only other summands next to C145/C.

The quantifier order is the point: the eventual D threshold precedes both C145 and C.

theorem MathlibNt.SieveTheory.exists_claim145_gap_constant_threshold_commonScale_uniform {A Δ : ℝ} (hA : 0 < A) (hΔ1 : Δ < 1) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (C145 C D : ℝ), 0 ≤ C145 → C = lemma144CommonScale A C145 → D0 ≤ D → C145 ≤ 27 * C * (1 - Δ) * Real.log D / 32

The Case-II endpoint inequality also depends only on C145/C. This explicit witness is uniform in the late Claim-14.5 constant and therefore can be dominated by the already chosen source constant C1.

Unlike exists_claim145_gap_constant_threshold, the witness below depends on A,Δ only, not on C145 or C.

theorem MathlibNt.SieveTheory.exists_lemma144_caseI_caseII_commonScale_cutoff_uniform {A B E d Δ : ℝ} (hA : 0 < A) (hB : 0 ≤ B) (hE : 0 ≤ E) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (C145 C D : ℝ), 0 ≤ C145 → C = lemma144CommonScale A C145 → D0 ≤ D → (∃ (q : Lemma144StrictFactor), q.ρ = (1 + sigma12ContractionMultiplier (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) Δ) / 2 ∧ caseISourceOrderCoefficient (C145 / C + B / C + E) D d ≤ 1 - q.ρ) ∧ C145 ≤ 27 * C * (1 - Δ) * Real.log D / 32

One outer cutoff simultaneously supplies the Case-I midpoint absorption and the Case-II endpoint-gap inequality. It is selected with A,B,E,d,Δ fixed and before the late constants C145,C; this is the exact quantifier order needed to choose C1 first.