Formalizing Structural Graph Theory in Lean 4

No flipped variant. Mählmann explains (p. 15) why no flipped variant of the comparability grid is needed: “any huge flipped comparability grid contains a still large non-flipped comparability grid as an induced subgraph”. We mirror this in our definition, using only the unflipped version as one of the four forbidden patterns in Definition MonadicDependence’s clause (3).

Adjacency convention. The third adjacency condition “\(i < i' \Leftrightarrow j < j'\)” is well-defined precisely when \(i \neq i'\) and \(j \neq j'\); otherwise one of the first two conditions applies, so we never evaluate the third condition with \(i = i'\) or \(j = j'\). In particular, the graph has no self-loops (the condition is restricted to distinct vertices).

Standard name. The same graph is called the “\(n \times n\) comparability grid” in standard graph theory. It is a dense, highly symmetric graph of order \(n^2\); the number of edges is \(n^2(n^2 - 1)/2 \cdot \bigl(\text{adjacency density}\bigr)\), where the adjacency density approaches \(1/2\) as \(n \to \infty\).

Lean encoding. We use SimpleGraph.fromRel over Fin n × Fin n with \[R\ p\ q := (p.1 = q.1) \lor (p.2 = q.2) \lor (p.1 < q.1 \leftrightarrow p.2 < q.2).\] fromRel automatically adds the \(p \neq q\) guard (so no self-loops) and symmetrizes by disjunction. The symmetrization adds \(R\ q\ p = (q.1 = p.1) \lor (q.2 = p.2) \lor (q.1 < p.1 \leftrightarrow q.2 < p.2)\); the first two disjuncts coincide with the forward clauses, and the third disjunct \(q.1 < p.1 \leftrightarrow q.2 < p.2\) coincides with \(p.1 < q.1 \leftrightarrow p.2 < q.2\) whenever both coordinates differ (by trichotomy on Fin n). Hence the adjacency of comparabilityGrid n matches the source verbatim.