Support geometry of digraph coordinates (shared regression infrastructure)

The support of a digraph coordinate, in its own module so that the foundational relational/directed carrier Graphon.InfiniteDigraph (D1) does not depend on the equality-pattern layer Graphon.RelEqualityPattern, where RelCoord.support is defined. Every D1 consumer would otherwise inherit that dependency for the sake of two lemmas neither it nor they use — the same reason Graphon.SimpleGraphDigraphBridge keeps SimpleGraph out of D1.

Both regressions for the R4 successor contract (#196) were proving this geometry independently; it is stated here once, over an arbitrary vertex type.

The pair is stated with [DecidableEq V] and proved by membership rather than by unfolding an image. That is not a stylistic choice: RelCoord.support is built with the classical instance, and over a concrete carrier the natural DecidableEq is not definitionally equal to it, so an image-shaped statement would be unusable at exactly the sites that need it.

theorem support_digraphCoord {V : Type u_1} [DecidableEq V] (a b : V) : (digraphCoord a b).support = {⟨(), a⟩, ⟨(), b⟩}

The support of a digraph coordinate is the pair of its endpoints. Proved by membership, so that the DecidableEq instance forming the pair is the caller's rather than the classical one used to build RelCoord.support.

theorem card_support_digraphCoord {V : Type u_1} [DecidableEq V] {a b : V} (hab : a ≠ b) : (digraphCoord a b).support.card = 2

An off-diagonal digraph coordinate has a two-point support.