🗺️ Map of Integer frieze patterns and Tabachnikov's four sign changes

🏷️ Combinatorics · frieze patterns and triangulations of polygons

10 results ✅ 0 entirely in Lean ◐ 2 partly in Lean ✅ 2 in Isabelle 💻 4 checked by a program written proof only (a result can carry several tags)

Dependencies in the written proof: an arrow A → B means that this proof of B uses A. Every result rests on its written proof; the tags record what was checked besides, and each statement's “Evidence & scope” block says how far. The colour of a box is its strongest tag, in the order above; the tags in the box give the rest. Boxes with a thick border are the main results; click a box to read the statement.

What the paper contributes

A negative answer to Problem 1 of Tabachnikov (A four-vertex theorem for frieze patterns?, 2018) for frieze patterns of positive integers, which the question left open:

for every even $n \geq 14$, two integer frieze patterns whose middle rows are strictly ordered (no sign change);
for every odd $n \geq 15$, two whose rows $\lfloor w/2 \rfloor$ differ with no zero and exactly two sign changes, inside the range $1 \le k \le [w/2]$ of the question;
an exhaustive search showing that $14$ and $15$ are the smallest values of $n$ for the two phenomena, when zeros may count as sign changes.

Both families are proved for every $n$ and checked in Isabelle/HOL; the two smallest pairs are also checked in Lean.

🚀 Start here: Lemma 1: antipodal ear insertion keeps the old diameters, adds one.

Main results:

Theorem A: even n ≥ 14: middle rows strictly ordered, no sign change
Theorem B: odd n ≥ 15: row ⌊w/2⌋, no zero, exactly two sign changes

🧭 Fields: where the paper lives and what it connects

Tools taken from other branches

Linear algebra in the plane → frieze patterns as unimodular lattice polygons: every entry a 2×2 determinant, an ear a sum of two vectors — Lemma 1, Theorem A, Theorem B
Exhaustive search → all pairs of integer frieze patterns of width ≤ 12, on a GPU, rechecked by three independent constructions — Proposition 1

What the results serve

Four-vertex theorems for discrete curves ← the integer case of Tabachnikov’s question, answered negatively from n = 14 on — Corollary 1