CausalGraph: Acyclicity, Ancestor Relation (V2)

IsDAG is a Prop mixin class on CausalGraph V (mirroring IsMarkovKernel from Mathlib/Probability/Kernel/Defs.lean): required only by operations that genuinely need acyclicity (topological sort, well-founded fixpoint induction).

The ancestor relation uses Relation.ReflTransGen directly (no intermediate adapter); consumers can use mathlib's existing API for reflexive-transitive closures.

def Core.Causal.CausalGraph.IsAncestor {V : Type u_1} (G : CausalGraph V) : V → V → Prop

IsAncestor G u v iff there is a chain v ← w₁ ← ... ← u via parents. Defined via mathlib's Relation.ReflTransGen over the inlined "is-parent-of" relation.

Equations

• G.IsAncestor = Relation.ReflTransGen fun (u v : V) => u ∈ G.parents v

def Core.Causal.CausalGraph.IsStrictAncestor {V : Type u_1} (G : CausalGraph V) : V → V → Prop

IsStrictAncestor G u v iff there is a nonempty chain via parents. Defined via mathlib's Relation.TransGen.

Equations

• G.IsStrictAncestor = Relation.TransGen fun (u v : V) => u ∈ G.parents v

@[implicit_reducible]

instance Core.Causal.CausalGraph.IsAncestor.decidable {V : Type u_1} [Fintype V] [DecidableEq V] (G : CausalGraph V) (u v : V) : Decidable (G.IsAncestor u v)

Decidable (G.IsAncestor u v) via the Core.Relation.ReflTransGen substrate's Fintype headline. The relation fun u v => u ∈ G.parents v has decidable successors G.children u (already defined as Finset.univ.filter (v ∈ G.parents ·) in Defs.lean).

Equations

• Core.Causal.CausalGraph.IsAncestor.decidable G u v = Relation.ReflTransGen.decidable_of_fintype_step G.children ⋯ u v

@[implicit_reducible]

instance Core.Causal.CausalGraph.IsStrictAncestor.decidable {V : Type u_1} [Fintype V] [DecidableEq V] (G : CausalGraph V) (u v : V) : Decidable (G.IsStrictAncestor u v)

Decidable (G.IsStrictAncestor u v) via the substrate's TransGen Fintype headline.

Equations

• Core.Causal.CausalGraph.IsStrictAncestor.decidable G u v = Relation.ReflTransGen.decidable_TransGen_of_fintype_step G.children ⋯ u v

class Core.Causal.CausalGraph.IsDAG {V : Type u_1} (G : CausalGraph V) : Prop

Acyclicity mixin: the strict-ancestor relation is well-founded — no infinite chain of parents. Required by topologicalOrder, develop fixpoint, and well-founded recursion over the parent relation.

Mathlib analogue: IsMarkovKernel from Mathlib.Probability.Kernel.Defs — a Prop class on a value of a structure, marking a property consumers may require.

A Std.Irrefl instance for IsStrictAncestor follows from well-foundedness; deferred until a consumer needs it.

• wf : WellFounded G.IsStrictAncestor

  The strict-ancestor relation has no infinite descending chain.

theorem Core.Causal.CausalGraph.IsDAG.of_depth {V : Type u_1} (G : CausalGraph V) (depth : V → ℕ) (hdepth : ∀ {u v : V}, u ∈ G.parents v → depth u < depth v) : G.IsDAG

Depth-based IsDAG construction: a graph is acyclic if every edge strictly decreases some ℕ-valued depth function (parent depth < child depth). Reuses Subrelation.wf over InvImage Nat.lt depth, which is well-founded by Nat's standard wellfoundedness.

The standard mathlib pattern for proving wellfoundedness of finite inductive relations: define a measure into ℕ, show the relation decreases it, conclude.