Dependencies

For each pair of naturals \((a, b) \ne (0, 0)\), the formulas \(c = (a^2 - b^2)/(a^2 + b^2)\) and \(s = 2ab/(a^2 + b^2)\) yield a rational point on the unit circle. Enumerating such pairs up to a resolution depending on a target maximum angle change yields a finite rational grid on the unit circle.

Applying a direct isometry vertex-wise to a convex polygon produces a convex polygon. Convexity is preserved because rotations preserve the cross products witnessing the “strictly left of” condition.

Given a finite list of candidate worms \(W\) and a finite list of isometries \(I\), a set \(M\) is a \((W, I)\)-approximate Moser set if for every \(w \in W\) there exists \(\varphi \in I\) with \(\varphi (w) \subseteq M\).

The area threshold is \(A_* := 232240 / 10^6 = 0.232240\). A Moser set with area strictly less than \(A_*\) would improve the current best lower bound.

Three concrete convex polygons are fixed as benchmark worms:

• the isosceles right triangle with legs of length \(1/2\),

• the unit square with side \(1/3\),

• the right triangle with legs \(1/3\) and \(2/3\).

The initial worm is taken to be the isosceles right triangle; by convention every candidate Moser set in the working set contains an un-shifted copy of it. Its area is exactly \(1/8\).

Remove every polygon whose area strictly exceeds \(A_*\). This preserves Invariant 2 because any Moser set of area below \(A_*\) cannot have a polygon of strictly larger area as a subset.

cleanup is the composition of big-set removal and superset removal. addWormAndCleanup adds a worm and then cleans up.

A point lies in a convex polygon iff it lies in every edge half-space. A convex polygon \(P\) is a subset of \(Q\) iff every vertex of \(P\) lies in \(Q\).

A convex polygon is a non-degenerate polygon in which, for every directed edge \(V_i \to V_{i+1}\), every other vertex lies strictly to the left of the edge. Strictness excludes collinear triples and therefore makes every vertex an extreme point of the convex hull of \(\{ V_i\} \).

The function convexHullRationalPoints returns, from a finite list of rational points, a list of extreme points in counterclockwise order starting at the lexicographically smallest point. ConvexPolygon.ofList upgrades this to an Option ConvexPolygon, returning none when fewer than three extreme points remain.

A direct isometry is a tuple \((c, s, t)\) with \(c, s \in \mathbb {Q}\), \(t \in \mathbb {Q}^2\), and \(c^2 + s^2 = 1\). It acts on \(p \in \mathbb {Q}^2\) by

For a granularity \(\epsilon {\gt} 0\), we form a finite list of direct isometries by pairing each angle from angleGrid with each translation on a rational grid intersected with the LocationRange (Definition 29). The angle resolution is scaled by the distance cutoff so that far-away points are still covered finely.

A (closed, resp. open) half-space is specified by a basepoint \(b \in \mathbb {Q}^2\) and a nonzero inward normal \(n \in \mathbb {Q}^2\); a point \(p\) belongs to the half-space iff \(n \cdot (p - b) \ge 0\) (resp. \({\gt} 0\)).

The initial working set contains exactly the initial worm.

Direct isometries are closed under composition, with \((c, s, t)_1 \circ (c, s, t)_2\) given by the usual product of rotation matrices and composed translation.

A line is a basepoint together with a nonzero direction vector. Two nonparallel lines have a unique intersection point, computed by Cramer’s rule.

Let \(\sigma := 4 A_*\). The location range is the square \([-\sigma , \sigma ]^2\), which upper-bounds the positions where a point of a working-set polygon may lie without already exceeding the area threshold (via a triangle formed with the initial worm). The distance cutoff is \(\sigma \cdot \overline{\sqrt{2}}\), where \(\overline{\sqrt{2}} = 1414213562373095/10^{15}\) is a rational upper bound on \(\sqrt2\).

The minimum area in a working set is the minimum of the shoelace areas of its polygons (taken as \(0\) on the empty set).

A set \(M \subseteq \mathbb {R}^2\) is a Moser set if for every worm \(w\) of unit length there exists a direct isometry \(\varphi \) with \(\varphi (w) \subseteq M\).

Given \(d, \tau {\gt} 0\), one may translate the basepoint of a half-space inward along its normal by an amount in \([d, d+\tau ]\), obtaining a new half-space contained in the original. The scaling factor is realised rationally via Lemma 10.

A non-degenerate polygon is a tuple consisting of a natural number \(n \ge 3\), a function \(V : \mathrm{Fin}\, n \to \mathbb {Q}^2\) giving the vertices in counterclockwise order, and a proof that \(V\) is injective.

Given a list of closed half-spaces, the convex polygon defined by their intersection is obtained by taking all pairwise boundary intersections and retaining those satisfying every half-space constraint.

For \(u, v \in \mathbb {Q}^2\) we define \(u \times v = u_0 v_1 - u_1 v_0\), \(u \cdot v = u_0 v_0 + u_1 v_1\), and \(\lVert v\rVert ^2 = v_0^2 + v_1^2\).

A rational point is an element of \(\mathbb {Q}^2\), represented as a function \(\mathrm{Fin}\, 2 \to \mathbb {Q}\).

Given \(0 \le \ell {\lt} u\) in \(\mathbb {Q}\), there is an explicit rational \(r {\gt} 0\) with \(\ell \le r^2 \le u\).

The map \(R : (x, y) \mapsto (-y, x)\) is a \(90^\circ \) counterclockwise rotation, and preserves squared length.

A worm can be scaled by any rational factor; scaling by \(1/\ell \) where \(\ell \) is the approximate length brings the worm to approximately unit length. A unit worm bundles a worm together with a uniform bound ensuring the approximate length tends to \(1\) as \(\epsilon \to 0\).

The area of a convex polygon with vertex list \((V_0, \ldots , V_{n-1})\) is

Given \(d, \tau {\gt} 0\), one shrinks a convex polygon by moving each edge inward by an amount in \([d, d + \tau ]\) and intersecting the resulting half-spaces. The output is an Option ConvexPolygon, since the result may be empty.

Given \(s \ge 0\) and \(\epsilon {\gt} 0\), the Newton iteration \(x_{n+1} = (x_n + s/x_n)/2\) produces a rational \(r\) with \(|r - \sqrt{s}| {\lt} \epsilon \). Applied componentwise, this yields a rational approximation distanceApprox of the Euclidean distance between two rational points.

Remove every polygon \(p\) in the list for which some distinct polygon \(q\) in the list is a subset of \(p\). The smaller \(q\) already witnesses Invariant 2 whenever \(p\) does.

Each edge of a convex polygon defines a closed half-space weakly to its left; the polygon coincides with the intersection of these half-spaces.

Given distinct points \(p_1, p_2 \in \mathbb {Q}^2\), the half-space strictly (resp. weakly) to the left of the directed segment \(p_1 \to p_2\) uses basepoint \(p_1\) and normal \(R(p_2 - p_1)\).

A working set is a list of convex polygons. Intended invariants:

1. every polygon in the list contains a copy of the initial worm (Definition 28) under some direct isometry;

2. every Moser set of area strictly less than \(A_*\) contains a copy of some polygon in the list under some direct isometry.

Invariant 1 is currently a convention maintained by construction; Invariant 2 is the core correctness statement the algorithm preserves.

A worm is a polygonal path with at least two rational vertices. Its approximate total length is the sum of distance approximations along consecutive vertices, with per-segment error budget divided equally so the total error remains below a given \(\epsilon \).

The convex hull of a worm is a convex polygon (when the worm has at least three non-collinear vertices); it summarises all rigid motions of the worm that embed it into a convex target.

Given an additional worm presented as a convex hull, for each polygon \(p\) in the current working set and for each isometry \(\varphi \) in the discretisation, form the convex hull of \(p\) together with the image under \(\varphi \) of the shrunk hull (to absorb discretisation error). The new working set collects all such unions. This step encodes the requirement that a Moser set must contain this worm in some pose.

Every \((c, s)\) produced by angleGrid satisfies \(c^2 + s^2 = 1\).

The output of convexHullRationalPoints has no duplicates.

The rational \(r\) returned by 9 satisfies \(r {\gt} 0\), \(\ell \le r^2\), and \(r^2 \le u\).

The action of a direct isometry on \(\mathbb {Q}^2\) is both injective and surjective.

For all \(v \in \mathbb {Q}^2\), \(\lVert v\rVert ^2 \ge 0\), with strict inequality when \(v \ne 0\).

If a working set satisfies Invariant 2 of Definition 37, so does the result of big set removal.

Any convex polygon containing the initial worm as well as a point outside the location range has area strictly greater than \(A_*\).

If a working set satisfies Invariant 2, so does the result of superset removal.

A finite list of worms ending the iteration with the empty working set can be found by computer search, e.g. starting from the benchmark worms of Definition 28 and augmenting with further worms arising from the enumeration scheme in Moser.Worm.Enumeration (currently stubbed).

If the isometry discretisation is fine enough relative to the shrink amount, then adding a worm preserves Invariant 2 of Definition 37.

There exists a finite list of worms \(W\) and a sequence of working-set updates that, starting from Definition 38 and adding the worms in \(W\) in turn using Definition 46, terminates with the empty working set. Consequently the area of every Moser set is at least \(A_*\):