Moser lower bounds

9 Lower bound theorem

The end goal of the working set iteration is the following claim.

Theorem 47 Computational lower bound
#

Uses

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_*\):

\[ \inf \{ \operatorname {area}(M) : M \text{ is a Moser set}\} \ge A_*. \]
Proof ▶

Any Moser set \(M\) of area \({\lt}A_*\) must contain, in some pose, every polygon ever present in a working set produced by addWormAndCleanup, by Propositions 41, 43, and 45. If the final working set is empty, this is a contradiction.

Proposition 48 Terminating sequence of worms
#

Uses

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).