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
METHOD

Enclose, subdivide, then check it a second way

The strongest wording we use is computer-assisted. This page says why, and what would have to be wrong for a result to fail.

Fix the object with exact numbers

Parameters are exact rationals; pi is an enclosure. The Phase-1 body is the one with beta = 23149/10^6 and a1 = 234433/10^6, not the output of an optimiser we cannot reproduce.

Enclose instead of estimate

Every quantity is an arbitrary-precision ball (python-flint). A statement such as K > 0 on a box means the enclosure of K on that box has a positive lower endpoint. A box that cannot be decided is a failure, never a success.

Subdivide until every box is decided

Adaptive branch and bound, with a centered form from forward-mode automatic differentiation, which is what makes certification feasible close to an exact threshold. Equilibria use Krawczyk uniqueness boxes and exclusion boxes.

Check it a second way

The second method shares no chart, no symmetry reduction and no polar cap with the first: Cartesian implicit-surface curvature on the six faces of a cube, with the equilibrium condition written as N x (x - c) = 0. Its coverage differs by result and is stated on each row.

Have it read cold

The engine was reviewed cold, with the aim of producing a false certificate. The review found no way for a box with K at or below zero to pass, and three real defects, all fixed (below). Human readers are still wanted for the perturbation argument.

Let a short program replay the answer

For the newer software results the search writes its answer as a record and a separate short checker re-evaluates every box. A search bug can make a search fail but not make a wrong record pass. See rows G1 to G3.

Label every row

Hand proof, two methods, computer-assisted, or exploratory. The build refuses a row that uses stronger wording than its tier.

WHAT THE REVIEW FOUND

Three defects, all fixed before the reported runs

  • The ball enclosing a box did not always contain it, and the centered form used an inexact midpoint. In a test, 511 of 2000 random deep boxes missed an endpoint. Fixed by taking the exact union of the two endpoint balls and forming every difference in ball arithmetic; no misses in 2000 tests afterwards.
  • The upper azimuth limit pi/m was below the true value by 1.2e-16. Fixed with a directed rounding.
  • One reported lower bound had been rounded up when printed. Fixed by recomputing every reported bound as an outward-rounded value from the exact endpoints.

The review did not re-run anything, did not check the code that encloses the maximum of g, and did not cover m = 0. A missing box centring in a Krawczyk step of the second m = 1 method was found by us and fixed before those runs.

TRUST BASE

What you still have to trust

  • python-flint's ball arithmetic.
  • Our symbolic derivatives, checked against finite differences and against the second method.
  • Our branch-and-bound drivers. A width-floor rule fired spuriously in one early Sloan run and was lowered.
  • No formally verified kernel is used. That is why the strongest wording is computer-assisted.
A WARNING FROM THE DATA

Float counts overcount flat bodies

Counting equilibria on a float grid reported 21 minima and 19 maxima on flat ridges for a body that has exactly one of each, and merge thresholds undercount. A number that moves with resolution is a property of the sampler, not of the body. This is why the ledger separates enclosures from scans, and why the harmonic explorer on the Bodies page is labelled an illustration.