Substrate Geometry
Computer-assisted interval computation / private preview
AConvex range of a spherical-harmonic perturbationHAND PROOFBConvexity thresholds for 27 harmonic bodiesCOMPUTER-ASSISTEDCEquilibrium counts for the m = 1 harmonic bodiesCOMPUTER-ASSISTEDD1Sloan shape 2: upper bound on the convex rangeHAND PROOFD2Sloan shape 2 is strictly convex for beta up to 0.03550477COMPUTER-ASSISTEDD3Sloan shape 2 has the origin as centroid and exactly two equilibriaHAND PROOFD4Sloan shape 1: upper bound on the convex rangeHAND PROOFD5Sloan shape 1 is strictly convex and mono-monostatic for beta up to 0.03229670385COMPUTER-ASSISTEDE1Phase-1 body: strictly convex2 METHODSE2Phase-1 body: exactly one stable and one unstable equilibrium2 METHODSF1Phase-1 gradient floorCOMPUTER-ASSISTEDF2Phase-1 Hessian at the equilibria: flat in one direction, steep in the otherCOMPUTER-ASSISTEDF3How much shape error Phase-1 toleratesCOMPUTER-ASSISTEDF4Is Phase-1 close to the best this family can do?EXPLORATORYG1Phase-1 equilibrium count as a replayable recordCOMPUTER-ASSISTEDG2Single-harmonic m=1 counts from the same checkerCOMPUTER-ASSISTEDG3Convexity of radial bodies, checked against the published thresholdsCOMPUTER-ASSISTEDG4Mesh trials: how much shape error a printed gomboc can takeEXPLORATORYG5A nearest-neighbour scan miscounts a flat bodyEXPLORATORYAConvex range of a spherical-harmonic perturbationHAND PROOFBConvexity thresholds for 27 harmonic bodiesCOMPUTER-ASSISTEDCEquilibrium counts for the m = 1 harmonic bodiesCOMPUTER-ASSISTEDD1Sloan shape 2: upper bound on the convex rangeHAND PROOFD2Sloan shape 2 is strictly convex for beta up to 0.03550477COMPUTER-ASSISTEDD3Sloan shape 2 has the origin as centroid and exactly two equilibriaHAND PROOFD4Sloan shape 1: upper bound on the convex rangeHAND PROOFD5Sloan shape 1 is strictly convex and mono-monostatic for beta up to 0.03229670385COMPUTER-ASSISTEDE1Phase-1 body: strictly convex2 METHODSE2Phase-1 body: exactly one stable and one unstable equilibrium2 METHODSF1Phase-1 gradient floorCOMPUTER-ASSISTEDF2Phase-1 Hessian at the equilibria: flat in one direction, steep in the otherCOMPUTER-ASSISTEDF3How much shape error Phase-1 toleratesCOMPUTER-ASSISTEDF4Is Phase-1 close to the best this family can do?EXPLORATORYG1Phase-1 equilibrium count as a replayable recordCOMPUTER-ASSISTEDG2Single-harmonic m=1 counts from the same checkerCOMPUTER-ASSISTEDG3Convexity of radial bodies, checked against the published thresholdsCOMPUTER-ASSISTEDG4Mesh trials: how much shape error a printed gomboc can takeEXPLORATORYG5A nearest-neighbour scan miscounts a flat bodyEXPLORATORY
REPRODUCE

Run it yourself

Each computer-assisted row has a script and a log. Scripts run from any directory through relative paths.

Environment

Python 3.11.9, python-flint 0.9.0, mpmath 1.3.0, sympy 1.14.0, numpy 2.4.6, scipy 1.17.1 (Windows). Timings are from one desktop machine with other jobs running; treat them as orders of magnitude.

ResultCommandTime
Phase-1 centroidpython -X utf8 phase1/phase1_centroid.pyseconds
Phase-1 convexity, primarypython -X utf8 phase1/phase1_convexity.pyunder 1 s
Phase-1 convexity, second methodpython -X utf8 phase1/phase1_audit.py326 s
Phase-1 count, primarypython -X utf8 phase1/phase1_count.py139 s
Phase-1 count, second methodpython -X utf8 phase1/phase1_count_audit.pyabout 190 s
Sloan convexity, primarypython -X utf8 sloan/certify_fine.pyabout 2,600 s
m = 1 counts, intervalpython -X utf8 m1/m1_interval.py 6 0.004303 0.0086075 28hours per l
m = 1 counts, second methodpython -X utf8 m1/m1_independent.py 3 1 25190 to 245 s
Gradient floorpython -X utf8 margins/phase1_robust.py 0.2 0.001210 to 20 s
Hessian marginpython -X utf8 margins/phase1_hessian.pyseconds
Perturbation tolerance tablepython -X utf8 margins/prop_tolerance_cert.pyseconds
Phase-1 count record (G1)python examples/make_count_certificate.py out.json (from software/eqcert)about 10 s to search, 3 s to replay
Harmonic m=1 count records (G2)PYTHONPATH=src python -m pytest tests/test_harmonic_counts.py (from software/eqcert)about 3 minutes
Radial convexity records (G3)python examples/make_radial_convexity.py (from software/eqcert)about 25 minutes
Mesh tolerance trials (G4)python mesh_tolerance_trials.py phase-1 20 120 (then sloan-shape-2)about 15 minutes each
Scan miscount (G5)open the notebook, run section 2seconds
Status
  • The public repository and a DOI have not been created yet. Until they are, the scripts and logs are not downloadable from this site.
  • Nothing here is a formally verified proof. See Method for the trust base.