6. Comparison of the sign-uncertainty constants
This chapter follows Appendix A of the report. Proposition A.1 is formalized in L^1
generality (modules CohnElkies.SignUncertainty.MellinCancellation,
CohnElkies.SignUncertainty.TailIntegral, CohnElkies.SignUncertainty.AppendixA). The appendix's
conclusion \mathsf{A}_+(d) < \mathsf{A}_-(d) needs, in addition, an extremizer attaining
\mathsf{A}_-(d) (Cohn–Gonçalves 2019, Theorem 1.4), whose proof is not part of the report. The
second half of the chapter formalizes that existence theorem, following Cohn–Gonçalves (§3.2):
the origin correction of their Lemma 3.1, the positivity and finiteness of the constants in every
dimension, weak sequential compactness in L^2, and — in place of the quantitative uncertainty
principle of Nazarov and Jaming they invoke — a qualitative "no concentration" lemma for
eigenfunctions of the Fourier transform, proved by compactness (modules
CohnElkies.SignUncertainty.OriginCorrection, CohnElkies.SignUncertainty.Finiteness,
CohnElkies.SignUncertainty.AppendixA,
CohnElkiesForMathlib.Analysis.InnerProductSpace.WeakSequentialCompactness,
CohnElkiesForMathlib.Analysis.Fourier.EigenfunctionConcentration). The nodes depend on the
definitions of the introduction and on the radial reduction of the preliminaries.