This page contains the computer programs needed to verify the results in the paper.
at.pari -- PARI file which computes the Molien series for Aut(Leech), using character values read off from "Atlas of Finite Groups".
molien.pari -- PARI file which computes the Molien series for Aut(D3), Aut(D4), Aut(E8), using the data about conjugacy classes prepared by groupfacts.mws and groupfacts.pari below.
groupfacts.mws -- Maple file which prepares the data about conjugacy classes in Aut(E8), using the cf. Coxeter/Weyl package by J. R. Stembridge.
groupfacts.pari -- PARI file which prepares the data about conjugacy classes in Aut(D3) and Aut(D4).
invpol.pari -- PARI file which computes bases for the spaces of invariant polynomials for Aut(D3), Aut(D4), Aut(E8).
(The following might be of interest, although not directly needed for any of our results: sfunctions.pari -- PARI file for decomposition of Sym^f(Sym^2(R^n)) into O(n)-irreducibles, and similar tasks.)
The following technical manual describes in detail how the programs work.
initboxes.pari -- PARI program which computes a good covering of the modified Grenier's fundamental domain by boxes in Iwasawa coordinates.
rationals.pari -- PARI program used for computations using exact integer arithmetic (rigorous lower and upper bounds).
global.c -- C program which checks that away from the fcc-box iself, the height function is strictly larger than at the fcc-point. The program uses the following auxiliary data file containing the definitions of the boxes, produced by initboxes.pari: boxes.dat. It also uses the following file containing Taylor coefficients used in the computation of the Complementary Incomplete Gamma Function (as well as some data used to compute cubic roots, and inverse), produced by running "printtaylorcoeffs()" in rationals.pari: taylorcoeffs.
sphere.pari -- A PARI program which proves that the Iwasawa fcc-box is contained inside the sphere of radius 0.18 about fcc.
local.pari -- PARI program which proves F(fcc)=0.113359752603..., and then uses Taylor expansion at the fcc point to check that this value is the unique minimum throughout the 0.18-sphere. It uses the following auxiliary data file with bases of invariant polynomials for Aut(D3), produced by invpol.pari: invpolD3.dat. (The following program using floating point arithmetic may be of interest for doing various types of tests: localf.pari.)