Child of #103; depends on R0 (#110). The carrier + coordinate/cylinder/extensionality layer for multi-sorted relational structures, generalizing Graphon/InfiniteGraph.lean so digraphs (#85) and bipartite arrays are instances. The compactness-based projective extension belongs to R2 (#105), not here.
Exact carrier:
abbrev RelCoord (Σ : RelSignature) (V : Σ.Sort → Type) :=
Σ R : Σ.Rel, (i : Fin (Σ.arity R)) → V (Σ.argSort R i)
def RelStructure (Σ : RelSignature) (V : Σ.Sort → Type) := RelCoord Σ V → Bool
-- carriers
Vfinite (n : Σ.Sort → ℕ) (s : Σ.Sort) := Fin (n s)
Vinfinite (s : Σ.Sort) := ℕ
Boolean relations only (drop any finite value type — that is a later extension; Boolean is already a large campaign).
Deliverables:
- the coordinate product /
RelStructure with its Boolean-product coordinate equivalence;
- restriction to finite size-vectors, sortwise relabelling, padding;
- compact, Polish, standard-Borel instances (via the coordinate equivalence, as for
InfiniteGraph);
- cylinder π-system generation and finite-restriction measure extensionality.
Correction: the current InfiniteGraph is the existing graph carrier; #85 is the digraph issue (not graphs). Keep R1 the single reusable coordinate/cylinder layer; specialize, don't rebuild.
Child of #103; depends on R0 (#110). The carrier + coordinate/cylinder/extensionality layer for multi-sorted relational structures, generalizing
Graphon/InfiniteGraph.leanso digraphs (#85) and bipartite arrays are instances. The compactness-based projective extension belongs to R2 (#105), not here.Exact carrier:
Boolean relations only (drop any finite value type — that is a later extension; Boolean is already a large campaign).
Deliverables:
RelStructurewith its Boolean-product coordinate equivalence;InfiniteGraph);Correction: the current
InfiniteGraphis the existing graph carrier; #85 is the digraph issue (not graphs). Keep R1 the single reusable coordinate/cylinder layer; specialize, don't rebuild.