Discovery.Linear­Disentanglement

Linear causal disentanglement: model layer

Formalization of the setup of Squires, Seigal, Bhate & Uhler, Linear Causal Disentanglement via Interventions (ICML 2023), arXiv:2211.16467.

We work over d latent variables (Fin d) and p ≥ d observed variables (Fin p). The latent DAG 𝒢 is ordered so that an edge j → i implies j > i; this makes the structural matrices upper triangular in the Fin d order.

For a fixed context, the latent SEM is Z = A Z + Ω^{1/2} ε, equivalently Z = B⁻¹ ε with B = Ω^{-1/2}(I − A). The observed vector is X = G Z with G ∈ ℝ^{p×d} full column rank, and H := G⁺ its left inverse (a full-row-rank d × p matrix with H G = I_d). The only observable content is the family of precision matrices Θ_k = Hᵀ Bₖᵀ Bₖ H ∈ ℝ^{p×p} (one per context).

We take an unnormalized algebraic relaxation of the model surrounding the paper's Theorem 2: the data is a tuple (H, {B_k}, {i_k}, {λ_k}), and uniqueness compares two such tuples that produce the same family {Θ_k}. The paper's row normalization (Assumption 1(c)), which removes scaling and sign ambiguity, is not encoded here. No Moore–Penrose pseudoinverse is needed: H enters only through LinearIndependent ℝ H (full row rank) and the formula for Θ_k.

Conventions for a Solution d p K: * context 0 is observational with matrix B0; contexts 1 … K are interventional with matrices Bint k, intervention target target k, and (perfect-intervention) scaling lam k > 0; * Edge j i means the latent edge j → i (j a parent of i), forced by hAcyc to satisfy i < j; * B0 is upper triangular (B0 i j = 0 for j < i), has positive diagonal, and its off-diagonal support is exactly Edge — this is what defines 𝒢; * hInt is Assumption 1(b) specialized to perfect interventions (Assumption 2): Bₖ = B₀ + e_{iₖ} cₖᵀ with cₖ = λₖ e_{iₖ} − B₀ᵀ e_{iₖ}.

S(𝒢) is the set of node relabelings preserving edge orientation (Edge j i → σ i < σ j); permMat σ is the corresponding permutation matrix (P_σ)_{ij} = ⟦i = σ j⟧, matching the paper.

Linear causal disentanglement: graph order and the partial-order RQ decomposition

We package the graph-theoretic notions used throughout (parents, ancestors, and the partial order ≺_𝒢 with i ≺ j ↔ j ∈ an(i)), and the partial order RQ decomposition of the paper (Definition 1 and Appendix D, Proposition 7): a generalization of the reduced RQ decomposition where the upper-triangular support of R is replaced by the partial order, and orthogonality of the rows of Q is required only along the order. porq_exists / porq_unique are its existence and uniqueness (Appendix D, Proposition 7), proved there by the Gram–Schmidt-style construction in Algorithm "Partial Order RQ Decomposition".

Linear causal disentanglement: the key rank-one identity

The algebraic backbone of the identifiability results (Squires–Seigal–Bhate–Uhler, §3.1). fact_transpose_mul is the rank-one decomposition BᵀB = Σᵢ (Bᵀeᵢ)⊗²; key_identity (their Proposition driving everything) computes the difference of precision matrices between an interventional and the observational context as a difference of two rank-one (outer-product) matrices, using that a single-node intervention changes only one row of B.

Linear causal disentanglement: rowspan inclusions and the corrected third clause

This file links the observable precision differences to the latent graph structure. By key_identity, rowspan(Θₖ − Θ₀) is spanned by the two vectors Hᵀ Bₖᵀ e_{iₖ}, Hᵀ B₀ᵀ e_{iₖ}, both lying in ⟨hᵢ : i ∈ Pa(iₖ)⟩. Full row rank of H makes this containment characterize the parent set:

* (a) rowspan(Θₖ − Θ₀) ⊆ ⟨hᵢ : i ∈ 𝓘⟩ iff Pa(iₖ) ⊆ 𝓘; * (b) rowspan(Θₖ − Θ₀) ⊆ ⟨qᵢ : i ∈ An(iₖ)⟩; * an ancestor-closed correction to the paper's printed Lemma 1(c): if the intervention changes the precision matrix, 𝓘 is ancestor-closed, and Pa(iₖ) ⊄ 𝓘, then rowspan(Θₖ − Θ₀) ⊄ ⟨qᵢ : i ∈ 𝓘⟩.

The printed clause quantifies over arbitrary 𝓘; the result formalized here deliberately does not claim that unrestricted statement.

The file also defines the three spans used in those statements: rowSpan for rows of an observable precision-difference matrix, hSpan for selected rows of the mixing pseudoinverse H, and qSpan for selected rows of a partial-order RQ factor Q.

Linear causal disentanglement: solution orbits under order-preserving permutations

This file proves the solution-orbit direction of the linear-disentanglement identifiability result. The definition Solution.permute constructs the relabelled model: it sends H to Pσ H, conjugates B₀ and every Bₖ by the permutation matrix, and sends each intervention target iₖ to σ(iₖ). The order-preservation hypothesis σ ∈ S(𝒢) is exactly what keeps the transformed observational matrix triangular in the ambient node order.

The theorem sigma_solutions then proves that this transformed solution has the same observable precision matrices Θ₀ and Θₖ. It constructs pure permutation ambiguities only; the separate unnormalized uniqueness theorem permits additional signed diagonal scalings, whose converse construction is not proved here.

Linear causal disentanglement: conditional unnormalized uniqueness, part 1

This first proof file develops the algebraic infrastructure for conditional unnormalized uniqueness. It proves invertibility of the structural matrices and the latent Gram matrix, obtains the change of basis H' = M H, transports the observable precision equalities to latent Gram identities, and rewrites them as rank-two identities.

It also supplies the target read-off lemmas and the summed Gram-difference identity used by Uniqueness_Part2, which continues with diagonal conjugation and orthogonalization. The overall route and final theorem are summarized in Uniqueness.

Linear causal disentanglement: conditional unnormalized uniqueness, part 2

This second proof file turns the summed Gram-difference identity from Uniqueness_Part1 into a diagonal conjugation identity and then an orthogonal change of coordinates. It provides the permutation-conjugation calculations and signed Cholesky lemmas needed to read monomial structure from that orthogonality.

Uniqueness_Part3 uses these tools in the model-specific geometric collapse and extracts the order-preserving permutation. The overall route and final theorem are summarized in Uniqueness.

Linear causal disentanglement: conditional unnormalized uniqueness, part 3

This third proof file contains the model-specific geometric core. Starting from the orthogonalized change of basis supplied by Uniqueness_Part2, it proves that the change of basis is monomial, pins its permutation to the graph order, and reads off the transformed structural matrices and intervention targets.

Its public result exists_orderPerm packages that collapse. Uniqueness_Part4 substitutes it into the recovered change of basis to state the final conditional uniqueness theorem. The overall route is summarized in Uniqueness.