CausalGraph: Bare Directed Graph over a Vertex Type (V2)

A CausalGraph V is the underlying DAG topology of a structural causal model: just parents : V → Finset V. No mechanisms, no value types, no acyclicity hypothesis (that lives in Graph/Basic.lean as the IsDAG mixin).

This separation mirrors mathlib's Mathlib/Combinatorics/Digraph/Basic.lean (structure Digraph V where adj : V → V → Prop) but uses Finset V parents because Pearl SEM API consumes parent enumerations directly (mechanisms fold over parents v).

structure Core.Causal.CausalGraph (V : Type u_1) : Type u_1

A directed graph over V represented by parent finsets. The graph structure is value-type-agnostic: mechanisms and values layer on top via Mechanism and Valuation.

• parents : V → Finset V

  The set of parents of each vertex.

def Core.Causal.CausalGraph.empty {V : Type u_1} : CausalGraph V

The empty graph: every vertex is a root.

Equations

• Core.Causal.CausalGraph.empty = { parents := fun (x : V) => ∅ }

@[implicit_reducible]

instance Core.Causal.CausalGraph.instInhabited {V : Type u_1} : Inhabited (CausalGraph V)

Equations

• Core.Causal.CausalGraph.instInhabited = { default := Core.Causal.CausalGraph.empty }

def Core.Causal.CausalGraph.isRoot {V : Type u_1} (G : CausalGraph V) (v : V) : Prop

A vertex is a root iff it has no parents.

Equations

• G.isRoot v = (G.parents v = ∅)

@[implicit_reducible]

instance Core.Causal.CausalGraph.instDecidableIsRootOfDecidableEq {V : Type u_1} (G : CausalGraph V) (v : V) [DecidableEq V] : Decidable (G.isRoot v)

Equations

• G.instDecidableIsRootOfDecidableEq v = Core.Causal.CausalGraph.instDecidableIsRootOfDecidableEq._aux_1 G v

def Core.Causal.CausalGraph.children {V : Type u_1} (G : CausalGraph V) [DecidableEq V] [Fintype V] (v : V) : Finset V

The children of a vertex: vertices u for which v ∈ parents u. Requires [DecidableEq V] [Fintype V] to enumerate candidates.

Equations

• G.children v = {u : V | v ∈ G.parents u}

@[simp]

theorem Core.Causal.CausalGraph.mem_children_iff {V : Type u_1} (G : CausalGraph V) [DecidableEq V] [Fintype V] {u v : V} : u ∈ G.children v ↔ v ∈ G.parents u

@[simp]

theorem Core.Causal.CausalGraph.isRoot_iff_parents_empty {V : Type u_1} (G : CausalGraph V) (v : V) : G.isRoot v ↔ G.parents v = ∅

theorem Core.Causal.CausalGraph.isRoot_iff_card_zero {V : Type u_1} (G : CausalGraph V) (v : V) : G.isRoot v ↔ (G.parents v).card = 0