Strictly convex intersection body

In this notebook we would like to prove that the intersection body \(IP\) of the icosahedron \(P\) centered at the origin is strictly convex. It is known that \(IP\) is convex, so we are left to prove that there are no line segments contained in its boundary. We compute the polynomials that define the boundary of \(IP\) using the Algorithm 1 from https://mathrepo.mis.mpg.de/intersection-bodies/. The output is a list of \(32\) polynomials: \(12\) quintics and \(20\) sextics. In order to achieve our goal, we prove computationally that there are no lines that vanish identically on the zero locus of any of these polynomials. Using the symmetries of the problem, it is enough to run this computation for one quintic and two sextics.

For the numerical computation we use HomotopyContinuation.jl.

[1]:

using HomotopyContinuation
@var x[1:3]

[1]:

(Variable[x₁, x₂, x₃],)

We start with the quintic. There are 12 such varieties, which coincide up to change of coordinates. Therefore, we run the computation only for one representative.

[2]:

quintic = (sqrt(5)*x[1] + sqrt(5)*x[2] - x[1] + x[2] + 2*x[3])*(sqrt(5)*x[1] + sqrt(5)*x[2] - x[1] + x[2] - 2*x[3])*(sqrt(5)*x[1] + sqrt(5)*x[3] + x[1] + 2*x[2] - x[3])*(sqrt(5)*x[1] - sqrt(5)*x[3] + x[1] + 2*x[2] + x[3])*x[2] - 8*sqrt(5)*x[1]^3*x[2] - 68*sqrt(5)*x[1]^2*x[2]^2 - 72*sqrt(5)*x[1]*x[2]^3 - 20*sqrt(5)*x[2]^4 + 40*sqrt(5)*x[1]*x[2]*x[3]^2 + 20*sqrt(5)*x[2]^2*x[3]^2 - 4*sqrt(5)*x[3]^4 - 8*x[1]^3*x[2] - 164*x[1]^2*x[2]^2 - 168*x[1]*x[2]^3 - 44*x[2]^4 + 8*x[1]^2*x[3]^2 + 72*x[1]*x[2]*x[3]^2 + 44*x[2]^2*x[3]^2 - 12*x[3]^4

[2]:
$$ -25.8885438199983*x₂*x₁^3 - 316.052622469986*x₂^2*x₁^2 + 88.7213595499958*x₂^2*x₃^2 - 328.996894379985*x₂^3*x₁ + 8*x₃^2*x₁^2 + 161.442719099992*x₂*x₃^2*x₁ + x₂*(1.23606797749979*x₁ + 3.23606797749979*x₂ + 2*x₃)*(1.23606797749979*x₁ + 3.23606797749979*x₂ - 2*x₃)*(3.23606797749979*x₁ + 2*x₂ + 1.23606797749979*x₃)*(3.23606797749979*x₁ + 2*x₂ - 1.23606797749979*x₃) - 88.7213595499958*x₂^4 - 20.9442719099992*x₃^4 $$

Parametrize a generic (real) line \(L \subset \mathbb{R}^3\) by \(L = \{ a t + b \}\) for some \(a,b \in \mathbb{R}^3\) and \(t\in \mathbb{R}\).

[3]:

@var a[1:3] b[1:3]
@var t

[3]:

(t,)

Then \(L\subset \{\)quintic\(=0\}\) if and only if the quintic evaluated at \(x=at+b\) is identically zero for some choice of \(a,b\).

[4]:

quinticL = subs(quintic,x=>a.*t+b)

[4]:
$$ -328.996894379985*(b₁ + t*a₁)*(b₂ + t*a₂)^3 - 316.052622469986*(b₁ + t*a₁)^2*(b₂ + t*a₂)^2 - 25.8885438199983*(b₁ + t*a₁)^3*(b₂ + t*a₂) + 8*(b₃ + t*a₃)^2*(b₁ + t*a₁)^2 + 88.7213595499958*(b₃ + t*a₃)^2*(b₂ + t*a₂)^2 + 161.442719099992*(b₃ + t*a₃)^2*(b₁ + t*a₁)*(b₂ + t*a₂) + (b₂ + t*a₂)*(1.23606797749979*(b₁ + t*a₁) + 3.23606797749979*(b₂ + t*a₂) - 2*(b₃ + t*a₃))*(1.23606797749979*(b₁ + t*a₁) + 3.23606797749979*(b₂ + t*a₂) + 2*(b₃ + t*a₃))*(3.23606797749979*(b₁ + t*a₁) + 2*(b₂ + t*a₂) + 1.23606797749979*(b₃ + t*a₃))*(3.23606797749979*(b₁ + t*a₁) + 2*(b₂ + t*a₂) - 1.23606797749979*(b₃ + t*a₃)) - 88.7213595499958*(b₂ + t*a₂)^4 - 20.9442719099992*(b₃ + t*a₃)^4 $$

Therefore, we want to see quinticL as a polynomial in \(t\), and find a common zero of all its coefficients.

[5]:

C = coefficients(quinticL,t)
solve(System(C))







<span class=”ansi-green-fg”>Tracking 6160 paths… 100%|████████████████████████████| Time: 0:00:56</span>


<span class=”ansi-blue-fg”>  # paths tracked:                  6160</span>
<span class=”ansi-blue-fg”>  # non-singular solutions (real):  0 (0)</span>
<span class=”ansi-blue-fg”>  # singular endpoints (real):      2985 (1727)</span>
<span class=”ansi-blue-fg”>  # total solutions (real):         2985 (1727)</span>
</pre>






textcolor{ansi-green}{Tracking 6160 paths{ldots} 100%|████████████████████████████| Time: 0:00:56}


textcolor{ansi-blue}{  # paths tracked:                  6160}
textcolor{ansi-blue}{  # non-singular solutions (real):  0 (0)}
textcolor{ansi-blue}{  # singular endpoints (real):      2985 (1727)}
textcolor{ansi-blue}{  # total solutions (real):         2985 (1727)}
end{sphinxVerbatim}






Tracking 6160 paths… 100%|████████████████████████████| Time: 0:00:56
  # paths tracked:                  6160
  # non-singular solutions (real):  0 (0)
  # singular endpoints (real):      2985 (1727)
  # total solutions (real):         2985 (1727)








[5]:







Result with 762 solutions
=========================
• 6160 paths tracked
• 0 non-singular solutions (0 real)
• 762 singular solutions (14 real)
• random_seed: 0xb565b966
• start_system: :polyhedral
• multiplicity table of singular solutions:
╭───────┬───────┬────────┬────────────╮
│ mult. │ total │ # real │ # non-real │
├───────┼───────┼────────┼────────────┤
│   1   │  587  │   3    │    584     │
│   2   │  34   │   0    │     34     │
│   3   │  14   │   0    │     14     │
│   4   │  16   │   0    │     16     │
│   5   │  110  │   10   │    100     │
│ 1674  │   1   │   1    │     0      │
╰───────┴───────┴────────┴────────────╯






Since there are no solutions, there are no lines contained in the zero locus of the polynomial quintic.


We repeat now the same process for the two types of sextics. We start with the first type, for which we have \(12\) polynomials that coincide up to symmetry.




[6]:





sextic1 = (sqrt(5)*x[1] + sqrt(5)*x[3] + x[1] + 2*x[2] - x[3])*(sqrt(5)*x[1] - sqrt(5)*x[3] + x[1] + 2*x[2] + x[3])*(sqrt(5)*x[2] + sqrt(5)*x[3] - 2*x[1] - x[2] +  x[3])*(sqrt(5)*x[2] - sqrt(5)*x[3] - 2*x[1] - x[2] - x[3])*x[1]*x[2] +  20*sqrt(5)*x[1]^4*x[2] - 20*sqrt(5)*x[1]^2*x[2]^3 - 4*sqrt(5)*x[1]*x[2]^4 +  4*sqrt(5)*x[2]^5 - 4*sqrt(5)*x[1]^3*x[3]^2 - 60*sqrt(5)*x[1]^2*x[2]*x[3]^2 -  12*sqrt(5)*x[1]*x[2]^2*x[3]^2 + 12*sqrt(5)*x[1]*x[3]^4 + 44*x[1]^4*x[2] -  8*x[1]^3*x[2]^2 - 44*x[1]^2*x[2]^3 + 12*x[1]*x[2]^4 + 12*x[2]^5 - 12*x[1]^3*x[3]^2- 156*x[1]^2*x[2]*x[3]^2 - 60*x[1]*x[2]^2*x[3]^2 - 8*x[2]^3*x[3]^2 + 28*x[1]*x[3]^4
sextic1L = subs(sextic1,x=>a.*t+b)
C = coefficients(sextic1L,t)
solve(System(C))





















<span class=”ansi-green-fg”>Tracking 34048 paths… 100%|███████████████████████████| Time: 0:11:38</span>


<span class=”ansi-blue-fg”>  # paths tracked:                  34048</span>
<span class=”ansi-blue-fg”>  # non-singular solutions (real):  0 (0)</span>
<span class=”ansi-blue-fg”>  # singular endpoints (real):      10214 (7560)</span>
<span class=”ansi-blue-fg”>  # total solutions (real):         10214 (7560)</span>
</pre>






textcolor{ansi-green}{Tracking 34048 paths{ldots} 100%|███████████████████████████| Time: 0:11:38}


textcolor{ansi-blue}{  # paths tracked:                  34048}
textcolor{ansi-blue}{  # non-singular solutions (real):  0 (0)}
textcolor{ansi-blue}{  # singular endpoints (real):      10214 (7560)}
textcolor{ansi-blue}{  # total solutions (real):         10214 (7560)}
end{sphinxVerbatim}






Tracking 34048 paths… 100%|███████████████████████████| Time: 0:11:38
  # paths tracked:                  34048
  # non-singular solutions (real):  0 (0)
  # singular endpoints (real):      10214 (7560)
  # total solutions (real):         10214 (7560)








[6]:







Result with 2180 solutions
==========================
• 34048 paths tracked
• 0 non-singular solutions (0 real)
• 2180 singular solutions (1 real)
• 3180 excess solutions
• random_seed: 0xcbf460d6
• start_system: :polyhedral
• multiplicity table of singular solutions:
╭───────┬───────┬────────┬────────────╮
│ mult. │ total │ # real │ # non-real │
├───────┼───────┼────────┼────────────┤
│   1   │ 1918  │   0    │    1918    │
│   2   │  126  │   0    │    126     │
│   3   │  62   │   0    │     62     │
│   4   │  71   │   0    │     71     │
│   6   │   1   │   0    │     1      │
│   8   │   1   │   0    │     1      │
│ 7560  │   1   │   1    │     0      │
╰───────┴───────┴────────┴────────────╯






Again: no solutions means no lines contained in the sextic.


Now we move to the second type of sextic. There are 8 such varieties, up to change of coordinates.




[7]:





sextic2 = (sqrt(5)*x[1] - sqrt(5)*x[2] - x[1] - x[2] + 2*x[3])*(sqrt(5)*x[1] - sqrt(5)*x[2] - x[1] - x[2] - 2*x[3])*(sqrt(5)*x[1] + sqrt(5)*x[3] + x[1] + 2*x[2] - x[3])*(sqrt(5)*x[1] + sqrt(5)*x[3] + x[1] - 2*x[2] - x[3])*(sqrt(5)*x[2] - sqrt(5)*x[3] + 2*x[1] - x[2] - x[3])*(sqrt(5)*x[2] - sqrt(5)*x[3] - 2*x[1] - x[2] - x[3]) + 32*sqrt(5)*x[1]^5 - 256*sqrt(5)*x[1]^4*x[2] - 64*sqrt(5)*x[1]^3*x[2]^2 + 160*sqrt(5)*x[1]^2*x[2]^3 + 32*sqrt(5)*x[1]*x[2]^4 - 32*sqrt(5)*x[2]^5 + 32*sqrt(5)*x[1]^4*x[3] - 64*sqrt(5)*x[1]^3*x[2]*x[3] - 672*sqrt(5)*x[1]^2*x[2]^2*x[3] - 64*sqrt(5)*x[1]*x[2]^3*x[3] + 256*sqrt(5)*x[2]^4*x[3] - 160*sqrt(5)*x[1]^3*x[3]^2 + 672*sqrt(5)*x[1]^2*x[2]*x[3]^2 - 672*sqrt(5)*x[1]*x[2]^2*x[3]^2 + 64*sqrt(5)*x[2]^3*x[3]^2 - 64*sqrt(5)*x[1]^2*x[3]^3 - 64*sqrt(5)*x[1]*x[2]*x[3]^3 - 160*sqrt(5)*x[2]^2*x[3]^3 + 256*sqrt(5)*x[1]*x[3]^4 - 32*sqrt(5)*x[2]*x[3]^4 + 32*sqrt(5)*x[3]^5 + 32*x[1]^5 - 576*x[1]^4*x[2] + 352*x[1]^2*x[2]^3 - 32*x[1]*x[2]^4 - 32*x[2]^5 - 32*x[1]^4*x[3] - 320*x[1]^3*x[2]*x[3] - 1056*x[1]^2*x[2]^2*x[3] - 320*x[1]*x[2]^3*x[3] + 576*x[2]^4*x[3] - 352*x[1]^3*x[3]^2 + 1056*x[1]^2*x[2]*x[3]^2 - 1056*x[1]*x[2]^2*x[3]^2 - 320*x[1]*x[2]*x[3]^3 - 352*x[2]^2*x[3]^3 + 576*x[1]*x[3]^4 + 32*x[2]*x[3]^4 + 32*x[3]^5
sextic2L = subs(sextic2,x=>a.*t+b)
C = coefficients(sextic2L,t)
solve(System(C))





















<span class=”ansi-green-fg”>Tracking 39492 paths… 100%|███████████████████████████| Time: 0:23:45</span>


<span class=”ansi-blue-fg”>  # paths tracked:                  39492</span>
<span class=”ansi-blue-fg”>  # non-singular solutions (real):  0 (0)</span>
<span class=”ansi-blue-fg”>  # singular endpoints (real):      11423 (7560)</span>
<span class=”ansi-blue-fg”>  # total solutions (real):         11423 (7560)</span>
</pre>






textcolor{ansi-green}{Tracking 39492 paths{ldots} 100%|███████████████████████████| Time: 0:23:45}


textcolor{ansi-blue}{  # paths tracked:                  39492}
textcolor{ansi-blue}{  # non-singular solutions (real):  0 (0)}
textcolor{ansi-blue}{  # singular endpoints (real):      11423 (7560)}
textcolor{ansi-blue}{  # total solutions (real):         11423 (7560)}
end{sphinxVerbatim}






Tracking 39492 paths… 100%|███████████████████████████| Time: 0:23:45
  # paths tracked:                  39492
  # non-singular solutions (real):  0 (0)
  # singular endpoints (real):      11423 (7560)
  # total solutions (real):         11423 (7560)








[7]:







Result with 3598 solutions
==========================
• 39492 paths tracked
• 0 non-singular solutions (0 real)
• 3598 singular solutions (1 real)
• 3180 excess solutions
• random_seed: 0xd435fb2a
• start_system: :polyhedral
• multiplicity table of singular solutions:
╭───────┬───────┬────────┬────────────╮
│ mult. │ total │ # real │ # non-real │
├───────┼───────┼────────┼────────────┤
│   1   │ 3419  │   0    │    3419    │
│   2   │  108  │   0    │    108     │
│   3   │  52   │   0    │     52     │
│   4   │  18   │   0    │     18     │
│ 7560  │   1   │   1    │     0      │
╰───────┴───────┴────────┴────────────╯






We then conclude that there are no line segments in the boundary of \(IP\), and that therefore \(IP\) is strictly convex.