Discovery.Invariant­Prediction.Linear­Gaussian

Invariant Causal Prediction — linear-Gaussian model layer

Setup for a specialization of the linear-Gaussian identifiability theorem of Peters, Bühlmann & Meinshausen, Causal inference using invariant prediction (JRSS-B 2016, arXiv:1501.01332), Theorem 2(i) (the do-intervention version). Unlike the paper's recursive-SEM formulation, this encoding separately assumes the target-exogeneity facts used by soundness.

This is a self-contained linear-Gaussian framework, deliberately separate from the nonparametric SWIG/kernel EnvFamily development in the parent directory. Variables are real functions on a probability space, with ∫/E[·] for moments and IdentDistrib for equality in distribution.

Encoding choices

* Index convention. The paper uses variables X₁,…,X_{p+1} with target Y = X₁ and predictors X₂,…,X_{p+1}. We index nodes by Fin (p+1) and put the target at index 0, predictors at 1,…,p. So target = 0 and the predictor index set is {1,…,p} = {k : k ≠ 0} (Finset.univ.erase 0). This is a pure 0-based relabelling of the paper's 1,…,p+1; PA(Y) is then a subset of {k : k ≠ 0}.

* One coefficient matrix, one DAG. The observational SEM e = 1 (eq:semmmmm) carries the coefficients β : Matrix (Fin (p+1)) (Fin (p+1)) ℝ with Xⱼ = Σ_{k≠j} βⱼₖ Xₖ + εⱼ. Acyclicity is witnessed by a DAG whose edge k → j holds exactly when βⱼₖ ≠ 0 (hEdge); reusing Causalean.Graph.DAG gives parents / descendants / topological order / the "youngest node" notion for free. PA(Y) = {k : β 0 k ≠ 0} is then literally dag.parents 0.

* Gaussian noise, random-variable form. The observational SEM has its own probability space with observed coordinates, and do-intervention environments live on that same probability space with the same structural noises. Independence of the noises and their Gaussian marginals are stated on the observational environment only (that is where the graph/β/Gaussianity live).

* Do-interventions (sec:idfirst). In environment e an intervention set A e ⊆ {1,…,p} and values a e : Fin (p+1) → ℝ replace the structural equation of each j ∈ A e by the constant a e j (zeroing its row of β and replacing εⱼ by a e j). Per the paper, 0 ∉ A e (never intervene on the target) and A 1 = ∅ (observational).

The do-version's proof in Completeness.lean is a mean-shift argument (R^{e₀} = α_{k₀} a_{k₀} + … vs. R^1 = α_{k₀} X_{k₀}^1 + …, eq:help1/help2), so the model exposes residual means / laws cleanly via IdentDistrib and ∫.

Invariant Causal Prediction — regression-invariance null and identified set

The observable layer of the linear-Gaussian ICP problem: the regression predictor in each environment, the regression-invariance null H_{0,S}, and the identified set S(E) (Peters–Bühlmann–Meinshausen 2016, eq:betapred, eq:H0Sregr, eq:ident).

Encoding choices (fidelity notes)

* Residual. residual γ env ω := Yᵉ(ω) − Σ_k γ k · Xₖᵉ(ω) with the sum over all coordinates (γ is supported on S, so k ∉ S contributes nothing). This is R^e(S) of the paper (R^e = Y^e − X^e β).

* Support on S. "γ supported on S" is ∀ k, γ k ≠ 0 → k ∈ S (SupportedOn). This is the paper's constraint β_k = 0 if k ∉ S.

* Regression-invariance null H_{0,S}. This file uses a pairwise-coordinate version of the regression null: there exist a coefficient vector γ supported on S and a fixed residual law Fε such that for every environment e, the residual R^e = Y^e − Σ γ_k X_k^e is (i) independent of each predictor coordinate in S and (ii) has law Fε (the same law across environments). In this jointly Gaussian linear-Gaussian setting, coordinatewise independence of the residual from each X_k, k ∈ S, is equivalent to joint independence from the vector X_S, so this matches the Peters-Buhlmann-Meinshausen regression null despite the weaker-looking form. The paper also requires γ = β^{pred,e}(S) (the population-OLS coefficient); under independence of R^e from X_S^e that is automatic (the residual is orthogonal to X_S, i.e. the normal equations hold), so we fold it into the independence clause and do not carry β^{pred} as a separate object. The observational environment obs is included as one of the environments (it is e = 1), so invariance is genuinely across the whole family.

* Residual law as a measure on ℝ. Fε : Measure ℝ; "R^e ∼ Fε" is Pᵉ.map (residual γ (env e)) = Fε. Equivalently IdentDistrib across environments; we phrase it via a single shared measure so the "same law" is one object. The mean-shift proof only needs that the two laws differ, which a shared-measure formulation exposes directly (hLawObs, hLawEnv).

* Identified set S(E) (eq:ident). S(E) := ⋂ {S : H_{0,S} holds}. We encode the intersection over the (finite) powerset of predictors that satisfy the null.

Invariant Causal Prediction — conditional completeness for do-interventions

A specialization of Peters–Bühlmann–Meinshausen 2016, Theorem 2(i): for a linear-Gaussian SEM whose interventions are do-interventions with shifted values (a^e_j ≠ E[X¹_j]) and at least one single-node intervention on every predictor, the identified set equals the parents of the target: S(E) = PA(Y). The formal model additionally assumes, through ObsSEM.hYexo and Env.hExo, the target-exogeneity consequences that the paper derives from its recursive SEM.

The intermediate lemmas mirror the paper's proof of Theorem 2(i):

1. Soundness icp_sound_linearGaussian_of_exogeneity (S(E) ⊆ PA(Y)) — H_{0,PA(Y)} holds with γ = γ* = β₀,· and residual ε₁, so PA(Y) is one of the intersected sets (propos:sem). 2. Youngest-node selection exists_youngest_nonzero — among the indices k with α_k ≠ 0 (α = γ* − β^{pred}(S)) there is one, k₀, with no directed path to any other such index (a sink in the induced subgraph). 3. Mean-shift residual_mean_shift_of_doIntervention — under the single do(X_{k₀} = a) intervention with a ≠ E[X¹_{k₀}] and α_{k₀} ≠ 0, the residual law in that environment differs from the observational one (their means differ by α_{k₀}·(a − E[X¹_{k₀}]) ≠ 0), contradicting invariance. 4. Completeness icp_complete_linearGaussian_of_exogeneity — combines 1–3: any null-satisfying S must contain PA(Y), so S(E) ⊇ PA(Y), and with soundness S(E) = PA(Y).

Encoding choices (fidelity notes)

* Single-intervention hypothesis (Theorem 2(i)). HasShiftedSingleInterventions: for each predictor j, some environment i has A i = {j} (single intervention on j) and a i j ≠ E[X¹_j] (the shift condition, with the mean taken under the observational law). This is exactly the paper's "`a^e_j ≠ E(X¹_j) and for each j ∈ {2,…,p+1} there is e with A^e = {j}`".

* E[X¹_j] is the observational mean ∫ ω, M.X ω j ∂P. Finiteness / integrability of the observational coordinates is bundled as hIntegrable (the Gaussian SEM has all moments; the theorem keeps this fact as an explicit integrability hypothesis rather than rebuilding Gaussian moment theory here).

* α and β^{pred}. The proof works with α k = γ*_k − γ_k for the null's coefficient γ (which, being orthogonal to X_S, is β^{pred}(S)). We do not introduce a separate β^{pred} object; α is defined inline in the lemmas.

* Exogeneity (the paper's Assumption 1). Soundness needs ε₀ ⊥ X_k for each parent k ∈ PA(Y). In a recursive Gaussian SEM this follows from joint noise independence + acyclicity, but the random-variable encoding here does not expose the ε → X solve, so it is carried as the structure fields ObsSEM.hYexo and Env.hExo (stated only for parents — it is false for descendants of Y).

* hyoung at the call site. residual_mean_shift_of_doIntervention takes a hyoung hypothesis — every other support index k ≠ k₀ with α_k ≠ 0 is not a descendant of k₀. In the completeness proof this is supplied exactly by the youngest-node selection (exists_youngest_nonzero over the support of α).