Sphere Packing in R^8

Blueprint Summary🔗

Overview
Total entries140completed: 45; deps incomplete: 40; sorries: 9; no proof: 39
Ready now30Entries with an actionable next formalization step.
Fully closed45Local code and prerequisite closure are both complete.
Actionable priorities24Entries ready now and already unlocking downstream work.
Current blockers10Missing external or incomplete Lean declarations.
Missing informal coverage7Entries with Lean code but missing an informal statement or proof block.
Actionable priorities (24)
  • «def:level-N-princ-cong-subgp»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 42
  • «def:phi4-phi2-phi0»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 6downstream unlocks: 19
  • SpherePacking(Lemma)
    Ready for proof work.
    stage: proofstatement: ready to formalizedirect uses: 5downstream unlocks: 18proof: ready to formalize
  • «def:Gamma-1-Action»(Lemma)
    Ready for proof work.
    stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 18proof: ready to formalize
  • «lemma:psi-new»(Lemma)
    Ready for proof work.
    stage: proofstatement: ready to formalizedirect uses: 2downstream unlocks: 13proof: ready to formalize
  • «lemma:mod_form_poly_growth»(Lemma)
    Ready for proof work.
    stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 12proof: ready to formalize
  • «lemma:psi-bound»(Lemma)
    Ready for proof work.
    stage: proofstatement: ready to formalizedirect uses: 2downstream unlocks: 11proof: ready to formalize
  • «thm:smooth-fast-decay-schwartz»(Theorem)
    Ready for proof work.
    stage: proofstatement: ready to formalizedirect uses: 2downstream unlocks: 9proof: ready to formalize
  • «lemma:log-der-inf»(Lemma)
    Ready for proof work.
    stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 8proof: ready to formalize
  • «lemma:Gaussian-Fourier»(Lemma)
    Ready for proof work.
    stage: proofstatement: ready to formalizedirect uses: 2downstream unlocks: 7proof: ready to formalize
  • Show all 14 more priorities
    • «lem:bound-I1-I3-I5»(Lemma)
      Ready for proof work.
      stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 7proof: ready to formalize
    • «lem:bound-I2-I4-I6»(Lemma)
      Ready for proof work.
      stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 7proof: ready to formalize
    • «lem:integral-bound»(Lemma)
      Ready for proof work.
      stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 7proof: ready to formalize
    • «lemma:bound-J1-J3-J5»(Lemma)
      Ready for proof work.
      stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 7proof: ready to formalize
    • «lemma:bound-J2-J4-J6»(Lemma)
      Ready for proof work.
      stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 7proof: ready to formalize
    • «lemma:Schwartz-summable»(Lemma)
      Ready for proof work.
      stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 6proof: ready to formalize
    • «lemma:inv-power-summable»(Lemma)
      Ready for proof work.
      stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 6proof: ready to formalize
    • «prop:a0»(Lemma)
      Ready for proof work.
      stage: proofstatement: formalizeddirect uses: 1downstream unlocks: 5proof: Lean code incomplete
      Associated lean decls (1)
    • «prop:b0»(Lemma)
      Ready for proof work.
      stage: proofstatement: formalizeddirect uses: 1downstream unlocks: 5proof: Lean code incomplete
      Associated lean decls (1)
    • «prop:ineqA»(Lemma)
      Ready for proof work.
      stage: proofstatement: formalizeddirect uses: 1downstream unlocks: 5proof: Lean code incomplete
      Associated lean decls (2)
    • «prop:ineqB»(Lemma)
      Ready for proof work.
      stage: proofstatement: formalizeddirect uses: 1downstream unlocks: 5proof: Lean code incomplete
      Associated lean decls (2)
    • «thm:Poisson-summation-formula»(Theorem)
      Ready for proof work.
      stage: proofstatement: formalizeddirect uses: 1downstream unlocks: 5proof: Lean code incomplete
      Associated lean decls (1)
    • «thm:periodic-packing-optimal»(Theorem)
      Ready for proof work.
      stage: proofstatement: formalizeddirect uses: 2downstream unlocks: 4proof: Lean code incomplete
      Associated lean decls (1)
    • «thm:g1»(Theorem)
      Ready for proof work.
      stage: proofstatement: formalizeddirect uses: 1downstream unlocks: 4proof: Lean code incomplete
      Associated lean decls (5)
Current blockers (10)
Missing informal coverage (7)
Entry index (140)
Definitions34completed: 18; deps incomplete: 9; sorries: 0; no proof: 0
Lemmas72completed: 21; deps incomplete: 21; sorries: 4; no proof: 26
Theorems19completed: 3; deps incomplete: 8; sorries: 4; no proof: 4
Corollaries15completed: 3; deps incomplete: 2; sorries: 1; no proof: 9
Informal-only entries45
Definition Index (34)
Theorem / Proposition / Lemma / Corollary Index (106)
By parent groups (19)
Periodic and lattice packings as a reduced optimization class. (1)
Auxiliary functions F and G and reformulation of inequalities. (6)
Summability lemmas and Poisson summation over lattices. (4)
Auxiliary modular expressions and integral formulas defining a. (5)
Auxiliary forms and integral formulas defining b. (2)
Schwartz, Fourier-eigenfunction, and double-zero properties of b. (9)
Volume-count asymptotics for lattice and periodic center sets. (3)
Eisenstein series, the discriminant form, and positivity/nonvanishing tools. (14)
Schwartz, Fourier-eigenfunction, and double-zero properties of a. (9)
Fourier transform and Schwartz-space preliminaries. (2)
Equivalent models of the E8 lattice. (1)
Basic structural and arithmetic properties of E8. (5)
Differential equations and monotonicity control. (6)
Scaling invariance of finite density and asymptotic density. (3)
Reduction from Cohn-Elkies bounds to the final dimension-8 theorem. (3)
Congruence groups, slash operators, and modular forms. (6)
Serre derivative identities and differential inequalities. (8)
Definition and density computation of the E8 sphere packing. (2)
Theta constants and identities used in the magic-function construction. (10)
Dependency insights
Statement-used entries116Entries reused in statement dependencies.
Proof-used entries17Entries reused in proof-only dependencies.
Tracked parent groups20Grouped health rollups for parents with more than one child entry.
Most used in statements (116)
Most used in proofs (17)
Group health (20)
  • Schwartz, Fourier-eigenfunction, and double-zero properties of b.magic_b_properties
    Grouped view over entries sharing the same parent.
    total: 9closed: 0local-only: 2ready: 4blocked: 3incomplete Lean: 1unlock score: 62
    Next: «lemma:psi-bound» stage: proofdownstream unlocks: 11
  • Schwartz, Fourier-eigenfunction, and double-zero properties of a.magic_a_properties
    Grouped view over entries sharing the same parent.
    total: 9closed: 0local-only: 2ready: 4blocked: 3incomplete Lean: 1unlock score: 58
    Next: «lem:bound-I1-I3-I5» stage: proofdownstream unlocks: 7
  • Summability lemmas and Poisson summation over lattices.poisson_formula
    Grouped view over entries sharing the same parent.
    total: 4closed: 0local-only: 0ready: 4blocked: 0incomplete Lean: 1unlock score: 26
    Next: «thm:smooth-fast-decay-schwartz» stage: proofdownstream unlocks: 9
  • Theta constants and identities used in the magic-function construction.theta_and_identities
    Grouped view over entries sharing the same parent.
    total: 12closed: 4local-only: 4ready: 3blocked: 1incomplete Lean: 0unlock score: 155
    Next: «prop:H2-fourier» stage: proofdownstream unlocks: 0
  • Eisenstein series, the discriminant form, and positivity/nonvanishing tools.eisenstein_discriminant
    Grouped view over entries sharing the same parent.
    total: 18closed: 12local-only: 3ready: 2blocked: 1incomplete Lean: 1unlock score: 376
    Next: «lemma:mod_form_poly_growth» stage: proofdownstream unlocks: 12
  • Congruence groups, slash operators, and modular forms.modular_forms_setup
    Grouped view over entries sharing the same parent.
    total: 12closed: 3local-only: 5ready: 2blocked: 2incomplete Lean: 0unlock score: 262
    Next: «def:level-N-princ-cong-subgp» stage: statementdownstream unlocks: 42
  • Auxiliary functions F and G and reformulation of inequalities.fg_setup
    Grouped view over entries sharing the same parent.
    total: 7closed: 1local-only: 3ready: 2blocked: 1incomplete Lean: 2unlock score: 49
    Next: «prop:ineqA» stage: proofdownstream unlocks: 5
  • Auxiliary forms and integral formulas defining b.magic_psi_construction
    Grouped view over entries sharing the same parent.
    total: 5closed: 0local-only: 0ready: 2blocked: 3incomplete Lean: 0unlock score: 43
    Next: «lemma:psi-new» stage: proofdownstream unlocks: 13
  • Auxiliary modular expressions and integral formulas defining a.magic_phi_construction
    Grouped view over entries sharing the same parent.
    total: 7closed: 1local-only: 1ready: 1blocked: 4incomplete Lean: 0unlock score: 81
    Next: «def:phi4-phi2-phi0» stage: statementdownstream unlocks: 19
  • Differential equations and monotonicity control.fg_differential
    Grouped view over entries sharing the same parent.
    total: 6closed: 0local-only: 4ready: 1blocked: 1incomplete Lean: 0unlock score: 45
    Next: «lemma:log-der-inf» stage: proofdownstream unlocks: 8
  • Show all 10 more groups
    • Periodic and lattice packings as a reduced optimization class.periodic_packings
      Grouped view over entries sharing the same parent.
      total: 5closed: 2local-only: 2ready: 1blocked: 0incomplete Lean: 1unlock score: 28
      Next: «thm:periodic-packing-optimal» stage: proofdownstream unlocks: 4
    • Fourier transform and Schwartz-space preliminaries.fourier_setup
      Grouped view over entries sharing the same parent.
      total: 4closed: 3local-only: 0ready: 1blocked: 0incomplete Lean: 0unlock score: 27
      Next: «lemma:Gaussian-Fourier» stage: proofdownstream unlocks: 7
    • Reduction from Cohn-Elkies bounds to the final dimension-8 theorem.sphere_main_statement
      Grouped view over entries sharing the same parent.
      total: 3closed: 0local-only: 0ready: 1blocked: 2incomplete Lean: 1unlock score: 3
      Next: MainTheorem stage: proofdownstream unlocks: 0
    • Serre derivative identities and differential inequalities.serre_derivative
      Grouped view over entries sharing the same parent.
      total: 10closed: 5local-only: 2ready: 0blocked: 3incomplete Lean: 0unlock score: 172
      Next: no ready child currently unlocks downstream work.
    • Definitions of sphere packings, density, and the optimization target.sphere_setup
      Grouped view over entries sharing the same parent.
      total: 4closed: 1local-only: 3ready: 0blocked: 0incomplete Lean: 0unlock score: 46
      Next: no ready child currently unlocks downstream work.
    • Equivalent models of the E8 lattice.e8_definitions
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 33
      Next: no ready child currently unlocks downstream work.
    • Basic structural and arithmetic properties of E8.e8_properties
      Grouped view over entries sharing the same parent.
      total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 16
      Next: no ready child currently unlocks downstream work.
    • Volume-count asymptotics for lattice and periodic center sets.density_periodic_counts
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 15
      Next: no ready child currently unlocks downstream work.
    • Definition and density computation of the E8 sphere packing.e8_density
      Grouped view over entries sharing the same parent.
      total: 3closed: 2local-only: 1ready: 0blocked: 0incomplete Lean: 0unlock score: 12
      Next: no ready child currently unlocks downstream work.
    • Scaling invariance of finite density and asymptotic density.sphere_scaling
      Grouped view over entries sharing the same parent.
      total: 4closed: 0local-only: 4ready: 0blocked: 0incomplete Lean: 0unlock score: 6
      Next: no ready child currently unlocks downstream work.
Metadata
Metadata audit
Missing owner140
Missing effort140
Untagged140
Missing owner (140)
Missing effort (140)
Untagged (140)
Structure and coverage
Informal-only45Statements with no associated Lean code yet.
Ready to formalize30Entries with an actionable next formalization step.
Formalized, ancestors open40Local Lean work is done, but prerequisite closure is still open.
Fully closed45Local code and ancestor closure are both complete.
Blocked or incomplete25Entries not covered by the highlighted readiness buckets above.
Heaviest prerequisites (111)
  • «thm:g1»(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 8statement deps: 8proof deps: 0direct uses: 1downstream unlocks: 4
    Associated lean decls (5)
  • «prop:a-schwartz»(Lemma)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 6statement deps: 2proof deps: 4direct uses: 1downstream unlocks: 6
    Associated lean decls (1)
  • «theorem:CE_Main»(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 6statement deps: 6proof deps: 0direct uses: 1downstream unlocks: 2
  • «theorem:psp-density»(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 5statement deps: 1proof deps: 4direct uses: 1downstream unlocks: 4
    Associated lean decls (1)
  • «prop:Qdec»(Lemma)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 7
    Associated lean decls (1)
  • «prop:a-fourier»(Lemma)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 5
    Associated lean decls (1)
  • «thm:Poisson-summation-formula»(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 5
    Associated lean decls (1)
  • «prop:b-schwartz»(Lemma)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 4statement deps: 1proof deps: 3direct uses: 1downstream unlocks: 6
    Associated lean decls (1)
  • «cor:MLDE-pos»(Corollary)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 8
  • «cor:phi0-bound»(Corollary)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 11
  • Show all 101 more heaviest-prerequisite entries
    • «cor:phi0-near-0-infty»(Corollary)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 8
    • «lemma:FG-de»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 9
      Associated lean decls (2)
    • «lemma:phi0-transform»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 9
    • «lemma:theta-slash-invariant»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 15
      Associated lean decls (3)
    • «prop:a-another-integral»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 6
    • «prop:b-another-integral»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 6
    • «prop:b-double-zeros»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 7
    • «prop:b-fourier»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 5
      Associated lean decls (1)
    • «prop:ineqA»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 5
      Associated lean decls (2)
    • «thm:ramanujan-formula»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 5downstream unlocks: 22
      Associated lean decls (6)
    • «SpherePacking.constant_eq_constant_normalized»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 2proof deps: 1direct uses: 0downstream unlocks: 0
      Associated lean decls (1)
    • «thm:Cohn-Elkies-periodic»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 2proof deps: 1direct uses: 1downstream unlocks: 4
      Associated lean decls (1)
    • «cor:ineqBnew»(Corollary)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 6
      Associated lean decls (1)
    • «cor:phi2-bound»(Corollary)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 9
    • «cor:phi4-bound»(Corollary)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 9
    • «def:FG-definition»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 9
      Associated lean decls (2)
    • «lemma:F-G-phi-psi-identities»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 8
      Associated lean decls (2)
    • «lemma:Qlim»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 7
      Associated lean decls (1)
    • «lemma:ineqABnew-equiv»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 7
    • «lemma:lv1-lv2-identities»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 10
    • «prop:a-double-zeros»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 7
    • «prop:ineqB»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 5
      Associated lean decls (2)
    • «prop:theta-der»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 10
    • «thm:lvl1_dims»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 27
      Associated lean decls (1)
    • «thm:serre-der-equiv-action»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 24
      Associated lean decls (1)
    • «thm:serre-der-modularity»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 23
      Associated lean decls (1)
    • «thm:Cohn-Elkies-general»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 3
      Associated lean decls (1)
    • «SpherePacking.scale_density»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 1
      Associated lean decls (1)
    • «lemma:sp-finite-density-bound»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 5
      Associated lean decls (2)
    • E8Packing(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 5
      Associated lean decls (1)
    • PeriodicSpherePacking(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 6
      Associated lean decls (1)
    • SpherePackingConstant(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 4
      Associated lean decls (1)
    • instLatticeE8(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
      Associated lean decls (1)
    • «E8-Lattice»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 6
      Associated lean decls (1)
    • «E8-defs-equivalent»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 10
      Associated lean decls (1)
    • «E8Packing-density»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 3
      Associated lean decls (1)
    • «SpherePacking.density»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 7downstream unlocks: 11
      Associated lean decls (1)
    • «SpherePacking.finiteDensity»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 15
      Associated lean decls (1)
    • «SpherePacking.scale_finiteDensity»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 2
      Associated lean decls (1)
    • «cor:dim-mf»(Corollary)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 25
    • «cor:logder-disc-E2»(Corollary)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 9
    • «cor:psiI-near-0-infty»(Corollary)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 8
    • «corollary:upper-bound-E8»(Corollary)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
    • «def:Periodic-sphere-packing-constant»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 5
      Associated lean decls (1)
    • «def:phi4-phi2-phi0»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 6downstream unlocks: 19
    • «def:serre-der»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 6downstream unlocks: 27
      Associated lean decls (1)
    • «def:slash-operator»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 17
    • «lemma:E2-transform-general»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 25
      Associated lean decls (1)
    • «lemma:Ek-is-modular-form»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 13
      Associated lean decls (1)
    • «lemma:F-G-pos»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 9
      Associated lean decls (2)
    • «lemma:Fourier-transform-is-automorphism»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
      Associated lean decls (1)
    • «lemma:disc-cuspform»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 16
      Associated lean decls (1)
    • «lemma:jacobi-identity»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 11
      Associated lean decls (1)
    • «lemma:theta-bounded-im-infty»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 14
      Associated lean decls (1)
    • «lemma:theta-modular»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 13
      Associated lean decls (3)
    • «lemma:theta-transform-S-T»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 21
      Associated lean decls (6)
    • «thm:anti-serre-der-pos»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 8
    • «thm:dim-mf-general-level»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
      Associated lean decls (1)
    • «thm:periodic-packing-optimal»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 4
      Associated lean decls (1)
    • «lemma:mod-div-disc-bound»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 0proof deps: 1direct uses: 3downstream unlocks: 14
      Associated lean decls (1)
    • MainTheorem(Corollary)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
      Associated lean decls (1)
    • instDiscreteE8Lattice(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
      Associated lean decls (1)
    • «E8-is-basis»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
      Associated lean decls (1)
    • «E8-vector-norms»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 8
      Associated lean decls (1)
    • «E8Packing-covol»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 4
      Associated lean decls (1)
    • «SpherePacking.scale»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 3
      Associated lean decls (1)
    • «cor:disc-nonvanishing»(Corollary)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 11
      Associated lean decls (1)
    • «cor:disc-pos»(Corollary)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 11
      Associated lean decls (1)
    • «cor:ineqAnew»(Corollary)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 6
      Associated lean decls (1)
    • «cor:theta-pos»(Corollary)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 12
      Associated lean decls (2)
    • «def:Gamma-generators»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 18
      Associated lean decls (4)
    • «def:H2-H3-H4»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 6downstream unlocks: 29
      Associated lean decls (3)
    • «def:Mk»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 6downstream unlocks: 33
      Associated lean decls (1)
    • «def:a-definition»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 10
      Associated lean decls (2)
    • «def:b-definition»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 8
    • «def:congruence-subgroup»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 34
    • «def:disc-definition»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 7downstream unlocks: 41
      Associated lean decls (2)
    • «def:h»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
    • «def:psiI-psiT-psiS»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 14
    • «lemma:E2-transform-S»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 28
      Associated lean decls (1)
    • «lemma:Ek-Fourier»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 14
      Associated lean decls (1)
    • «lemma:Gamma-1-generators»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 15
      Associated lean decls (1)
    • «lemma:Gamma-2-generators»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 16
      Associated lean decls (1)
    • «lemma:Gaussian-Fourier»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 7
    • «lemma:Schwartz-summable»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 6
    • «lemma:automorphy-factor-chain-rule»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 17
      Associated lean decls (1)
    • «lemma:dedekind_eta_transformation»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 17
      Associated lean decls (1)
    • «lemma:der-q-series»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 9
      Associated lean decls (1)
    • «lemma:disc-E4E6»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 28
      Associated lean decls (1)
    • «lemma:log-der-inf»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 8
    • «lemma:psiI-psiT-psiS-fourier»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 8
    • «lemma:slash-negI-even-weight»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 16
      Associated lean decls (1)
    • «lemma:slash-operator-chain-rule»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 16
      Associated lean decls (1)
    • «prop:H2-fourier»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
    • «prop:H3-fourier»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
    • «prop:H4-fourier»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
    • «prop:a0»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 5
      Associated lean decls (1)
    • «prop:b0»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 5
      Associated lean decls (1)
    • «thm:g»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
    • «thm:nonpos_wt»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
      Associated lean decls (2)
    • «thm:serre-der-prod-rule»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 10
      Associated lean decls (1)
No prerequisites (29)
No dependents (10)
Proof debt hotspots (8)
  • Auxiliary functions F and G and reformulation of inequalities.fg_setup
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 2incomplete decls: 2missing decls: 0total debt: 2
  • Assembly of the final theorem producing the optimal function.g_theorem
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 1incomplete decls: 2missing decls: 0total debt: 2
  • Eisenstein series, the discriminant form, and positivity/nonvanishing tools.eisenstein_discriminant
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 1incomplete decls: 1missing decls: 0total debt: 1
  • Periodic and lattice packings as a reduced optimization class.periodic_packings
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 1incomplete decls: 1missing decls: 0total debt: 1
  • Reduction from Cohn-Elkies bounds to the final dimension-8 theorem.sphere_main_statement
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 1incomplete decls: 1missing decls: 0total debt: 1
  • Schwartz, Fourier-eigenfunction, and double-zero properties of a.magic_a_properties
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 1incomplete decls: 1missing decls: 0total debt: 1
  • Schwartz, Fourier-eigenfunction, and double-zero properties of b.magic_b_properties
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 1incomplete decls: 1missing decls: 0total debt: 1
  • Summability lemmas and Poisson summation over lattices.poisson_formula
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 1incomplete decls: 1missing decls: 0total debt: 1