1 · The result
Insert ears after the positions \(j\) and \(j + h\). The diameters of the new polygon are the old ones, in the same cyclic order, together with one new diameter between the two new vertices, of value
Hence if \(D_i(U) {\lt} D_i(V)\) for all \(i\) and \(S(U, j) {\lt} S(V, j)\), the strict order survives the insertion.
2 · In plain words
\paragraph{In plain words (commentary, not part of the paper).} Gluing a triangle on a side of a triangulated polygon adds a vertex; in vectors, the new vertex is the sum of the two vectors at the ends of that side, so no old entry changes. Glue two triangles at opposite sides of an even polygon. Every old diameter still joins two opposite vertices of the bigger polygon, because one new vertex lands on each of its sides; the only new diameter joins the two new vertices. So comparing two polygons after the gluing only needs one new number, $S$, and the lemma reduces Theorem A to an inequality between two values of $S$.
next →3 · How it is proved
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.
It rests on:
- Linear algebra in the plane — frieze patterns as unimodular lattice polygons: every entry a 2×2 determinant, an ear a sum of two vectors
- Exhaustive search — all pairs of integer frieze patterns of width ≤ 12, on a GPU, rechecked by three independent constructions
4 · What is checked
🟢 2 formal · 🟡 2 formal in part · 🔵 2 computation.
Proof: in this note · Formalized: Isabelle/HOL, by the author (public formalizations repository) · Covers: the whole statement · Cite: Lemma 1, p. 4, doi:10.5281/zenodo.23656979
What a referee has to check by hand →
next →5 · Try it
Labs in your browser (they load Python the first time):
- Figures 4 and 5 live: the family of Theorem B, member by member (thm:B)
- Test your own pair: are there four sign changes? (prop:min)
Cite: doi:10.5281/zenodo.23656979