Introduction
The root lattice D 5 = { x ∈ Z 5 : x 1 + ⋯ + x 5 ∈ 2 Z } D_{5}=\{x\in\mathbb{Z}^{5}:x_{1}+\cdots+x_{5}\in2\mathbb{Z}\} D 5 = { x ∈ Z 5 : x 1 + ⋯ + x 5 ∈ 2 Z } [8 Ch. 4, §7.1] , scaled by 2 \sqrt{2} 2 π 2 / ( 15 2 ) \pi^{2}/(15\sqrt{2}) π 2 / ( 15 2 ) R 5 \mathbb{R}^{5} R 5 [11 ] . Whether D 5 D_{5} D 5 R 5 \mathbb{R}^{5} R 5 [12 ] , Conway and Sloane placed them in a family of layered packings [7 ] , and Cohn and Rajagopal [6 ] found further examples after Szöllősi’s discovery of a new kissing configuration of 40 points [16 ] .
A periodic packing is a finite union of translates of one lattice. After lattices, the next case is two translates, P = Λ ∪ ( Λ + b ) P=\Lambda\cup(\Lambda+b) P = Λ ∪ ( Λ + b ) [1 ] extended Voronoi’s algorithm for perfect forms [17 ] to such sets. In dimension 5 their enumeration found that the maximal density is that of D 5 D_{5} D 5 D 5 D_{5} D 5 [1 §4] . Cohn and Rajagopal cite the bound as a theorem of [1 ] [6 §4.2] . We prove the bound together with the list of equality cases. The four-dimensional statement is proved in [3 ] .
Throughout, Λ m \Lambda_m Λ m b m b_m b m P m = Λ m ∪ ( Λ m + b m ) P_m=\Lambda_m\cup(\Lambda_m+b_m) P m = Λ m ∪ ( Λ m + b m ) Λ m \Lambda_m Λ m ( Λ , b ) (\Lambda,b) ( Λ , b ) ( Λ ′ , b ′ ) (\Lambda',b') ( Λ ′ , b ′ ) R 5 \mathbb{R}^{5} R 5 Λ \Lambda Λ Λ ′ \Lambda' Λ ′ Λ + b \Lambda+b Λ + b Λ ′ + b ′ \Lambda'+b' Λ ′ + b ′
Theorem 1.1. Let Λ ⊂ R 5 \Lambda\subset\mathbb{R}^{5} Λ ⊂ R 5 b ∈ R 5 ∖ Λ b\in\mathbb{R}^{5}\setminus\Lambda b ∈ R 5 ∖ Λ ∣ x − y ∣ ≥ 2 |x-y|\ge2 ∣ x − y ∣ ≥ 2 x , y ∈ P = Λ ∪ ( Λ + b ) x,y\in P=\Lambda\cup(\Lambda+b) x , y ∈ P = Λ ∪ ( Λ + b ) covol ( Λ ) ≥ 16 2 \operatorname{covol}(\Lambda)\ge16\sqrt{2} covol ( Λ ) ≥ 16 2 ( Λ , b ) (\Lambda,b) ( Λ , b ) ( 2 Λ m , 2 b m ) (\sqrt{2}\Lambda_m,\sqrt{2}b_m) ( 2 Λ m , 2 b m ) m ∈ { 0 , … , 4 } m\in\{0,\ldots,4\} m ∈ { 0 , … , 4 } P P P π 2 / ( 15 2 ) \pi^{2}/(15\sqrt{2}) π 2 / ( 15 2 ) P P P 2 D 5 \sqrt{2}D_{5} 2 D 5 2 P 1 \sqrt{2}P_{1} 2 P 1 2 P 2 \sqrt{2}P_{2} 2 P 2
The sets P 0 P_{0} P 0 P 3 P_{3} P 3 P 4 P_{4} P 4 D 5 D_{5} D 5 D 5 D_{5} D 5 Λ 0 \Lambda_{0} Λ 0 Λ 3 \Lambda_{3} Λ 3 Λ 4 \Lambda_{4} Λ 4 2 P 1 \sqrt{2}P_{1} 2 P 1 Q 5 Q_{5} Q 5 [6 Table 4.2] . The set 2 P 2 \sqrt{2}P_2 2 P 2 L 5 L_5 L 5 [12 , 6 ] . The three sets are pairwise not congruent.
Table 1. The five extremal configurations, at minimal distance 2 \sqrt{2} 2 1 = ( 1 , 1 , 1 , 1 , 1 ) \mathbf{1}=(1,1,1,1,1) 1 = ( 1 , 1 , 1 , 1 , 1 ) D n = { x ∈ Z n : ∑ x i ∈ 2 Z } D_n=\{x\in\mathbb{Z}^n:\sum x_i\in2\mathbb{Z}\} D n = { x ∈ Z n : ∑ x i ∈ 2 Z } ∣ Min Λ m ∣ |\operatorname{Min}\Lambda_m| ∣ Min Λ m ∣ Λ m \Lambda_m Λ m
Figure 1.1. Two translates of a lattice, drawn in three dimensions: the points of Λ \Lambda Λ Λ + b \Lambda+b Λ + b Λ \Lambda Λ b b b 2 D 5 \sqrt{2}D_5 2 D 5 2 P 1 \sqrt{2}P_1 2 P 1 2 P 2 \sqrt{2}P_2 2 P 2 Theorem 1.1 ).
A lattice L L L Λ \Lambda Λ covol ( L ) = 1 2 covol ( Λ ) \operatorname{covol}(L)=\frac{1}{2}\operatorname{covol}(\Lambda) covol ( L ) = 2 1 covol ( Λ ) Theorem 1.1 contains the five-dimensional case of the theorem of Korkine and Zolotarev: a lattice in R 5 \mathbb{R}^5 R 5 8 2 8\sqrt{2} 8 2 2 D 5 \sqrt{2}D_5 2 D 5
Corollary 1.2. Let P ⊂ R 5 P\subset\mathbb{R}^5 P ⊂ R 5 P P P P P P 8 2 8\sqrt{2} 8 2 2 D 5 \sqrt{2}D_5 2 D 5 P P P 2 D 5 \sqrt{2}D_5 2 D 5 2 P 1 \sqrt{2}P_1 2 P 1 2 P 2 \sqrt{2}P_2 2 P 2
Method
A pair ( Λ , b ) (\Lambda,b) ( Λ , b ) 6 × 6 6\times6 6 × 6 J J J Λ \Lambda Λ b b b J [ k ] ≥ 4 J[k]\ge4 J [ k ] ≥ 4 R \mathcal{R} R § 8 ). Packings are the points of R \mathcal{R} R det J = 0 \det J=0 det J = 0 det Q \det Q det Q Q Q Q 5 × 5 5 \times5 5 × 5 J J J det Q \det Q det Q R \mathcal{R} R log det Q \log\det Q log det Q Q Q Q J J J
Up to the integral symmetries of the problem, R \mathcal{R} R det J > 0 \det J > 0 det J > 0 det J < 0 \det J < 0 det J < 0
The equality case is proved by hand in § 5 . A deep hole of a lattice is surrounded by lattice points that span the space affinely (Lemma 5.1). Perturbing along the directions of R \mathcal{R} R R \mathcal{R} R § 6 identifies the five configurations.
Two-periodic sets and the polyhedron R \mathcal{R} R
Notation
Notation. Sym n \operatorname{Sym}_n Sym n n × n n \times n n × n ∥ ⋅ ∥ \lVert\cdot\rVert ∥ ⋅ ∥ J ∈ Sym 6 J \in\operatorname{Sym}_6 J ∈ Sym 6 x ∈ R 6 x \in\mathbb{R}^6 x ∈ R 6 J [ x ] = x T J x J[x] = x^{\mathsf{T}}Jx J [ x ] = x T J x
J = ( Q r r T s ) , Q = Q ( J ) ∈ Sym 5 , r ∈ R 5 , s ∈ R . J = \begin{pmatrix} Q & r \\ r^{\mathsf{T}} & s \end{pmatrix}, \qquad Q = Q(J) \in\operatorname{Sym}_5,\ r \in\mathbb{R}^5,\ s \in\mathbb{R}. J = ( Q r T r s ) , Q = Q ( J ) ∈ Sym 5 , r ∈ R 5 , s ∈ R . Let M = Z 5 × { − 1 , 0 , 1 } ⊂ Z 6 \mathcal{M} = \mathbb{Z}^5 \times\{-1,0,1\} \subset\mathbb{Z}^6 M = Z 5 × { − 1 , 0 , 1 } ⊂ Z 6 M ∗ = M ∖ { 0 } \mathcal{M}^* = \mathcal{M} \setminus\{0\} M ∗ = M ∖ { 0 } M \mathcal{M} M k = ( n , l ) k = (n,l) k = ( n , l ) n ∈ Z 5 n \in\mathbb{Z}^5 n ∈ Z 5 l ∈ { − 1 , 0 , 1 } l \in\{-1,0,1\} l ∈ { − 1 , 0 , 1 }
R = { J ∈ Sym 6 : J [ k ] ≥ 4 for all k ∈ M ∗ } . \mathcal{R} = \{J \in\operatorname{Sym}_6 : J[k] \ge4 \text{ for all } k \in\mathcal{M}^*\}. R = { J ∈ Sym 6 : J [ k ] ≥ 4 for all k ∈ M ∗ } . R \mathcal{R} R J ∈ R J \in\mathcal{R} J ∈ R
Min ( J ) = { k ∈ M ∗ : J [ k ] = 4 } , C J = { X ∈ Sym 6 : X [ k ] ≥ 0 for all k ∈ Min ( J ) } , \operatorname{Min}(J) = \{k \in\mathcal{M}^* : J[k] = 4\}, \qquad C_J = \{X \in\operatorname{Sym}_6 : X[k] \ge0 \text{ for all } k \in\operatorname{Min}(J)\}, Min ( J ) = { k ∈ M ∗ : J [ k ] = 4 } , C J = { X ∈ Sym 6 : X [ k ] ≥ 0 for all k ∈ Min ( J )} , L J = C J ∩ ( − C J ) = { X ∈ Sym 6 : X [ k ] = 0 for all k ∈ Min ( J ) } , L_J = C_J \cap(-C_J) = \{X \in\operatorname{Sym}_6 : X[k] = 0 \text{ for all } k \in\operatorname{Min}(J)\}, L J = C J ∩ ( − C J ) = { X ∈ Sym 6 : X [ k ] = 0 for all k ∈ Min ( J )} , and d ( J ) = dim L J d(J) = \dim L_J d ( J ) = dim L J k k k − k -k − k ± k \pm k ± k Min ( J ) \operatorname{Min}(J) Min ( J )
Let Λ ⊂ R 5 \Lambda\subset\mathbb{R}^5 Λ ⊂ R 5 a = ( a 1 , … , a 5 ) a = (a_1,\ldots,a_5) a = ( a 1 , … , a 5 ) b ∈ R 5 b \in\mathbb{R}^5 b ∈ R 5 ( a 1 , … , a 5 , b ) (a_1,\ldots,a_5,b) ( a 1 , … , a 5 , b ) J ( a , b ) J(a,b) J ( a , b )
J ( a , b ) [ ( n , l ) ] = ∣ ∑ i = 1 5 n i a i + l b ∣ 2 . (1) J(a,b)[(n,l)] = \left\lvert\sum_{i=1}^{5} n_i a_i + lb \right\rvert^2. \tag*{(1)} J ( a , b ) [( n , l )] = i = 1 ∑ 5 n i a i + l b 2 . (1) Lemma 2.1. Let b ∉ Λ b \notin\Lambda b ∈ / Λ Λ ∪ ( Λ + b ) \Lambda\cup(\Lambda+ b) Λ ∪ ( Λ + b ) J ( a , b ) ∈ R J(a,b) \in\mathcal{R} J ( a , b ) ∈ R
Proof. Since Λ \Lambda Λ Λ + b \Lambda+ b Λ + b ( Λ ∖ 0 ) ∪ ( Λ + b ) ∪ ( Λ − b ) (\Lambda\setminus0) \cup(\Lambda+ b) \cup(\Lambda- b) ( Λ ∖ 0 ) ∪ ( Λ + b ) ∪ ( Λ − b ) ∑ n i a i + l b \sum n_i a_i + lb ∑ n i a i + l b ( n , l ) ∈ M ∗ (n,l) \in\mathcal{M}^* ( n , l ) ∈ M ∗ (1) . □ \square □
Lemma 2.2. For J ∈ R J \in\mathcal{R} J ∈ R Q ( J ) Q(J) Q ( J )
Proof. We have Q [ n ] = J [ ( n , 0 ) ] ≥ 4 Q[n] = J[(n,0)] \ge4 Q [ n ] = J [( n , 0 )] ≥ 4 n ∈ Z 5 ∖ 0 n \in\mathbb{Z}^5 \setminus0 n ∈ Z 5 ∖ 0 Q [ x ] < 0 Q[x] < 0 Q [ x ] < 0 x ∈ R 5 x \in\mathbb{R}^5 x ∈ R 5 { Q < 0 } \{Q < 0\} { Q < 0 } n ≠ 0 n \ne0 n = 0 Q [ n ] < 0 Q[n] < 0 Q [ n ] < 0 Q Q Q Q v = 0 Qv = 0 Q v = 0 max i ∣ v i ∣ = 1 \max_i |v_i| = 1 max i ∣ v i ∣ = 1 N ≥ 1 N \ge1 N ≥ 1 N 5 N^5 N 5 n ∈ Z 5 n \in\mathbb{Z}^5 n ∈ Z 5 max i ∣ m v i − n i ∣ ≤ 1 / N \max_i |mv_i-n_i| \le1/N max i ∣ m v i − n i ∣ ≤ 1/ N n ≠ 0 n \ne0 n = 0 max i ∣ m v i ∣ = m ≥ 1 > 1 / N \max_i |mv_i|=m \ge1>1/N max i ∣ m v i ∣ = m ≥ 1 > 1/ N Q [ n ] = Q [ n − m v ] ≤ 25 ∥ Q ∥ ∞ / N 2 Q[n]=Q[n-mv]\le25\lVert Q\rVert_\infty/N^2 Q [ n ] = Q [ n − m v ] ≤ 25 ∥ Q ∥ ∞ / N 2 ∥ Q ∥ ∞ \lVert Q\rVert_\infty ∥ Q ∥ ∞ N N N Q Q Q
Let Sym 6 + = { J ∈ Sym 6 : Q ( J ) positive definite } \operatorname{Sym}^{+}_6=\{J\in\operatorname{Sym}_6:Q(J)\text{ positive definite}\} Sym 6 + = { J ∈ Sym 6 : Q ( J ) positive definite } R \mathcal{R} R J ∈ Sym 6 + J\in\operatorname{Sym}^{+}_6 J ∈ Sym 6 +
q ( J ) = Q − 1 r , σ ( J ) = s − r T Q − 1 r . q(J)=Q^{-1}r,\qquad\sigma(J)=s-r^{\mathsf T}Q^{-1}r. q ( J ) = Q − 1 r , σ ( J ) = s − r T Q − 1 r . Lemma 2.3. Let J ∈ Sym 6 + J\in\operatorname{Sym}^{+}_6 J ∈ Sym 6 +
(1) J [ ( x , l ) ] = Q [ x + l q ( J ) ] + l 2 σ ( J ) J[(x,l)]=Q[x+lq(J)]+l^2\sigma(J) J [( x , l )] = Q [ x + l q ( J )] + l 2 σ ( J ) x ∈ R 5 x\in\mathbb{R}^5 x ∈ R 5 l ∈ R l\in\mathbb{R} l ∈ R
(2) σ ( J ) = min x ∈ R 5 J [ ( x , 1 ) ] \sigma(J)=\min_{x\in\mathbb{R}^5}J[(x,1)] σ ( J ) = min x ∈ R 5 J [( x , 1 )] x = − q ( J ) x=-q(J) x = − q ( J ) σ ( J ′ ) ≤ J ′ [ u ] \sigma(J')\le J'[u] σ ( J ′ ) ≤ J ′ [ u ] J ′ ∈ Sym 6 + J'\in\operatorname{Sym}^{+}_6 J ′ ∈ Sym 6 + u ∈ R 5 × { 1 } u\in\mathbb{R}^5\times\{1\} u ∈ R 5 × { 1 } σ \sigma σ Sym 6 + \operatorname{Sym}^{+}_6 Sym 6 +
(3) det J = det Q ⋅ σ ( J ) \det J=\det Q\cdot\sigma(J) det J = det Q ⋅ σ ( J )
Proof. (1) is completing the square, (2) follows from (1) because Q Q Q J J J
Lemma 2.4. Let J ∈ R J\in\mathcal{R} J ∈ R
(1) σ ( J ) = 0 \sigma(J)=0 σ ( J ) = 0 J = J ( a , b ) J=J(a,b) J = J ( a , b ) a a a Λ ⊂ R 5 \Lambda\subset\mathbb{R}^5 Λ ⊂ R 5 b ∉ Λ b\notin\Lambda b ∈ / Λ Λ ∪ ( Λ + b ) \Lambda\cup(\Lambda+b) Λ ∪ ( Λ + b ) det Q ( J ) = covol ( Λ ) 2 \det Q(J)=\operatorname{covol}(\Lambda)^2 det Q ( J ) = covol ( Λ ) 2
(2) If σ ( J ) < 0 \sigma(J)<0 σ ( J ) < 0 J + ∣ σ ( J ) ∣ e 6 e 6 T ∈ R J+|\sigma(J)|e_6e_6^{\mathsf T}\in\mathcal{R} J + ∣ σ ( J ) ∣ e 6 e 6 T ∈ R Q Q Q Q ( J ) Q(J) Q ( J ) σ \sigma σ
Proof. (1) If σ ( J ) = 0 \sigma(J)=0 σ ( J ) = 0 J J J Lemma 2.3 (1), (3) and Lemma 2.2, hence the Gram matrix of six vectors a 1 , … , a 5 , b a_1,\ldots,a_5,b a 1 , … , a 5 , b R 5 \mathbb{R}^5 R 5 a 1 , … , a 5 a_1,\ldots,a_5 a 1 , … , a 5 Q Q Q b b b ∑ n i a i \sum n_i a_i ∑ n i a i J [ ( − n , 1 ) ] = 0 < 4 J[(-n,1)]=0<4 J [( − n , 1 )] = 0 < 4 J ( a , b ) J(a,b) J ( a , b ) R 5 \mathbb{R}^5 R 5 det J ( a , b ) = 0 \det J(a,b)=0 det J ( a , b ) = 0 σ = 0 \sigma=0 σ = 0 Lemma 2.3 (3). Finally det Q = det ( a i ⋅ a j ) = covol ( Λ ) 2 \det Q=\det(a_i\cdot a_j)=\operatorname{covol}(\Lambda)^2 det Q = det ( a i ⋅ a j ) = covol ( Λ ) 2
(2) Adding ∣ σ ∣ e 6 e 6 T |\sigma|e_6e_6^{\mathsf T} ∣ σ ∣ e 6 e 6 T J [ ( n , l ) ] J[(n,l)] J [( n , l )] l 2 ∣ σ ∣ ≥ 0 l^2|\sigma|\ge0 l 2 ∣ σ ∣ ≥ 0 Q Q Q r r r s s s σ \sigma σ ∣ σ ∣ |\sigma| ∣ σ ∣
Lemma 2.5. For J ∈ R J\in\mathcal{R} J ∈ R det Q ( J ) ≥ 64 π 4 / 225 \det Q(J)\ge64\pi^4/225 det Q ( J ) ≥ 64 π 4 /225
Proof. Q Q Q Λ \Lambda Λ R 5 \mathbb{R}^5 R 5 2 5 ⋅ 8 π 2 / 15 2^5\cdot8\pi^2/15 2 5 ⋅ 8 π 2 /15 [5 Ch. III] it contains a nonzero point of Λ \Lambda Λ 2 5 covol ( Λ ) 2^5\operatorname{covol}(\Lambda) 2 5 covol ( Λ ) covol ( Λ ) ≥ 8 π 2 / 15 \operatorname{covol}(\Lambda)\ge8\pi^2/15 covol ( Λ ) ≥ 8 π 2 /15
Local structure
Lemma 2.6.
(1) For every compact set K ⊂ Sym 6 + K\subset\operatorname{Sym}^{+}_6 K ⊂ Sym 6 + M K = { k ∈ M ∗ : J [ k ] ≤ 5 for some J ∈ K } M_K=\{k\in\mathcal{M}^*:J[k]\le5\text{ for some }J\in K\} M K = { k ∈ M ∗ : J [ k ] ≤ 5 for some J ∈ K }
(2) For every J ∈ R J\in\mathcal{R} J ∈ R ε > 0 \varepsilon>0 ε > 0 X ∈ Sym 6 X\in\operatorname{Sym}_6 X ∈ Sym 6 ∥ X ∥ ≤ ε \lVert X\rVert\le\varepsilon ∥ X ∥ ≤ ε J + X ∈ R J+X\in\mathcal{R} J + X ∈ R X ∈ C J X\in C_J X ∈ C J
(3) For every J ∈ R J\in\mathcal{R} J ∈ R Min ( J ) \operatorname{Min}(J) Min ( J ) R ⊆ J + C J \mathcal{R}\subseteq J+C_J R ⊆ J + C J
Proof. (1) On K K K Q Q Q μ > 0 \mu>0 μ > 0 ∣ q ( J ) ∣ ≤ ρ |q(J)|\le\rho ∣ q ( J ) ∣ ≤ ρ ∣ σ ( J ) ∣ ≤ ρ |\sigma(J)|\le\rho ∣ σ ( J ) ∣ ≤ ρ ρ \rho ρ k = ( n , l ) ∈ M ∗ k=(n,l)\in\mathcal{M}^* k = ( n , l ) ∈ M ∗ J ∈ K J\in K J ∈ K Lemma 2.3 (1) gives J [ k ] ≥ μ ∣ n + l q ( J ) ∣ 2 − ρ J[k]\ge\mu|n+lq(J)|^2-\rho J [ k ] ≥ μ ∣ n + l q ( J ) ∣ 2 − ρ ∣ n ∣ > ρ + ( 5 + ρ ) / μ |n|>\rho+\sqrt{(5+\rho)/\mu} ∣ n ∣ > ρ + ( 5 + ρ ) / μ ∣ n + l q ( J ) ∣ ≥ ∣ n ∣ − ρ |n+lq(J)|\ge|n|-\rho ∣ n + l q ( J ) ∣ ≥ ∣ n ∣ − ρ J [ k ] > 5 J[k]>5 J [ k ] > 5 ε 0 > 0 \varepsilon_0>0 ε 0 > 0 K = B ‾ ( J , ε 0 ) K=\overline{B}(J,\varepsilon_0) K = B ( J , ε 0 ) Sym 6 + \operatorname{Sym}^{+}_6 Sym 6 + k ∈ M K ∖ Min ( J ) k\in\mathcal{M}_K\setminus\operatorname{Min}(J) k ∈ M K ∖ Min ( J ) J [ k ] > 4 J[k]>4 J [ k ] > 4 ε ≤ ε 0 \varepsilon\le\varepsilon_0 ε ≤ ε 0 ( J + X ) [ k ] > 4 (J+X)[k]>4 ( J + X ) [ k ] > 4 ∥ X ∥ ≤ ε \lVert X\rVert\le\varepsilon ∥ X ∥ ≤ ε X X X k ∉ M K k\notin\mathcal{M}_K k ∈ / M K ( J + X ) [ k ] > 5 (J+X)[k]>5 ( J + X ) [ k ] > 5 J + X ∈ R J+X\in\mathcal{R} J + X ∈ R ( J + X ) [ k ] = 4 + X [ k ] ≥ 4 (J+X)[k]=4+X[k]\ge4 ( J + X ) [ k ] = 4 + X [ k ] ≥ 4 k ∈ Min ( J ) k\in\operatorname{Min}(J) k ∈ Min ( J ) Min ( J ) ⊂ M { J } \operatorname{Min}(J)\subset\mathcal{M}_{\{J\}} Min ( J ) ⊂ M { J } J ′ ∈ R J' \in\mathcal{R} J ′ ∈ R J + λ ( J ′ − J ) ∈ R J+\lambda(J'-J) \in\mathcal{R} J + λ ( J ′ − J ) ∈ R λ ∈ [ 0 , 1 ] \lambda\in[0,1] λ ∈ [ 0 , 1 ] λ ( J ′ − J ) ∈ C J \lambda(J'-J) \in C_J λ ( J ′ − J ) ∈ C J λ > 0 \lambda>0 λ > 0 C J C_J C J
Lemma 2.7. R \mathcal{R} R
Proof. If J + τ X ∈ R J+\tau X \in\mathcal{R} J + τ X ∈ R τ ∈ R \tau\in\mathbb{R} τ ∈ R X [ k ] = 0 X[k]=0 X [ k ] = 0 k ∈ M ∗ k \in\mathcal{M}^* k ∈ M ∗ k k T kk^{\mathsf T} k k T k = e i k=e_i k = e i 1 ≤ i ≤ 6 1\leq i\leq6 1 ≤ i ≤ 6 k = e i + e j k=e_i+e_j k = e i + e j 1 ≤ i < j ≤ 6 1\leq i<j\leq6 1 ≤ i < j ≤ 6 M ∗ \mathcal{M}^* M ∗ Sym 6 \operatorname{Sym}_6 Sym 6 X = 0 X=0 X = 0
Definition 2.8. A vertex of R \mathcal{R} R J ∈ R J\in\mathcal{R} J ∈ R d ( J ) = 0 d(J)=0 d ( J ) = 0 C J C_J C J X [ k ] ≥ 0 X[k]\geq0 X [ k ] ≥ 0 k ∈ Min ( J ) k\in\operatorname{Min}(J) k ∈ Min ( J ) Sym 6 \operatorname{Sym}_6 Sym 6 C J C_J C J R ≥ 0 Y \mathbb{R}_{\geq0}Y R ≥ 0 Y Y ≠ 0 Y\ne0 Y = 0 Y ∈ C J Y\in C_J Y ∈ C J X ↦ X [ k ] X\mapsto X[k] X ↦ X [ k ] k ∈ Min ( J ) k\in\operatorname{Min}(J) k ∈ Min ( J ) Y [ k ] = 0 Y[k]=0 Y [ k ] = 0 Y Y Y
t ∗ ( J , Y ) = sup { t ≥ 0 : J + t Y ∈ R } ∈ ( 0 , ∞ ] , t^*(J,Y)=\sup\{t\geq0:J+tY\in\mathcal{R}\}\in(0,\infty], t ∗ ( J , Y ) = sup { t ≥ 0 : J + t Y ∈ R } ∈ ( 0 , ∞ ] , which is positive by Lemma 2.6 (2). The set { J + t Y : 0 ≤ t ≤ t ∗ } \{J+tY:0\leq t\leq t^*\} { J + t Y : 0 ≤ t ≤ t ∗ } t < ∞ t<\infty t < ∞ R \mathcal{R} R J J J Y Y Y t ∗ < ∞ t^*<\infty t ∗ < ∞
We use two standard facts on polyhedral cones [18 Lecture 1] : a pointed polyhedral cone has finitely many extreme rays and is their conical hull, and a nonzero vector of the cone spans an extreme ray exactly when the inequalities it satisfies with equality have rank one less than the dimension.
Lemma 2.9. Let J J J Y Y Y C J C_J C J Z = { k ∈ Min ( J ) : Y [ k ] = 0 } Z=\{k\in\operatorname{Min}(J):Y[k]=0\} Z = { k ∈ Min ( J ) : Y [ k ] = 0 }
{ t ≥ 0 : J + t Y ∈ R } \{t\geq0:J+tY\in\mathcal{R}\} { t ≥ 0 : J + t Y ∈ R } [ 0 , t ∗ ] [0,t^*] [ 0 , t ∗ ] [ 0 , ∞ ) [0,\infty) [ 0 , ∞ ) t ∗ = ∞ t^*=\infty t ∗ = ∞ t ∗ < ∞ t^*<\infty t ∗ < ∞ J + t ∗ Y J+t^*Y J + t ∗ Y
For 0 < t < t ∗ 0<t<t^* 0 < t < t ∗ Min ( J + t Y ) = Z \operatorname{Min}(J+tY)=Z Min ( J + t Y ) = Z d ( J + t Y ) = 1 d(J+tY)=1 d ( J + t Y ) = 1
Every J ′ ∈ R J'\in\mathcal{R} J ′ ∈ R d ( J ′ ) = 1 d(J')=1 d ( J ′ ) = 1 J ′ = J v + t Y ′ J'=J_v+tY' J ′ = J v + t Y ′ J v J_v J v Y ′ Y' Y ′ C J v C_{J_v} C J v 0 < t < t ∗ ( J v , Y ′ ) 0<t<t^*(J_v,Y') 0 < t < t ∗ ( J v , Y ′ )
Proof. (1) The set is convex and closed. Let J 1 = J + t ∗ Y J_1=J+t^*Y J 1 = J + t ∗ Y t ∗ < ∞ t^*<\infty t ∗ < ∞ k ∈ Z k\in Z k ∈ Z J 1 [ k ] = 4 J_1[k]=4 J 1 [ k ] = 4 Z ⊆ Min ( J 1 ) Z\subseteq\operatorname{Min}(J_1) Z ⊆ Min ( J 1 ) J 1 + η Y ∉ R J_1+\eta Y\notin\mathcal{R} J 1 + η Y ∈ / R η > 0 \eta>0 η > 0 Lemma 2.6 (2) gives Y ∉ C J 1 Y\notin C_{J_1} Y ∈ / C J 1 k 1 ∈ Min ( J 1 ) k_1\in\operatorname{Min}(J_1) k 1 ∈ Min ( J 1 ) Y [ k 1 ] < 0 Y[k_1]<0 Y [ k 1 ] < 0 Z Z Z Y Y Y k 1 k_1 k 1 Y Y Y L J 1 = 0 L_{J_1}=0 L J 1 = 0 k ∈ M ∗ k\in\mathcal{M}^* k ∈ M ∗ τ ↦ ( J + τ Y ) [ k ] \tau\mapsto(J+\tau Y)[k] τ ↦ ( J + τ Y ) [ k ] [ 0 , t ] [0,t] [ 0 , t ] t t t t t t J [ k ] = 4 J[k]=4 J [ k ] = 4 Y [ k ] = 0 Y[k]=0 Y [ k ] = 0 Min ( J + t Y ) = Z \operatorname{Min}(J+tY)=Z Min ( J + t Y ) = Z L J + t Y L_{J+tY} L J + t Y Z Z Z L J ′ = R X 0 L_{J'}=\mathbb{R}X_0 L J ′ = R X 0 I 0 = { τ : J ′ + τ X 0 ∈ R } I_0=\{\tau:J'+\tau X_0\in\mathcal{R}\} I 0 = { τ : J ′ + τ X 0 ∈ R } Lemma 2.6 (2) and is not R \mathbb{R} R Lemma 2.7 . Let τ e \tau_e τ e J v = J ′ + τ e X 0 J_v=J'+\tau_eX_0 J v = J ′ + τ e X 0 Y ′ = − sgn ( τ e ) X 0 Y'=-\operatorname{sgn}(\tau_e)X_0 Y ′ = − sgn ( τ e ) X 0 X 0 [ k ] = 0 X_0[k]=0 X 0 [ k ] = 0 k ∈ Min ( J ′ ) k\in\operatorname{Min}(J') k ∈ Min ( J ′ ) Min ( J ′ ) ⊆ Min ( J v ) \operatorname{Min}(J')\subseteq\operatorname{Min}(J_v) Min ( J ′ ) ⊆ Min ( J v ) L J v ⊆ L J ′ L_{J_v}\subseteq L_{J'} L J v ⊆ L J ′ X 0 ∈ L J v X_0\in L_{J_v} X 0 ∈ L J v J v ± η X 0 ∈ R J_v\pm\eta X_0\in\mathcal{R} J v ± η X 0 ∈ R η \eta η Lemma 2.6 (2), contradicting the choice of τ e \tau_e τ e d ( J v ) = 0 d(J_v)=0 d ( J v ) = 0 J v J_v J v J ′ J' J ′ R \mathcal{R} R Y ′ ∈ C J v Y'\in C_{J_v} Y ′ ∈ C J v Lemma 2.6 (2), and Y ′ Y' Y ′ Min ( J ′ ) \operatorname{Min}(J') Min ( J ′ ) Y ′ Y' Y ′ C J v C_{J_v} C J v J ′ = J v + ∣ τ e ∣ Y ′ J'=J_v+|\tau_e|Y' J ′ = J v + ∣ τ e ∣ Y ′ ∣ τ e ∣ < t ∗ ( J v , Y ′ ) |\tau_e|<t^*(J_v,Y') ∣ τ e ∣ < t ∗ ( J v , Y ′ ) J ′ J' J ′
Symmetries
Let T \mathcal{T} T
T = ( U v 0 ϵ ) , U ∈ GL 5 ( Z ) , v ∈ Z 5 , ϵ ∈ { 1 , − 1 } . T=\begin{pmatrix} U & v \\ 0 & \epsilon\end{pmatrix},\qquad U\in\operatorname{GL}_5(\mathbb{Z}),\ v\in\mathbb{Z}^5,\ \epsilon\in\{1,-1\}. T = ( U 0 v ϵ ) , U ∈ GL 5 ( Z ) , v ∈ Z 5 , ϵ ∈ { 1 , − 1 } . Then T ( n , l ) = ( U n + l v , ϵ l ) T(n,l)=(Un+lv,\epsilon l) T ( n , l ) = ( U n + l v , ϵ l ) T T T M \mathcal{M} M J ↦ T T J T J\mapsto T^{\mathsf T}JT J ↦ T T J T R \mathcal{R} R ( T T J T ) [ k ] = J [ T k ] (T^{\mathsf T}JT)[k]=J[Tk] ( T T J T ) [ k ] = J [ T k ] Min ( T T J T ) = T − 1 Min ( J ) \operatorname{Min}(T^{\mathsf T}JT)=T^{-1}\operatorname{Min}(J) Min ( T T J T ) = T − 1 Min ( J ) T T X T T^{\mathsf T}XT T T X T C J C_J C J C T T J T C_{T^{\mathsf T}JT} C T T J T t ∗ t^* t ∗ Q ( T T J T ) = T T Q T Q(T^{\mathsf T}JT)=T^{\mathsf T}QT Q ( T T J T ) = T T QT det Q \det Q det Q det J \det J det J σ = det J / det Q \sigma=\det J/\det Q σ = det J / det Q Γ \Gamma Γ J , J ′ J,J' J , J ′ J ′ = T T J T J'=T^{\mathsf T}JT J ′ = T T J T T ∈ Γ T\in\Gamma T ∈ Γ Γ J \Gamma_J Γ J J J J
Lemma 2.10. Let a , a ′ a,a' a , a ′ Λ , Λ ′ ⊂ R 5 \Lambda,\Lambda'\subset\mathbb{R}^5 Λ , Λ ′ ⊂ R 5 b , b ′ ∈ R 5 b,b'\in\mathbb{R}^5 b , b ′ ∈ R 5 J ( a , b ) J(a,b) J ( a , b ) J ( a ′ , b ′ ) J(a',b') J ( a ′ , b ′ ) ( Λ , b ) (\Lambda,b) ( Λ , b ) ( Λ ′ , b ′ ) (\Lambda',b') ( Λ ′ , b ′ )
Proof. Suppose J ( a ′ , b ′ ) = T T J ( a , b ) T J(a',b')=T^{\mathsf T}J(a,b)T J ( a ′ , b ′ ) = T T J ( a , b ) T T T T ( a ′ , b ′ ) (a',b') ( a ′ , b ′ ) ( a U , ε b + ∑ v i a i ) (aU,\varepsilon b+\sum v_i a_i) ( a U , ε b + ∑ v i a i ) a ′ a' a ′ R 5 \mathbb{R}^5 R 5 ψ \psi ψ a ′ a' a ′ a U aU a U b ′ b' b ′ ε b + ∑ v i a i \varepsilon b+\sum v_i a_i ε b + ∑ v i a i ψ ( Λ ′ ) = Λ \psi(\Lambda')=\Lambda ψ ( Λ ′ ) = Λ ψ ( Λ ′ + b ′ ) = Λ + ε b \psi(\Lambda'+b')=\Lambda+\varepsilon b ψ ( Λ ′ + b ′ ) = Λ + ε b ε = − 1 \varepsilon=-1 ε = − 1 ψ \psi ψ − ψ -\psi − ψ Λ ′ \Lambda' Λ ′ Λ \Lambda Λ Λ ′ + b ′ \Lambda'+b' Λ ′ + b ′ Λ + b \Lambda+b Λ + b f f f Λ ′ \Lambda' Λ ′ Λ \Lambda Λ Λ ′ + b ′ \Lambda'+b' Λ ′ + b ′ Λ + b \Lambda+b Λ + b f ( 0 ) ∈ Λ f(0)\in\Lambda f ( 0 ) ∈ Λ ψ = f − f ( 0 ) \psi=f-f(0) ψ = f − f ( 0 ) ψ ( Λ ′ ) = Λ \psi(\Lambda')=\Lambda ψ ( Λ ′ ) = Λ ψ ( Λ ′ + b ′ ) = Λ + b \psi(\Lambda'+b')=\Lambda+b ψ ( Λ ′ + b ′ ) = Λ + b ψ ( a ′ ) = a U \psi(a')=aU ψ ( a ′ ) = a U U ∈ GL 5 ( Z ) U\in\operatorname{GL}_5(\mathbb{Z}) U ∈ GL 5 ( Z ) ψ ( b ′ ) = b + ∑ v i a i \psi(b')=b+\sum v_i a_i ψ ( b ′ ) = b + ∑ v i a i v ∈ Z 5 v\in\mathbb{Z}^5 v ∈ Z 5 J ( a ′ , b ′ ) = T T J ( a , b ) T J(a',b')=T^{\mathsf T}J(a,b)T J ( a ′ , b ′ ) = T T J ( a , b ) T ε = 1 \varepsilon=1 ε = 1
Reaching all vertices
Proposition 2.11. Let v v v w w w R R R v = v 0 , v 1 , … , v m = w v=v_0,v_1,\ldots,v_m=w v = v 0 , v 1 , … , v m = w v s + 1 = v s + t ∗ Y s v_{s+1}=v_s+t^*Y_s v s + 1 = v s + t ∗ Y s Y s Y_s Y s C v s C_{v_s} C v s t ∗ ( v s , Y s ) < ∞ t^*(v_s,Y_s)<\infty t ∗ ( v s , Y s ) < ∞
Proof. Let ℓ ( X ) = ∑ k ∈ Min ( w ) X [ k ] \ell(X)=\sum_{k\in\operatorname{Min}(w)}X[k] ℓ ( X ) = ∑ k ∈ Min ( w ) X [ k ] ℓ ≥ 0 \ell\geq0 ℓ ≥ 0 C w C_w C w ℓ ( X ) = 0 \ell(X)=0 ℓ ( X ) = 0 X ∈ C w X\in C_w X ∈ C w X ∈ L w = 0 X\in L_w=0 X ∈ L w = 0 { X ∈ C w : ∥ X ∥ = 1 } \{X\in C_w:\lVert X\rVert=1\} { X ∈ C w : ∥ X ∥ = 1 } δ > 0 \delta>0 δ > 0 ℓ ( X ) ≥ δ ∥ X ∥ \ell(X)\geq\delta\lVert X\rVert ℓ ( X ) ≥ δ ∥ X ∥ C w C_w C w Lemma 2.6 (3), R ⊆ w + C w R\subseteq w+C_w R ⊆ w + C w ℓ ( J ) > ℓ ( w ) \ell(J)>\ell(w) ℓ ( J ) > ℓ ( w ) J ∈ R ∖ { w } J\in R\setminus\{w\} J ∈ R ∖ { w } c c c S c = { J ∈ R : ℓ ( J ) ≤ c } S_c=\{J\in R:\ell(J)\leq c\} S c = { J ∈ R : ℓ ( J ) ≤ c } J J J J [ k ] = 4 J[k]=4 J [ k ] = 4 k ∈ Min ( J ) k\in\operatorname{Min}(J) k ∈ Min ( J ) S c S_c S c Min ( J ) ⊆ M S c \operatorname{Min}(J)\subseteq\mathcal{M}_{S_c} Min ( J ) ⊆ M S c Lemma 2.6 (1). So S c S_c S c
Let u u u u ≠ w u\neq w u = w ℓ ( Y ) ≥ 0 \ell(Y)\geq0 ℓ ( Y ) ≥ 0 C u C_u C u ℓ ≥ 0 \ell\geq0 ℓ ≥ 0 C u C_u C u R ⊆ u + C u R\subseteq u+C_u R ⊆ u + C u ℓ ( w ) ≥ ℓ ( u ) \ell(w)\geq\ell(u) ℓ ( w ) ≥ ℓ ( u ) Y Y Y C u C_u C u ℓ ( Y ) < 0 \ell(Y)<0 ℓ ( Y ) < 0 u + t Y u+tY u + t Y ℓ \ell ℓ S ℓ ( u ) S_{\ell(u)} S ℓ ( u ) t ∗ ( u , Y ) < ∞ t^*(u,Y)<\infty t ∗ ( u , Y ) < ∞ u ′ = u + t ∗ Y u'=u+t^*Y u ′ = u + t ∗ Y Lemma 2.9 ) with ℓ ( u ′ ) < ℓ ( u ) \ell(u')<\ell(u) ℓ ( u ′ ) < ℓ ( u ) u = v u=v u = v S ℓ ( v ) S_{\ell(v)} S ℓ ( v ) ℓ \ell ℓ w w w
Corollary 2.12. Let J 0 , … , J N J_0,\ldots,J_N J 0 , … , J N R R R i i i Y Y Y C J i C_{J_i} C J i t ∗ ( J i , Y ) < ∞ t^*(J_i,Y)<\infty t ∗ ( J i , Y ) < ∞ J i + t ∗ Y J_i+t^*Y J i + t ∗ Y J j J_j J j R R R J j J_j J j R R R J j J_j J j
Proof. Let w w w J 0 = v 0 , … , v m = w J_0=v_0,\ldots,v_m=w J 0 = v 0 , … , v m = w Proposition 2.11 . If v s = T T J i T v_s=T^{\mathsf T}J_iT v s = T T J i T Y ′ = T − 1 Y s T − T Y'=T^{-1}Y_sT^{-\mathsf T} Y ′ = T − 1 Y s T − T C J i C_{J_i} C J i t ∗ t^* t ∗ v s + 1 = T T ( J i + t ∗ Y ′ ) T v_{s+1}=T^{\mathsf T}(J_i+t^*Y')T v s + 1 = T T ( J i + t ∗ Y ′ ) T J j J_j J j w w w J j J_j J j w = T T J j T w=T^{\mathsf T}J_jT w = T T J j T Y Y Y T T T J j J_j J j T − T Y T − 1 T^{-\mathsf T}YT^{-1} T − T Y T − 1
Reduction to vertices and edges
Lemma 3.1. Let Q Q Q H ∈ Sym 5 H\in\operatorname{Sym}_5 H ∈ Sym 5 H ≠ 0 H\neq0 H = 0 τ \tau τ Q + τ H Q+\tau H Q + τ H ψ ( τ ) = log det ( Q + τ H ) \psi(\tau)=\log\det(Q+\tau H) ψ ( τ ) = log det ( Q + τ H )
Proof. With Q τ = Q + τ H Q_\tau=Q+\tau H Q τ = Q + τ H ψ ′ ( τ ) = tr ( Q τ − 1 H ) \psi'(\tau)=\operatorname{tr}(Q_\tau^{-1}H) ψ ′ ( τ ) = tr ( Q τ − 1 H ) ψ ′ ′ ( τ ) = − tr ( ( Q τ − 1 / 2 H Q τ − 1 / 2 ) 2 ) < 0 \psi''(\tau)=-\operatorname{tr}((Q_\tau^{-1/2}HQ_\tau^{-1/2})^2)<0 ψ ′′ ( τ ) = − tr (( Q τ − 1/2 H Q τ − 1/2 ) 2 ) < 0 Q τ − 1 / 2 H Q τ − 1 / 2 Q_\tau^{-1/2}HQ_\tau^{-1/2} Q τ − 1/2 H Q τ − 1/2
Let
S = { J ∈ R : σ ( J ) ≤ 0 } , C = { J ∈ S : d ( J ) = 0 } ∪ { J ∈ R : d ( J ) = 1 , σ ( J ) = 0 } . S=\{J\in R:\sigma(J)\leq0\},\qquad C=\{J\in S:d(J)=0\}\cup\{J\in R:d(J)=1,\ \sigma(J)=0\}. S = { J ∈ R : σ ( J ) ≤ 0 } , C = { J ∈ S : d ( J ) = 0 } ∪ { J ∈ R : d ( J ) = 1 , σ ( J ) = 0 } . So C \mathcal{C} C det J ≤ 0 \det J \le0 det J ≤ 0 det J = 0 \det J = 0 det J = 0 det Q \det Q det Q S \mathcal{S} S covol ( Λ ) 2 \operatorname{covol}(\Lambda)^2 covol ( Λ ) 2
Proposition 3.2. For every J ∈ S J \in\mathcal{S} J ∈ S J ′ ∈ C J' \in\mathcal{C} J ′ ∈ C det Q ( J ′ ) ≤ det Q ( J ) \det Q(J') \le\det Q(J) det Q ( J ′ ) ≤ det Q ( J )
Proof. Write f ( J ) = log det Q ( J ) f(J) = \log\det Q(J) f ( J ) = log det Q ( J ) π ( J ) = 2 d ( J ) + [ σ ( J ) < 0 ] \pi(J) = 2d(J) + [\sigma(J) < 0] π ( J ) = 2 d ( J ) + [ σ ( J ) < 0 ] [ ⋅ ] [\cdot] [ ⋅ ] J ∈ S ∖ C J \in\mathcal{S} \setminus\mathcal{C} J ∈ S ∖ C J 1 ∈ S J_1 \in\mathcal{S} J 1 ∈ S f ( J 1 ) ≤ f ( J ) f(J_1) \le f(J) f ( J 1 ) ≤ f ( J ) π ( J 1 ) < π ( J ) \pi(J_1) < \pi(J) π ( J 1 ) < π ( J ) π \pi π
Let J ∈ S ∖ C J \in\mathcal{S} \setminus\mathcal{C} J ∈ S ∖ C σ ( J ) < 0 \sigma(J) < 0 σ ( J ) < 0 d ( J ) ≥ 1 d(J) \ge1 d ( J ) ≥ 1 σ ( J ) = 0 \sigma(J) = 0 σ ( J ) = 0 d ( J ) ≥ 2 d(J) \ge2 d ( J ) ≥ 2 X ∈ L J ∖ 0 X \in L_J \setminus0 X ∈ L J ∖ 0 u = ( − q ( J ) , 1 ) ∈ R 6 u = (-q(J),1) \in\mathbb{R}^6 u = ( − q ( J ) , 1 ) ∈ R 6 J [ u ] = σ ( J ) = 0 J[u] = \sigma(J) = 0 J [ u ] = σ ( J ) = 0 X ∈ L J ∖ 0 X \in L_J \setminus0 X ∈ L J ∖ 0 X [ u ] = 0 X[u] = 0 X [ u ] = 0 dim L J ≥ 2 \dim L_J \ge2 dim L J ≥ 2 J ( τ ) = J + τ X J(\tau) = J + \tau X J ( τ ) = J + τ X
I 0 = { τ ∈ R : J ( τ ) ∈ R } . I_0 = \{\tau\in\mathbb{R} : J(\tau) \in\mathcal{R}\}. I 0 = { τ ∈ R : J ( τ ) ∈ R } . I 0 I_0 I 0 ± X ∈ C J \pm X \in C_J ± X ∈ C J I 0 ≠ R I_0 \ne\mathbb{R} I 0 = R X [ k ] = 0 X[k] = 0 X [ k ] = 0 k ∈ Min ( J ) k \in\operatorname{Min}(J) k ∈ Min ( J ) J ( τ ) [ k ] = 4 J(\tau)[k] = 4 J ( τ ) [ k ] = 4 k k k
Min ( J ) ⊆ Min ( J ( τ ) ) and L J ( τ ) ⊆ L J ( τ ∈ I 0 ) . (2) \operatorname{Min}(J) \subseteq\operatorname{Min}(J(\tau)) \quad\text{and}\quad L_{J(\tau)} \subseteq L_J \qquad(\tau\in I_0). \tag*{(2)} Min ( J ) ⊆ Min ( J ( τ )) and L J ( τ ) ⊆ L J ( τ ∈ I 0 ) . (2) In case (b), Lemma 2.3(2) gives σ ( J ( τ ) ) ≤ J ( τ ) [ u ] = J [ u ] + τ X [ u ] = 0 \sigma(J(\tau)) \le J(\tau)[u] = J[u] + \tau X[u] = 0 σ ( J ( τ )) ≤ J ( τ ) [ u ] = J [ u ] + τ X [ u ] = 0 τ ∈ I 0 \tau\in I_0 τ ∈ I 0 I = I 0 I = I_0 I = I 0 τ ↦ σ ( J ( τ ) ) \tau\mapsto\sigma(J(\tau)) τ ↦ σ ( J ( τ )) I 0 I_0 I 0 I I I { τ ∈ I 0 : σ ( J ( τ ) ) ≤ 0 } \{\tau\in I_0 : \sigma(J(\tau)) \le0\} { τ ∈ I 0 : σ ( J ( τ )) ≤ 0 } I I I I I I I ≠ R I \ne\mathbb{R} I = R J ( τ ) ∈ S J(\tau) \in\mathcal{S} J ( τ ) ∈ S τ ∈ I \tau\in I τ ∈ I
The function φ ( τ ) = f ( J ( τ ) ) \varphi(\tau) = f(J(\tau)) φ ( τ ) = f ( J ( τ )) I I I Q ( X ) = 0 Q(X) = 0 Q ( X ) = 0 I = [ α , β ] I = [\alpha,\beta] I = [ α , β ] φ ( 0 ) ≥ min ( φ ( α ) , φ ( β ) ) \varphi(0) \ge\min(\varphi(\alpha),\varphi(\beta)) φ ( 0 ) ≥ min ( φ ( α ) , φ ( β )) I = [ α , ∞ ) I = [\alpha,\infty) I = [ α , ∞ ) φ \varphi φ − ∞ -\infty − ∞ φ ( α ) ≤ φ ( 0 ) \varphi(\alpha) \le\varphi(0) φ ( α ) ≤ φ ( 0 ) I = ( − ∞ , β ] I = (-\infty,\beta] I = ( − ∞ , β ] τ 0 \tau_0 τ 0 I I I φ ( τ 0 ) ≤ φ ( 0 ) \varphi(\tau_0) \le\varphi(0) φ ( τ 0 ) ≤ φ ( 0 ) J 1 = J ( τ 0 ) J_1 = J(\tau_0) J 1 = J ( τ 0 ) J 1 ∈ S J_1 \in\mathcal{S} J 1 ∈ S f ( J 1 ) ≤ f ( J ) f(J_1) \le f(J) f ( J 1 ) ≤ f ( J )
If τ 0 \tau_0 τ 0 I 0 I_0 I 0 X ∉ L J 1 X \notin L_{J_1} X ∈ / L J 1 J 1 ± η X ∈ R J_1 \pm\eta X \in\mathcal{R} J 1 ± η X ∈ R η > 0 \eta> 0 η > 0 d ( J 1 ) ≤ d ( J ) − 1 d(J_1) \le d(J)-1 d ( J 1 ) ≤ d ( J ) − 1 π ( J 1 ) ≤ 2 d ( J ) − 1 < π ( J ) \pi(J_1) \le2d(J)-1 < \pi(J) π ( J 1 ) ≤ 2 d ( J ) − 1 < π ( J ) τ 0 \tau_0 τ 0 I 0 I_0 I 0 σ ( J 1 ) = 0 \sigma(J_1) = 0 σ ( J 1 ) = 0 I I I π ( J 1 ) = 2 d ( J 1 ) ≤ 2 d ( J ) < π ( J ) \pi(J_1) = 2d(J_1) \le2d(J) < \pi(J) π ( J 1 ) = 2 d ( J 1 ) ≤ 2 d ( J ) < π ( J )
The vertices and edges of R \mathcal{R} R
Definition 4.1. For u ∈ Z 5 u \in\mathbb{Z}^5 u ∈ Z 5 a ∈ Z a \in\mathbb{Z} a ∈ Z p = ( u , − a ) p = (u,-a) p = ( u , − a ) q = ( u , − a − 1 ) ∈ Z 6 q = (u,-a-1) \in\mathbb{Z}^6 q = ( u , − a − 1 ) ∈ Z 6 X u , a = p q T + q p T X_{u,a} = pq^{\mathsf{T}} + qp^{\mathsf{T}} X u , a = p q T + q p T Q ( X u , a ) = 2 u u T Q(X_{u,a}) = 2uu^{\mathsf{T}} Q ( X u , a ) = 2 u u T
X u , a [ ( n , l ) ] = 2 ( u ⋅ n − a l ) ( u ⋅ n − ( a + 1 ) l ) . X_{u,a}[(n,l)] = 2(u \cdot n-al)(u \cdot n-(a+1)l). X u , a [( n , l )] = 2 ( u ⋅ n − a l ) ( u ⋅ n − ( a + 1 ) l ) . Lemma 4.2. X u , a [ k ] ≥ 0 X_{u,a}[k] \ge0 X u , a [ k ] ≥ 0 k ∈ M k \in\mathcal{M} k ∈ M J + t X u , a ∈ R J+tX_{u,a} \in\mathcal{R} J + t X u , a ∈ R J ∈ R J \in\mathcal{R} J ∈ R t ≥ 0 t \ge0 t ≥ 0
det Q ( J + t X u , a ) = det Q ( J ) + 2 t adj ( Q ( J ) ) [ u ] . \det Q(J+tX_{u,a}) = \det Q(J)+2t\operatorname{adj}(Q(J))[u]. det Q ( J + t X u , a ) = det Q ( J ) + 2 t adj ( Q ( J )) [ u ] . Proof. For k = ( n , l ) k = (n,l) k = ( n , l ) u ⋅ n − a l u \cdot n-al u ⋅ n − a l u ⋅ n − ( a + 1 ) l u \cdot n-(a+1)l u ⋅ n − ( a + 1 ) l l ∈ { − 1 , 0 , 1 } l \in\{-1,0,1\} l ∈ { − 1 , 0 , 1 } Q + 2 t u u T Q+2tuu^{\mathsf{T}} Q + 2 t u u T
Proposition 4.3. The matrices J 0 , … , J 33 J_0,\ldots,J_{33} J 0 , … , J 33 R \mathcal{R} R i i i G i G_i G i
Figure 3.1. One step of the proof of Proposition 3.2 in a two-dimensional face F F F R \mathcal{R} R σ ( J ) = 0 \sigma(J)=0 σ ( J ) = 0 F ∩ { σ > 0 } F\cap\{\sigma>0\} F ∩ { σ > 0 } σ \sigma σ J J J X X X X [ u ] = 0 X[u]=0 X [ u ] = 0 σ ≤ 0 \sigma\leq0 σ ≤ 0 log det Q \log\det Q log det Q J 1 J_1 J 1 det Q ( J 1 ) ≤ det Q ( J ) \det Q(J_1)\leq\det Q(J) det Q ( J 1 ) ≤ det Q ( J ) J 1 J_1 J 1 F F F σ = 0 \sigma=0 σ = 0
for every extreme ray Y Y Y C J i C_{J_i} C J i t ∗ ( J i , Y ) < ∞ t^*(J_i,Y)<\infty t ∗ ( J i , Y ) < ∞ J i + t ∗ Y J_i+t^*Y J i + t ∗ Y J j J_j J j j j j G i G_i G i
for every extreme ray Y Y Y C J i C_{J_i} C J i t ≥ 0 t\geq0 t ≥ 0 t ≤ t ∗ ( J i , Y ) t\leq t^*(J_i,Y) t ≤ t ∗ ( J i , Y ) det ( J i + t Y ) > 0 \det(J_i+tY)>0 det ( J i + t Y ) > 0 det Q ( J i + t Y ) ≥ 512 \det Q(J_i+tY)\geq512 det Q ( J i + t Y ) ≥ 512 det ( J i + t Y ) = 0 \det(J_i+tY)=0 det ( J i + t Y ) = 0 det Q ( J i + t Y ) = 512 \det Q(J_i+tY)=512 det Q ( J i + t Y ) = 512 J i + t Y J_i+tY J i + t Y E 0 , … , E 4 E_0,\ldots,E_4 E 0 , … , E 4 Proposition 4.5 ;
every extreme ray Y Y Y C J i C_{J_i} C J i t ∗ ( J i , Y ) = ∞ t^*(J_i,Y)=\infty t ∗ ( J i , Y ) = ∞ X u , a X_{u,a} X u , a u ∈ Z 5 u\in\mathbb{Z}^5 u ∈ Z 5 a ∈ { − 2 , − 1 , 0 } a\in\{-2,-1,0\} a ∈ { − 2 , − 1 , 0 } G i G_i G i Table 4.2 .
Table 4.2. The unbounded edges J i + t X u , a J_i+tX_{u,a} J i + t X u , a t ≥ 0 t\geq0 t ≥ 0 G i G_i G i N N N N N N t 0 t_0 t 0 det ( J i + t X u , a ) \det(J_i+tX_{u,a}) det ( J i + t X u , a ) det Q \det Q det Q det Q \det Q det Q Lemma 4.2 ); 320 + 128 6 ≈ 633.5 320+128\sqrt{6}\approx633.5 320 + 128 6 ≈ 633.5 342 + 108 10 ≈ 683.5 342+108\sqrt{10}\approx683.5 342 + 108 10 ≈ 683.5 378 + 216 3 ≈ 752.1 378+216\sqrt{3}\approx752.1 378 + 216 3 ≈ 752.1
Proof. This is a finite computation in exact integer and rational arithmetic, described in Appendix B. The certificate lists, for each i i i J i J_i J i G i G_i G i C J i C_{J_i} C J i Y Y Y G i G_i G i t ∗ t^* t ∗ j j j T ∈ Γ T\in\Gamma T ∈ Γ T T J j T = J i + t ∗ Y T^{\mathsf{T}}J_jT=J_i+t^*Y T T J j T = J i + t ∗ Y ( u , a ) (u,a) ( u , a ) g Y g T gYg^{\mathsf{T}} g Y g T g ∈ G i g\in G_i g ∈ G i J i J_i J i Y Y Y J ↦ g T J g J\mapsto g^{\mathsf{T}}Jg J ↦ g T J g § 2.3 ), so the statements for the listed rays imply them for all rays. Statement (2) is decided on each listed edge from the polynomials det ( J i + t Y ) \det(J_i+tY) det ( J i + t Y ) det Q ( J i + t Y ) \det Q(J_i+tY) det Q ( J i + t Y ) □ \square □
By Corollary 2.12 and Proposition 4.3 (1), every vertex of R \mathcal{R} R J i J_i J i R \mathcal{R} R J i J_i J i
Remark 4.4. The concavity of σ \sigma σ Lemma 2.3 (2)) locates the points of C C C Table 4.1 , σ ( J i ) \sigma(J_i) σ ( J i ) i = 1 , 2 i=1,2 i = 1 , 2 i = 0 i=0 i = 0 σ ≥ 0 \sigma\geq0 σ ≥ 0 σ \sigma σ C C C J 1 J_1 J 1 J 2 J_2 J 2 det J = 16 t ( t − 4 ) ( t − 2 ) ( t + 2 ) \det J=16t(t-4)(t-2)(t+2) det J = 16 t ( t − 4 ) ( t − 2 ) ( t + 2 ) t ∗ = 2 t^*=2 t ∗ = 2 det J ≡ 0 \det J\equiv0 det J ≡ 0 det Q = 512 ( 1 + τ − τ 2 ) \det Q=512(1+\tau-\tau^2) det Q = 512 ( 1 + τ − τ 2 ) τ = t / t ∗ \tau=t/t^* τ = t / t ∗ [1 §4.3] contained in the set of packings, with det Q > 512 \det Q>512 det Q > 512 J 1 J_1 J 1 J 2 J_2 J 2 det J \det J det J det Q \det Q det Q J 1 J_1 J 1 J 2 J_2 J 2 det J < 0 \det J<0 det J < 0 Proposition 4.3 (2) records these facts; they are not used separately.
Table 4.1. The 34 vertices J i J_i J i R \mathcal{R} R ∣ Min ∣ |\operatorname{Min}| ∣ Min ∣ ± k \pm k ± k C J i C_{J_i} C J i G i ⊆ Γ J i G_i \subseteq\Gamma_{J_i} G i ⊆ Γ J i J i J_i J i ( det Q , det J ) (\det Q,\det J) ( det Q , det J ) J i J_i J i
Proposition 4.5. Let
E 0 = J 0 , E 1 = J 3 + 5 6 X e 1 , − 1 , E 2 = J 5 + 3 X e 5 , 0 , E 3 = J 7 + 2 X e 5 , 0 , E 4 = J 8 + 2 X e 1 , − 1 . E_0=J_0,\quad E_1=J_3+\frac{5}{6}X_{e_1,-1},\quad E_2=J_5+3X_{e_5,0},\quad E_3=J_7+2X_{e_5,0},\quad E_4=J_8+2X_{e_1,-1}. E 0 = J 0 , E 1 = J 3 + 6 5 X e 1 , − 1 , E 2 = J 5 + 3 X e 5 , 0 , E 3 = J 7 + 2 X e 5 , 0 , E 4 = J 8 + 2 X e 1 , − 1 . Every J ∈ C J\in C J ∈ C det Q ( J ) ≥ 512 \det Q(J)\ge512 det Q ( J ) ≥ 512 J J J E 0 , … , E 4 E_0,\ldots,E_4 E 0 , … , E 4
Proof. Let J ∈ C J\in C J ∈ C d ( J ) = 0 d(J)=0 d ( J ) = 0 J J J J i J_i J i σ ( J i ) ≤ 0 \sigma(J_i)\le0 σ ( J i ) ≤ 0 det J i ≤ 0 \det J_i\le0 det J i ≤ 0 Table 4.1 , i ∈ { 0 , 1 , 2 } i\in\{0,1,2\} i ∈ { 0 , 1 , 2 } det Q ( J ) ∈ { 512 , 1024 , 768 } \det Q(J)\in\{512,1024,768\} det Q ( J ) ∈ { 512 , 1024 , 768 } J 0 = E 0 J_0=E_0 J 0 = E 0
If d ( J ) = 1 d(J)=1 d ( J ) = 1 σ ( J ) = 0 \sigma(J)=0 σ ( J ) = 0 Lemma 2.9 (3) places J J J Γ \Gamma Γ J = J i + t Y J=J_i+tY J = J i + t Y Y Y Y C J i C_{J_i} C J i 0 < t < t ∗ ( J i , Y ) 0<t<t^*(J_i,Y) 0 < t < t ∗ ( J i , Y ) det J = det Q ( J ) σ ( J ) = 0 \det J=\det Q(J)\sigma(J)=0 det J = det Q ( J ) σ ( J ) = 0 Proposition 4.3 (2) gives det Q ( J ) ≥ 512 \det Q(J)\ge512 det Q ( J ) ≥ 512 J J J E m E_m E m
Conversely, E 0 = J 0 E_0=J_0 E 0 = J 0 det J 0 = 0 \det J_0=0 det J 0 = 0 det Q ( J 0 ) = 512 \det Q(J_0)=512 det Q ( J 0 ) = 512 m ≥ 1 m\geq1 m ≥ 1 E m E_m E m t 0 t_0 t 0 Table 4.2 with det Q ( t 0 ) = 512 \det Q(t_0)=512 det Q ( t 0 ) = 512 d ( E m ) = 1 d(E_m)=1 d ( E m ) = 1 Lemma 2.9 (2), and σ ( E m ) = det E m / det Q ( E m ) = 0. □ \sigma(E_m)=\det E_m/\det Q(E_m)=0. \square σ ( E m ) = det E m / det Q ( E m ) = 0. □
Corollary 4.6. det Q ( J ) ≥ 512 \det Q(J)\geq512 det Q ( J ) ≥ 512 J ∈ S J\in S J ∈ S
Proof. Propositions 3.2 and 4.5. □ \square □
The equality case
Lemma 5.1. Let Λ ⊂ R n \Lambda\subset\mathbb{R}^n Λ ⊂ R n ρ = max z ∈ R n dist ( z , Λ ) \rho=\max_{z\in\mathbb{R}^n}\operatorname{dist}(z,\Lambda) ρ = max z ∈ R n dist ( z , Λ ) c ∈ R n c\in\mathbb{R}^n c ∈ R n dist ( c , Λ ) = ρ \operatorname{dist}(c,\Lambda)=\rho dist ( c , Λ ) = ρ N ( c ) = { v ∈ Λ : ∣ v − c ∣ = ρ } N(c)=\{v\in\Lambda:|v-c|=\rho\} N ( c ) = { v ∈ Λ : ∣ v − c ∣ = ρ }
Figure 5.1. Lemma 5.1 in the plane. Left: a deep hole c c c ρ \rho ρ c c c N ( c ) N(c) N ( c ) N ( c ) N(c) N ( c ) H H H c c c H H H ε w \varepsilon w εw N ( c ) N(c) N ( c ) ρ \rho ρ
Proof. The maximum exists because z ↦ dist ( z , Λ ) z \mapsto\operatorname{dist}(z,\Lambda) z ↦ dist ( z , Λ ) Λ \Lambda Λ N ( c ) N(c) N ( c ) Λ \Lambda Λ δ > 0 \delta> 0 δ > 0 ∣ v − c ∣ ≥ ρ + δ \lvert v-c\rvert\ge\rho+\delta ∣ v − c ∣ ≥ ρ + δ v ∈ Λ ∖ N ( c ) v \in\Lambda\setminus N(c) v ∈ Λ ∖ N ( c ) ⟨ v , z ⟩ = α \langle v,z\rangle= \alpha ⟨ v , z ⟩ = α v ∈ N ( c ) v \in N(c) v ∈ N ( c ) ∣ z ∣ = 1 \lvert z\rvert= 1 ∣ z ∣ = 1 β = α − ⟨ c , z ⟩ \beta= \alpha-\langle c,z\rangle β = α − ⟨ c , z ⟩ ⟨ v − c , z ⟩ = β \langle v-c,z\rangle= \beta ⟨ v − c , z ⟩ = β N ( c ) N(c) N ( c ) w = − z w=-z w = − z β > 0 \beta>0 β > 0 w = z w=z w = z 0 < ε < δ 0<\varepsilon<\delta 0 < ε < δ v ∈ N ( c ) v \in N(c) v ∈ N ( c )
∣ v − c − ε w ∣ 2 = ρ 2 − 2 ε ⟨ v − c , w ⟩ + ε 2 = ρ 2 + 2 ε ∣ β ∣ + ε 2 > ρ 2 \lvert v-c-\varepsilon w\rvert^2=\rho^2-2\varepsilon\langle v-c,w\rangle+\varepsilon^2=\rho^2+2\varepsilon\lvert\beta\rvert+\varepsilon^2>\rho^2 ∣ v − c − εw ∣ 2 = ρ 2 − 2 ε ⟨ v − c , w ⟩ + ε 2 = ρ 2 + 2 ε ∣ β ∣ + ε 2 > ρ 2 and for v ∈ Λ ∖ N ( c ) v \in\Lambda\setminus N(c) v ∈ Λ ∖ N ( c ) ∣ v − c − ε w ∣ ≥ ρ + δ − ε > ρ \lvert v-c-\varepsilon w\rvert\ge\rho+\delta-\varepsilon>\rho ∣ v − c − εw ∣ ≥ ρ + δ − ε > ρ dist ( c + ε w , Λ ) > ρ \operatorname{dist}(c+\varepsilon w,\Lambda)>\rho dist ( c + εw , Λ ) > ρ ρ \rho ρ
A point c c c dist ( c , Λ ) = ρ \operatorname{dist}(c,\Lambda)=\rho dist ( c , Λ ) = ρ deep hole of Λ \Lambda Λ
Lemma 5.2. Let J ∈ Sym 6 + J \in\operatorname{Sym}^{+}_{6} J ∈ Sym 6 + A A A 5 × 5 5 \times5 5 × 5 A T A = Q ( J ) A^{\mathsf T}A=Q(J) A T A = Q ( J ) Λ = A Z 5 \Lambda= A\mathbb{Z}^{5} Λ = A Z 5 c = − A q ( J ) c=-Aq(J) c = − A q ( J ) J [ ( n , 0 ) ] = ∣ A n ∣ 2 J[(n,0)]=\lvert An\rvert^2 J [( n , 0 )] = ∣ A n ∣ 2 J [ ( n , 1 ) ] = ∣ A n − c ∣ 2 + σ ( J ) J[(n,1)]=\lvert An-c\rvert^2+\sigma(J) J [( n , 1 )] = ∣ A n − c ∣ 2 + σ ( J ) n ∈ Z 5 n \in\mathbb{Z}^{5} n ∈ Z 5 J ∈ R J \in\mathcal{R} J ∈ R ∣ v ∣ ≥ 2 \lvert v\rvert\ge2 ∣ v ∣ ≥ 2 v ∈ Λ ∖ 0 v \in\Lambda\setminus0 v ∈ Λ ∖ 0 dist ( c , Λ ) 2 ≥ 4 − σ ( J ) \operatorname{dist}(c,\Lambda)^2\ge4-\sigma(J) dist ( c , Λ ) 2 ≥ 4 − σ ( J ) J ∈ R J \in\mathcal{R} J ∈ R ( n , 1 ) ∈ Min ( J ) (n,1)\in\operatorname{Min}(J) ( n , 1 ) ∈ Min ( J ) ∣ A n − c ∣ 2 = 4 − σ ( J ) \lvert An-c\rvert^2=4-\sigma(J) ∣ A n − c ∣ 2 = 4 − σ ( J )
Proof. By Lemma 2.3 (1), J [ ( n , l ) ] = ∣ A ( n + l q ( J ) ) ∣ 2 + l 2 σ ( J ) = ∣ A n − l c ∣ 2 + l 2 σ ( J ) J[(n,l)]=\lvert A(n+lq(J))\rvert^2+l^2\sigma(J)=\lvert An-lc\rvert^2+l^2\sigma(J) J [( n , l )] = ∣ A ( n + l q ( J )) ∣ 2 + l 2 σ ( J ) = ∣ A n − l c ∣ 2 + l 2 σ ( J ) ( n , − 1 ) (n,-1) ( n , − 1 ) ( − n , 1 ) (-n,1) ( − n , 1 )
Proposition 5.3. Let J ∈ S J \in\mathcal{S} J ∈ S det Q ( J ) = 512 \det Q(J)=512 det Q ( J ) = 512 σ ( J ) = 0 \sigma(J)=0 σ ( J ) = 0 d ( J ) ≤ 1 d(J)\le1 d ( J ) ≤ 1 J ∈ C J \in\mathcal{C} J ∈ C J J J E 0 , … , E 4 E_0,\ldots,E_4 E 0 , … , E 4
Proof. We first record two consequences of Corollary 4.6 for any J ′ ∈ S J' \in\mathcal{S} J ′ ∈ S det Q ( J ′ ) = 512 \det Q(J')=512 det Q ( J ′ ) = 512 X ∈ L J ′ X \in L_{J'} X ∈ L J ′ σ ( J ′ ) < 0 \sigma(J')<0 σ ( J ′ ) < 0 X [ u ′ ] = 0 X[u']=0 X [ u ′ ] = 0 u ′ = ( − q ( J ′ ) , 1 ) u'=(-q(J'),1) u ′ = ( − q ( J ′ ) , 1 )
(a) Q ( X ) = 0 Q(X)=0 Q ( X ) = 0
(b) writing X = ( 0 x x T y ) X=\begin{pmatrix}0 & x \\ x^{\mathsf T} & y\end{pmatrix} X = ( 0 x T x y ) 2 x ⋅ n + y = 0 2x\cdot n+y=0 2 x ⋅ n + y = 0 ( n , 1 ) ∈ Min ( J ′ ) (n,1)\in\operatorname{Min}(J') ( n , 1 ) ∈ Min ( J ′ )
For (a): J ′ + τ X ∈ R J'+\tau X\in\mathcal{R} J ′ + τ X ∈ R ∣ τ ∣ \lvert\tau\rvert ∣ τ ∣ Lemma 2.6 (2), since ± X ∈ C J ′ \pm X\in C_{J'} ± X ∈ C J ′ σ ( J ′ ) < 0 \sigma(J')<0 σ ( J ′ ) < 0 σ ( J ′ + τ X ) < 0 \sigma(J'+\tau X)<0 σ ( J ′ + τ X ) < 0 ∣ τ ∣ \lvert\tau\rvert ∣ τ ∣ X [ u ′ ] = 0 X[u']=0 X [ u ′ ] = 0
{#eq:5.1}
caption: Bases of Λ m \Lambda_m Λ m b ≡ b m ( m o d Λ m ) b \equiv b_m \pmod{\Lambda_m} b ≡ b m ( mod Λ m ) 2 ( a 1 , … , a 5 , b ) \sqrt{2}(a_1,\ldots,a_5,b) 2 ( a 1 , … , a 5 , b ) E m E_m E m k ˉ = − k \bar{k}=-k k ˉ = − k
:::
σ ( J ′ ) ≤ 0 \sigma(J') \le0 σ ( J ′ ) ≤ 0 J ′ + τ X ∈ S J' + \tau X \in S J ′ + τ X ∈ S 0 0 0 φ ( τ ) = log det Q ( J ′ + τ X ) \varphi(\tau)=\log\det Q(J'+\tau X) φ ( τ ) = log det Q ( J ′ + τ X ) log 512 \log512 log 512 log 512 \log512 log 512 τ = 0 \tau=0 τ = 0 Q ( X ) = 0 Q(X)=0 Q ( X ) = 0 Q ( X ) = 0 Q(X)=0 Q ( X ) = 0 X [ ( n , 1 ) ] = 2 x ⋅ n + y X[(n,1)]=2x\cdot n+y X [( n , 1 )] = 2 x ⋅ n + y Min ( J ′ ) \operatorname{Min}(J') Min ( J ′ ) X ∈ L J ′ X\in L_{J'} X ∈ L J ′
Now let J J J A A A Λ \Lambda Λ c c c ρ \rho ρ Λ \Lambda Λ J ∈ R J\in\mathcal{R} J ∈ R σ ( J ) ≤ 0 \sigma(J)\le0 σ ( J ) ≤ 0 ρ 2 ≥ dist ( c , Λ ) 2 ≥ 4 − σ ( J ) ≥ 4 \rho^2\ge\operatorname{dist}(c,\Lambda)^2\ge4-\sigma(J)\ge4 ρ 2 ≥ dist ( c , Λ ) 2 ≥ 4 − σ ( J ) ≥ 4
Suppose ρ > 2 \rho>2 ρ > 2 c ′ c' c ′ Λ \Lambda Λ q ′ = − A − 1 c ′ q'=-A^{-1}c' q ′ = − A − 1 c ′ σ ′ = 4 − ρ 2 < 0 \sigma'=4-\rho^2<0 σ ′ = 4 − ρ 2 < 0
J ′ = ( Q Q q ′ q ′ T Q σ ′ + Q [ q ′ ] ) , Q = Q ( J ) . J'=\begin{pmatrix} Q & Qq' \\ {q'}^{T}Q & \sigma'+Q[{q'}] \end{pmatrix},\qquad Q=Q(J). J ′ = ( Q q ′ T Q Q q ′ σ ′ + Q [ q ′ ] ) , Q = Q ( J ) . Then Q ( J ′ ) = Q Q(J')=Q Q ( J ′ ) = Q q ( J ′ ) = q ′ q(J')=q' q ( J ′ ) = q ′ σ ( J ′ ) = σ ′ \sigma(J')=\sigma' σ ( J ′ ) = σ ′ J ′ ∈ R J'\in\mathcal{R} J ′ ∈ R Λ \Lambda Λ 2 2 2 dist ( c ′ , Λ ) 2 = ρ 2 = 4 − σ ′ \operatorname{dist}(c',\Lambda)^2=\rho^2=4-\sigma' dist ( c ′ , Λ ) 2 = ρ 2 = 4 − σ ′ ( n , 1 ) ∈ Min ( J ′ ) (n,1)\in\operatorname{Min}(J') ( n , 1 ) ∈ Min ( J ′ ) A n ∈ N ( c ′ ) An\in N(c') A n ∈ N ( c ′ ) J ′ ∈ S J'\in S J ′ ∈ S det Q ( J ′ ) = 512 \det Q(J')=512 det Q ( J ′ ) = 512 X ∈ L J ′ X\in L_{J'} X ∈ L J ′ σ ( J ′ ) < 0 \sigma(J')<0 σ ( J ′ ) < 0 Q ( X ) = 0 Q(X)=0 Q ( X ) = 0 v ↦ 2 x ⋅ A − 1 v + y v\mapsto2x\cdot A^{-1}v+y v ↦ 2 x ⋅ A − 1 v + y N ( c ′ ) N(c') N ( c ′ ) N ( c ′ ) N(c') N ( c ′ ) x = 0 x=0 x = 0 y = 0 y=0 y = 0 X = 0 X=0 X = 0 d ( J ′ ) = 0 d(J')=0 d ( J ′ ) = 0 J ′ J' J ′ det J ′ = 512 σ ′ < 0 \det J'=512\sigma'<0 det J ′ = 512 σ ′ < 0 J 1 J_1 J 1 J 2 J_2 J 2 J i J_i J i det J i < 0 \det J_i<0 det J i < 0 det Q ( J 1 ) = 1024 \det Q(J_1)=1024 det Q ( J 1 ) = 1024 det Q ( J 2 ) = 768 \det Q(J_2)=768 det Q ( J 2 ) = 768 ρ = 2 \rho=2 ρ = 2
Then 4 ≥ dist ( c , Λ ) 2 ≥ 4 − σ ( J ) 4\ge\operatorname{dist}(c,\Lambda)^2\ge4-\sigma(J) 4 ≥ dist ( c , Λ ) 2 ≥ 4 − σ ( J ) σ ( J ) = 0 \sigma(J)=0 σ ( J ) = 0 dist ( c , Λ ) = 2 = ρ \operatorname{dist}(c,\Lambda)=2=\rho dist ( c , Λ ) = 2 = ρ c c c Λ \Lambda Λ ( n , 1 ) ∈ Min ( J ) (n,1)\in\operatorname{Min}(J) ( n , 1 ) ∈ Min ( J ) A n ∈ N ( c ) An\in N(c) A n ∈ N ( c ) u = ( − q ( J ) , 1 ) u=(-q(J),1) u = ( − q ( J ) , 1 ) X ∈ L J X\in L_J X ∈ L J X [ u ] = 0 X[u]=0 X [ u ] = 0 Q ( X ) = 0 Q(X)=0 Q ( X ) = 0 v ↦ 2 x ⋅ A − 1 v + y v\mapsto2x\cdot A^{-1}v+y v ↦ 2 x ⋅ A − 1 v + y N ( c ) N(c) N ( c ) X = 0 X=0 X = 0 L J → R L_J\to\mathbb{R} L J → R X ↦ X [ u ] X\mapsto X[u] X ↦ X [ u ] d ( J ) ≤ 1 d(J)\le1 d ( J ) ≤ 1 J ∈ C J\in\mathcal{C} J ∈ C
The five extremal configurations
Lemma 6.1. For each m m m a 1 , … , a 5 a_1,\ldots,a_5 a 1 , … , a 5 Λ m \Lambda_m Λ m b b b b − b m ∈ Λ m b-b_m\in\Lambda_m b − b m ∈ Λ m 2 a 1 , … , 2 a 5 , 2 b \sqrt{2}a_1,\ldots,\sqrt{2}a_5,\sqrt{2}b 2 a 1 , … , 2 a 5 , 2 b E m E_m E m Λ m \Lambda_m Λ m 4 4 4 2 2 2 ∣ Min Λ m ∣ |\operatorname{Min}\Lambda_m| ∣ Min Λ m ∣
Proof. Λ 0 \Lambda_0 Λ 0 Λ 3 \Lambda_3 Λ 3 Λ 4 \Lambda_4 Λ 4 4 4 4 Z 5 \mathbb{Z}^5 Z 5 Λ 1 \Lambda_1 Λ 1 A 4 A_4 A 4 5 5 5 Z 1 5 1 \mathbb{Z}_{\frac{1}{5}}1 Z 5 1 1 16 5 \frac{16}{5} 5 16 Λ 2 \Lambda_2 Λ 2 x 5 = 2 j x_5=2j x 5 = 2 j D 4 D_4 D 4 2 2 2 2 2 2 4 4 4 a i a_i a i Λ m \Lambda_m Λ m ∣ det ( a 1 , … , a 5 ) ∣ = 4 \lvert\det(a_1,\ldots,a_5)\rvert=4 ∣ det ( a 1 , … , a 5 )∣ = 4 b − b m ∈ Λ m b-b_m\in\Lambda_m b − b m ∈ Λ m 4 ⋅ 3 + 4 ⋅ 1 = 16 4\cdot3+4\cdot1=16 4 ⋅ 3 + 4 ⋅ 1 = 16 ± e i ± e j \pm e_i\pm e_j ± e i ± e j D 3 ⊕ D 2 D_3\oplus D_2 D 3 ⊕ D 2 20 20 20 A 4 A_4 A 4 Λ 1 \Lambda_1 Λ 1 16 5 \frac{16}{5} 5 16 24 24 24 D 4 × 0 D_4\times0 D 4 × 0 Λ 2 \Lambda_2 Λ 2 x 5 = 2 j ≠ 0 x_5=2j\ne0 x 5 = 2 j = 0 1 + 4 = 5 1+4=5 1 + 4 = 5 24 24 24 D 4 × 0 D_4\times0 D 4 × 0 Λ 3 \Lambda_3 Λ 3 20 20 20 e i − e j e_i-e_j e i − e j Λ 4 \Lambda_4 Λ 4
Lemma 6.2. (1) P 0 = P 3 = P 4 = D 5 P_0=P_3=P_4=D_5 P 0 = P 3 = P 4 = D 5
(2) For m = 1 , 2 m=1,2 m = 1 , 2 2 b m ∉ Λ m 2b_m\notin\Lambda_m 2 b m ∈ / Λ m P m P_m P m { y : P m + y = P m } \{y:P_m+y=P_m\} { y : P m + y = P m } Λ m \Lambda_m Λ m
(3) The five pairs ( Λ m , b m ) (\Lambda_m,b_m) ( Λ m , b m ) P 1 P_1 P 1 P 2 P_2 P 2 D 5 D_5 D 5
Proof. (1) Λ m ⊂ D 5 \Lambda_m\subset D_5 Λ m ⊂ D 5 m = 0 , 3 , 4 m=0,3,4 m = 0 , 3 , 4 covol ( D 5 ) = 2 \operatorname{covol}(D_5)=2 covol ( D 5 ) = 2 b m ∈ D 5 ∖ Λ m b_m\in D_5\setminus\Lambda_m b m ∈ D 5 ∖ Λ m P m P_m P m Λ m \Lambda_m Λ m D 5 D_5 D 5 2 b 1 = 2 e 1 + 2 e 5 2b_1=2e_1+2e_5 2 b 1 = 2 e 1 + 2 e 5 1 \mathbf{1} 1 4 5 1 \frac{4}{5}\mathbf{1} 5 4 1 2 b 1 − 4 5 1 = 2 5 ( 3 , − 2 , − 2 , − 2 , 3 ) ∉ Z 5 2b_1-\frac{4}{5}\mathbf{1}=\frac{2}{5}(3,-2,-2,-2,3)\notin\mathbb{Z}^5 2 b 1 − 5 4 1 = 5 2 ( 3 , − 2 , − 2 , − 2 , 3 ) ∈ / Z 5 2 b 1 ∉ Λ 1 2b_1\notin\Lambda_1 2 b 1 ∈ / Λ 1 2 b 2 = 2 e 1 + 2 e 5 2b_2=2e_1+2e_5 2 b 2 = 2 e 1 + 2 e 5 x 5 = 2 x_5=2 x 5 = 2 Λ 2 \Lambda_2 Λ 2 x 5 = 2 x_5=2 x 5 = 2 ( D 4 + h ) × { 2 } (D_4+h)\times\{2\} ( D 4 + h ) × { 2 } 2 e 1 2e_1 2 e 1 y y y P = Λ ∪ ( Λ + b ) P=\Lambda\cup(\Lambda+b) P = Λ ∪ ( Λ + b ) b ∉ Λ b\notin\Lambda b ∈ / Λ 2 b ∉ Λ 2b\notin\Lambda 2 b ∈ / Λ y = 0 + y ∈ P y=0+y\in P y = 0 + y ∈ P y ∈ Λ + b y\in\Lambda+b y ∈ Λ + b y + b ∈ Λ + 2 b y+b\in\Lambda+2b y + b ∈ Λ + 2 b Λ \Lambda Λ Λ + b \Lambda+b Λ + b y ∈ Λ y\in\Lambda y ∈ Λ y ∈ Λ y\in\Lambda y ∈ Λ P ≠ Λ P\ne\Lambda P = Λ P P P Λ \Lambda Λ Λ ′ \Lambda' Λ ′ ∣ Min Λ ∣ |\operatorname{Min}\Lambda| ∣ Min Λ∣ 2 b ∈ Λ 2b\in\Lambda 2 b ∈ Λ ( ∣ Min Λ m ∣ , [ 2 b m ∈ Λ m ] ) (|\operatorname{Min}\Lambda_m|,[2b_m\in\Lambda_m]) ( ∣ Min Λ m ∣ , [ 2 b m ∈ Λ m ]) ( 16 , 1 ) (16,1) ( 16 , 1 ) ( 20 , 0 ) (20,0) ( 20 , 0 ) ( 24 , 0 ) (24,0) ( 24 , 0 ) ( 24 , 1 ) (24,1) ( 24 , 1 ) ( 20 , 1 ) (20,1) ( 20 , 1 ) D 5 D_5 D 5 P 1 , P 2 P_1,P_2 P 1 , P 2 P 1 → P 2 P_1\to P_2 P 1 → P 2 Λ 1 \Lambda_1 Λ 1 Λ 2 \Lambda_2 Λ 2
Remark 6.3. (1) Every splitting of D 5 D_5 D 5 D 5 D_5 D 5 D 5 → Z / 2 D_5\to\mathbb{Z}/2 D 5 → Z /2 x ↦ x i x\mapsto x_i x ↦ x i x ↦ x i + x j x\mapsto x_i+x_j x ↦ x i + x j x ↦ 1 2 ∑ i ε i x i x\mapsto\frac{1}{2}\sum_i\varepsilon_i x_i x ↦ 2 1 ∑ i ε i x i ε ∈ { ± 1 } 5 \varepsilon\in\{\pm1\}^5 ε ∈ { ± 1 } 5 Λ 3 \Lambda_3 Λ 3 Λ 0 \Lambda_0 Λ 0 Λ 4 \Lambda_4 Λ 4
(2) Translations by Λ \Lambda Λ x ↦ b − x x\mapsto b-x x ↦ b − x P = Λ ∪ ( Λ + b ) P=\Lambda\cup(\Lambda+b) P = Λ ∪ ( Λ + b ) P P P P 1 P_1 P 1 P 2 P_2 P 2 2 \sqrt{2} 2 x ↦ − ( x 4 , x 2 , x 3 , x 1 , x 5 ) x\mapsto-(x_4,x_2,x_3,x_1,x_5) x ↦ − ( x 4 , x 2 , x 3 , x 1 , x 5 ) Λ 1 \Lambda_1 Λ 1 b 1 b_1 b 1 − e 4 − e 5 -e_4-e_5 − e 4 − e 5 P 1 P_1 P 1 e 1 − e 2 , … , e 4 − e 5 , 4 5 1 e_1-e_2,\ldots,e_4-e_5,\frac{4}{5}\mathbf{1} e 1 − e 2 , … , e 4 − e 5 , 5 4 1 0 , ( 0 , 0 , 0 , − 1 , − 1 ) 0,(0,0,0,-1,-1) 0 , ( 0 , 0 , 0 , − 1 , − 1 ) [6 Table 4.2] : the uniform packing with kissing configuration Q 5 Q_5 Q 5 J 5 , 5 J_{5,5} J 5 , 5 [1 ] [6 §1] .
(3) P 2 = ⋃ i ∈ Z ( D 4 + c i ) × { i } P_2=\bigcup_{i\in\mathbb{Z}}(D_4+c_i)\times\{i\} P 2 = ⋃ i ∈ Z ( D 4 + c i ) × { i } c i = 0 , e 1 , h , e 1 + h c_i=0,e_1,h,e_1+h c i = 0 , e 1 , h , e 1 + h i ≡ 0 , 1 , 2 , 3 ( m o d 4 ) i\equiv0,1,2,3\pmod4 i ≡ 0 , 1 , 2 , 3 ( mod 4 ) D 4 D_4 D 4 i = 0 i=0 i = 0 ( ± e k , 1 ) (\pm e_k,1) ( ± e k , 1 ) 1 ≤ k ≤ 4 1\le k\le4 1 ≤ k ≤ 4 ( 1 2 ( ± 1 , ± 1 , ± 1 , ± 1 ) , − 1 ) (\frac{1}{2}(\pm1,\pm1,\pm1,\pm1),-1) ( 2 1 ( ± 1 , ± 1 , ± 1 , ± 1 ) , − 1 ) L 5 L_5 L 5 [12 ] , as described in [6 §2] , reflected in the hyperplane x 5 = 0 x_5=0 x 5 = 0 Lemma 6.2 (2), P 2 P_2 P 2 [6 ] , so by [6 Theorem 4.3] and [7 §5] , 2 P 2 \sqrt{2}P_2 2 P 2
Proofs of Theorem 1.1 and Corollary 1.2
Proof of Theorem 1.1. Let Λ \Lambda Λ b b b a a a Λ \Lambda Λ J = J ( a , b ) J=J(a,b) J = J ( a , b ) 2.4 , J ∈ R J\in\mathcal{R} J ∈ R σ ( J ) = 0 \sigma(J)=0 σ ( J ) = 0 J ∈ S J\in\mathcal{S} J ∈ S det Q ( J ) = covol ( Λ ) 2 \det Q(J)=\operatorname{covol}(\Lambda)^2 det Q ( J ) = covol ( Λ ) 2 covol ( Λ ) ≥ 512 = 16 2 \operatorname{covol}(\Lambda)\ge\sqrt{512}=16\sqrt{2} covol ( Λ ) ≥ 512 = 16 2
If covol ( Λ ) = 16 2 \operatorname{covol}(\Lambda)=16\sqrt{2} covol ( Λ ) = 16 2 det Q ( J ) = 512 \det Q(J)=512 det Q ( J ) = 512 J J J E m E_m E m Lemma 6.1 , E m = J ( 2 a ( m ) , 2 b ( m ) ) E_m=J(\sqrt{2}a^{(m)},\sqrt{2}b^{(m)}) E m = J ( 2 a ( m ) , 2 b ( m ) ) a ( m ) , b ( m ) a^{(m)},b^{(m)} a ( m ) , b ( m ) a ( m ) a^{(m)} a ( m ) Λ m \Lambda_m Λ m Λ m + b ( m ) = Λ m + b m \Lambda_m+b^{(m)}=\Lambda_m+b_m Λ m + b ( m ) = Λ m + b m Lemma 2.10 , ( Λ , b ) (\Lambda,b) ( Λ , b ) ( 2 Λ m , 2 b m ) (\sqrt{2}\Lambda_m,\sqrt{2}b_m) ( 2 Λ m , 2 b m )
Conversely, E m ∈ C ⊂ R E_m\in\mathcal{C}\subset\mathcal{R} E m ∈ C ⊂ R σ ( E m ) = 0 \sigma(E_m)=0 σ ( E m ) = 0 Proposition 4.5 ), so by Lemmas 2.4 and 6.1 the pair ( 2 Λ m , 2 b m ) (\sqrt{2}\Lambda_m,\sqrt{2}b_m) ( 2 Λ m , 2 b m ) b m ∉ Λ m b_m\notin\Lambda_m b m ∈ / Λ m covol ( 2 Λ m ) 2 = det Q ( E m ) = 512 \operatorname{covol}(\sqrt{2}\Lambda_m)^2=\det Q(E_m)=512 covol ( 2 Λ m ) 2 = det Q ( E m ) = 512 Lemma 6.2 (3).
Finally, P P P Λ \Lambda Λ P P P 2 ⋅ 8 π 2 15 / covol ( Λ ) ≤ π 2 15 2 2 \cdot\frac{8\pi^2}{15}/\operatorname{covol}(\Lambda) \le\frac{\pi^2}{15\sqrt{2}} 2 ⋅ 15 8 π 2 / covol ( Λ ) ≤ 15 2 π 2 ( Λ , b ) (\Lambda,b) ( Λ , b ) ( 2 Λ m , 2 b m ) (\sqrt{2}\Lambda_m,\sqrt{2}b_m) ( 2 Λ m , 2 b m ) P P P 2 P m \sqrt{2}P_m 2 P m Lemma 6.2 , these sets are 2 D 5 \sqrt{2}D_5 2 D 5 2 P 1 \sqrt{2}P_1 2 P 1 2 P 2 \sqrt{2}P_2 2 P 2
Proof of Corollary 1.2. If P = L P=L P = L l 1 , … , l 5 l_1,\ldots,l_5 l 1 , … , l 5 Λ \Lambda Λ 2 l 1 , l 2 , … , l 5 2l_1,l_2,\ldots,l_5 2 l 1 , l 2 , … , l 5 b = l 1 b=l_1 b = l 1 P = Λ ∪ ( Λ + b ) P=\Lambda\cup(\Lambda+b) P = Λ ∪ ( Λ + b ) P = Λ ∪ ( Λ + b ) P=\Lambda\cup(\Lambda+b) P = Λ ∪ ( Λ + b ) b ∉ Λ b\notin\Lambda b ∈ / Λ x ↦ b − x x\mapsto b-x x ↦ b − x P P P Λ \Lambda Λ Λ + b \Lambda+b Λ + b V 0 V_0 V 0 0 0 0 V b V_b V b b b b Λ \Lambda Λ V 0 ∪ V b V_0\cup V_b V 0 ∪ V b Λ \Lambda Λ 1 2 covol ( Λ ) ≥ 8 2 \frac{1}{2}\operatorname{covol}(\Lambda)\ge8\sqrt{2} 2 1 covol ( Λ ) ≥ 8 2 Theorem 1.1 , with equality exactly for the sets listed there. The Voronoi cell of 2 D 5 \sqrt{2}D_5 2 D 5 covol ( 2 D 5 ) = 2 ⋅ 2 5 / 2 = 8 2 \operatorname{covol}(\sqrt{2}D_5)=2\cdot2^{5/2}=8\sqrt{2} covol ( 2 D 5 ) = 2 ⋅ 2 5/2 = 8 2
Appendix A. Tables
Appendix B. Computation and verification
The computation behind Proposition 4.3 follows [1 ] and Voronoi’s algorithm [17 , 15 ] , in exact arithmetic throughout. The programs, the data, the certificate and the Lean formalization are archived at Zenodo [4 ] .
Enumeration
Enumeration. Starting from J 0 J_0 J 0 J J J Min ( J ) \operatorname{Min}(J) Min ( J ) [9 ] , applied to the decomposition of Lemma 2.3 (1); we compute the extreme rays of C J C_J C J [10 ] in exact rational arithmetic; we compute automorphisms of J J J Γ \Gamma Γ G G G Y Y Y t ∗ = ∞ t^*=\infty t ∗ = ∞ Lemma 4.2 ) and otherwise find t ∗ t^* t ∗ Γ \Gamma Γ J + t ∗ Y J+t^*Y J + t ∗ Y G i G_i G i C J i C_{J_i} C J i t ∗ t^* t ∗ j j j T ∈ Γ T\in\Gamma T ∈ Γ T T J j T = J i + t ∗ Y T^TJ_jT=J_i+t^*Y T T J j T = J i + t ∗ Y ( u , a ) (u,a) ( u , a ) E m E_m E m
Independent checks of the certificate
Independent checks of the certificate. Four independent implementations, in C and C++ with rational arithmetic on multiprecision integers, in Julia and in Python with exact rationals, read the certificate and check, without using the enumeration: that each J i J_i J i R \mathcal{R} R k ∈ M ∗ k\in\mathcal{M}^* k ∈ M ∗ J i [ k ] ≤ 4 J_i[k]\le4 J i [ k ] ≤ 4 L D L T LDL^T L D L T Γ \Gamma Γ J i J_i J i C J i C_{J_i} C J i J i + t ∗ Y ∈ R J_i+t^*Y\in\mathcal{R} J i + t ∗ Y ∈ R k k k J i + t ∗ Y J_i+t^*Y J i + t ∗ Y Y [ k ] < 0 Y[k]<0 Y [ k ] < 0 T T J j T = J i + t ∗ Y T^TJ_jT=J_i+t^*Y T T J j T = J i + t ∗ Y T ∈ Γ T\in\Gamma T ∈ Γ Y = X u , a Y=X_{u,a} Y = X u , a Y [ k ] ≥ 0 Y[k]\ge0 Y [ k ] ≥ 0 M \mathcal{M} M Proposition 4.3 , by computing det ( J i + t Y ) \det(J_i+tY) det ( J i + t Y ) det Q ( J i + t Y ) \det Q(J_i+tY) det Q ( J i + t Y ) det ( J i + t Y ) \det(J_i+tY) det ( J i + t Y ) ( 0 , t ∗ ) (0,t^*) ( 0 , t ∗ ) det Q < 512 \det Q<512 det Q < 512 = 512 =512 = 512 > 512 >512 > 512 E 0 , … , E 4 E_0,\ldots,E_4 E 0 , … , E 4 det J = 0 \det J=0 det J = 0 det Q ≤ 512 \det Q\le512 det Q ≤ 512
Table A.1. The entries J a b J_{ab} J ab a ≤ b a \le b a ≤ b J 0 , … , J 33 J_0,\ldots,J_{33} J 0 , … , J 33 E 1 , … , E 4 E_1,\ldots,E_4 E 1 , … , E 4 Proposition 4.5 ; E 0 = J 0 E_0=J_0 E 0 = J 0
Completeness of the extreme rays
The certificate lists all extreme rays of each cone C J i C_{J_i} C J i [10 ] , an implementation of the reverse search method of Avis and Fukuda [2 ] , and two further implementations of the double description method written independently, in C and in Julia, which start from a simplicial cone, add the inequalities one at a time and keep exactly the extreme rays by the combinatorial adjacency test.
A proof in Lean 4 with Mathlib [14 , 13 ] , in which every step is checked by the kernel with no evaluation by compiled code and which uses only the axioms of propositional extensionality, choice and quotient soundness, proves the following for the 34 matrices J i J_i J i J i J_i J i R \mathcal{R} R Min ( J i ) \operatorname{Min}(J_i) Min ( J i ) det J i \det J_i det J i det Q ( J i ) \det Q(J_i) det Q ( J i ) Table 4.1 . Along every representative edge, det ( J i + t Y ) > 0 \det(J_i + tY) > 0 det ( J i + t Y ) > 0 det Q ( J i + t Y ) ≥ 512 \det Q(J_i + tY) \ge512 det Q ( J i + t Y ) ≥ 512 det = 0 \det= 0 det = 0 det Q = 512 \det Q = 512 det Q = 512 t ∗ > 0 t^* > 0 t ∗ > 0 J i + t ∗ Y = T T J j T J_i + t^*Y = T^{\mathsf{T}}J_jT J i + t ∗ Y = T T J j T T ∈ Γ T \in\Gamma T ∈ Γ
Table A.2. The edges at J i J_i J i G i G_i G i j e j^e j e e e e J j J_j J j ∞ e \infty^e ∞ e
some k ∈ M ∗ k \in\mathcal{M}^{*} k ∈ M ∗ ( J i + t Y ) [ k ] < 4 (J_i+tY)[k] < 4 ( J i + t Y ) [ k ] < 4 t > t ∗ t>t^{*} t > t ∗ Y [ k ] ≥ 0 Y[k] \ge0 Y [ k ] ≥ 0 k ∈ M ∗ k \in\mathcal{M}^{*} k ∈ M ∗ R \mathcal{R} R M ∗ \mathcal{M}^{*} M ∗ Γ \Gamma Γ J i J_i J i
Equality configurations
A separate exact computation recomputes the points of C \mathcal{C} C det Q = 512 \det Q = 512 det Q = 512 § 5 , all pairs ( Q , c ) (Q,c) ( Q , c ) Q Q Q Q Q Q c c c Q Q Q 2 D 5 \sqrt{2}\,D_5 2 D 5 Lemma 6.1 , Lemma 6.2 and the statements of Remark 6.3 that concern P 1 P_1 P 1 P 2 P_2 P 2 D 5 D_5 D 5
Floating-point numbers are used only to choose enumeration boxes, which are then enlarged; every decision is made in exact arithmetic. The values 512, 320 + 128 6 320+128\sqrt{6} 320 + 128 6 det Q \det Q det Q Table 4.2 correspond to the centre densities 1 / ( 8 2 ) 1/(8\sqrt{2}) 1/ ( 8 2 ) ( 3 − 2 ) / 4 (\sqrt{3}-\sqrt{2})/4 ( 3 − 2 ) /4 1 / ( 9 2 ) 1/(9\sqrt{2}) 1/ ( 9 2 ) 1 / ( 8 3 ) 1/(8\sqrt{3}) 1/ ( 8 3 ) [1 §4.3] , and the 34 vertices, the two with det J < 0 \det J < 0 det J < 0 det J ≡ 0 \det J \equiv0 det J ≡ 0 [1 §4.3] .
Acknowledgements
The authors used the generative AI tool Claude (Anthropic), through Claude Code, to assist with the proofs, the Lean formalization, the computations and the preparation of this article. The authors reviewed and edited the content and take full responsibility for it.
Statements and Declarations
Competing interests
Competing interests. None.
Funding
Funding. None.
Data availability
Data availability. Deep Bhattacharjee computed the Lean formalization and the Julia, C, C++, shell and Python computations with the help of AI assistance (Claude, Anthropic). The Lean formalization of the finite part of the proof, together with the programs, the data and the certificate of Appendix B, is archived at Zenodo [4 ] , doi:10.5281/zenodo.23387908. The paper is available at https://github.com/creelie/D5/blob/main/preprintAndreanovKallusTwoPeriodicPackingD5/AndreanovKallusTwoPeriodicPackingD5.pdf.
References
Formerly, Electro-Gravitational Space Propulsion Laboratory (EGSPL), Bhubaneswar, Odisha 751030, India
Email address: itsdeep@live.com
Email address: d.bhattacharjee@erl-forschung.de
Formerly, National Taiwan University, Taipei 106319, Taiwan
Email address: rai.bhattacharya.in@gmail.com
