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/).
The compatible class for a graphical partial-identification problem: the structural causal models M that share the SWIG graph G, satisfy the structural assumptions As, and are observationally equivalent to the reference model M₀ (their derived observational kernels agree). This is the class over which a bound must hold to be sound.
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)
The compatible interval of a real-valued causal query: its range over the compatible class. This is the graphical identified set; a partial-identification bound [L, U] is sound exactly when this set is contained in Set.Icc L U, and sharp when they are equal. Built on the abstract IdentifiedInterval, so the order-convexity / sharpness lemmas of the partial-identification layer apply.
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.
A bound [L, U] is sharp for the real-valued query obj over the compatible class of (G, As, M₀) when the identified set (the range of obj over the compatible class) is exactly the closed interval [L, U].
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.