Optimal paper Möbius band

AbbreviationUnit strip#✓fully proved

The unit strip is the set of points \((x, y) \in \mathbb{R}^2\) with \(0 \le x \le 1\), that is, \([0, 1] \times \mathbb{R}\).

abbrev unitStrip : Set ℝ² :=
  {x | x 0 ∈ Set.Icc 0 1}

Used by 1

Used byMoebius embedding

DefinitionGluing map of the Moebius band#✓fully proved

For a real number \(a\), this is the map \(\mathbb{R}^2 \to \mathbb{R}^2\) given by \((x, y) \mapsto (1 - x, y + a)\).

def period (a : ℝ) : ℝ² → ℝ² :=
  fun x ↦ !₂[1 - x 0, x 1 + a]

Used by 1

Used byMoebius embedding

DefinitionFundamental domain of the Moebius band#✓fully proved

For a real number \(a\), this is the set of points \((x, y) \in \mathbb{R}^2\) with \(0 \le x \le 1\) and \(0 \le y < a\).

def fundamentalDomain (a : ℝ) : Set ℝ² :=
  {x | x 0 ∈ Set.Icc 0 1 ∧ x 1 ∈ Set.Ico 0 a}

Used by 1

Used byMoebius embedding

StructureMoebius embedding#✓fully proved

Let \(a\) be a real number, let \(S = [0, 1] \times \mathbb{R}\) be the unit strip and let \(f : \mathbb{R}^2 \to \mathbb{R}^3\). Then \(f\) is a Moebius embedding of aspect ratio \(a\) if \(f(1 - x, y + a) = f(x, y)\) for every \((x, y) \in S\), \(f\) is \(C^\infty\) on \(S\), at every point of \(S\) the derivative of \(f\) within \(S\) is a linear isometry \(\mathbb{R}^2 \to \mathbb{R}^3\), and \(f\) is injective on \([0, 1] \times [0, a)\).

This encodes the paper's smooth isometric embedding of a Moebius band: the strip is glued into a band by the first condition, and injectivity on a fundamental domain makes the glued map an embedding.

structure IsMoebiusEmbedding (a : ℝ) (f : ℝ² → ℝ³) : Prop where
  periodic : ∀ x ∈ unitStrip, f (period a x) = f x
  smooth : ContDiffOn ℝ ∞ f unitStrip
  isometry : ∀ x ∈ unitStrip, Isometry (fderivWithin ℝ f unitStrip x)
  embedding : Set.InjOn f (fundamentalDomain a)

Uses 3 · Used by 1

Statement usesFundamental domain of the Moebius band · Gluing map of the Moebius band · Unit strip

Used bySchwartz's optimal paper Moebius band theorem

TheoremSchwartz's optimal paper Moebius band theorem#●ready to prove

Let \(a > 0\). If \(f : \mathbb{R}^2 \to \mathbb{R}^3\) is a Moebius embedding of aspect ratio \(a\), then \(a > \sqrt{3}\). That is, a smooth embedded paper Moebius band has aspect ratio greater than \(\sqrt{3}\).

public theorem_wanted theorem_1_1 (a : ℝ) (ha : a > 0) (f : ℝ² → ℝ³) (hf : IsMoebiusEmbedding a f) :
    a > √3

Sources

• R. E. Schwartz, The optimal paper Moebius band, Annals of Math, 201 (1) 2025. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_optimal_moebius of the lean-eval benchmark.

Uses 1

Statement usesMoebius embedding

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.