D1: directed graph foundations (InfiniteDigraph space)
Sub-issue of the directed umbrella (#84). Mathlib already has the right carrier (Digraph, an arbitrary relation permitting loops, with Fintype instances). Add locally, closely mirroring Graphon/InfiniteGraph.lean (comparatively low risk):
Digraph.comap, relabelling, finite restriction, padding;InfiniteDigraph := Digraph ℕ;- the coordinate equivalence with the Boolean product
(ℕ × ℕ) → Bool (the FULL square including the diagonal — loops are part of the object);
- compact, Polish, standard-Borel instances;
- cylinder generation and finite-restriction measure extensionality.
Relation to the generic AHK framework (#103): the directed carrier is the one-sort, single binary relation, ordered-arguments, diagonal-permitted case of R1 (#104 RelSignature / RelStructure). D1 transports only the carrier, topology, finite restrictions, relabelling, cylinders, and finite-restriction measure extensionality through the Digraph–relational-structure equivalence (an explicit measurable / homeomorphic equivalence, per #109). The compactness-based projective extension is NOT built here — it lives in R2 (#105), and D2 (#86) transports the extension / law theory. Build the extension once in R2; do not re-derive it in D1.
D1: directed graph foundations (InfiniteDigraph space)
Sub-issue of the directed umbrella (#84). Mathlib already has the right carrier (
Digraph, an arbitrary relation permitting loops, with Fintype instances). Add locally, closely mirroringGraphon/InfiniteGraph.lean(comparatively low risk):Digraph.comap, relabelling, finite restriction, padding;InfiniteDigraph := Digraph ℕ;(ℕ × ℕ) → Bool(the FULL square including the diagonal — loops are part of the object);Relation to the generic AHK framework (#103): the directed carrier is the one-sort, single binary relation, ordered-arguments, diagonal-permitted case of R1 (#104
RelSignature/RelStructure). D1 transports only the carrier, topology, finite restrictions, relabelling, cylinders, and finite-restriction measure extensionality through theDigraph–relational-structure equivalence (an explicit measurable / homeomorphic equivalence, per #109). The compactness-based projective extension is NOT built here — it lives in R2 (#105), and D2 (#86) transports the extension / law theory. Build the extension once in R2; do not re-derive it in D1.