Dev/MonadicDependence/ComparabilityGrid/Contract.lean
| 1 | import Mathlib.Combinatorics.SimpleGraph.Basic |
| 2 | |
| 3 | namespace Dev.MonadicDependence.ComparabilityGrid |
| 4 | |
| 5 | /-- The comparability grid of order `n` (Mählmann, p. 15) is the graph on |
| 6 | vertex set `Fin n × Fin n` in which two distinct vertices `(i, j)` and |
| 7 | `(i', j')` are adjacent iff at least one of: `i = i'` (same row), |
| 8 | `j = j'` (same column), or `i < i' ↔ j < j'` (comparable — ordered the |
| 9 | same way in both coordinates). |
| 10 | |
| 11 | Built with `SimpleGraph.fromRel`, which adds the `p ≠ q` guard and |
| 12 | symmetrizes by disjunction. The extra disjunct from symmetrization, |
| 13 | `j' < j ↔ i' < i`, coincides with `i < i' ↔ j < j'` whenever the two |
| 14 | pairs differ in both coordinates (by trichotomy on `Fin n`), so the |
| 15 | adjacency of `comparabilityGrid n` matches the source verbatim — see |
| 16 | `review.tex`. -/ |
| 17 | def comparabilityGrid (n : ℕ) : SimpleGraph (Fin n × Fin n) := |
| 18 | SimpleGraph.fromRel fun p q => |
| 19 | p.1 = q.1 ∨ p.2 = q.2 ∨ (p.1 < q.1 ↔ p.2 < q.2) |
| 20 | |
| 21 | end Dev.MonadicDependence.ComparabilityGrid |
| 22 |