7.5. Parameters of the upper construction🔗

The formalization uses exactly the parameters of Definition 5.2.1: u_* = -1 + \tfrac{\log\lambda}{4\lambda}, u_0 = 1 + \tfrac\epsilon4, U = 1 + \tfrac\epsilon2, B = \epsilon^{-3}, Q = e^{-3\epsilon B/8}, \beta = \epsilon/4, a_0 = \epsilon^2, A = \log(1/\epsilon), b(a) = 1 - 2\epsilon(1+a), the exponents 1/12 for the central windows, and the residue cutoff N = \lceil\log\lambda\rceil of Lemma 4.10 (CohnElkies.N_ℓ). The original single-file formalization had larger safety margins (a_0 = \epsilon^3, A = 10\log(1/\epsilon), b(a) = 1 - 10\epsilon(1+a), N = \lceil 20\log\lambda\rceil); each was switched to the report's value and the proofs re-tuned. The margins had been used only asymptotically (a_0 \to 0, A \to \infty, the ratio of Lemma 4.6, the factorial-tail majorant of Lemma 4.10), except for the taper: with b(0) = 1 - 2\epsilon the damping margin of Lemma 4.2 cannot exceed 1 - 2\epsilon, so the absolute constant of (54) is c = 2 and the constants derived from it downstream (2\epsilon D_\gamma \le D_u, V_s \le (1 - 2\epsilon)V_\gamma, the cubic-window and negative-contour constants) were adjusted; the limiting radius constant 1/\pi is unchanged.

Several lemmas of Section 4 are formalized in the weaker form that the sign conclusions need. In Lemma 5.5.3 the formal statement is the positivity consequence: uniformly on 0 \le r \le r_*, e^y|S_N(y) - e^{-y}| < \tfrac12 and e^y|\mathcal{R}_{\lambda}(r)| < \tfrac12, whose sum gives f_+(r)/f_+(0) > 0, rather than the full relative asymptotic (82). Likewise the formal versions of Lemma 5.4.1 conclude with the strict inequality |I_{\lambda,P}(u) - P(iu)\sqrt{2\pi/(\lambda V(u))}| < |P(iu)|\sqrt{2\pi/(\lambda V(u))}, uniformly on the stated ranges, which is all that the signs in Theorem 5.4.2 require. The radius-coverage step of Corollary 4.9 is proved by continuity of v and v(u) \to \infty with the intermediate value theorem; strict monotonicity of v is not needed there. The absolute constants of Lemmas 4.2 and 4.4–4.7 are made explicit (c = 2, 1/(8e), 1/100, 1/5000, and so on) and the O(\epsilon)-displacement of Lemma 4.2 is replaced by the limit \epsilon \downarrow 0.