Discrete Geometry

Motivation

A linear set of a projective space over a finite field is the set of points spanned by the nonzero vectors of a subspace over a subfield. They have been used to construct and characterize semifields, rank-metric codes, translation spreads, translation ovoids, two-intersection sets and the blocking sets for which Lunardon introduced them (Polverino 2010; Lavrauw–Van de Voorde 2015). On the projective line $\mathrm{PG}(1, q^n)$ the extremal objects, the maximum scattered linear sets, are equivalent to scattered polynomials over $\mathbb F_{q^n}$, and each scattered polynomial $f$ gives an $\mathbb F_q$-linear maximum rank-distance (MRD) code $\mathcal C_f = \{ax + bf(x) : a, b \in \mathbb F_{q^n}\}$ of minimum distance $n-1$ (Sheekey 2016). Rank-distance codes are studied in network coding theory (p. 2).

Scattered polynomials are scarce. Before this paper, only three families were known for infinitely many $n$:

• 2000. The monomials $x^{q^s}$ with $\gcd(s, n) = 1$ (pseudoregulus type). Blokhuis and Lavrauw (2000) proved that a scattered linear set of $\mathrm{PG}(1, q^n)$ has rank at most $n$.
• 2001, 2016. The binomials $\delta x^{q^s} + x^{q^{n-s}}$ with $N_{q^n/q}(\delta) \notin \{0, 1\}$ (Lunardon–Polverino 2001, Sheekey 2016).
• 2021. For $q$ odd and $n = 2t$, the polynomial $\tfrac12(x^q + x^{q^{t-1}} - x^{q^{t+1}} + x^{q^{2t-1}})$ and its variants (Longobardi–Zanella 2021).
• 2018–2020. Further families exist only for $n \in \{6, 8\}$ (Csajbók–Marino–Polverino–Zanella 2018; Csajbók–Marino–Zullo 2018; Bartoli–Zanella–Zullo 2020). Asymptotic classification results suggest that scattered polynomials are rare (Bartoli–Zhou 2018).

Longobardi, Marino, Trombetti and Zhou construct a fourth family, defined for every even $n \ge 6$ and odd $q$. This mission formalizes that construction, Theorem 3.1 of the paper.

Setting

Let $p$ be an odd prime, $r \ge 1$, $q = p^r$, $t \ge 3$ and $n = 2t$. Let $F = \mathbb F_{q^n}$ be the finite field of order $q^{2t}$. For $m \mid n$, write $\mathbb F_{q^m}$ for its subfield of order $q^m$, the set of $x$ with $x^{q^m} = x$.

A $q$-polynomial over $F$ is a map $f(x) = \sum_{i=0}^{n-1} c_i x^{q^i}$ with $c_i \in F$. It is $\mathbb F_q$-linear. Its graph $U_f = \{(x, f(x)) : x \in F\}$ is an $n$-dimensional $\mathbb F_q$-subspace of $F^2$, and it defines the linear set $L_f = \{\langle (x, f(x))\rangle_{\mathbb F_{q^n}} : x \in F^*\}$ of $\mathrm{PG}(1, q^n)$.

The polynomial $f$ is scattered when, for all $z, y \in F^*$,

$$\frac{f(z)}{z} = \frac{f(y)}{y} \quad\Longrightarrow\quad z \text{ and } y \text{ are } \mathbb F_q\text{-linearly dependent.}$$

Equivalently, $L_f$ has the maximum size $(q^n - 1)/(q - 1)$.

Fix $h \in F$ with $h^{q^t + 1} = -1$. The paper's polynomial is

$$\psi_{h,t}(x) = x^q + x^{q^{t-1}} - h^{1-q^{t+1}} x^{q^{t+1}} + h^{1-q^{2t-1}} x^{q^{2t-1}}.$$

The proof splits it as $\psi_{h,t} = L + M$ with

$$L(x) = x^q - h^{1-q^{t+1}} x^{q^{t+1}}, \qquad M(x) = x^{q^{t-1}} + h^{1-q^{2t-1}} x^{q^{2t-1}},$$

and it also uses the $\mathbb F_{q^t}$-linear maps $R(x) = x^{q^t} + h^{q^{t-1}-q} x$ and $T(x) = x^{q^t} + h^{q-q^{t-1}} x$. The Lean development uses the same letters: psi, Lmap, Mmap, Rmap, Tmap, IsScatteredPoly, qpoly, graph.

Formalization targets

Goal: Theorem 3.1

For $q$ odd, $n = 2t$, $t \ge 3$, and every $h \in \mathbb F_{q^n} \setminus \mathbb F_{q^t}$ with $h^{q^t+1} = -1$,

$$\forall z, y \in \mathbb F_{q^n}^* :\quad \frac{\psi_{h,t}(z)}{z} = \frac{\psi_{h,t}(y)}{y} \;\Longrightarrow\; \exists c \in \mathbb F_q,\ z = c\,y .$$

Milestones

1. The equivalence of three conditions (§1, p. 2): $L_f$ is scattered; $f$ is scattered; and $f(\gamma x) = \gamma f(x)$ with $x \neq 0$ forces $\gamma \in \mathbb F_q$.
2. Proposition 3.2: $h^{q^t+1} = -1$ implies $h^{q^2+1} \neq 1$ and $h^{q^{t-2}} \neq -h$.
3. $L$ and $M$ are $\mathbb F_{q^t}$-semilinear (p. 7).
4. The kernels of $L$ and $M$, displays (4)–(5), are 1-dimensional $\mathbb F_{q^t}$-subspaces.
5. The images of $L$ and $M$, displays (6)–(7), are 1-dimensional $\mathbb F_{q^t}$-subspaces.
6. Proposition 3.3: $\mathbb F_{q^n} = \ker L \oplus \ker M = \operatorname{im} L \oplus \operatorname{im} M$.
7. $\dim \ker R = \dim \ker T = 1$ and $\ker T = h^{q^{t-1}-q}\ker R$ (p. 8).
8. Lemma 3.4: the $\mathbb F_{q^t}$-bases $\{1, \rho\}$, $\{1, \tau\}$ and the change of components (9).
9. Proposition 3.5: $a \in \ker R \iff av \in \ker L \iff aM(u) \in \operatorname{im} L$.
10. Proposition 3.6: $b \in \ker T \iff bu \in \ker M \iff bL(v) \in \operatorname{im} M$.

Significance

The result. Theorem 3.1 produces, for every odd $q$ and even $n \ge 6$, maximum scattered linear sets of $\mathrm{PG}(1, q^n)$ and MRD codes of $\mathbb F_q^{n \times n}$ with minimum distance $n - 1$. For $t = 3$ the polynomials $\psi_{h,3}$ are those of Bartoli, Zanella and Zullo. If $h$ were allowed in $\mathbb F_{q^t}$, then $h \in \mathbb F_{q^2}$ and $\psi_{h,t}$ would reduce to the Longobardi–Zanella polynomials (p. 6). The second half of the paper (Theorem 5.1, a companion mission) shows that for $t > 4$ the family contains a number of $\mathrm{P\Gamma L}$-inequivalent members that grows exponentially in $n$. Every previously known family contributes fewer than $q^2\varphi(n)/2$ classes.

Formalizing it. The theorem has a complete published proof. No scattered polynomial, linear set of the projective line or linearized-polynomial kernel computation is formalized on the platform, and none appears in Mathlib. The work is to formalize the paper's proof: the semilinear-algebra lemmas of §3 and the case analysis that follows them. The milestones are reusable statements about $q$-polynomials of $\mathbb F_{q^{2t}}$ seen as an $\mathbb F_{q^t}$-plane.

Difficulty

Writing $\psi_{h,t}(\gamma x) = \gamma \psi_{h,t}(x)$ out coefficient by coefficient gives a system in $x$ and $\gamma$ with exponents $q, q^{t\pm1}, q^{2t-1}$ that does not separate directly. The paper's route goes through two $\mathbb F_{q^t}$-direct-sum decompositions of $\mathbb F_{q^n}$ and two changes of $\mathbb F_{q^t}$-basis. Each identity involves negative powers of $h$ and holds only through $h^{q^t+1} = -1$ and the parity of $q$. The hypothesis $h \notin \mathbb F_{q^t}$ enters only at the end, and a formalization must carry the arithmetic of the exponent towers modulo $q^{2t} - 1$ throughout. The tempting shortcut, checking the statement on a few small fields, proves nothing: the theorem is uniform in $q$ and $t$.

Formalization scope

• Field. $F$ is a finite field with CharP F p, p prime, Odd p, $q = p^r$ with $r \ge 1$ (an explicit q with hq : q = p ^ r), and Fintype.card F = q ^ (2 * t). So $F$ is $\mathbb F_{q^{2t}}$ up to isomorphism, and no particular model is chosen.
• Subfields. $\mathbb F_q$ and $\mathbb F_{q^t}$ are the fixed fields of $x \mapsto x^q$ and $x \mapsto x^{q^t}$, taken from the published definition ScatCaps.LinearSets.subfieldOf F p r m.
• Scattered. "Scattered" is the literal definition of p. 2, with $z, y$ ranging over all of $F^*$. The scattered-linear-set side of milestone 1 uses the published weight-one predicate ScatCaps.LinearSets.IsScattered, which is equivalent to the cardinality definition of p. 1.
• Powers of $h$. A negative or difference power of $h$ is written as a field quotient, e.g. $h^{1-q^{t+1}}$ as h / h ^ q ^ (t+1). This is exact because $h^{q^t+1} = -1$ forces $h \neq 0$. Natural-number subtractions in exponents ($t-1$, $2t-1$, $3t-2$) are exact in the stated ranges.
• Linear-algebra encodings. "1-dimensional $\mathbb F_{q^t}$-subspace" means closed under addition and $\mathbb F_{q^t}$-scalars, containing $0$, and of cardinality $|\mathbb F_{q^t}|$ (published IsFqSubspace, HasRank). A direct sum is stated as unique decomposition, and an $\mathbb F_{q^t}$-basis $\{1, \rho\}$ as unique representation $\lambda + \mu\rho$ with $\lambda, \mu \in \mathbb F_{q^t}$.
• Pinned readings. (1) The standing hypotheses of §3 ($q$ odd, $n = 2t$, $t \ge 3$, $h^{q^t+1} = -1$) are carried into every §3 lemma, even where its printed statement omits them. $h \notin \mathbb F_{q^t}$ is added only to Theorem 3.1, because the lemmas do not use it. (2) Proposition 3.2 is printed with $t \ge 1$ and without "$q$ odd". "$q$ odd" is added (its proof uses it, and $q$ even gives a counterexample), and $h^{q^{t-2}}$ is read as $h^{q^{3t-2}}$, which is equal to it for $t \ge 2$ and defined at $t = 1$.
• Ruling out trivial versions. A formalization in which $\mathbb F_q$ is the whole field (every map is then "scattered"), in which $\gamma$ or $z, y$ range only over a subfield, or in which $h^{1-q^{t+1}}$ is a truncated natural-number power, would not state the theorem. The statements here quantify over all of $F^*$ and conclude membership in the fixed field of $x \mapsto x^q$.
• Infrastructure. A complete development needs: Frobenius iterates on finite fields, fixed fields and their cardinalities, kernels and images of $\mathbb F_{q^t}$-semilinear maps of $\mathbb F_{q^{2t}}$, and the solution count of $x^{q^t - 1} = c$. These are reusable well beyond this mission. Proofs of any milestone, and alternative arguments, are welcome.

Selected references

• G. Longobardi, G. Marino, R. Trombetti, Y. Zhou, A large family of maximum scattered linear sets of PG(1, q^n) and their associated MRD codes, arXiv:2102.08287v3, 2021 (Combinatorica 43, 2023). https://arxiv.org/abs/2102.08287v3
• A. Blokhuis, M. Lavrauw, Scattered spaces with respect to a spread in PG(n, q), Geometriae Dedicata 81, 2000.
• G. Lunardon, O. Polverino, Blocking sets and derivable partial spreads, J. Algebraic Combin. 14, 2001.
• J. Sheekey, A new family of linear maximum rank distance codes, Adv. Math. Commun. 10(3), 2016.
• G. Longobardi, C. Zanella, Linear sets and MRD-codes arising from a class of scattered linearized polynomials, J. Algebraic Combin., 2021. https://doi.org/10.1007/s10801-020-01011-9
• D. Bartoli, C. Zanella, F. Zullo, A new family of maximum scattered linear sets in PG(1, q^6), Ars Math. Contemp. 19(1), 2020.
• B. Csajbók, G. Marino, O. Polverino, C. Zanella, A new family of MRD-codes, Linear Algebra Appl. 548, 2018.
• B. Csajbók, G. Marino, F. Zullo, New maximum scattered linear sets of the projective line, Finite Fields Appl. 54, 2018.
• D. Bartoli, Y. Zhou, Exceptional scattered polynomials, J. Algebra 509, 2018.
• M. Lavrauw, G. Van de Voorde, Field reduction and linear sets in finite geometry, Contemp. Math. 632, AMS, 2015, pp. 271–293.
• O. Polverino, Linear sets in finite projective spaces, Discrete Math. (22): 3096–3107, 2010.

Motivation

Incidence bounds count how often points can lie on lines, planes or other simple objects. Over the reals the model result is the Szemerédi–Trotter theorem for points and lines in the plane (Szemerédi–Trotter 1983). Its proofs use the order or topology of $\mathbb R$ (cuttings, crossing numbers, polynomial partitioning), so they say nothing over finite fields or fields of positive characteristic. These are the settings that matter for the sum–product problem in $\mathbb F_p$ and for the finite-field versions of Erdős-type distance problems, where the absence of an incidence theorem was long the bottleneck.

M. Rudnev, On the number of incidences between points and planes in three dimensions (Combinatorica 38 (2018), doi:10.1007/s00493-016-3329-6), proves a point–plane incidence bound in $\mathbb P^3$ valid over every field of characteristic $\neq2$, with a constraint only in terms of the characteristic. It became the standard tool for sum–product estimates in positive characteristic: for example, Roche-Newton, Rudnev and Shkredov and Stevens and de Zeeuw build their bounds on it.

Timeline:

• 2010: Guth and Katz settle the Erdős distinct-distances problem in $\mathbb R^2$ via a bound on line–line incidences in $\mathbb R^3$ (arXiv:1011.4105). The part of their argument that uses no ordering of $\mathbb R$ rests on the Cayley–Salmon–Monge theorem on ruled surfaces.
• 2014: Kollár carries the Guth–Katz line–line bound over to arbitrary fields under the constraint $n=O(p^2)$ (arXiv:1405.2243).
• 2014–2015: Rudnev (arXiv:1407.0426, versions v1–v5) reduces point–plane incidences in $\mathbb P^3$ to line–line incidences on a three-dimensional quadric in $\mathbb P^5$, and proves the line–line bound there.
• 2016: de Zeeuw gives a shorter proof of the same bound, using the Guth–Katz–Kollár line theorem in $\mathbb P^3$ (arXiv:1612.02719).

Setting

Let $\mathbb F$ be a field and $\mathbb P^3$ the projective three-space over $\mathbb F$. A point $q=(q_0:q_1:q_2:q_3)$ and a plane $\pi=(\pi_0:\pi_1:\pi_2:\pi_3)$ are both nonzero vectors of $\mathbb F^4$ up to scaling. The point lies on the plane, $q\in\pi$, when $q_0\pi_0+q_1\pi_1+q_2\pi_2+q_3\pi_3=0$. A line of $\mathbb P^3$ is a 2-dimensional subspace of $\mathbb F^4$. For finite sets $P$ of $m$ points and $\Pi$ of $n$ planes, the incidence count is

$$|I(P,\Pi)|=\#\{(q,\pi)\in P\times\Pi:\ q\in\pi\}.$$

The collinearity parameter $k$ is the largest number of planes of $\Pi$ that contain a common line.

The proof works in the space of lines of $\mathbb P^3$. The line through $q$ and $u$ has Plücker vector $L=(P_{01}:P_{02}:P_{03}:P_{23}:P_{31}:P_{12})\in\mathbb P^5$, $P_{ij}=q_iu_j-q_ju_i$. These vectors fill the Klein quadric $\mathcal K=\{P_{01}P_{23}+P_{02}P_{31}+P_{03}P_{12}=0\}$. A point $q$ defines its α-plane (the lines through $q$) and a plane $\pi$ its β-plane (the lines in $\pi$), both projective planes inside $\mathcal K$. Cutting $\mathcal K$ with a hyperplane $S$ that is not tangent to it gives a three-quadric $\mathcal G=\mathcal K\cap S\subset S\cong\mathbb P^4$, and every α- and β-plane meets $\mathcal G$ in a line.

Formalization targets

Goal: Theorem 3

There are absolute constants $c,C>0$ such that for every field $\mathbb F$ of characteristic $\neq2$, every set $P$ of $m$ points and every set $\Pi$ of $n\le m$ planes in $\mathbb P^3$, with $n\le cp^2$ when $\mathbb F$ has positive characteristic $p$,

$$|I(P,\Pi)|\le C\big(m\sqrt n+km\big).$$

In characteristic $0$ there is no constraint on $n$.

Milestones

The proof decomposes as: point–plane incidences in $\mathbb P^3$ equal line–line incidences between two families of mutually skew lines in $\mathcal G$ (Lemma 9), and those are bounded by

$$|I(L_\alpha,L_\beta)|\le C\big(m\sqrt n+km\big)\qquad(\text{Theorem 12}),$$

where $k$ now counts lines of $L_\beta$ in a three-dimensional section of $\mathcal G$. The supporting milestones are: the incidence criterion (9) for Plücker vectors, the intersection pattern of α- and β-planes, Lemma 6 on sections of $\mathcal G$, the generic projection from $\mathbb P^4$ to $\mathbb P^3$, the existence of a low-degree vanishing polynomial, the bound of $d$ zeros on a line, and Salmon's theorem (Theorem 2) on surfaces with many lines.

Significance

Theorem 3 gives the incidence bound $O(m\sqrt n+km)$ with no assumption on the field beyond characteristic. The paper shows that its main term is sharp in positive characteristic under the constraint $\min(m,n)=O(p^2)$ alone (Remark 4), and that the bound is tight for $n=m$, $k=\sqrt m$ (§6.2). It yields the paper's applications (distinct bilinear products of a planar point set over $\mathbb F_p$, and a pinned Erdős distance bound in positive characteristic), and it is the incidence input to sum–product estimates over $\mathbb F_p$ such as $|AA|+|A+A|\gg|A|^{6/5}$.

The theorem is proved and published; it is not open. As far as is known, neither it nor its ingredients (the Klein correspondence in Plücker coordinates, the Guth–Katz polynomial argument over an arbitrary field, Salmon's theorem) has a machine-checked proof. This mission's statements give a formal target for the whole chain. Several milestones (the Plücker incidence criterion, the vanishing polynomial, zeros on a line, the generic projection) are standard facts of projective geometry over arbitrary fields that are useful well beyond this paper.

Difficulty

The obvious route, cell decomposition by polynomial partitioning as over $\mathbb R$, fails over a general field: there is no ordering, so no cells. The Guth–Katz algebraic argument survives, but in $\mathbb P^3$ it needs the hypothesis that few lines are concurrent, which point–plane arrangements violate. Rudnev's way out is to move the problem into the three-quadric $\mathcal G$. There the two line families are skew within themselves, and the collinearity parameter $k$ becomes a count of lines in a three-dimensional section of $\mathcal G$.

The hard step is Theorem 12. It needs the polynomial method over an arbitrary field together with Salmon's theorem on flecnodal surfaces. That theorem holds in characteristic $p$ only for degree $d<p$, which is the source of the constraint $n=O(p^2)$. It also needs a structure theory of ruled surfaces to rule out many incidences inside non-quadric ruled components. Salmon's theorem alone has no formal proof anywhere.

Formalization scope

Points and planes of $\mathbb P^3$ are elements of Mathlib's ℙ F (Fin 4 → F). Finite sets of them are Finsets of projective classes, so they contain distinct points and planes. Incidence is Projectivization.orthogonal. Lines of $\mathbb P^3$, $\mathbb P^4$ and $\mathbb P^5$ are 2-dimensional subspaces. Two lines meet when their intersection is a nonzero subspace, and they are skew when it is zero. Plücker vectors are indexed in the order $(P_{01},P_{02},P_{03},P_{23},P_{31},P_{12})$. A hyperplane $S$ of $\mathbb P^5$ is given by its covector $(\boldsymbol u:\boldsymbol w)$, and "not tangent to $\mathcal K$" is $\boldsymbol u\cdot\boldsymbol w\neq0$. A three-subspace of $S$ is a 4-dimensional subspace of $S$.

Committed conventions:

• The constants $c$ and $C$ of Theorems 3 and 12 are quantified before the field and the configuration, because the paper declares $O(\cdot)$ and $c$ absolute (p. 1).
• "$n=O(p^2)$" is read as $n\le cp^2$ for an existential absolute $c>0$. It applies only in positive characteristic.
• $k$ is any upper bound on the relevant count, which is equivalent to the maximum because the bound is monotone in $k$.
• The field ranges over Type. Bounds are stated in $\mathbb R$, and Salmon's threshold $d(11d-24)$ is computed in $\mathbb Z$.
• "Ruled" means that every point of the surface lies on a line contained in it.
• Lemma 6 carries the hypothesis $S_1\neq S_2$, without which it is false.

Trivializing formalizations are excluded:

• the constants may not depend on the field, the characteristic or $k$;
• the characteristic constraint is not imposed in characteristic $0$, where it would force $n=0$;
• $k$ is not a junk supremum over the infinitely many lines;
• vector Finsets that would count one point twice are not used;
• Theorem 12 is about lines in $\mathcal G\subset\mathbb P^4$, not lines in $\mathbb P^3$ (that would be the Guth–Katz theorem, with different hypotheses).

A complete development needs Plücker coordinates and the Klein correspondence over arbitrary fields, homogeneous polynomials on $\mathbb P^3$ and their zero sets, irreducible factorization, Salmon's theorem, and the Guth–Katz induction. Lemma 8 of the paper (generators of ruled surfaces as curves in $\mathcal K$) is not posed. Proofs of any milestone are welcome, as are proofs of the projective-geometry milestones as standalone Mathlib-style lemmas.

Selected references

• M. Rudnev, On the number of incidences between points and planes in three dimensions, Combinatorica 38 (2018); arXiv:1407.0426v5 (the version formalized). https://arxiv.org/abs/1407.0426
• L. Guth, N. H. Katz, On the Erdős distinct distances problem in the plane, Ann. of Math. 181 (2015) 155–190. https://arxiv.org/abs/1011.4105
• J. Kollár, Szemerédi–Trotter-type theorems in dimension 3, Adv. Math. 271 (2015) 30–61. https://arxiv.org/abs/1405.2243
• J. F. Voloch, Surfaces in $\mathbb P^3$ over finite fields, Contemp. Math. 324 (2003). https://doi.org/10.1090/conm/324
• F. de Zeeuw, A short proof of Rudnev's point-plane incidence bound, arXiv:1612.02719 (2016). https://arxiv.org/abs/1612.02719
• E. Szemerédi, W. T. Trotter, Extremal problems in discrete geometry, Combinatorica 3 (1983) 381–392. https://doi.org/10.1007/BF02579194

Motivation

A proper coloring of a graph assigns colors to its vertices so that adjacent vertices get different colors; the least number of colors that suffices is the chromatic number $\chi(G)$. The clique number $\omega(G)$ is the size of a largest set of pairwise adjacent vertices, and $\chi(G)\ge\omega(G)$ always. A class of graphs is $\chi$-bounded if $\chi$ is bounded by a function of $\omega$ on the class. Abstract triangle-free graphs ($\omega\le2$) of arbitrarily large chromatic number have been known since Zykov (1949) and Mycielski (1955), so the question is which geometric classes are $\chi$-bounded.

For geometric intersection graphs (one vertex per set, an edge for each intersecting pair) the history is as follows.

• 1960: Asplund and Grünbaum prove that families of axis-aligned rectangles in the plane are $\chi$-bounded.
• 1965: Burling constructs triangle-free families of axis-aligned boxes in $\mathbb R^3$ with arbitrarily large chromatic number.
• 1970s: Erdős asks whether families of line segments in the plane are $\chi$-bounded (Brass–Moser–Pach, Research Problems in Discrete Geometry, §9.6, Problem 2; Gyárfás 1987, Problem 1.9).
• 2000–2014: positive special cases. McGuinness (2000) obtains bounds for triangle-free families; Suk (2014) improves them, proving that families of segments meeting a common line, and families of unit-length segments, are $\chi$-bounded.
• 2014: Pawlik, Kozik, Krawczyk, Lasoń, Micek, Trotter and Walczak answer Erdős's question negatively (arXiv:1209.1595).

The same construction disproves Scott's conjecture (1997) that graphs excluding induced subdivisions of a fixed graph are $\chi$-bounded, as first observed by Fox and Pach.

Setting

Points of the plane are pairs $(x,y)\in\mathbb R\times\mathbb R$. A line segment is a closed set $\operatorname{seg}(u,v)=\{(1-t)u+tv: 0\le t\le1\}$ with two distinct endpoints $u\neq v$. A family of segments $\mathcal S=(\sigma_i)_{i<N}$ is a finite indexed list of pairwise distinct segments. Its intersection graph has vertex set $\{0,\dots,N-1\}$, and $i\neq j$ are adjacent exactly when $\sigma_i\cap\sigma_j\neq\emptyset$. The family is triangle-free if no three of its segments pairwise intersect, and $\chi(\mathcal S)$ is the chromatic number of its intersection graph.

The milestones use the paper's auxiliary notions. An axis-aligned rectangle is $R=[a,c]\times[b,d]$, with $x\in[a,c]$ and $y\in[b,d]$. For a family $\mathcal S$ inside the open interior of $R$, a probe for $(\mathcal S,R)$ is a rectangle $P=[a',c]\times[b',d']$ sharing the right edge line of $R$ such that (i) $a<a'<c$ and $b<b'<d'<d$; (ii) no segment meets the left edge of $P$; (iii) no segment has an endpoint in the closed rectangle $P$; (iv) the segments meeting $P$ are pairwise disjoint. The diagonal $D_P$ runs from the bottom-left corner $(a',b')$ to the top-right corner $(c,d')$ of $P$. The sequences $s_k,p_k$ are given by $s_1=p_1=1$, $s_{k+1}=(p_k+1)s_k+p_k^2$ and $p_{k+1}=2p_k^2$.

Formalization targets

Goal: Theorem 1 (p. 2)

For every integer $k\ge1$ there is a finite family $\mathcal S$ of distinct line segments in the plane with triangle-free intersection graph and

$$\chi(\mathcal S)>k .$$

The goal fixes no size for $\mathcal S$ and no particular construction.

Milestones

1. Base case of Lemma 2 (p. 3): one segment and one probe in any rectangle of positive area.
2. Diagonal claim (p. 3): for a probe $Q$ of a family inside the interior of $R$, a segment meets $D_Q$ if and only if it meets $Q$.
3. Color-count dichotomy (p. 4): for a proper coloring of an intersection graph and two index sets $X$, $Y$ each seeing at least $k$ colors, if the color sets differ then $X\cup Y$ sees at least $k+1$ colors; if they agree, a member adjacent to all of $Y$ gets a new color, and $X$ together with it sees at least $k+1$ colors.
4. Induction step (pp. 3–4): Lemma 2 at $k$ for every rectangle gives Lemma 2 at $k+1$ for every rectangle.
5. Lemma 2 (p. 3): for $k\ge1$ and a rectangle $R$ of positive area there are a triangle-free family $\mathcal S_k$ of exactly $s_k$ segments in the interior of $R$ and $p_k$ pairwise disjoint probes for $(\mathcal S_k,R)$ such that every proper coloring of $\mathcal S_k$ uses at least $k$ colors on the segments meeting some probe.
6. The family $\tilde{\mathcal S}_k$ (p. 4): adding the diagonals of all probes to a family with the conclusion of Lemma 2 gives a triangle-free family with $\chi>k$.

Significance

Theorem 1 shows that segment intersection graphs are not $\chi$-bounded, and it settles negatively the question for every class containing them: intersection graphs of curves crossing at most once (Kratochvíl–Nešetřil), McGuinness's class of arcwise connected sets with connected pairwise intersections, and string graphs in general. Through the Fox–Pach observation it refutes Scott's conjecture on induced subdivisions, a purely graph-theoretic statement. The counts in Lemma 2 give $|\tilde{\mathcal S}_k|=s_k+p_k$, so the maximum chromatic number of a triangle-free family of $n$ segments is $\Omega(\log\log n)$ (§4 of the paper). The family $\tilde{\mathcal S}_k$ has the same intersection graph as Burling's boxes.

The theorem is proved on paper; to the best of current knowledge no machine-checked proof exists. The mission produces a Lean 4 statement of the result about actual segments in $\mathbb R^2$, a reusable definition of intersection graphs of plane sets, and the paper's probe machinery stated precisely enough to support a full formal proof.

Difficulty

Abstract triangle-free graphs with large chromatic number are easy to build, but almost none of them are intersection graphs of segments, and the standard constructions (Mycielski, Zykov, shift graphs) do not come with a geometric realization. The difficulty is geometric: the construction has to place every new segment so that it meets exactly a prescribed independent set of old segments and nothing else, at every level of a doubly exponential nesting, while keeping finitely many rectangles disjoint and segment endpoints out of them. In a formal development the burden falls on the planar facts the paper treats as evident in one line each: which edges of a rectangle a segment can cross, when two segments must cross, and why the probe conditions survive when families are nested inside one another.

Formalization scope

• The plane is ℝ × ℝ (first coordinate $x$, second $y$), and segments are Mathlib's closed segment ℝ u v. A family is e : Fin N → (ℝ × ℝ) × (ℝ × ℝ) (endpoint pairs) with seg (e i) the $i$-th segment. "A family of line segments" is read as non-degenerate ((e i).1 ≠ (e i).2) and pairwise distinct (Function.Injective (fun i => seg (e i))).
• interGraph F : SimpleGraph ι is the intersection graph of an indexed family of plane sets: i ≠ j ∧ (F i ∩ F j).Nonempty. Triangle-free is CliqueFree 3; $\chi$ is Mathlib's chromaticNumber : ℕ∞, and the goal states the literal $(k:\mathbb N_\infty)<\chi$.
• Rectangles keep the page's letter order, Rect = ⟨a, c, b, d⟩ for $[a,c]\times[b,d]$, with positive area as a separate hypothesis. A probe is stored as $(a',b',d')$ and is the closed rectangle $[a',c]\times[b',d']$; the interior of $R$ is open.
• sSeq k, pSeq k are $s_k,p_k$, 1-based; every statement assumes $k\ge1$ (the value at $0$ is junk).
• Proper colorings take values in an arbitrary type, and "uses at least $k$ colors on the segments meeting $P$" is $k\le$ ncard of the image of those segments.
• The diagonal claim and the $\tilde{\mathcal S}_k$ milestone are stated for any data with the relevant properties, not only for the paper's construction; the hypotheses are exactly those the page's sentences use.
• The goal is about the intersection graph of the segments the existential provides. A statement about an abstract triangle-free graph with $\chi>k$ is a different, much weaker theorem (already available via Mycielski's construction) and does not count.

Needed infrastructure: elementary planar geometry of segments and axis-aligned rectangles (membership, edges, crossing of two segments via the intermediate value theorem), affine images of segment families, and finite coloring counts. The segment and intersection-graph definitions are reusable for other questions on geometric intersection graphs. Contributions are welcome on any milestone, in particular a complete proof of the diagonal claim and of the induction step.

Selected references

• A. Pawlik, J. Kozik, T. Krawczyk, M. Lasoń, P. Micek, W. T. Trotter, B. Walczak, Triangle-free intersection graphs of line segments with large chromatic number, J. Combin. Theory Ser. B 105 (2014) 6–10; preprint arXiv:1209.1595v5 (2014). https://arxiv.org/abs/1209.1595
• A. Pawlik, J. Kozik, T. Krawczyk, M. Lasoń, P. Micek, W. T. Trotter, B. Walczak, Triangle-free geometric intersection graphs with large chromatic number, Discrete Comput. Geom. 50(3) (2013) 714–726. https://arxiv.org/abs/1212.2058
• J. P. Burling, On coloring problems of families of prototypes, PhD thesis, University of Colorado, Boulder, 1965.
• E. Asplund, B. Grünbaum, On a colouring problem, Math. Scand. 8 (1960) 181–188.
• P. Brass, W. Moser, J. Pach, Research Problems in Discrete Geometry, Springer, 2005.
• A. Gyárfás, Problems from the world surrounding perfect graphs, Zastos. Mat. 19 (1987) 413–441.
• A. Suk, Coloring intersection graphs of x-monotone curves in the plane, Combinatorica 34(4) (2014) 487–505.
• A. D. Scott, Induced trees in graphs of large chromatic number, J. Graph Theory 24(4) (1997) 297–311.
• J. Mycielski, Sur le coloriage des graphes, Colloq. Math. 3 (1955) 161–162.

Motivation

The associahedron $\mathrm{Ass}_n$ is the $n$-dimensional simple polytope whose faces correspond to the sets of pairwise non-crossing diagonals of a convex $(n+3)$-gon, ordered by reverse inclusion: its vertices are the triangulations of the polygon and its facets are the diagonals. It appears in homotopy theory (Stasheff), in the theory of cluster algebras of type $A$, and as the secondary polytope of a convex polygon. Many explicit realizations are known, and a natural question is which of them are genuinely different.

Ceballos, Santos and Ziegler (arXiv:1109.5544, Combinatorica 2014) compare realizations up to normal isomorphism: two polytopes are normally isomorphic if some linear isomorphism of the ambient spaces sends every cone of one normal fan to a cone of the other (their Definition 2.1). This notion ignores the right-hand sides of the defining inequalities and keeps only the linear structure of the facet normals, which is what the classical constructions fix.

One family of realizations is due to Hohlweg and Lange (arXiv:math/0510614, Discrete Comput. Geom. 2007): one associahedron $\mathrm{Ass}^I_n(\sigma)$ for every sign sequence $\sigma \in \{+,-\}^{n-1}$. The constant sequence gives Loday's associahedron (arXiv:math/0212126), and the alternating sequence gives, up to normal isomorphism, the Chapoton–Fomin–Zelevinsky associahedron (arXiv:math/0202004). This mission formalizes the classification of the Hohlweg–Lange family up to normal isomorphism, Theorem 4.9 of Ceballos–Santos–Ziegler.

Setting

Fix $n \ge 0$. The vertices of a convex $(n+3)$-gon are its positions $0, \dots, n+2$ in counterclockwise order. A diagonal joins two distinct non-adjacent positions; two diagonals cross when their endpoints are distinct and alternate around the boundary. The dihedral symmetries are the $2(n+3)$ maps $i \mapsto r + i$ and $i \mapsto r - i$ modulo $n+3$.

For $\sigma \in \{+,-\}^{n-1}$, the sign word $\widetilde\sigma = \{+,-,\sigma,-,+\}$ assigns signs to the labels $0, 1, \dots, n+2$. The polygon $P_{n+3}(\sigma)$ places the labels from left to right, positive ones above a horizontal line and negative ones below; going counterclockwise, it visits the negative labels in increasing order and then the positive labels in decreasing order. For a diagonal $ij$ with labels $i < j$, the set $R_{ij}(\sigma)$ consists of the labels strictly below the diagonal, and $S_{ij}(\sigma) \subseteq [n+1] = \{1,\dots,n+1\}$ is obtained from it by replacing $0$ by $i$ and $n+2$ by $j$. The facet of $\mathrm{Ass}^I_n(\sigma)$ for the diagonal $\delta$ has normal vector $e_{S_\delta(\sigma)}$, the characteristic vector of $S_\delta(\sigma)$ taken modulo $e_{[n+1]} = (1, \dots, 1)$. In coordinates this is the vector

$$v_\delta(\sigma) = \big(\mathbf 1[k \in S_\delta(\sigma)] - \mathbf 1[n+1 \in S_\delta(\sigma)]\big)_{k = 1, \dots, n} \in \mathbb R^n .$$

The normal fan of $\mathrm{Ass}^I_n(\sigma)$ is the collection of cones $\mathbb R_{\ge 0}\{v_\delta(\sigma) : \delta \in D\}$, one for each set $D$ of pairwise non-crossing diagonals. Two facets are parallel when their normals are negative multiples of each other. The reflection of $\sigma$ is $-\sigma$ (all signs flipped), and its reversal $\sigma^t$ is $\sigma$ read backwards.

Formalization targets

Goal: Theorem 4.9

For all $\sigma_1, \sigma_2 \in \{+,-\}^{n-1}$,

$$\mathrm{Ass}^I_n(\sigma_1) \text{ and } \mathrm{Ass}^I_n(\sigma_2) \text{ are normally isomorphic} \iff \sigma_2 \in \{\sigma_1, -\sigma_1, \sigma_1^t, -\sigma_1^t\}.$$

Both directions are content.

Milestones

1. Lemma 2.2. Every bijection of the diagonals that preserves crossing is induced by a dihedral symmetry; for $n \ge 2$, that symmetry is unique.
2. The fan-isomorphism step. A linear isomorphism of the two normal fans induces a crossing-preserving bijection of the diagonals that maps parallel pairs to parallel pairs.
3. Proposition 4.7. $\mathrm{Ass}^I_n(\sigma)$ has exactly $n$ pairs of parallel facets, with normals $e_{[j]}$ and $e_{\overline{[j]}}$. They are the diagonals of explicit quadrilaterals $\{i, j, j+1, k\}$.
4. The four diagonals. The diagonals crossing at least one member of every parallel pair are those joining $\{0,1\}$ to $\{n+1, n+2\}$.
5. Rigidity. A dihedral symmetry mapping the parallel pairs of $P_{n+3}(\sigma_1)$ onto those of $P_{n+3}(\sigma_2)$ forces $\sigma_2 \in \{\sigma_1, -\sigma_1, \sigma_1^t, -\sigma_1^t\}$.
6. Reflection. $\mathrm{Ass}^I_n(\sigma) \cong \mathrm{Ass}^I_n(-\sigma)$, with $\{S_\delta(-\sigma)\} = \{[n+1] \setminus S_\delta(\sigma)\}$.
7. Reversal. $\mathrm{Ass}^I_n(\sigma) \cong \mathrm{Ass}^I_n(\sigma^t)$, with $\{S_\delta(\sigma^t)\} = \{\tau(S_\delta(\sigma))\}$ for $\tau(i) = n + 2 - i$.

Significance

The theorem gives an exact count. The number of normally non-isomorphic Hohlweg–Lange associahedra equals the number of sign sequences of length $n-1$ up to reflection and reversal, which is $2^{n-3} + 2^{\lfloor (n-3)/2 \rfloor}$ for $n \ge 3$ (OEIS A005418). Together with Hohlweg–Lange's identification of the constant and alternating sequences, it shows that Loday's associahedron and the Chapoton–Fomin–Zelevinsky associahedron are not normally isomorphic for $n \ge 3$. It is one of the two classifications on which the paper's main result (Theorem 6.1, that the Hohlweg–Lange and Santos families meet only in the Chapoton–Fomin–Zelevinsky associahedron) rests.

Bergeron, Hohlweg, Lange and Thomas (Isometry classes of generalized associahedra, Sém. Lothar. Combin. 61A, 2009) classified the same family up to isometry of normal fans and obtained the same classes. As Remark 4.10 of the paper explains, that classification does not imply this one, because a normal isomorphism need not be an isometry. Combining the two gives Proposition 4.11, that normal isomorphism and isometry coincide for this family.

Theorem 4.9 is proved in the paper; no machine-checked version is known. A formalization would supply the first formal treatment of the crossing graph of polygon diagonals and its automorphisms (Lemma 2.2), of the Hohlweg–Lange normal vectors, and of linear isomorphisms of simplicial fans given by rays on diagonals.

Difficulty

The "if" direction needs two explicit linear isomorphisms. Their action on the sets $S_\delta$ is not diagonal by diagonal: $P_{n+3}(\sigma)$ and $P_{n+3}(-\sigma)$ have different boundary edges, so the matching of diagonals goes through a mirror image and through the sign swaps of Remark 4.2. One must show that this matching preserves the cone structure, not just the set of normals.

The "only if" direction cannot compare the two polygons by label, since $P_{n+3}(\sigma_1)$ and $P_{n+3}(\sigma_2)$ order their labels differently around the boundary. A linear isomorphism of fans first has to be turned into a combinatorial object. Linearity has to be used twice: it maps rays to rays and preserves cones, which yields a crossing-preserving bijection, and it preserves opposite pairs of normals. Lemma 2.2 then reduces that bijection to one of $2n+6$ dihedral symmetries. The remaining step is a case analysis showing that a symmetry preserving the parallel pairs, and the four distinguished diagonals they determine, is a reflection or reversal of $\widetilde\sigma$. Comparing the multisets of normal vectors alone is not enough: every $\sigma$ gives exactly $n$ parallel pairs with the same normals $\pm e_{[j]}$.

Formalization scope

• Polygon conventions. Polygon vertices are Fin (n + 3), diagonals are Sym2 (Fin (n + 3)), and crossing, diagonal and triangulation come from the published definition ChvatalArtGallery.FanPartition.Triangulation, used as a reference item. Signs are Bool, and $\sigma$ is a function Fin (n - 1) → Bool. Positions and labels are kept apart: hlLabel n σ p is the label at position p.
• Fan-level encoding. All statements are about normal fans, not polytopes. The normal fan of $\mathrm{Ass}^I_n(\sigma)$ is encoded as the fan of the vectors $v_\delta(\sigma)$, with one cone per set of pairwise non-crossing diagonals. That this is its normal fan is Hohlweg–Lange's theorem (Proposition 4.3 of the paper, [17, Prop. 1.3]), assumed by the encoding and not proved. The projection modulo $e_{[n+1]}$ is $x \mapsto (x_k - x_{n+1})_{k \le n}$; linear-isomorphism classes do not depend on this choice.
• Normal isomorphism. This is Definition 2.1 read literally: a LinearEquiv that sends every cone of the first fan to a cone of the second.
• Corrected statements. Three printed slips are corrected:
  • In the four-diagonal claim, only those of the four label pairs that are diagonals count. For constant $\sigma$ one of them is a polygon edge.
  • The complement in milestone 6 is taken in $[n+1]$, where the page prints $[n]$.
  • The reversal in milestone 7 is $\tau(i) = n+2-i$, where the page prints $n+1-i$.
• Dimension threshold. Lemma 2.2 applies $n \ge 2$ only to uniqueness, exactly as the page does; existence holds also for $n=0,1$.
• Ruled-out trivializations. The isomorphism must be linear, since a homeomorphism or a bijection of cones would identify every pair. Cones are nonnegative spans of the actual vectors $v_\delta(\sigma)$, not index sets. Symmetries of the polygon are the $2(n+3)$ dihedral maps, not arbitrary permutations of the vertices.
• What to build. Lemma 2.2 and the fan-isomorphism step are reusable for every classification of associahedra by normal fans, including the Santos family in the companion missions. Contributions to Lemma 2.2 and to the simplicial-fan step are particularly welcome.

Selected references

• C. Ceballos, F. Santos, G. M. Ziegler, Many non-equivalent realizations of the associahedron, Combinatorica 34 (2014); arXiv:1109.5544v2. https://arxiv.org/abs/1109.5544
• C. Hohlweg, C. E. M. C. Lange, Realizations of the associahedron and cyclohedron, Discrete Comput. Geom. 37 (2007). https://arxiv.org/abs/math/0510614
• J.-L. Loday, Realization of the Stasheff polytope, Arch. Math. 83 (2004). https://arxiv.org/abs/math/0212126
• F. Chapoton, S. Fomin, A. Zelevinsky, Polytopal realizations of generalized associahedra, Canad. Math. Bull. 45 (2002). https://arxiv.org/abs/math/0202004
• N. Bergeron, C. Hohlweg, C. Lange, H. Thomas, Isometry classes of generalized associahedra, Sém. Lothar. Combin. 61A (2009).

Motivation

An associahedron of dimension $n$ is a simple polytope whose nonempty faces correspond, reversing inclusion, to the sets of pairwise non-crossing diagonals of a convex $(n+3)$-gon: its vertices are the triangulations of the polygon and its facets are the diagonals. Associahedra appear in the combinatorics of parenthesizations (Tamari, Stasheff), in the theory of cluster algebras of type $A$, where the Chapoton–Fomin–Zelevinsky construction realizes the cluster complex as the normal fan of a polytope, and in the study of secondary polytopes (Gelfand–Kapranov–Zelevinsky).

Many different polytopes realize the associahedron. Ceballos, Santos and Ziegler (arXiv:1109.5544v2) compare them up to normal isomorphism, a linear isomorphism of normal fans. One of the families they study, the "type II" family, is a construction of Santos presented at a conference in 2004 and first published in that paper (§5, pp. 18–23). It produces one associahedron for every triangulation $T_0$ of the $(n+3)$-gon, the seed triangulation, and contains the Chapoton–Fomin–Zelevinsky associahedron as the case of the snake seed. This mission formalizes the statement that the construction works for every seed: Theorems 5.1 and 5.2 of the paper.

Setting

Let $n \ge 0$ and $N = n+3$, and number the vertices of a convex $N$-gon $0, 1, \dots, N-1$ counterclockwise. A diagonal joins two non-adjacent vertices; two diagonals cross when their endpoints are distinct and alternate around the boundary; a triangulation is a maximal set of pairwise non-crossing diagonals, and has $n$ elements. Two triangulations differ by a flip when $T_1 \setminus T_2 = \{v_1\}$ and $T_2 \setminus T_1 = \{v_2\}$.

Fix a triangulation $T_0$ and let $V = \mathbb R^{T_0}$, with basis vectors $\alpha_\delta$, $\delta \in T_0$. Santos' vectors (p. 19) are

$$v_{pq} = -\alpha_\delta \ \text{ if } pq = \delta \in T_0, \qquad v_{pq} = \sum_{\delta \in T_0,\ pq \text{ crosses } \delta} \alpha_\delta \ \text{ if } pq \notin T_0.$$

For a set $D$ of diagonals, $\mathbb R_{\ge 0} D$ is the cone spanned by the vectors $v_e$, $e \in D$. The fan $\mathcal F_{T_0}$ is the collection of the cones $\mathbb R_{\ge 0} D$ for all non-crossing sets $D$, the empty set giving $\{0\}$.

The cones $\mathbb R_{\ge 0}T$ of the triangulations form a complete simplicial fan when the vectors of each triangulation are linearly independent, every vector of $V$ lies in one of these cones, and any two of them meet in the cone of their common diagonals.

For a polytope $P \subseteq \mathbb R^{T_0}$ and $x \in P$, the exterior normal cone is $N_P(x) = \{c : \langle c, y\rangle \le \langle c, x\rangle \text{ for all } y \in P\}$, where $\langle c, y\rangle = \sum_\delta c_\delta y_\delta$. The normal fan of $P$ is the set of all $N_P(x)$, $x \in P$, one cone for each nonempty face (p. 5).

Formalization targets

Goal: Theorems 5.1 and 5.2 (p. 19)

For every triangulation $T_0$ of the $(n+3)$-gon,

$$\{\mathbb R_{\ge0} T : T \text{ a triangulation}\} \text{ is a complete simplicial fan in } V, \quad\text{and}\quad \mathcal F_{T_0} = \{N_P(x) : x \in P\} \text{ for some polytope } P.$$

A polytope with normal fan $\mathcal F_{T_0}$ is an $n$-dimensional associahedron. The goal fixes no weights and no right-hand sides: it asserts only that some polytope has this normal fan.

Milestones

1. Theorem 5.1 (p. 19): the cones of the triangulations form a complete simplicial fan.
2. Assertion (1) of §5.1 (p. 20): $\mathbb R_{\ge 0}T_0$ is the closed negative orthant, a simplicial cone, and the only cone of $\mathcal F_{T_0}$ meeting the open negative orthant.
3. Lemma 5.3 (p. 20), with assertion (2): if $T_1, T_2$ differ by a flip removing $v_1$ and inserting $v_2$, the vectors of $T_1 \cup T_2$ have a linear dependence with nonzero coefficients of the same sign at $v_1$ and $v_2$.
4. Lemma 5.4 (p. 22): a complete simplicial fan of this kind is the normal fan of a polytope if and only if there are weights $\omega > 0$ on the generators such that $\sum_v \lambda(v)\omega(v) > 0$ for the dependence $\lambda$ of every pair of adjacent maximal cones, signed positively on the two flipped generators.
5. The inequality of p. 23: $g_{ij} = (j-i)(n+3+i-j)$ satisfies $g_{ik} + g_{jl} > \max\{g_{ij} + g_{kl}, g_{il} + g_{jk}\}$ for $1 \le i < j < k < l \le n+3$.
6. The weights of pp. 22–23: for all sufficiently small $\varepsilon > 0$, $\omega_{ij} = 2$ on $T_0$ and $\omega_{ij} = 1 + \varepsilon g_{ij}$ off $T_0$ satisfy the condition of Lemma 5.4.

Significance

Theorems 5.1 and 5.2 are what make Santos' family a family of associahedra at all. Every later statement of the paper about type II, including the classification up to normal isomorphism (Corollary 5.7: seeds agreeing up to rotation and reflection) and the identification of the Chapoton–Fomin–Zelevinsky associahedron as the only realization of both types (Theorem 6.1), compares the fans $\mathcal F_{T_0}$, and the word "associahedron" in them rests on these two theorems. The construction yields Catalan-many fans with facet normals in $\{0, \pm 1\}$-coordinates, and modulo rotations and reflections they are pairwise non-isomorphic.

The theorems are proved in the paper; to the best of a search of the Prove2Me catalogue, nothing about normal fans of polytopes, complete simplicial fans or associahedra has been formalized there, and Mathlib at the pinned revision has no notion of fan. The formalization would provide a machine-checked polytopality criterion for complete simplicial fans (Lemma 5.4), an explicit flip analysis of Santos' vectors (Lemma 5.3), and a polytopal realization of the associahedron for every seed.

Difficulty

Theorem 5.1 is not a direct computation. Linear independence of each triangulation and a sign condition for each flip do not by themselves make a fan; the paper combines them with assertion (1), a region covered by exactly one cone, and appeals to a covering criterion for vector configurations (De Loera–Rambau–Santos, Triangulations, Cor. 4.5.20, properties (ICoP) and (IPP)). A solver will likely need to formalize that criterion, or an equivalent argument that a pseudo-manifold of simplicial cones with these properties covers the space exactly once.

Lemma 5.3 requires a case analysis of how the seed triangulation meets the quadrilateral of a flip; the paper distinguishes four configurations, each with its own dependence (equations (4)–(7), p. 21), and showing that the four are exhaustive is itself a combinatorial statement about triangulations. Lemma 5.4 requires constructing a polytope from weights and identifying all of its normal cones, including the lower-dimensional ones, with the cones of the fan. Finally, the uniform constant $\varepsilon_0$ has to work for all flips at once; for the dependence (4) the unperturbed weights ($2$ on $T_0$, $1$ elsewhere) give exactly zero, so a perturbation is unavoidable and must not spoil the other cases.

Formalization scope

Vertices of the polygon are Fin (n + 3), chords are Sym2 (Fin (n + 3)), and diagonals, crossing and triangulations are reused from the published definition ChvatalArtGallery.FanPartition.Triangulation. The space $V$ is {d // d ∈ T₀} → ℝ, coordinate $d$ being the coefficient of $\alpha_d$. Cones are nonnegative hulls (PointedCone.hull ℝ). The fan contains every face, including $\{0\}$.

"Normal fan of a polytope" is encoded as: $P$ is the convex hull of a finite set, and the set of cones equals $\{N_P(x) : x \in P\}$ with exterior normal cones, functionals identified with vectors by the coordinate pairing. Because $\{0\}$ is a cone of $\mathcal F_{T_0}$, the polytope must be full-dimensional; a point, a lower-dimensional polytope, or "some polytope whose facet normals are the rays" does not satisfy the goal. The inner-normal convention would give the fan $-\mathcal F_{T_0}$, which is a different statement. The polytope is specified only through its normal fan, as in the paper.

Lemma 5.4 is stated for fans whose rays are indexed by the diagonals and whose maximal cones are the triangulations, the case in which the paper uses it; adjacent maximal cones are flip pairs. Lemma 5.3 requires the two coefficients to be strictly positive, as assertion (2) does, so the zero dependence is excluded. The ε of milestone 6 is quantified as $\exists \varepsilon_0 > 0\ \forall \varepsilon \in (0, \varepsilon_0)$. The weight $g$ is computed on 0-based positions as $(b-a)(n+3+a-b)$ for $a < b$, which equals the paper's 1-based $g_{ij}$.

A complete development needs basic fan theory (simplicial cones, a covering criterion), the polar construction behind Lemma 5.4, and the flip case analysis. The first two are reusable beyond this mission, for any polytopality argument on simplicial fans. Contributions of general lemmas on simplicial cones and on normal cones of polytopes are welcome.

Selected references

• C. Ceballos, F. Santos, G. M. Ziegler, Many non-equivalent realizations of the associahedron, Combinatorica 34 (2014); arXiv:1109.5544v2. https://arxiv.org/abs/1109.5544 — DOI 10.1007/s00493-014-2959-9
• J. A. De Loera, J. Rambau, F. Santos, Triangulations: Structures for Algorithms and Applications, Springer, 2010. https://doi.org/10.1007/978-3-642-12971-1
• F. Chapoton, S. Fomin, A. Zelevinsky, Polytopal realizations of generalized associahedra, Canad. Math. Bull. 45 (2002). https://arxiv.org/abs/math/0202004
• G. M. Ziegler, Lectures on Polytopes, Springer GTM 152, 1995. https://doi.org/10.1007/978-1-4613-8431-1

Motivation

An associahedron is a polytope whose faces encode ways to dissect a convex polygon without crossing diagonals. Its vertices represent triangulations. Associahedra occur in geometric combinatorics because the same combinatorial object admits many geometric realizations. Ceballos, Santos and Ziegler ask when two such realizations have the same normal fan up to a linear change of coordinates. This question distinguishes geometric constructions that have identical face lattices but different arrangements of facet normals. Their Santos family is indexed by seed triangulations, so its classification asks exactly how much of a seed can be recovered from its fan. Ceballos, Santos and Ziegler, §5.3.

Santos' construction was presented at a conference in 2004 and first appeared in print in this paper. The paper proves that the number of normal-isomorphism classes in this family is the number of polygon triangulations modulo rotations and reflections. It also explains a useful limit of the result: the set of normal vectors alone determines only the abstract dual tree of the seed triangulation, while the fan retains the further information needed for classification. Ceballos, Santos and Ziegler, §5 and Proposition 5.8.

Setting

Take a convex polygon with $N=n+3$ vertices in cyclic order and label its positions $0,\ldots,N-1$. A diagonal joins two nonadjacent vertices. A triangulation $T$ is a maximal collection of diagonals with no crossings. Each triangulation has $n$ diagonals. A flip removes one diagonal shared by two triangles and inserts the other diagonal of their quadrilateral.

Choose a seed triangulation $T_0$. Let $V_{T_0}=\mathbb R^{T_0}$, with a coordinate $\alpha_d$ for each seed diagonal $d$. Santos assigns a vector to every polygon diagonal $e$:

$$v_e(T_0)= \begin{cases} -\alpha_e,&e\in T_0,\\ \displaystyle\sum_{d\in T_0:\,e\text{ crosses }d}\alpha_d,&e\notin T_0. \end{cases}$$

For each noncrossing set $D$ of diagonals, take the cone spanned by the vectors $v_e(T_0)$, $e\in D$, with nonnegative real coefficients. The collection of these cones is the fan $F(T_0)$. The paper proves that it is complete and is the normal fan of an associahedron. This mission uses that explicit fan as the meaning of $\mathrm{Ass}^{II}_n(T_0)$, following the paper's own convention in §5.3. Ceballos, Santos and Ziegler, pp. 19, 23, Theorems 5.1–5.2.

Two fans are normally isomorphic here when an invertible real linear map sends every cone of the first to a cone of the second. A dihedral symmetry is a rotation or a reflection of the cyclically ordered polygon. It acts on a triangulation by relabelling both endpoints of each diagonal. Write $T_1\sim_D T_2$ when such a symmetry sends $T_1$ to $T_2$.

Formalization targets

Classification of Santos associahedra

For every $n\ge 0$ and triangulations $T_1,T_2$ of the $(n+3)$-gon, the goal is Corollary 5.7:

$$F(T_1)\cong_{\mathrm{lin}}F(T_2) \quad\Longleftrightarrow\quad T_1\sim_D T_2.$$

The left side compares all cones of the two fans through a linear isomorphism. The right side permits only the $2(n+3)$ rotations and reflections of the polygon. It makes no choice of an ordering for the diagonals within either seed.

Intermediate source results

The milestone list follows the paper's argument: the polygon symmetry theorem for the associahedron's face lattice (Lemma 2.2); the induced crossing and parallelism preserving bijection of diagonals; the description and count of parallel facet pairs for Santos fans (Proposition 5.5); the injectivity of $T\mapsto B_T$, where $B_T$ contains a seed and all single-flip insertions (Lemma 5.6); and invariance under rotations and reflections. Ceballos, Santos and Ziegler, pp. 6, 23–24.

Significance

The classification says precisely which apparent choices of seed triangulation are redundant. In particular, different dihedral orbits produce different normal-fan geometries even though all the resulting polytopes have the associahedron's face lattice. Parallel facet pairs supply an intrinsic geometric trace of the seed: they correspond to each seed diagonal and its flip. Lemma 5.6 then separates distinct seeds from their collections of these pairs. Ceballos, Santos and Ziegler, Proposition 5.5, Lemma 5.6 and Corollary 5.7.

The result is proved in the paper. The formalization work is to give a machine-checked account of its fan model and classification, including the polygon combinatorics and the linear-algebraic implications of a fan isomorphism. The supplied statements are proof targets, with sorry at theorem bodies; a complete Lean proof of the classification is not yet claimed. The explicit diagonal and crossing representation and the seed-indexed vector construction can also be reused to formalize the paper's fan and polytopality theorems.

Difficulty

A face-lattice isomorphism alone does not identify the seed: every associahedron in the family has the same face lattice. A first attempt to compare only the vectors also loses information. Proposition 5.8 shows that two different seed triangulations with isomorphic dual trees can yield linearly equivalent vector sets. The full fan records which vectors span cones together. The central task is to recover a crossing-preserving map of diagonals from a linear map of fans, then use the opposite directions of facet normals to recover $B_T$. Ceballos, Santos and Ziegler, pp. 23–24, Propositions 5.5 and 5.8.

Formalization scope

Lean represents polygon positions by Fin (n + 3) and unordered diagonals by Sym2; crossings and triangulations come from the published Chvátal triangulation definition. The ambient real vector space for a seed is the function space on the subtype of its actual diagonals. This makes the basis intrinsic to $T$. A cone is the nonnegative real hull of the Santos vectors attached to a noncrossing diagonal set. NormallyIsomorphic demands a real linear equivalence of these ambient spaces. The classifying symmetry is explicitly $i\mapsto r+i$ or $i\mapsto r-i$ modulo $n+3$.

No premise asserts the classification, and the fan is built from the paper's vectors rather than from a chosen list of abstract cones. Arbitrary permutations of diagonals, nonlinear maps, and an abstractly isomorphic dual tree do not satisfy the target's symmetry condition. The goal and the diagonal-action clause of Lemma 2.2 cover every $n$; the separate group-order clause in Lemma 2.2 applies for $n\ge2$. Lemma 5.6 carries the printed bound $n\ge2$. The triangular and quadrilateral cases are included in the goal and require their own boundary treatment in a proof. Contributions on crossing preservation, ray distinctness, linear independence of maximal cones, single-flip combinatorics, and dihedral equivariance are welcome.

Selected references

• C. Ceballos, F. Santos and G. M. Ziegler, Many non-equivalent realizations of the associahedron, Combinatorica 34 (2014), 513–551; preprint arXiv:1109.5544v2 (2013). arXiv, DOI.

Motivation

An associahedron is a polytope whose vertices represent triangulations of a convex polygon and whose edges represent flips between triangulations. The same combinatorial polytope can be realized in different vector spaces with different facet directions. This matters when a construction uses the geometry of the realization, rather than only its face lattice: a linear change of coordinates can preserve its normal fan, while a general combinatorial relabelling need not. Ceballos, Santos and Ziegler compare three constructions and use parallel facets to distinguish them.

Two of those constructions form large families. Hohlweg–Lange choose a word of signs; Santos chooses a triangulation as a seed. Both yield associahedra, and both include the Chapoton–Fomin–Zelevinsky (CFZ) realization. The paper proves that CFZ is their only shared normal-isomorphism class. Its Theorem 6.1 is the target here; the result was announced as Theorem 1.1 in the introduction. Source, pp. 4 and 28.

Setting

Fix $n\ge0$ and a convex polygon with $n+3$ cyclically ordered vertices. A diagonal joins two nonadjacent vertices. Two diagonals cross when their endpoints alternate around the boundary. A triangulation is a maximal collection of pairwise noncrossing diagonals. Every triangulation has $n$ diagonals, and replacing one diagonal with the other diagonal of the quadrilateral it borders is a flip. The faces of an associahedron correspond to noncrossing sets of diagonals, while its vertices correspond to triangulations. Source, pp. 5 and 18–19.

A normal fan records the outward normal directions of all faces of a polytope and the cones they span. Two complete fans are linearly isomorphic when a real linear equivalence sends every cone of the first to a cone of the second. Polytopes are normally isomorphic when their normal fans are linearly isomorphic. This is Definition 2.1 of the paper; the comparison is geometric because it requires a linear map. Source, p. 5.

For the Hohlweg–Lange family, choose a sign word $\sigma\in\{+,-\}^{n-1}$ and extend it to $\widetilde\sigma=(+,-,\sigma,-,+)$ on the labels $0,\ldots,n+2$. The negative labels, in increasing order, form one boundary chain; the positive labels, in decreasing order, form the other. For a diagonal with endpoint labels $i<j$, let $R_{ij}(\sigma)$ contain the labels strictly below it. Form $S_{ij}(\sigma)$ by replacing $0$ with $i$ and $n+2$ with $j$ if those labels occur in $R_{ij}(\sigma)$. The characteristic vector of $S_{ij}(\sigma)$, considered modulo the all-ones vector, gives its facet normal. Source, pp. 14–16, Definition 4.1.

For the Santos family, choose a seed triangulation $T_0$ and use one basis vector $\alpha_d$ for each seed diagonal $d$. The normal assigned to a diagonal $e$ is $-\alpha_e$ when $e\in T_0$. Otherwise it is the sum of $\alpha_d$ over seed diagonals crossing $e$. The cones spanned by compatible diagonal vectors give the fan. The distinguished snake seed joins alternating polygon positions $1,n+2,2,n+1,3,\ldots$; this seed gives the CFZ fan. Source, pp. 13 and 18–19.

Formalization targets

The only shared class

Let $F^I_n(\sigma)$ and $F^{II}_n(T)$ be the two normal fans, and let $S_n$ be the fixed snake. If $T$ is a triangulation, the target says

$$F^I_n(\sigma)\cong_{\mathrm{lin}}F^{II}_n(T) \quad\Longrightarrow\quad T=g(S_n)\text{ for some rotation or reflection }g,$$

and it also asserts that $F^I_n(+,-,+,-,\ldots)\cong_{\mathrm{lin}}F^{II}_n(S_n)$. Together these are the uniqueness and existence parts of Theorem 6.1. The result covers dimensions zero and one as well as higher dimensions; Lemma 2.2 uses $n\ge2$ only for its second sentence, the uniqueness of the inducing symmetry. Source, pp. 6, 16 and 28–29.

Supporting targets

The milestone list follows the paper's stated intermediate results: polygon symmetries of the associahedron, the parallel-facet pairs in each family, and the three properties of triangles in the seed that force the snake. Proposition 4.4 supplies the alternating-sign realization used for existence. The parallel-pair targets retain the source's exact count of $n$ pairs, through their characterization by the $n$ seed flips or the $n$ labelled quadrilaterals. Source, pp. 6, 16–17, 23 and 28–29.

Significance

Theorem 6.1 gives a complete answer to a comparison question that face-lattice data alone cannot settle: every member of either family has the same associahedral combinatorics, but almost no cross-family pair has linearly equivalent normal fans. It identifies the exceptional class without fixing coordinates for either construction. The characterization of parallel facets also gives a concrete invariant for later comparisons among associahedron realizations. Source, pp. 23 and 27–28.

The paper proves the result mathematically. A complete Lean development would add machine-checked definitions of the two ray systems and a proof of the classification, including the geometric step that a linear fan isomorphism induces a compatible correspondence of facet rays. The polygon triangulation and crossing definitions are already available as a published reusable component; proofs about fans and the two constructions are the remaining work.

Difficulty

An isomorphism of abstract face lattices gives too little information: it exists between all associahedra of the same dimension. The useful comparison must control a linear map on the actual normal vectors. The first obstacle is proving that such a map preserves the rays and therefore preserves which facets are parallel. Then the two explicit descriptions of parallel pairs must be reconciled, and the resulting sign restriction on a triangulation must force alternating turns of its dual path. Showing only that the dual tree is a path is insufficient; path triangulations can make consecutive turns on the same side. Source, pp. 17, 23 and 28–29.

Formalization scope

Vertices are Fin (n+3) in counterclockwise positions, with zero-based indexing; Hohlweg–Lange signs apply to labels carried by those positions. Diagonals are unordered pairs. The imported Chvátal triangulation definition gives boundary edges, crossings, maximal noncrossing sets, and their triangles. A cone is the nonnegative span of the vectors assigned to a noncrossing set. The type I vectors are represented in $\mathbb R^n$ using quotient coordinates $x_k-x_{n+1}$; type II vectors are functions on the seed diagonals. Hohlweg–Lange Proposition 4.3, cited in the paper, identifies the maximal cones of the type I normal fan with triangulations. Source, pp. 15–16.

Normal isomorphism uses a real linear equivalence, dihedral symmetry uses only rotations and reflections of the polygon, and the snake is the explicit alternating triangulation. The cones use the actual facet vectors. These commitments exclude a mere bijection of index sets, an arbitrary permutation of vertices, and a path triangulation with nonalternating turns. The condition $n\ge2$ appears only where the page has it, in the second sentence of Lemma 2.2 (uniqueness of the inducing symmetry); facet-normal comparisons quantify only over diagonals, exactly the facets represented in the paper. Reusable contributions include combinatorial flip lemmas, linear independence of triangulation rays, and general results about linear maps of simplicial fans.

Selected references

• César Ceballos, Francisco Santos, and Günter M. Ziegler, Many non-equivalent realizations of the associahedron, Combinatorica 34 (2014), 513–551. arXiv:1109.5544v2.