The Cohn–Elkies exponent and sign uncertainty

7.11. Statements added in the reformalization🔗

The original formalization proves Theorem 1.1 in full, including the passage from unrestricted admissible functions to radial ones (Lemma 3.2.9) and the bridge to the packing density (Theorem 1.1.8), but only an anti-self-Fourier Schwartz obstruction in place of the sign-uncertainty results. The reformalization adds, following the report's statements:

  • Proposition 3.1 and the Schwartz case of Proposition 3.7 for both eigenvalues \varsigma \in \{-1,+1\} (Proposition 4.1.35, Proposition 4.2.1), through the structure CohnElkies.RadialEigenfunction (a radial eigenfunction without sign hypothesis), of which the former CohnElkies.AntiSelfFourierWitness is now the special case \varsigma = -1 with the exterior sign condition;

  • the L^1 class \mathcal{E}_\varsigma(d) with its continuous representative, the radius r(g) and the constants \mathsf{A}_\pm(d) (Definition 1.2.1, Definition 1.2.2, Definition 1.2.3);

  • the radial reduction and Schwartz approximation of Section 2.1 for integrable eigenfunctions (Lemma 3.2.13, Lemma 3.2.18), the L^1 case of Proposition 3.7 and Theorem 1.2 (Theorem 1.2.4, Theorem 5.5.7), in the modules CohnElkies.SignUncertainty.*;

  • the self-Fourier function f_0 with P_0(\zeta) = -(1+\zeta^2) (Lemma 5.2.17, Theorem 5.4.2), obtained by making the saddle lemmas generic in the polynomial P (CohnElkies.IsSaddlePolynomial, CohnElkies.mellinProfile, CohnElkies.mellinMultiplier_mul_spectrum_neg; module CohnElkies.UpperBound.SelfFourier);

  • the nonemptiness of \mathcal{A}_d (Lemma 1.1.7) and the comparator statements of the main theorems (ComparatorChallenges/CohnElkies.lean).

Appendix A is formalized in L^1 generality (Proposition 6.1.7); the strict inequality (Theorem 6.1.9) rests on the existence of extremizers for \mathsf{A}_-(d) (Theorem 6.2.11), which is not part of the report (see the next section).