gen
plain-language theorem explainer
Defines the directed base adjacency relation of a finite world: two vertices are adjacent exactly when their ordered pair appears in the edge list. Anyone counting locked domains or interface components cites it as the generator of the path-equivalence. The body is pure list membership; orientation is later erased by equivalence closure.
Claim. Given a finite vertex type $V$ and an edge list $E$ of ordered pairs in $V\times V$, the base adjacency predicate holds of $(a,b)$ if and only if $(a,b)\in E$.
background
The module proves a dimension-free bound on locked domains in Recognition cosmogenesis: on any finite connected world, the number of monochromatic components is at most the number of bichromatic (interface) edges plus one. A world is a finite vertex type $V$ with a charge colouring $c:V\to\beta$ and an adjacency list $E:\mathrm{List}(V\times V)$ (4-neighbour diamond in 2D, 6-neighbour octahedron in 3D, line in 1D).
Monochromatic edges generate locked domains; bichromatic edges form the interface. Component count is the cardinality of the quotient by the equivalence closure of the edge relation. This definition supplies that raw edge relation before symmetrization or path-closure: membership of an ordered pair in $E$.
Downstream, the connectivity closure is the least equivalence containing this relation, so two vertices are related exactly when a path of edges joins them. The orientation of each pair is irrelevant once that closure is taken.
proof idea
One-line definitional abbreviation: the predicate is list membership of the ordered pair in $E$. No lemmas, tactics, or algebraic reduction.
why it matters
This is the atomic adjacency seed for the whole interface-component stack. The immediate consumer is the connectivity closure clos, defined as the equivalence generated by this relation; that closure underwrites component counting via Nat.card of the quotient under only Finite V.
From there the module builds the merge bounds (comp_le_comp_cons, comp_le_comp_append) and the headline inequality that monochromatic components are at most bichromatic edges plus one, closing the open connected-graph fact from the 2D/3D domain-coarsening engines. Connectivity of the ambient lattices is discharged by descent-height criteria on diamonds and octahedra.
In the broader Recognition picture this is graph infrastructure for domain coarsening under the recognition pull, not a forcing-chain (T0–T8) step; it makes the locked-domain bound a theorem rather than a numeric check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.