Constants for Moser's Worm Problem

This file defines the key constants used in the computational approach:

• areaThreshold: Maximum area for candidate Moser sets
• distanceCutoff: Maximum distance from origin for polygon vertices

def Moser.areaThreshold : ℚ

Area threshold for candidate Moser sets (0.232240) This is the number we are trying to beat with our working set polygons.

Equations

• Moser.areaThreshold = Rat.divInt 232240 1000000

def Moser.IsocelesRightTriangleWorm : ConvexPolygon

The isoceles right triangle with legs of length 1/2.

Equations

• One or more equations did not get rendered due to their size.

def Moser.SquareWorm : ConvexPolygon

A square of side length 1/3.

Equations

• One or more equations did not get rendered due to their size.

def Moser.RightTriangleOntThirdWorm : ConvexPolygon

A right triangle with legs of length 1/3 and 2/3. TODO parameterize this and the above worms by leg lengths, and then optimize over those parameters.

Equations

• One or more equations did not get rendered due to their size.

def Moser.InitialWorm : ConvexPolygon

The "initial worm" is a worm that we assume any set in our working set must contain an unshifted copy of.

This makes it convenient to exclude points from working set polygons on the basis of containing a point such that the hull of such a point with the initial worm would have area > threshold.

We could consider redefining this when optimizing. For now, we take it to be the isoceles right triangle worm, since this seems to work well.

Equations

• Moser.InitialWorm = Moser.IsocelesRightTriangleWorm

def Moser.offset : ℚ

Half-side length of the square LocationRange, scaled from the area threshold.

Equations

• Moser.offset = Moser.areaThreshold * 4

def Moser.LocationRange : ConvexPolygon

A convex polygon representing an upper bound on the range of locations a point in the working set can contain.

This is the square with vertices at (± offset, ± offset). Any point outside this square cannot be contained in a convex polygon that also contains the InitialWorm without exceeding the area threshold. (Because otherwise there would be a triangle that was too large.)

TODO We could potentially optimize this to the smallest polygon for which the above is true. Which would in turn let us improve the distance cutoff and thus reduce the fineness needed in angle discretization.

Equations

• One or more equations did not get rendered due to their size.

def Moser.upperBoundSqrtTwo : ℚ

A rational upper bound on √2, accurate to 15 decimal places.

Equations

• Moser.upperBoundSqrtTwo = Rat.divInt 1414213562373095 1000000000000000

def Moser.distanceCutoff : ℚ

An upper bound on the distance from the origin for points in the LocationRange

Equations

• Moser.distanceCutoff = Moser.offset * Moser.upperBoundSqrtTwo