Dev.MonadicDependence.StarCrossing
Definition
For \(r \geq 1\) and \(n \in \mathbb{N}\), the star \(r\)-crossing of order \(n\) is the \(r\)-subdivided biclique of order \(n\), i.e. the graph \((K_{n,n})^{(r)}\) (Definition Subdivision, Definition Biclique).
Concretely, its vertex set consists of
- the \(2n\) roots \(a_1, \ldots, a_n, b_1, \ldots, b_n\), and
- for every pair \((i, j) \in [n]^2\), \(r\) fresh path vertices \(\pi_{i,j,1}, \ldots, \pi_{i,j,r}\), pairwise disjoint across \((i, j)\).
For every \((i, j) \in [n]^2\) the edges \(a_i\,\pi_{i,j,1},\ \pi_{i,j,1}\,\pi_{i,j,2},\ \ldots,\ \pi_{i,j,r-1}\,\pi_{i,j,r},\ \pi_{i,j,r}\,b_j\) form an \((r+1)\)-edge path from \(a_i\) to \(b_j\); no other edges are present. In particular roots appear on no path, and two roots \(a_i, a_{i'}\) (resp. \(b_j, b_{j'}\)) are never adjacent.
Layer partition. The vertices of the star \(r\)-crossing of order \(n\) are partitioned into \(r + 2\) layers \(L_0, L_1, \ldots, L_{r+1}\):
- \(L_0 := \{a_1, \ldots, a_n\}\),
- \(L_\ell := \{\pi_{i,j,\ell} : i, j \in [n]\}\) for \(\ell \in [r]\),
- \(L_{r+1} := \{b_1, \ldots, b_n\}\).
Write \(\mathcal{L}_{r,n}^{\mathrm{star}} := \{L_0, \ldots, L_{r+1}\}\) for the layer partition.
Flipped star \(r\)-crossing. For \(r \geq 1\) and \(n \in \mathbb{N}\), a graph \(H\) is a flipped star \(r\)-crossing of order \(n\) if there exists a symmetric relation \(F \subseteq (\mathcal{L}_{r,n}^{\mathrm{star}})^2\) such that \(H\) is (isomorphic to) the flip \(\mathrm{Star}_{r,n} \oplus F\) of the star \(r\)-crossing \(\mathrm{Star}_{r,n}\) of order \(n\) via the layer partition \(\mathcal{L}_{r,n}^{\mathrm{star}}\) (Definition Flip).
The number of flipped star \(r\)-crossings of order \(n\) (up to isomorphism) is at most \(2^{(r+2)^2}\). Taking \(F = \emptyset\) gives the (unflipped) star \(r\)-crossing of order \(n\) as a special case.
Review notes
The star \(r\)-crossing of order \(n\) coincides with the \(r\)-subdivided biclique of order \(n\) (Definition Subdivision). Mählmann introduces both names: the former in Section 2.2 (Forbidden Patterns, p. 14) as one of a family of “crossings” (star, clique, half-graph) used to characterize monadic stability and dependence, and the latter implicitly throughout Chapter 13 when analyzing Ramsey-type arguments on bipartite subdivisions (e.g. the statement and proof of Lemma 13.8 on p. 167). We keep both names so that downstream references read faithfully to their sources.
Layers and flipped variants. The layer partition is introduced in the same paragraph on p. 14 and is uniform across the three crossing types (star, clique, half-graph). A flipped \(X\) \(r\)-crossing is any flip of the base \(X\) \(r\)-crossing through its layer partition. We record the layer partition and the flipped variant here for the star case; the clique and half-graph entries follow the same pattern.
Unflipped is a special case. Taking \(F = \emptyset\) in Definition Flip yields \(G \oplus \emptyset = G\), so the unflipped star \(r\)-crossing of order \(n\) is itself a flipped star \(r\)-crossing of order \(n\) (with the trivial flip). This matters for the proof of Lemma WeaklySparseMonDepIsNowhereDense (Lemma 13.7), where an induced unflipped star \(r\)-crossing automatically witnesses the exclusion from Definition MonadicDependence’s clause (3).
Lean encoding: abbrev identity. starCrossing n r is
an abbrev for subdividedBiclique n r from
Definition Subdivision. This means the two graphs
are definitionally equal, which lets the proof of Lemma 13.7 apply
the unflipped-is-flipped bridge without rewriting.
Layer partition is shared. The function
layer : SubdividedBicliqueVert n r → Fin (r + 2) is defined
once in StarCrossing.Contract and re-opened in
CliqueCrossing.Contract and HalfGraphCrossing.Contract.
This matches Mählmann’s single-layer-partition-per-paragraph
(p. 14). The codomain Fin (r + 2) indexes the \(r + 2\)
layers \(L_0, L_1, \ldots, L_{r+1}\); layer v returns the
index of \(v\)’s layer.
Flipped predicate.
IsFlippedStarCrossing H n r is an existential over \((F,
\texttt{Fsymm})\) with \(F : \texttt{Fin (r+2)} \to \texttt{Fin (r+2)}
\to \texttt{Prop}\) symmetric, asking for a graph isomorphism from \(H\)
to flip (starCrossing n r) layer F Fsymm. We carry
Nonempty (...) rather than a raw isomorphism, matching the
“there exists an isomorphism” reading of the source.
Dev/MonadicDependence/StarCrossing/Contract.lean (full)
| 1 | import Mathlib.Combinatorics.SimpleGraph.Maps |
| 2 | import Dev.MonadicDependence.Subdivision.Contract |
| 3 | import Dev.MonadicDependence.Flip.Contract |
| 4 | |
| 5 | namespace Dev.MonadicDependence.StarCrossing |
| 6 | |
| 7 | open Dev.MonadicDependence.Subdivision |
| 8 | open Dev.MonadicDependence.Flip |
| 9 | |
| 10 | /-- The star `r`-crossing of order `n` (Mählmann p. 14): the |
| 11 | `r`-subdivided biclique. It has `2n` roots `a_i, b_j` and, for every |
| 12 | `(i, j) ∈ [n]²`, an internal `r`-vertex path |
| 13 | `a_i — π_{i,j,1} — ⋯ — π_{i,j,r} — b_j`; no other edges are present. |
| 14 | Definitionally equal to `subdividedBiclique n r`. -/ |
| 15 | abbrev starCrossing (n r : ℕ) : SimpleGraph (SubdividedBicliqueVert n r) := |
| 16 | subdividedBiclique n r |
| 17 | |
| 18 | /-- The layer partition of the star / clique / half-graph `r`-crossing |
| 19 | vertex set (`SubdividedBicliqueVert n r`), indexed by `Fin (r + 2)`: |
| 20 | layer `0` = left roots `a_i` (`.inl (.inl _)`); layer `ℓ + 1` for |
| 21 | `ℓ : Fin r` = path vertices `π_{i,j,ℓ+1}` (`.inr ⟨_, ℓ⟩`); layer `r + 1` |
| 22 | = right roots `b_j` (`.inl (.inr _)`). Shared across the three crossing |
| 23 | types. -/ |
| 24 | def layer {n r : ℕ} : SubdividedBicliqueVert n r → Fin (r + 2) |
| 25 | | .inl (.inl _) => ⟨0, by omega⟩ |
| 26 | | .inr ⟨_, ℓ⟩ => ⟨ℓ.val + 1, by omega⟩ |
| 27 | | .inl (.inr _) => ⟨r + 1, by omega⟩ |
| 28 | |
| 29 | /-- A graph `H` is a *flipped star `r`-crossing of order `n`* |
| 30 | (Mählmann p. 14) iff it is isomorphic to `flip (starCrossing n r) layer |
| 31 | F Fsymm` for some symmetric relation `F` on the `r + 2` layers. Taking |
| 32 | `F = ⊥` recovers the unflipped star `r`-crossing as a special case. -/ |
| 33 | def IsFlippedStarCrossing {V : Type*} (H : SimpleGraph V) (n r : ℕ) : Prop := |
| 34 | ∃ (F : Fin (r + 2) → Fin (r + 2) → Prop) (Fsymm : Symmetric F), |
| 35 | Nonempty (H ≃g flip (starCrossing n r) layer F Fsymm) |
| 36 | |
| 37 | end Dev.MonadicDependence.StarCrossing |
| 38 |