SCM.PartialID
Partial-identification infrastructure for SCMs: compatible model classes, interval bounds, and sharpness certificates.
CanonicalModel 3 core · 1 supporting This file provides the object over which graphical partial identification quantifies: the class of structural causal models that share a given causal diagram, satisfy stated structural assumptions, and reproduce a refere ★ CompatibleSCM★ compatibleSCM_self★ compatibleIdentifiedSet
Compatible structural causal models for graphical partial identification
This file provides the object over which graphical partial identification quantifies: the class of structural causal models that share a given causal diagram, satisfy stated structural assumptions, and reproduce a reference observational law. A bound on a causal query is sound when every model in this class satisfies it, and the resulting identified set is the range of the query over the class.
Concretely, fixing a SWIG graph G, a structural-assumption predicate As, and a reference
model M₀, the compatible class collects the models M that (i) have diagram G, (ii)
satisfy As, and (iii) are observationally equivalent to M₀ (same derived observational
kernel). The compatible identified set of a real-valued query is the range of that query
over the compatible class — an instance of the shared abstract IdentifiedSet.
Finite response-function reduction
For finite observed-variable domains, Theorem 1 of Zhang, Tian, and Bareinboim (2022),
Partial Counterfactual Identification from Observational and Experimental Data, gives a
canonical representation with finite exogenous domains that preserves counterfactual
distributions. That result does not justify a finite reduction for the arbitrary measurable
value spaces admitted here, and no such reduction is formalized in this file. Soundness of a
bound uses only the compatible class. The library's finite Balke–Pearl realization instead
lives in the potential-outcomes framework (Causalean/PO/ID/Partial/BalkePearl/).
For a finite collection of distinguishable node labels with measurable value spaces, a SWIG graph, a predicate specifying structural assumptions, and a reference structural causal model, the compatible-model class is the collection of structural causal models that have the given graph, satisfy the given assumptions, and are observationally equivalent to the reference model.
For any graph G, structural-assumption predicate As, and reference model M₀, if M₀'s own SWIG graph is G and M₀ satisfies the structural assumptions As, then M₀ belongs to its own compatible class CompatibleSCM G As M₀.
Formal statement
Proof (Lean source)
For a finite collection of distinguishable node labels with measurable value spaces, a SWIG graph, a predicate specifying structural assumptions, a reference structural causal model, and a real-valued causal query, the compatible identified set is the set of all query values attained by structural causal models compatible with that graph, assumptions, and reference model.
Definition (Lean source)
1 supporting declaration (lemmas, instances)
-
compatibleSCM_monotheorem — If the structural-assumption predicate As' is stronger than As, i.e. every model satisfying As' also satisfies As, then every model compatible with the reference model M₀ under the stricter assumptions As' is also compatible under the weaker assumptions As — strengthening the structural assumptions can only shrink the compatible class.Proof (Lean source)
theorem compatibleSCM_mono {G : SWIGGraph N} {As As' : SCM N Ω → Prop} {M₀ : SCM N Ω} (h : ∀ M, As' M → As M) : ∀ M, CompatibleSCM G As' M₀ M → CompatibleSCM G As M₀ M := fun _ hM => ⟨hM.1, h _ hM.2.1, hM.2.2⟩
SharpnessCertificate 2 core · 0 supporting For a graphical partial-identification problem, a valid bound [L, U] on a real-valued causal query is sharp when the identified set — the range of the query over the compatible class of structural causal models — is exac ★ IsSharp★ isSharp_of_attaining
Sharpness certificates for graphical partial-identification bounds
For a graphical partial-identification problem, a valid bound [L, U] on a real-valued causal
query is sharp when the identified set — the range of the query over the compatible class
of structural causal models — is exactly [L, U]. Sharpness is preferred but not required:
a valid relaxed bound stands on its own; a sharpness claim must additionally exhibit compatible
models attaining each endpoint.
This file records the sharpness predicate and the standard certificate: if the identified
set is order-convex, lies inside [L, U] (soundness), and the endpoints L and U are each
attained by some compatible model, then the bound is sharp. The order-convexity hypothesis is
the usual mixing-path input (a continuous family of compatible models interpolating the query
value); it is left as a hypothesis so the certificate applies to any problem that supplies it.
For a finite node set with measurable node-value spaces, a SWIG graph, a structural-assumption predicate, a baseline structural causal model, a real-valued query of such models, and lower and upper endpoints, the sharpness predicate holds exactly when the query's range over compatible models is the closed interval with those endpoints.
Sharpness certificate. For a real-valued query obj over the compatible class of (G, As, M₀), if the identified set is contained in the interval [L, U] (soundness), the identified set is order-connected, some compatible model attains the value L, and some compatible model attains the value U, then the identified set equals [L, U], i.e. the bound is sharp.