CausalGraph: Acyclicity, Ancestor Relation

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.

Acyclicity certificates come bundled as Ranking (parents rank strictly below children) and its strict-successor refinement TimeIndex (parents immediately precede children, the time-indexed causal models of [CWL25]); IsDAG.of_depth passes the loose form.

def Causation.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 Causation.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

@[instance_reducible]

instance Causation.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

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

@[instance_reducible]

instance Causation.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

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

@[reducible, inline]

abbrev Causation.CausalGraph.IsDAG {V : Type u_1} (G : CausalGraph V) : Prop

Acyclicity: the strict-ancestor relation is well-founded — no infinite chain of parents. An abbrev for mathlib's IsWellFounded class, so its API (IsWellFounded.wf, induction, fix) applies directly; required by the develop fixpoint and well-founded recursion over the parent relation.

Equations

• G.IsDAG = IsWellFounded V G.IsStrictAncestor

@[reducible, inline]

abbrev Causation.CausalGraph.Ranking {V : Type u_1} (G : CausalGraph V) : Type u_1

A ranking of a causal graph is a relation homomorphism from the parent relation into < on ℕ — mathlib's RelHom, so the bundled form of the depth certificate consumed by IsDAG.of_depth and, per model, by the fuel bridges.

Equations

• G.Ranking = ((fun (x1 x2 : V) => x1 ∈ G.parents x2) →r fun (x1 x2 : ℕ) => x1 < x2)

theorem Causation.CausalGraph.Ranking.isDAG {V : Type u_1} {G : CausalGraph V} (r : G.Ranking) : G.IsDAG

A ranking certifies acyclicity: well-foundedness transfers along the homomorphism (RelHomClass.wellFounded) and lifts to the transitive closure (WellFounded.transGen).

theorem Causation.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

A graph is acyclic if every edge strictly decreases some ℕ-valued depth function — Ranking.isDAG with the certificate passed loose.

structure Causation.CausalGraph.TimeIndex {V : Type u_1} (G : CausalGraph V) : Type u_1

A time index for a causal graph is a timestep assignment on which each parent sits exactly one step before its children — the time-indexed causal models of [CWL25] (their definition 1) and [CGK+23].

• time : V → ℕ

  The timestep of each variable.

• parent_succ {u v : V} : u ∈ G.parents v → self.time u + 1 = self.time v

  Parents immediately precede their children.

def Causation.CausalGraph.TimeIndex.toRanking {V : Type u_1} {G : CausalGraph V} (ti : G.TimeIndex) : G.Ranking

The ranking underlying a time index.

Equations

• ti.toRanking = { toFun := ti.time, map_rel' := ⋯ }

theorem Causation.CausalGraph.TimeIndex.isDAG {V : Type u_1} {G : CausalGraph V} (ti : G.TimeIndex) : G.IsDAG

A time index certifies acyclicity.