The root-sink expressibility lemma (A2)

Statements split from the original Statements.lean skeleton (one file per proving task); see AUDIT-NOTES A2 and papers/inflation-nontermination/paper/sections/12-pair-source.tex (Lemma lem:rootsink) for the mathematics.

isAISet_iff_decomposition, isAISet_glue and gExpFeasible_iff_gAIFeasible are proved. Two statements of the original skeleton were false as written and have been removed: gInjectable_iff_raw needed 1 ≤ t (the corrected form is gInjectable_iff_raw_of_one_le, and not_forall_gInjectable_iff_raw refutes the unrestricted one), and expressible_iff_ai holds only for targets satisfying the ancestral-independence prescriptions (its intended content is Expressible.isAISet together with gExpFeasible_iff_gAIFeasible). The two consequences flip_gExpFeasible and compatible_gExpFeasible are proved at the end of this file from the root-sink lemma. Everything in this file is proved.

Auxiliary material

Everything in this section is new; the five statements of the task are unchanged and appear below in their original form.

Incidence, ancestors and the shared-parent relation

theorem TriangleInflation.Graph.RootSinkAux.inc_nonempty {Γ : PairGraph} (v : Γ.V) : (Γ.inc v).Nonempty

No vertex is isolated, so every vertex is incident to a source.

theorem TriangleInflation.Graph.RootSinkAux.gAncestors_nonempty {Γ : PairGraph} {t : ℕ} (o : GObs Γ t) : (gAncestors o).Nonempty

Every copied observation has at least one copied latent ancestor.

theorem TriangleInflation.Graph.RootSinkAux.sharesParent_refl {Γ : PairGraph} {t : ℕ} (o : GObs Γ t) : SharesParent o o

theorem TriangleInflation.Graph.RootSinkAux.sharesParent_symm {Γ : PairGraph} {t : ℕ} {o p : GObs Γ t} (h : SharesParent o p) : SharesParent p o

theorem TriangleInflation.Graph.RootSinkAux.not_sharesParent_of_ai {Γ : PairGraph} {t : ℕ} {S T : Finset (GObs Γ t)} (h : GAncestrallyIndependent S T) {o p : GObs Γ t} (ho : o ∈ S) (hp : p ∈ T) : ¬SharesParent o p

theorem TriangleInflation.Graph.RootSinkAux.ai_of_not_sharesParent {Γ : PairGraph} {t : ℕ} {S T : Finset (GObs Γ t)} (h : ∀ o ∈ S, ∀ p ∈ T, ¬SharesParent o p) : GAncestrallyIndependent S T

theorem TriangleInflation.Graph.RootSinkAux.gAI_symm {Γ : PairGraph} {t : ℕ} {S T : Finset (GObs Γ t)} (h : GAncestrallyIndependent S T) : GAncestrallyIndependent T S

theorem TriangleInflation.Graph.RootSinkAux.disjoint_of_ai {Γ : PairGraph} {t : ℕ} {S T : Finset (GObs Γ t)} (h : GAncestrallyIndependent S T) : Disjoint S T

theorem TriangleInflation.Graph.RootSinkAux.GInjectable.mono {Γ : PairGraph} {t : ℕ} {S T : Finset (GObs Γ t)} (hST : S ⊆ T) (h : GInjectable T) : GInjectable S

Connectivity in the shared-parent graph, on the ambient type

def TriangleInflation.Graph.RootSinkAux.connStep {Γ : PairGraph} {t : ℕ} (S : Finset (GObs Γ t)) (x y : GObs Γ t) : Prop

One step of the shared-parent graph on S.

Equations

• TriangleInflation.Graph.RootSinkAux.connStep S x y = (x ∈ S ∧ y ∈ S ∧ TriangleInflation.Graph.SharesParent x y)

def TriangleInflation.Graph.RootSinkAux.conn {Γ : PairGraph} {t : ℕ} (S : Finset (GObs Γ t)) : GObs Γ t → GObs Γ t → Prop

Connectivity in the shared-parent graph on S, phrased on the ambient type rather than on the subtype, so that the same statement can be read for different ambient sets.

Equations

• TriangleInflation.Graph.RootSinkAux.conn S = Relation.ReflTransGen (TriangleInflation.Graph.RootSinkAux.connStep S)

theorem TriangleInflation.Graph.RootSinkAux.conn_refl {Γ : PairGraph} {t : ℕ} (S : Finset (GObs Γ t)) (a : GObs Γ t) : conn S a a

theorem TriangleInflation.Graph.RootSinkAux.conn_mem_right {Γ : PairGraph} {t : ℕ} {S : Finset (GObs Γ t)} {a b : GObs Γ t} (h : conn S a b) (ha : a ∈ S) : b ∈ S

theorem TriangleInflation.Graph.RootSinkAux.conn_symm {Γ : PairGraph} {t : ℕ} {S : Finset (GObs Γ t)} {a b : GObs Γ t} (h : conn S a b) : conn S b a

theorem TriangleInflation.Graph.RootSinkAux.conn_trans {Γ : PairGraph} {t : ℕ} {S : Finset (GObs Γ t)} {a b c : GObs Γ t} (h : conn S a b) (h' : conn S b c) : conn S a c

theorem TriangleInflation.Graph.RootSinkAux.conn_mono {Γ : PairGraph} {t : ℕ} {S T : Finset (GObs Γ t)} (hST : S ⊆ T) {a b : GObs Γ t} (h : conn S a b) : conn T a b

theorem TriangleInflation.Graph.RootSinkAux.conn_restrict {Γ : PairGraph} {t : ℕ} {S T : Finset (GObs Γ t)} {a b : GObs Γ t} (hcl : ∀ (p : GObs Γ t), conn T a p → p ∈ S) (h : conn T a b) : conn S a b

If everything connected to a inside T already lies in the smaller set S, then connectivity inside T from a is connectivity inside S.

theorem TriangleInflation.Graph.RootSinkAux.conn_of_sharedComponent {Γ : PairGraph} {t : ℕ} {S : Finset (GObs Γ t)} {x y : ↥S} (h : sharedComponent S x y) : conn S ↑x ↑y

theorem TriangleInflation.Graph.RootSinkAux.sharedComponent_of_conn {Γ : PairGraph} {t : ℕ} {S : Finset (GObs Γ t)} {a b : GObs Γ t} (h : conn S a b) (ha : a ∈ S) (hb : b ∈ S) : sharedComponent S ⟨a, ha⟩ ⟨b, hb⟩

theorem TriangleInflation.Graph.RootSinkAux.isAISet_iff_conn {Γ : PairGraph} {t : ℕ} (S : Finset (GObs Γ t)) : IsAISet S ↔ ∀ o ∈ S, ∃ (B : Finset (GObs Γ t)), (∀ (p : GObs Γ t), p ∈ B ↔ conn S o p) ∧ GInjectable B

IsAISet in terms of conn: every component, described by conn, is injectable.

Components and decompositions

theorem TriangleInflation.Graph.RootSinkAux.exists_aiDecomposition_aux {Γ : PairGraph} {t : ℕ} (n : ℕ) (S : Finset (GObs Γ t)) : S.card ≤ n → IsAISet S → ∃ (D : AIDecomposition S), ∀ (m : Fin D.n), ∀ p ∈ D.block m, ∀ (q : GObs Γ t), q ∈ D.block m ↔ conn S p q

Every AI set has an AI decomposition: peel off the component of one member.

theorem TriangleInflation.Graph.RootSinkAux.isAISet_of_decomposition {Γ : PairGraph} {t : ℕ} {S : Finset (GObs Γ t)} (D : AIDecomposition S) : IsAISet S

A set with an AI decomposition is an AI set: the component of a member is contained in any block containing it, because a step of the shared-parent graph cannot leave a block.

Chains, trails and d-separation

theorem TriangleInflation.Graph.RootSinkAux.exists_chain_of_conn {Γ : PairGraph} {t : ℕ} {S : Finset (GObs Γ t)} {a b : GObs Γ t} (h : conn S a b) : a = b ∨ ∃ (mid : List (GObs Γ t)), (∀ c ∈ mid, c ∈ S) ∧ List.IsChain SharesParent (a :: (mid ++ [b]))

Connectivity inside S is witnessed by a chain whose interior lies in S.

theorem TriangleInflation.Graph.RootSinkAux.exists_activeTrail {Γ : PairGraph} {t : ℕ} {X Y Z : Finset (GObs Γ t)} (n : ℕ) (a b : GObs Γ t) (mid : List (GObs Γ t)) : mid.length ≤ n → a ∈ X → b ∈ Y → (∀ c ∈ mid, c ∈ X ∪ Y ∪ Z) → List.IsChain SharesParent (a :: (mid ++ [b])) → ∃ (o₀ : GObs Γ t) (m : List (GObs Γ t)) (o₁ : GObs Γ t), ActiveTrail X Y Z o₀ m o₁

A chain from X to Y inside X ∪ Y ∪ Z yields a trail that is active given Z: cut the chain at the first place where it returns to X or reaches Y.

theorem TriangleInflation.Graph.RootSinkAux.not_conn_of_dsep {Γ : PairGraph} {t : ℕ} {X Y Z : Finset (GObs Γ t)} (hXY : Disjoint X Y) (hd : dsep X Y Z) {a b : GObs Γ t} (ha : a ∈ X) (hb : b ∈ Y) : ¬conn (X ∪ Y ∪ Z) a b

d-separation forbids connectivity from X to Y inside X ∪ Y ∪ Z.

Injectability

theorem TriangleInflation.Graph.RootSinkAux.mem_copySet_iff {Γ : PairGraph} {t : ℕ} {ι : Γ.Edge → Fin t} {o : GObs Γ t} : o ∈ copySet ι ↔ ∀ (e : ↥(Γ.inc o.fst)), o.snd e = ι ↑e

theorem TriangleInflation.Graph.RootSinkAux.gInjectable_iff_raw_of_one_le {Γ : PairGraph} {t : ℕ} (ht : 1 ≤ t) (S : Finset (GObs Γ t)) : GInjectable S ↔ GInjectableRaw S

AUDIT-NOTES A1/A2: for 1 ≤ t the working definition of injectability agrees with the primitive Wolfe–Spekkens–Fritz condition. The hypothesis 1 ≤ t is needed for the backward direction: it supplies a copy index for the sources that the set leaves unconstrained.

Pushforward helpers

theorem TriangleInflation.Graph.RootSinkAux.pushforward_mono_of_subset {Γ : PairGraph} {t : ℕ} {S T : Finset (GObs Γ t)} (hST : S ⊆ T) {Δ : GAssign Γ t → ℝ} (hΔ : ∀ (ω : GAssign Γ t), 0 ≤ Δ ω) (φ : ↥T → Bool) : pushforward Δ (gRestrict T) φ ≤ pushforward Δ (gRestrict S) (subRestrict hST φ)

Restricting further can only increase the mass of a fibre: the marginal of a nonnegative weight on a smaller set dominates the marginal on a larger one.

The marginal of an AI set

theorem TriangleInflation.Graph.RootSinkAux.readOnBlock_self {Γ : PairGraph} {t : ℕ} {S : Finset (GObs Γ t)} (φ : ↥S → Bool) : readOnBlock S S φ = φ

theorem TriangleInflation.Graph.RootSinkAux.readOnBlock_sub {Γ : PairGraph} {t : ℕ} {B A W : Finset (GObs Γ t)} (hBA : B ⊆ A) (hAW : A ⊆ W) (φ : ↥W → Bool) : readOnBlock B A (subRestrict hAW φ) = readOnBlock B W φ

theorem TriangleInflation.Graph.RootSinkAux.marginal_eq_aiProduct {Γ : PairGraph} {t : ℕ} {Δ : GAssign Γ t → ℝ} {P : GTarget Γ} (hprod : GAncestralProducts t Δ P) {S : Finset (GObs Γ t)} (D : AIDecomposition S) : pushforward Δ (gRestrict S) = aiProduct S D P

Under a witness satisfying the ancestral-independence prescriptions, the marginal on a set with an AI decomposition is the product of the injectable marginals of its blocks.

theorem TriangleInflation.Graph.RootSinkAux.conn_component_side {Γ : PairGraph} {t : ℕ} {X Y Z : Finset (GObs Γ t)} (hXY : Disjoint X Y) (hd : dsep X Y Z) {o : GObs Γ t} (ho : o ∈ X ∪ Y ∪ Z) : (∀ (p : GObs Γ t), conn (X ∪ Y ∪ Z) o p → p ∈ X ∪ Z) ∨ ∀ (p : GObs Γ t), conn (X ∪ Y ∪ Z) o p → p ∈ Y ∪ Z

Under d-separation, the component of a member of X ∪ Y ∪ Z in the shared-parent graph lies inside X ∪ Z or inside Y ∪ Z: a shortest path joining X to Y inside a component has all its interior in Z, so it is an active trail.

theorem TriangleInflation.Graph.RootSinkAux.not_forall_gInjectable_iff_raw : ¬∀ (Γ : PairGraph) (t : ℕ) (S : Finset (GObs Γ t)), GInjectable S ↔ GInjectableRaw S

The unrestricted form of gInjectable_iff_raw_of_one_le is false: at t = 0 a scenario with a vertex has no copied observations at all (every vertex is incident to a source, and there is no map from a nonempty type to Fin 0), so the only set of copied observations is ∅. That set satisfies the primitive Wolfe–Spekkens–Fritz condition vacuously, while GInjectable ∅ asks for a global index assignment Γ.Edge → Fin 0, which does not exist.

A2: the root-sink expressibility lemma

theorem TriangleInflation.Graph.isAISet_iff_decomposition {Γ : PairGraph} {t : ℕ} (S : Finset (GObs Γ t)) : IsAISet S ↔ Nonempty (AIDecomposition S)

An AI set is exactly a set presented as a union of pairwise ancestrally independent injectable blocks: the blocks may be taken to be the connected components of the shared-parent graph (AUDIT-NOTES A2).

theorem TriangleInflation.Graph.isAISet_glue {Γ : PairGraph} {t : ℕ} {X Y Z : Finset (GObs Γ t)} (hX : IsAISet (X ∪ Z)) (hY : IsAISet (Y ∪ Z)) (hXY : Disjoint X Y) (hd : dsep X Y Z) : IsAISet (X ∪ Y ∪ Z)

AUDIT-NOTES A2, the geometric half of the root-sink lemma. If X ∪ Z and Y ∪ Z are AI sets and X is d-separated from Y by Z, then every connected component of the shared-parent graph on X ∪ Y ∪ Z lies inside X ∪ Z or inside Y ∪ Z, hence is injectable, so X ∪ Y ∪ Z is again an AI set. (Take a shortest path inside a component from X to Y: its internal vertices lie in Z, so it is an active trail.)

Consequences of the glue lemma

Subsets of AI sets are AI sets, so every expressible set is an AI set.

theorem TriangleInflation.Graph.RootSinkAux.isAISet_subset {Γ : PairGraph} {t : ℕ} {S S' : Finset (GObs Γ t)} (hS : IsAISet S) (hsub : S' ⊆ S) : IsAISet S'

theorem TriangleInflation.Graph.RootSinkAux.isAISet_of_injectable {Γ : PairGraph} {t : ℕ} {S : Finset (GObs Γ t)} (hS : GInjectable S) : IsAISet S

theorem TriangleInflation.Graph.RootSinkAux.Expressible.isAISet {Γ : PairGraph} {t : ℕ} {P : GTarget Γ} {S : Finset (GObs Γ t)} {μ : (↥S → Bool) → ℝ} (h : Expressible t P S μ) : IsAISet S

Every recursively expressible set is an AI set (AUDIT-NOTES A2).

From the AI prescriptions to the expressible prescriptions

def TriangleInflation.Graph.RootSinkAux.restrictDecomp {Γ : PairGraph} {t : ℕ} {W : Finset (GObs Γ t)} (D : AIDecomposition W) (A : Finset (GObs Γ t)) (hA : A ⊆ W) : AIDecomposition A

Intersecting the blocks of an AI decomposition of W with a subset A gives an AI decomposition of A.

Equations

• TriangleInflation.Graph.RootSinkAux.restrictDecomp D A hA = { n := D.n, block := fun (m : Fin D.n) => D.block m ∩ A, inj := ⋯, ai := ⋯, cover := ⋯ }

theorem TriangleInflation.Graph.RootSinkAux.marginal_sub_eq_prod {Γ : PairGraph} {t : ℕ} {Δ : GAssign Γ t → ℝ} {P : GTarget Γ} (hprod : GAncestralProducts t Δ P) {W A : Finset (GObs Γ t)} (D : AIDecomposition W) (hA : A ⊆ W) (φ : ↥W → Bool) : pushforward Δ (gRestrict A) (subRestrict hA φ) = ∏ m : Fin D.n, pushforward P (gPartyRead (D.block m ∩ A)) (readOnBlock (D.block m ∩ A) W φ)

theorem TriangleInflation.Graph.RootSinkAux.expPrescriptions_of_ai {Γ : PairGraph} {t : ℕ} {Δ : GAssign Γ t → ℝ} {P : GTarget Γ} (hlaw : IsLaw Δ) (hinjm : GInjectableMarginals t Δ P) (hprod : GAncestralProducts t Δ P) (S : Finset (GObs Γ t)) (μ : (↥S → Bool) → ℝ) : Expressible t P S μ → pushforward Δ (gRestrict S) = μ

AUDIT-NOTES A2: a witness satisfying the injectable and ancestral-independence prescriptions satisfies every expressible prescription.

From the expressible prescriptions to the AI prescriptions

theorem TriangleInflation.Graph.RootSinkAux.readOnBlock_eq_subRestrict {Γ : PairGraph} {t : ℕ} {B W : Finset (GObs Γ t)} (h : B ⊆ W) (φ : ↥W → Bool) : readOnBlock B W φ = subRestrict h φ

theorem TriangleInflation.Graph.RootSinkAux.castMem {Γ : PairGraph} {t : ℕ} {S T : Finset (GObs Γ t)} (h : S = T) {p : GObs Γ t} (hp : p ∈ S) : p ∈ T

Transport of membership along an equality of sets.

theorem TriangleInflation.Graph.RootSinkAux.Expressible.reindex {Γ : PairGraph} {t : ℕ} {P : GTarget Γ} {S T : Finset (GObs Γ t)} (h : S = T) {μ : (↥S → Bool) → ℝ} (hμ : Expressible t P S μ) : Expressible t P T fun (ψ : ↥T → Bool) => μ fun (o : ↥S) => ψ ⟨↑o, ⋯⟩

Expressibility transports along an equality of sets.

theorem TriangleInflation.Graph.RootSinkAux.pushforward_gRestrict_reindex {Γ : PairGraph} {t : ℕ} {S T : Finset (GObs Γ t)} (h : S = T) (Δ : GAssign Γ t → ℝ) (ψ : ↥T → Bool) : (pushforward Δ (gRestrict S) fun (o : ↥S) => ψ ⟨↑o, ⋯⟩) = pushforward Δ (gRestrict T) ψ

theorem TriangleInflation.Graph.RootSinkAux.eq_of_empty_fun {Γ : PairGraph} {t : ℕ} (a b : ↥∅ → Bool) : a = b

theorem TriangleInflation.Graph.RootSinkAux.pushforward_to_empty {Γ : PairGraph} {t : ℕ} {S : Finset (GObs Γ t)} (ν : (↥S → Bool) → ℝ) (h : ∅ ⊆ S) (χ : ↥∅ → Bool) : pushforward ν (subRestrict h) χ = ∑ ψ : ↥S → Bool, ν ψ

theorem TriangleInflation.Graph.RootSinkAux.dsep_empty_of_ai {Γ : PairGraph} {t : ℕ} {A B : Finset (GObs Γ t)} (hAB : GAncestrallyIndependent A B) : dsep A B ∅

Ancestrally independent sets are d-separated by the empty set: a trail between them would need an interior vertex, which the empty conditioning set cannot supply.

theorem TriangleInflation.Graph.RootSinkAux.expressible_union_of_ai {Γ : PairGraph} {t : ℕ} {P : GTarget Γ} {A B : Finset (GObs Γ t)} {νA : (↥A → Bool) → ℝ} {νB : (↥B → Bool) → ℝ} (hA : Expressible t P A νA) (hB : Expressible t P B νB) (hAB : GAncestrallyIndependent A B) : ∃ (μ : (↥(A ∪ B) → Bool) → ℝ), Expressible t P (A ∪ B) μ

Two ancestrally independent expressible sets glue, with Z = ∅, to their union.

theorem TriangleInflation.Graph.RootSinkAux.marginal_union_of_ai {Γ : PairGraph} {t : ℕ} {Δ : GAssign Γ t → ℝ} {P : GTarget Γ} (hlaw : IsLaw Δ) (hexp : ∀ (S : Finset (GObs Γ t)) (μ : (↥S → Bool) → ℝ), Expressible t P S μ → pushforward Δ (gRestrict S) = μ) {A B : Finset (GObs Γ t)} {νA : (↥A → Bool) → ℝ} {νB : (↥B → Bool) → ℝ} (hA : Expressible t P A νA) (hB : Expressible t P B νB) (hAB : GAncestrallyIndependent A B) (φ : ↥(A ∪ B) → Bool) : pushforward Δ (gRestrict (A ∪ B)) φ = pushforward Δ (gRestrict A) (subRestrict ⋯ φ) * pushforward Δ (gRestrict B) (subRestrict ⋯ φ)

Under a witness satisfying the expressible prescriptions, ancestrally independent sets are independent.

theorem TriangleInflation.Graph.RootSinkAux.marginal_biUnion_prod {Γ : PairGraph} {t : ℕ} {Δ : GAssign Γ t → ℝ} {P : GTarget Γ} (hlaw : IsLaw Δ) (hexp : ∀ (S : Finset (GObs Γ t)) (μ : (↥S → Bool) → ℝ), Expressible t P S μ → pushforward Δ (gRestrict S) = μ) {n : ℕ} (S : Fin n → Finset (GObs Γ t)) (hinj : ∀ (m : Fin n), GInjectable (S m)) (hai : ∀ (m m' : Fin n), m ≠ m' → GAncestrallyIndependent (S m) (S m')) (hempty : GInjectable ∅) (I : Finset (Fin n)) (V : Finset (GObs Γ t)) : V = I.biUnion S → (∃ (μ : (↥V → Bool) → ℝ), Expressible t P V μ) ∧ ∀ (φ : ↥V → Bool), pushforward Δ (gRestrict V) φ = ∏ m ∈ I, pushforward Δ (gRestrict (S m)) (readOnBlock (S m) V φ)

Iterated gluing with Z = ∅: the marginal on a union of pairwise ancestrally independent injectable sets is the product of their marginals.

theorem TriangleInflation.Graph.RootSinkAux.gAncestralProducts_of_exp {Γ : PairGraph} {t : ℕ} {Δ : GAssign Γ t → ℝ} {P : GTarget Γ} (hlaw : IsLaw Δ) (hexp : ∀ (S : Finset (GObs Γ t)) (μ : (↥S → Bool) → ℝ), Expressible t P S μ → pushforward Δ (gRestrict S) = μ) : GAncestralProducts t Δ P

AUDIT-NOTES A2: a witness satisfying the expressible prescriptions satisfies the ancestral-independence prescriptions.

theorem TriangleInflation.Graph.gExpFeasible_iff_gAIFeasible (Γ : PairGraph) (t : ℕ) (P : GTarget Γ) : GExpFeasible Γ t P ↔ GAIFeasible Γ t P

AUDIT-NOTES A2, the consequence for the hierarchies: for pair-source scenarios, which are root-sink scenarios, the recursively expressible hierarchy coincides with the ancestral-independence hierarchy at every order.

theorem TriangleInflation.Graph.flip_gExpFeasible (Γ : PairGraph) (t : ℕ) (P : GTarget Γ) (η : ℝ) (h0 : 0 ≤ η) (h1 : η ≤ 1) (h : GExpFeasible Γ t P) : GExpFeasible Γ t (flipLaw η P)

Local flips preserve the recursively expressible test, via gExpFeasible_iff_gAIFeasible and flip_gAIFeasible. (This does not follow from the flip structure alone: flipping the conditioning coordinates of a glue prescription does not commute with the conditional law; the identification of the glue prescriptions with products of injectable marginals is what makes it true.)

theorem TriangleInflation.Graph.compatible_gExpFeasible (Γ : PairGraph) (t : ℕ) (P : GTarget Γ) (h : GCompatible Γ P) : GExpFeasible Γ t P

A genuine model gives a witness satisfying every expressible prescription: run the inflated model (compatible_gAIFeasible) and use the root-sink lemma.