Dev.MonadicDependence.HalfGraphCrossing
Definition
For \(r \geq 1\) and \(n \in \mathbb{N}\), the half-graph \(r\)-crossing of order \(n\) has the same vertex set as the star \(r\)-crossing of order \(n\) (Definition StarCrossing): the \(2n\) roots \(a_1, \ldots, a_n, b_1, \ldots, b_n\) and the interior path vertices \(\pi_{i,j,\ell}\) for \((i, j) \in [n]^2\) and \(\ell \in [r]\).
The edges are:
- for every \((i, j) \in [n]^2\), the \(r\) internal-path edges \(\pi_{i,j,1}\,\pi_{i,j,2},\ \ldots,\ \pi_{i,j,r-1}\,\pi_{i,j,r}\);
- for every \(i \in [n]\) and every \((i', j) \in [n]^2\) with \(i \leq i'\), the edge \(a_i\,\pi_{i',j,1}\);
- for every \(j \in [n]\) and every \((i, j') \in [n]^2\) with \(j \leq j'\), the edge \(b_j\,\pi_{i,j',r}\).
No other edges are present. In particular, for \(r \geq 2\), the interior path vertices \(\pi_{i,j,\ell}\) with \(\ell \in [2, r-1]\) still have only their two path-neighbors \(\pi_{i,j,\ell-1}\) and \(\pi_{i,j,\ell+1}\); the half-graph pattern differs from the star \(r\)-crossing only at the ends of the paths (near \(a_i\) and \(b_j\)).
Layer partition. The layer partition is the same as for the star \(r\)-crossing: \(\mathcal{L}_{r,n}^{\mathrm{hg}} := \{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 half-graph \(r\)-crossing. For \(r \geq 1\) and \(n \in \mathbb{N}\), a graph \(H\) is a flipped half-graph \(r\)-crossing of order \(n\) if there exists a symmetric relation \(F \subseteq (\mathcal{L}_{r,n}^{\mathrm{hg}})^2\) such that \(H\) is (isomorphic to) the flip \(\mathrm{HG}_{r,n} \oplus F\) of the half-graph \(r\)-crossing \(\mathrm{HG}_{r,n}\) of order \(n\) via the layer partition \(\mathcal{L}_{r,n}^{\mathrm{hg}}\) (Definition Flip).
The number of flipped half-graph \(r\)-crossings of order \(n\) (up to isomorphism) is at most \(2^{(r+2)^2}\). Taking \(F = \emptyset\) gives the unflipped half-graph \(r\)-crossing of order \(n\).
Review notes
Shared vertex type with Definition StarCrossing.
The half-graph, star, and clique \(r\)-crossings of order \(n\) all live on
the same vertex type SubdividedBicliqueVert n r, introduced in
Definition Subdivision. This matches Mählmann’s
convention on p. 14 (same roots and subdivision vertices across the
three crossing patterns; only the edge set differs). The shared
vertex type is essential for the Lean formulation of
Definition MonadicDependence, where every crossing
is flipped through the same layer function.
Reuse of the layer partition.
Contract.lean reuses
Dev.MonadicDependence.StarCrossing.layer verbatim, matching
Mählmann’s single layer-partition definition on p. 14 used across all
three crossing types.
Encoding of the half-graph end pattern.
The definition uses a single SimpleGraph.fromRel with three
match clauses:
- interior path edges \(\pi_{i,j,\ell} \pi_{i,j,\ell+1}\);
- left end edges \(a_i\,\pi_{i',j,1}\) for \(i \leq i'\);
- right end edges \(b_j\,\pi_{i,j',r}\) for \(j \leq j'\).
The order relations \(i \leq i'\) and \(j \leq j'\) are taken directly on
Fin n, where ≤ is decidable and monotonically
compatible with the natural-number ordering. The \(\leq\) convention
(inclusive, matching the source literally) introduces the reflexive
edges \(a_i \pi_{i,j,1}\) and \(b_j \pi_{i,j,r}\), which coincide with
the star-crossing path edges.
Edge case \(r = 0\).
Mählmann’s definition is “for \(r \geq 1\)”. In Lean, the definition
compiles for \(r = 0\) but yields the empty graph on
SubdividedBicliqueVert n 0 (the path-vertex component is
indexed by Fin 0 = ∅; there are no interior vertices, and the
half-graph end patterns cannot be satisfied — both \(k.\mathrm{val} = 0\)
and \(k.\mathrm{val} = r - 1 = 0\) would require a path vertex
which doesn’t exist). This is outside Mählmann’s scope and downstream
uses always have \(r \geq 1\); we do not specialize the definition.
Imports. Contract.lean imports
Dev.MonadicDependence.StarCrossing.Contract (for
layer) and Dev.MonadicDependence.Flip.Contract (for
flip). The statement_deps in meta.yaml
lists only StarCrossing; Subdivision and
Flip resolve transitively through StarCrossing.
Flipped variant. IsFlippedHalfGraphCrossing H n r is
existentially quantified over a symmetric relation
F : Fin (r + 2) → Fin (r + 2) → Prop, exactly the shape used
in Definition MonadicDependence.
Dev/MonadicDependence/HalfGraphCrossing/Contract.lean (full)
| 1 | import Mathlib.Combinatorics.SimpleGraph.Maps |
| 2 | import Dev.MonadicDependence.Flip.Contract |
| 3 | import Dev.MonadicDependence.StarCrossing.Contract |
| 4 | |
| 5 | namespace Dev.MonadicDependence.HalfGraphCrossing |
| 6 | |
| 7 | open Dev.MonadicDependence.Subdivision |
| 8 | open Dev.MonadicDependence.Flip |
| 9 | open Dev.MonadicDependence.StarCrossing |
| 10 | |
| 11 | /-- The half-graph `r`-crossing of order `n` (Mählmann p. 14). Same |
| 12 | vertex set as the star `r`-crossing (`SubdividedBicliqueVert n r`). |
| 13 | Edges: |
| 14 | |
| 15 | * interior path edges |
| 16 | `π_{i,j,ℓ} — π_{i,j,ℓ+1}` for every `(i, j) ∈ [n]²` and `ℓ ∈ [r − 1]`; |
| 17 | * left half-graph ends `a_i — π_{i',j,1}` for every `i ≤ i'` and |
| 18 | `j ∈ [n]`; |
| 19 | * right half-graph ends `b_j — π_{i,j',r}` for every `j ≤ j'` and |
| 20 | `i ∈ [n]`. |
| 21 | |
| 22 | No other edges. Intended for `r ≥ 1`; for `r = 0` the definition yields |
| 23 | the empty graph on `SubdividedBicliqueVert n 0 ≃ Fin n ⊕ Fin n` (no |
| 24 | path vertices, no root edges), which lies outside Mählmann's scope. -/ |
| 25 | def halfGraphCrossing (n r : ℕ) : SimpleGraph (SubdividedBicliqueVert n r) := |
| 26 | SimpleGraph.fromRel fun x y => |
| 27 | match x, y with |
| 28 | | .inr ⟨e, k⟩, .inr ⟨e', k'⟩ => e = e' ∧ k.val + 1 = k'.val |
| 29 | | .inl (.inl i), .inr ⟨⟨i', _⟩, k⟩ => i ≤ i' ∧ k.val = 0 |
| 30 | | .inl (.inr j), .inr ⟨⟨_, j'⟩, k⟩ => j ≤ j' ∧ k.val = r - 1 |
| 31 | | _, _ => False |
| 32 | |
| 33 | /-- A graph `H` is a *flipped half-graph `r`-crossing of order `n`* |
| 34 | (Mählmann p. 14) iff it is isomorphic to `flip (halfGraphCrossing n r) |
| 35 | layer F Fsymm` for some symmetric relation `F` on the `r + 2` layers. |
| 36 | The layer partition is shared with the star `r`-crossing |
| 37 | (`Dev.MonadicDependence.StarCrossing.layer`). -/ |
| 38 | def IsFlippedHalfGraphCrossing {V : Type*} (H : SimpleGraph V) (n r : ℕ) : Prop := |
| 39 | ∃ (F : Fin (r + 2) → Fin (r + 2) → Prop) (Fsymm : Symmetric F), |
| 40 | Nonempty (H ≃g flip (halfGraphCrossing n r) layer F Fsymm) |
| 41 | |
| 42 | end Dev.MonadicDependence.HalfGraphCrossing |
| 43 |