SCM.PartialID
Partial-identification infrastructure for SCMs: compatible model classes, interval bounds, and sharpness certificates.
CanonicalModel 4 core · 0 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★ compatibleSCM_mono★ compatibleInterval
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 interval of a real-valued query is the range of that query over
the compatible class — an instance of the abstract IdentifiedInterval from the
potential-outcomes partial-identification layer, so the existing sharpness / order-convexity
lemmas apply.
Finite response-function reduction
The finite canonical response-function reduction says that every measure-theoretic model in
the compatible class is behaviourally matched by a model over a finite exogenous domain
(Zhang–Tian–Bareinboim). It is not included here: the Causalean SCM layer is
measure-theoretic (Causalean.SCM carries MeasureTheory.Measure latents), so this reduction
is a genuine theorem, not a definitional unfolding. It is needed only when a sharpness claim
must be discharged by enumerating finitely many realising models; soundness of a bound does not
require it. The only finite realisation currently in the library is the Balke–Pearl construction
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)
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.
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 interval is the set of all query values attained by structural causal models compatible with that graph, assumptions, and reference model.
Definition (Lean source)
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 class of structural causal models, a baseline structural causal model, a real-valued query of such models, and two real numbers and , the sharpness predicate holds exactly when the query's range over models compatible with the graph, class, and baseline model is the closed interval .
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.