The Cohn–Elkies exponent and sign uncertainty

 The Cohn–Elkies exponent and sign uncertainty🔗

Compiled2026-10-05T23:04:42ZProject22a40c6principle -> inequality (#9)Leanleanprover/lean4:v4.34.0VersoBlueprintv4.34.0@a48eea9ecb17Mathlibv4.34.0@5ed296525643

This blueprint follows Chapter 1 of the report Ten proofs (OpenAI): the exact exponential rate \mathrm{LP}_d^{1/d} \to \sqrt{e/(2\pi)} of the Cohn–Elkies linear programming bound for sphere packings (Theorem 1.1) and the asymptotics \mathsf{A}_\pm(d)/\sqrt d \to 1/\pi of the sign-uncertainty constants (Theorem 1.2).

Contents

  1. 1. Introduction
  2. 2. The Cohn–Elkies bound
  3. 3. Fourier-analytic preliminaries
  4. 4. The universal Cohn–Elkies lower bound
  5. 5. The admissible primal upper bound
  6. 6. Comparison of the sign-uncertainty constants
  7. 7. Report versus formalization
  8. Dependency Graph
  9. Blueprint Summary