Formalizing Structural Graph Theory in Lean 4

For \(r \geq 1\) and \(n \in \mathbb{N}\), the clique \(r\)-crossing of order \(n\) is the graph obtained from the star \(r\)-crossing of order \(n\) (Definition StarCrossing) by adding, for every root \(a_i\) (\(i \in [n]\)), all edges turning \(\{\operatorname{start}(\pi_{i,j}) : j \in [n]\} = \{\pi_{i,j,1} : j \in [n]\}\) into a clique, and similarly, for every root \(b_j\) (\(j \in [n]\)), all edges turning \(\{\operatorname{end}(\pi_{i,j}) : i \in [n]\} = \{\pi_{i,j,r} : i \in [n]\}\) into a clique.

Equivalently, the vertex set is the same as for the star \(r\)-crossing and the edges are:

• the \((r+1)\)-edge path \(a_i, \pi_{i,j,1}, \ldots, \pi_{i,j,r}, b_j\) for every \((i, j) \in [n]^2\) (shared with the star \(r\)-crossing);
• for every \(i \in [n]\) and distinct \(j, j' \in [n]\), the edge \(\pi_{i,j,1} \pi_{i,j',1}\);
• for every \(j \in [n]\) and distinct \(i, i' \in [n]\), the edge \(\pi_{i,j,r} \pi_{i',j,r}\).

No other edges are present. In particular, the \((r+1)\)-edge paths are still internally vertex-disjoint across \((i, j)\), and the interior path vertices \(\pi_{i,j,\ell}\) for \(\ell \in [2, r-1]\) have the same neighborhoods as in the star \(r\)-crossing.

Layer partition. The layer partition of the clique \(r\)-crossing of order \(n\) is the same as that of the star \(r\)-crossing (Definition StarCrossing): \(\mathcal{L}_{r,n}^{\mathrm{clique}} := \{L_0, L_1, \ldots, L_{r+1}\}\) with \(L_0 = \{a_i\}\), \(L_\ell = \{\pi_{i,j,\ell} : i, j \in [n]\}\) for \(\ell \in [r]\), \(L_{r+1} = \{b_j\}\).

Flipped clique \(r\)-crossing. For \(r \geq 1\) and \(n \in \mathbb{N}\), a graph \(H\) is a flipped clique \(r\)-crossing of order \(n\) if there exists a symmetric relation \(F \subseteq (\mathcal{L}_{r,n}^{\mathrm{clique}})^2\) such that \(H\) is (isomorphic to) the flip \(\mathrm{Clique}_{r,n} \oplus F\) of the clique \(r\)-crossing \(\mathrm{Clique}_{r,n}\) of order \(n\) via the layer partition \(\mathcal{L}_{r,n}^{\mathrm{clique}}\) (Definition Flip).

The number of flipped clique \(r\)-crossings of order \(n\) (up to isomorphism) is at most \(2^{(r+2)^2}\). Taking \(F = \emptyset\) gives the unflipped clique \(r\)-crossing of order \(n\).