Sphere Packing in R^8

Blueprint Summary🔗

Overview
Total entries140completed: 44; deps incomplete: 37; sorries: 9; no proof: 43
Ready now10Entries whose next formalization step is currently unblocked.
Fully closed44Local code and prerequisite closure are both complete.
Actionable priorities25Entries ready now and already unlocking downstream work.
Current blockers9Missing external or incomplete Lean declarations.
Missing informal coverage2Entries with Lean code but missing an informal statement or proof block.
Ready next (25)
  • «def:level-N-princ-cong-subgp»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 56
  • «def:Gamma-1-Action»(Lemma)
    Ready for proof work.
    stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 29proof: ready to formalize
  • «lemma:mod_form_poly_growth»(Lemma)
    Ready for proof work.
    stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 21proof: ready to formalize
  • «def:phi4-phi2-phi0»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 5downstream unlocks: 19
  • SpherePacking(Lemma)
    Ready for proof work.
    stage: proofstatement: ready to formalizedirect uses: 5downstream unlocks: 18proof: ready to formalize
  • «def:h»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 15
  • «lemma:psi-new»(Lemma)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 3downstream unlocks: 13proof: not ready
  • «lemma:psi-bound»(Lemma)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 3downstream unlocks: 11proof: not ready
  • «thm:smooth-fast-decay-schwartz»(Theorem)
    Ready for proof work.
    stage: proofstatement: ready to formalizedirect uses: 2downstream unlocks: 9proof: ready to formalize
  • «lem:integral-bound»(Lemma)
    Ready for proof work.
    stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 9proof: ready to formalize
  • Show all 15 more priorities
    • «lem:bound-I1-I3-I5»(Lemma)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 9proof: not ready
    • «lem:bound-I2-I4-I6»(Lemma)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 9proof: not ready
    • «lemma:log-der-inf»(Lemma)
      Ready for proof work.
      stage: proofstatement: ready to formalizedirect uses: 2downstream 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
    • «lemma:Qlim»(Lemma)
      Ready for proof work.
      stage: proofstatement: formalizeddirect uses: 1downstream unlocks: 7proof: Lean code incomplete
      Associated lean decls (1)
    • «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
    • «cor:ineqAnew»(Corollary)
      Ready for proof work.
      stage: proofstatement: formalizeddirect uses: 1downstream unlocks: 6proof: Lean code incomplete
      Associated lean decls (1)
    • «cor:ineqBnew»(Corollary)
      Ready for proof work.
      stage: proofstatement: formalizeddirect uses: 1downstream unlocks: 6proof: Lean code incomplete
      Associated lean decls (1)
    • «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: 2downstream unlocks: 5proof: Lean code incomplete
      Associated lean decls (1)
    • «prop:b0»(Lemma)
      Ready for proof work.
      stage: proofstatement: formalizeddirect uses: 2downstream unlocks: 5proof: Lean code incomplete
      Associated lean decls (1)
    • «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: 3downstream unlocks: 4proof: Lean code incomplete
      Associated lean decls (1)
Current blockers (9)
Missing informal coverage (2)
Entry index (140)
Definitions34completed: 18; deps incomplete: 9; sorries: 0; no proof: 0
Lemmas72completed: 21; deps incomplete: 19; sorries: 3; no proof: 29
Theorems19completed: 3; deps incomplete: 8; sorries: 3; no proof: 5
Corollaries15completed: 2; deps incomplete: 1; sorries: 3; no proof: 9
Informal-only entries49
Definition Index (34)
Theorem / 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 entries117Entries reused in statement dependencies.
Proof-used entries63Entries reused in proof-only dependencies.
Tracked parent groups20Grouped health rollups for parents with more than one child entry.
Most used in statements (117)
  • «def:E2»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 8proof uses: 1direct uses: 9downstream unlocks: 48
    Associated lean decls (1)
  • «SpherePacking.density»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 11
    Associated lean decls (1)
  • «def:disc-definition»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 6proof uses: 2direct uses: 8downstream unlocks: 51
    Associated lean decls (1)
  • «def:Mk»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 48
    Associated lean decls (1)
  • «def:H2-H3-H4»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 38
    Associated lean decls (3)
  • «def:serre-der»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 36
    Associated lean decls (1)
  • «thm:ramanujan-formula»(Theorem)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 5proof uses: 3direct uses: 8downstream unlocks: 31
    Associated lean decls (6)
  • «lemma:theta-transform-S-T»(Lemma)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 5proof uses: 3direct uses: 8downstream unlocks: 28
    Associated lean decls (6)
  • «def:phi4-phi2-phi0»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 19
  • «def:psiI-psiT-psiS»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 5proof uses: 1direct uses: 6downstream unlocks: 14
  • Show all 107 more statement-used entries
    • «def:Ek»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 35
      Associated lean decls (1)
    • «lemma:Ek-Fourier»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 23
      Associated lean decls (1)
    • SpherePacking(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 1direct uses: 5downstream unlocks: 18
    • «def:a-definition»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 14
      Associated lean decls (2)
    • «def:Fourier-Transform»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 12
      Associated lean decls (1)
    • «lemma:E2-transform-S»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 37
      Associated lean decls (1)
    • «lemma:mod-div-disc-bound»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 2direct uses: 5downstream unlocks: 23
      Associated lean decls (1)
    • «SpherePacking.finiteDensity»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 15
      Associated lean decls (1)
    • «lemma:F-G-pos»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 2direct uses: 5downstream unlocks: 9
      Associated lean decls (2)
    • «lemma:F-G-phi-psi-identities»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 1direct uses: 4downstream unlocks: 8
    • «def:Schwartz-Space»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 8
      Associated lean decls (1)
    • «def:level-N-princ-cong-subgp»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 56
    • «def:dedekind_eta»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 53
      Associated lean decls (1)
    • «thm:lvl1_dims»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 42
      Associated lean decls (1)
    • «cor:dim-mf»(Corollary)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 40
    • «def:derivative»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 39
      Associated lean decls (1)
    • «def:th00-th01-th10»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 39
      Associated lean decls (3)
    • «lemma:E2-transform-general»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 34
      Associated lean decls (1)
    • «def:automorphy-factor»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 31
      Associated lean decls (1)
    • «def:Gamma-generators»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 29
      Associated lean decls (4)
    • «lemma:theta-slash-invariant»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 26
      Associated lean decls (3)
    • «lemma:disc-cuspform»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 24
      Associated lean decls (1)
    • «lemma:theta-modular»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 24
      Associated lean decls (3)
    • «lemma:jacobi-identity»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 2direct uses: 4downstream unlocks: 23
      Associated lean decls (1)
    • «cor:phi0-bound»(Corollary)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 3direct uses: 5downstream unlocks: 20
    • «SpherePacking.balls»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 16
      Associated lean decls (1)
    • «lemma:Ek-is-modular-form»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 15
      Associated lean decls (1)
    • «lemma:psi-new»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 13
    • «cor:theta-pos»(Corollary)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 2direct uses: 4downstream unlocks: 12
      Associated lean decls (2)
    • «E8-Matrix»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 12
      Associated lean decls (1)
    • «cor:disc-pos»(Corollary)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 2direct uses: 4downstream unlocks: 11
      Associated lean decls (1)
    • «lemma:psi-bound»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 11
    • «E8-Set»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 11
      Associated lean decls (1)
    • «cor:disc-nonvanishing»(Corollary)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 11
      Associated lean decls (1)
    • «lemma:phi0-transform»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 11
    • «thm:serre-der-prod-rule»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 10
      Associated lean decls (1)
    • «E8-defs-equivalent»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 10
      Associated lean decls (1)
    • «prop:a-double-zeros»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 2direct uses: 4downstream unlocks: 9
    • «E8-vector-norms»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 8
      Associated lean decls (1)
    • «def:b-definition»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 8
    • «lemma:psiI-psiT-psiS-fourier»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 8
    • «prop:b-double-zeros»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 2direct uses: 4downstream unlocks: 7
    • «lemma:Gaussian-Fourier»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 7
    • «lemma:ineqABnew-equiv»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 7
    • «E8-Lattice»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 6
      Associated lean decls (1)
    • SpherePackingConstant(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 4
      Associated lean decls (1)
    • «SpherePacking.scale»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
      Associated lean decls (1)
    • «def:congruence-subgroup»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 49
    • «lemma:disc-E4E6»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 43
      Associated lean decls (1)
    • «thm:serre-der-equiv-action»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 33
      Associated lean decls (1)
    • «thm:serre-der-modularity»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 32
      Associated lean decls (1)
    • «def:Gamma-1-Action»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 29
    • «def:slash-operator»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 28
    • «lemma:automorphy-factor-chain-rule»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 28
      Associated lean decls (1)
    • «lemma:Gamma-2-generators»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 2direct uses: 3downstream unlocks: 27
      Associated lean decls (1)
    • «lemma:slash-negI-even-weight»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 27
      Associated lean decls (1)
    • «lemma:slash-operator-chain-rule»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 27
      Associated lean decls (1)
    • «lemma:Gamma-1-generators»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 26
      Associated lean decls (1)
    • «lemma:dedekind_eta_transformation»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 25
      Associated lean decls (1)
    • «lemma:theta-bounded-im-infty»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 25
      Associated lean decls (1)
    • «lemma:mod_form_poly_growth»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 21
    • «lemma:lv1-lv2-identities»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 2direct uses: 3downstream unlocks: 18
    • «def:h»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 15
    • «cor:phi2-bound»(Corollary)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 11
    • «cor:phi4-bound»(Corollary)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 11
    • «cor:phi0-near-0-infty»(Corollary)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 10
    • «prop:theta-der»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 10
    • «lemma:der-q-series»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 9
      Associated lean decls (1)
    • «cor:logder-disc-E2»(Corollary)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
    • «def:FG-definition»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
      Associated lean decls (2)
    • «lemma:FG-de»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
      Associated lean decls (2)
    • «prop:a-another-integral»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 2direct uses: 3downstream unlocks: 8
    • «cor:MLDE-pos»(Corollary)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 8
    • «cor:psiI-near-0-infty»(Corollary)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 8
    • «lemma:log-der-inf»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 8
    • «prop:a-schwartz»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 8
      Associated lean decls (1)
    • «thm:anti-serre-der-pos»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 8
    • IsZLattice(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
      Associated lean decls (1)
    • «lemma:Qlim»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
      Associated lean decls (1)
    • «prop:Qdec»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
      Associated lean decls (1)
    • «prop:a-fourier»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 6
      Associated lean decls (1)
    • «prop:b-another-integral»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 6
    • PeriodicSpherePacking(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
      Associated lean decls (1)
    • «cor:ineqAnew»(Corollary)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
      Associated lean decls (1)
    • «cor:ineqBnew»(Corollary)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
      Associated lean decls (1)
    • «def:dual-lattice»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
      Associated lean decls (1)
    • «lemma:Schwartz-summable»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
    • «lemma:inv-power-summable»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
    • «prop:b-schwartz»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
      Associated lean decls (1)
    • «prop:a0»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 5
      Associated lean decls (1)
    • «prop:b0»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 5
      Associated lean decls (1)
    • «prop:ineqA»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 5
    • E8Packing(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
      Associated lean decls (1)
    • «def:Periodic-sphere-packing-constant»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
      Associated lean decls (1)
    • «prop:b-fourier»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
      Associated lean decls (1)
    • «prop:ineqB»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
    • «thm:periodic-packing-optimal»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 2direct uses: 3downstream unlocks: 4
      Associated lean decls (1)
    • «E8Packing-covol»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
      Associated lean decls (1)
    • «theorem:psp-density»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
      Associated lean decls (1)
    • «thm:g1»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
    • «thm:Cohn-Elkies-general»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 3
      Associated lean decls (1)
    • «thm:g»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 3
    • «E8Packing-density»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
      Associated lean decls (1)
    • «theorem:CE_Main»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 2
    • «corollary:upper-bound-E8»(Corollary)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 1
    • instDiscreteE8Lattice(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
      Associated lean decls (1)
    • «E8-is-basis»(Lemma)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
      Associated lean decls (1)
Most used in proofs (63)
Group health (20)
  • 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: 73
    Next: «lem:integral-bound» stage: proofdownstream unlocks: 9
  • 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: statementdownstream unlocks: 11
  • 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: 3local-only: 5ready: 3blocked: 1incomplete Lean: 0unlock score: 233
    Next: no ready child currently unlocks downstream work.
  • Differential equations and monotonicity control.fg_differential
    Grouped view over entries sharing the same parent.
    total: 6closed: 0local-only: 2ready: 3blocked: 1incomplete Lean: 2unlock score: 45
    Next: «lemma:log-der-inf» stage: proofdownstream unlocks: 8
  • 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: 556
    Next: «lemma:mod_form_poly_growth» stage: proofdownstream unlocks: 21
  • 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: 405
    Next: «def:level-N-princ-cong-subgp» stage: statementdownstream unlocks: 56
  • 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: 58
    Next: «def:h» stage: statementdownstream unlocks: 15
  • 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: 109
    Next: «def:phi4-phi2-phi0» stage: statementdownstream unlocks: 19
  • Auxiliary functions F and G and reformulation of inequalities.fg_setup
    Grouped view over entries sharing the same parent.
    total: 7closed: 1local-only: 1ready: 1blocked: 4incomplete Lean: 1unlock score: 49
    Next: «cor:ineqAnew» stage: proofdownstream unlocks: 6
  • 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: no ready child currently unlocks downstream work.
    • 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: 217
      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-only49Statements with no associated Lean code yet.
Ready to formalize10Entries whose next step is currently unblocked.
Formalized, ancestors open37Local Lean work is done, but prerequisite closure is still open.
Fully closed44Local code and ancestor closure are both complete.
Heaviest prerequisites (115)
  • «thm:g1»(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 10statement deps: 8proof deps: 7direct uses: 1downstream unlocks: 4
  • «prop:a-schwartz»(Lemma)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 6statement deps: 2proof deps: 4direct uses: 2downstream unlocks: 8
    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: 2direct uses: 2downstream unlocks: 2
  • «prop:b-schwartz»(Lemma)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 5statement deps: 1proof deps: 4direct uses: 1downstream unlocks: 6
    Associated lean decls (1)
  • «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: 3direct uses: 1downstream unlocks: 7
    Associated lean decls (1)
  • «prop:b-fourier»(Lemma)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 5statement deps: 4proof deps: 1direct uses: 1downstream unlocks: 5
    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: 2downstream unlocks: 6
    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)
  • «lemma:FG-de»(Lemma)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 4statement deps: 4proof deps: 4direct uses: 1downstream unlocks: 9
    Associated lean decls (2)
  • Show all 105 more heaviest-prerequisite entries
    • «lemma:theta-slash-invariant»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 4direct uses: 3downstream unlocks: 26
      Associated lean decls (3)
    • «cor:MLDE-pos»(Corollary)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 3direct uses: 2downstream unlocks: 8
    • «thm:ramanujan-formula»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 2direct uses: 8downstream unlocks: 31
      Associated lean decls (6)
    • «prop:b-another-integral»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 3proof deps: 2direct uses: 2downstream unlocks: 6
    • «lemma:theta-bounded-im-infty»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 2proof deps: 2direct uses: 2downstream unlocks: 25
      Associated lean decls (1)
    • «cor:phi0-bound»(Corollary)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 1direct uses: 5downstream unlocks: 20
    • «prop:a-another-integral»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 1direct uses: 3downstream unlocks: 8
    • «prop:b-double-zeros»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 1direct uses: 4downstream unlocks: 7
    • «lemma:lv1-lv2-identities»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 3proof deps: 1direct uses: 3downstream unlocks: 18
    • «thm:lvl1_dims»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 3proof deps: 1direct uses: 2downstream unlocks: 42
      Associated lean decls (1)
    • «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: 2downstream unlocks: 10
    • «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: 11
    • «prop:ineqA»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 5
    • «lemma:ineqABnew-equiv»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 3direct uses: 2downstream unlocks: 7
    • «cor:ineqBnew»(Corollary)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 1direct uses: 1downstream unlocks: 6
      Associated lean decls (1)
    • «prop:a-double-zeros»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 1direct uses: 4downstream unlocks: 9
    • «thm:serre-der-modularity»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 1direct uses: 2downstream unlocks: 32
      Associated lean decls (1)
    • «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:phi2-bound»(Corollary)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 11
    • «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: 11
    • «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: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)
    • «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
    • «prop:theta-der»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 10
    • «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: 2downstream unlocks: 33
      Associated lean decls (1)
    • «corollary:upper-bound-E8»(Corollary)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 2direct uses: 2downstream unlocks: 1
    • «lemma:F-G-pos»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 2direct uses: 5downstream unlocks: 9
      Associated lean decls (2)
    • «lemma:theta-modular»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 2direct uses: 2downstream unlocks: 24
      Associated lean decls (3)
    • «lemma:psi-bound»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 0proof deps: 2direct uses: 3downstream unlocks: 11
    • «lemma:psi-new»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 0proof deps: 2direct uses: 3downstream unlocks: 13
    • «thm:Cohn-Elkies-general»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 0proof deps: 2direct uses: 2downstream unlocks: 3
      Associated lean decls (1)
    • «cor:logder-disc-E2»(Corollary)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 1direct 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: 1direct uses: 2downstream unlocks: 8
    • «cor:theta-pos»(Corollary)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 1direct uses: 4downstream unlocks: 12
      Associated lean decls (2)
    • «lemma:F-G-phi-psi-identities»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 1direct uses: 4downstream unlocks: 8
    • «lemma:disc-cuspform»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 1direct uses: 2downstream unlocks: 24
      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: 3downstream unlocks: 40
    • «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: 5downstream 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: 36
      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: 28
    • «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: 34
      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: 15
      Associated lean decls (1)
    • «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:jacobi-identity»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 23
      Associated lean decls (1)
    • «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: 8downstream unlocks: 28
      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: 2downstream 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: 3downstream unlocks: 4
      Associated lean decls (1)
    • MainTheorem(Corollary)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 1direct uses: 0downstream unlocks: 0
      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: 1direct uses: 4downstream 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: 1direct uses: 1downstream unlocks: 6
      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: 1direct uses: 2downstream unlocks: 9
      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: 1direct uses: 2downstream unlocks: 8
    • «lem:bound-I1-I3-I5»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 9
    • «lem:bound-I2-I4-I6»(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 9
    • «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: 5downstream unlocks: 23
      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)
    • «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: 29
      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: 38
      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: 48
      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: 14
      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: 49
    • «def:disc-definition»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 8downstream unlocks: 51
      Associated lean decls (1)
    • «def:h»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 15
    • «def:psiI-psiT-psiS»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 6downstream 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: 37
      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: 23
      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: 26
      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: 3downstream unlocks: 27
      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: 28
      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: 2downstream unlocks: 25
      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: 43
      Associated lean decls (1)
    • «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: 2downstream unlocks: 27
      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: 2downstream unlocks: 27
      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: 2downstream 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: 2downstream 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: 2downstream 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: 1downstream unlocks: 43
      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: 3downstream unlocks: 10
      Associated lean decls (1)
No prerequisites (25)
No dependents (8)
Proof debt hotspots (8)
  • Differential equations and monotonicity control.fg_differential
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 2incomplete decls: 2missing decls: 0total debt: 2
  • Auxiliary functions F and G and reformulation of inequalities.fg_setup
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 1incomplete decls: 1missing decls: 0total debt: 1
  • 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