Formalization: One Intervention per Latent Variable: Generic Identification of Nonlinear Causal Representations on Fixed-sign Compact Strata
The complete Lean development behind this paper — every definition, lemma, and theorem of its module, including helpers the paper text never cites. Identifiers link within this page, into the Causalean library, or out to the official Mathlib docs.
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Basic 29 declarations This file fixes the latent finite-DAG mechanism, its observed environment family, and the population assumptions shared by the paper's results.
Cover-ratio causal representation model
This file fixes the latent finite-DAG mechanism, its observed environment family, and the population assumptions shared by the paper's results.
For a finite dimension, the latent state space is the real coordinate space.
Definition (Lean source)
The closed latent cube.
Definition (Lean source)
A sign vector with every coordinate equal to -1 or 1.
Definition (Lean source)
A family of observational conditional densities and parent-independent intervention densities. The proof field makes the parent scope part of the carrier.
Definition (Lean source)
Values and the first two derivatives within the closed domain of every mechanism slot, each equipped with uniform convergence there. Pulling this topology back gives the paper's finite relative product C² topology, including its one-sided boundary derivatives, rather than Lean's default pointwise function topology.
Definition (Lean source)
For a finite latent dimension and DAG, the mechanism space carries the relative product C² topology.
Definition (Lean source)
The intervention distribution function Q_i(v) = ∫₀ᵛ q_i(u) du.
The observational product density.
Definition (Lean source)
The density after replacing exactly the target mechanism by q_i.
Definition (Lean source)
The observational law on the compact latent cube.
Definition (Lean source)
The target-i perfect-intervention law on the latent cube.
Definition (Lean source)
Finite-coordinate projection, used to state conditional independence.
Definition (Lean source)
Conditional independence of latent coordinate blocks under the observational law.
Definition (Lean source)
The own-coordinate derivative of the latent log density ratio.
Definition (Lean source)
For a finite node set and DAG, the ancestral cover relation consists of cover pairs in the DAG's ancestor order.
Every observational and intervention mechanism is a positive normalized C³ density on its closed cube, with each conditional normalized in its own coordinate.
Definition (Lean source)
Each latent log ratio has the prescribed strict own-coordinate derivative sign.
Definition (Lean source)
Every direct causal edge remains conditionally dependent given the other parents.
Every observational conditional independence is graphically entailed by d-separation.
The positive, normalized, smooth, causal-minimal, fixed-sign mechanism stratum.
Definition (Lean source)
The mechanism subtype carrying the relative product C² topology.
Definition (Lean source)
The shared observed-space representation and the supplied family of observed laws and ratios.
Definition (Lean source)
The identity-mixing environment family generated directly by a mechanism and target permutation. This is used for the explicit witness calculations.
Definition (Lean source)
The observed support is the image of the latent cube.
Definition (Lean source)
The observed random vector obtained from a latent state.
Definition (Lean source)
The environment-label DAG obtained by pulling G back through the target permutation.
Definition (Lean source)
The observable log-ratio coordinate.
Definition (Lean source)
The observed laws are the shared pushforwards of one observational and one distinct single-target intervention law, and the supplied ratios are their Radon--Nikodym derivatives.
Definition (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.AffinePathTopology 10 declarations This file records compact-uniform continuity of all six value and within-derivative coordinates of the affine mechanism path, and hence continuity in the induced relative product C² topology.
Topology of the affine witness path
This file records compact-uniform continuity of all six value and within-derivative coordinates of
the affine mechanism path, and hence continuity in the induced relative product C² topology.
Restricting a differentiable function on the product cube to one coordinate turns its within Fréchet derivative into evaluation on the corresponding coordinate basis vector. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Given the selected directed edge, the observational-factor value coordinate of the unrestricted affine path varies continuously in the compact-uniform topology.
Formal statement
Proof (Lean source)
Given the selected directed edge, the intervention-factor value coordinate of the unrestricted affine path varies continuously in the compact-uniform topology.
Formal statement
Proof (Lean source)
Given the selected directed edge, the observational-factor first within-derivative coordinate varies continuously along the unrestricted affine path.
Formal statement
Proof (Lean source)
Given the selected directed edge, the observational-factor second within-derivative coordinate varies continuously along the unrestricted affine path.
Formal statement
Proof (Lean source)
Given the selected directed edge, the intervention-factor first within-derivative coordinate varies continuously along the unrestricted affine path.
Formal statement
Proof (Lean source)
Given the selected directed edge, the intervention-factor second within-derivative coordinate varies continuously along the unrestricted affine path.
Formal statement
Proof (Lean source)
Given the selected directed edge, the unrestricted affine mechanism path is continuous in the induced relative product C² topology.
Formal statement
Proof (Lean source)
The unrestricted affine mechanism path tends to its initial stratum point at parameter zero. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The observational factors of the affine path are uniformly close to their initial values for all nodes and cube points when the parameter is sufficiently small. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.AnalyticEdgePerturbation 52 declarations The lemma states the path integral identity, analytic nonidentity certificate, isolated-zero property, and arbitrarily small stratum-preserving perturbation.
Analytic edge perturbation
The lemma states the path integral identity, analytic nonidentity certificate, isolated-zero property, and arbitrarily small stratum-preserving perturbation.
A strict uniform lower bound for finitely many affine families on a compact space defines an open set of parameters. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Strict affine lower-bound constraints are convex in the scalar parameter. the stated conclusion follows.
Formal statement
Proof (Lean source)
The ordered two-point finset is equivalent to Fin 2.
Definition (Lean source)
Fubini's theorem for a two-coordinate product measure in coordinate order. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Direct-edge contrast along the identity-target affine path.
Definition (Lean source)
The explicit rational-integral expression for the direct-edge path contrast.
Definition (Lean source)
The degree-one polynomial whose value at t is the affine interpolation from a to b.
Definition (Lean source)
The degree-one factor polynomial evaluates to affine interpolation.
Formal statement
Proof (Lean source)
The affine factor polynomial has degree at most one.
Formal statement
Proof (Lean source)
Polynomial encoding of the complete numerator in affinePathContrastIntegral.
Definition (Lean source)
Evaluating the numerator polynomial recovers exactly the affine-path numerator. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Coefficients of the affine-path numerator, padded to the uniform degree bound n + 3.
Definition (Lean source)
If every coefficient of the first polynomial family is continuous and every coefficient of the second is continuous, then each product coefficient is continuous.
Formal statement
Proof (Lean source)
If the first endpoint varies continuously and the second endpoint varies continuously, then every affine-factor coefficient varies continuously.
Formal statement
Proof (Lean source)
If every coefficient in a finite polynomial family is continuous, then every coefficient of its finite product is continuous.
Formal statement
Proof (Lean source)
The uniform padding bound really contains every numerator coefficient. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The padded coefficient family evaluates to the complete affine numerator. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Every padded numerator coefficient is continuous on the compact latent cube. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
A globally continuous extension of each cube coefficient, needed because the generic parametric-integral API states measurability on the ambient sample space. the stated conclusion follows.
Formal statement
Proof (Lean source)
For a finite dimension, DAG, sign pattern, stratum point, directed edge endpoints, edge certificate, and coefficient index, the globally continuous extension of the affine numerator coefficient agrees on the cube.
Definition (Lean source)
Given the selected directed edge, the extended affine numerator coefficient is continuous on the ambient latent space.
Formal statement
Proof (Lean source)
Given the selected directed edge and a point in the latent cube, the coefficient extension agrees with the original coefficient.
Formal statement
Proof (Lean source)
Given the selected directed edge and a point in the latent cube, the extended polynomial numerator equals the original numerator polynomial evaluation.
Formal statement
Proof (Lean source)
Given the selected directed edge, the extended affine numerator coefficient is measurable.
Formal statement
Proof (Lean source)
Given the selected directed edge, the extended numerator coefficients have uniform bounds on the compact latent cube.
Formal statement
Proof (Lean source)
A globally continuous representative of the initial distinguished denominator factor.
Definition (Lean source)
A globally continuous representative of the terminal distinguished denominator factor.
Definition (Lean source)
The initial denominator extension is continuous on the ambient latent space.
Formal statement
Proof (Lean source)
Given the selected directed edge, the terminal denominator extension is continuous on the ambient latent space.
Formal statement
Proof (Lean source)
For a point in the latent cube, the initial denominator extension agrees with the stratum mechanism factor.
Formal statement
Proof (Lean source)
Given the selected directed edge and a point in the latent cube, the terminal denominator extension agrees with the sparse-witness factor.
Formal statement
Proof (Lean source)
The unrestricted affine extension starts at the supplied stratum point. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The unrestricted affine extension ends at the edge-specific sparse witness. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The unrestricted affine extension is normalized and C³ for every real path parameter; only positivity requires restricting the parameter to a neighborhood of the closed unit interval. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Positivity and compactness give one strict lower bound valid for every observational mechanism slot on the latent cube. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Positivity and compactness give one strict lower bound valid for every intervention mechanism slot on the unit interval. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The closed affine path admits an open parameter enlargement on which all factors remain positive and the distinguished observational denominator has one uniform separation margin. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The ambient continuous extensions used by the generic analytic theorem give exactly the paper's rational integral, because the integration measure is restricted to the latent cube. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The affine-path rational integral is analytic on the common positive enlargement. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The paper's scalar own-coordinate log-ratio derivative is the difference of the intervention logarithmic derivative and the full-cube observational Fréchet derivative in the own-coordinate direction. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
At the initial endpoint, the affine-path contrast is the original mechanism's contrast. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
At the terminal endpoint, the affine-path contrast is the embedded sparse contrast. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
For a positive normalized mechanism and distinct intervention and ratio targets, the canonical second-moment contrast equals the rational mechanism integral obtained by cancelling the observational child-density factor. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
On the closed affine path, the contrast is exactly its rational mechanism integral. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
A real analytic function on a preconnected set that is nonzero somewhere has an isolated zero at every point of the set. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
On the explicit three-node edge, the affine path ends at the quantitatively separated sparse witness. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Every edge-specific affine path ends at a sparse mechanism with nonzero contrast. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Causal minimality persists for sufficiently small positive parameters along the affine path. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The prescribed own-coordinate derivative signs persist uniformly for small affine-path parameters. Compactness is used only in the latent-state variable; finiteness then combines the nodewise neighborhoods. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
All three paper-local stratum conditions hold simultaneously along a sufficiently short positive initial segment of the affine path. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Once the analytic package is available, isolated zeros, affine-path continuity, and local stratum preservation produce the arbitrarily small nonzero perturbation used by the headline. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Every edge admits arbitrarily small stratum-preserving affine perturbations with nonzero second-moment contrast; the contrast has the stated analytic integral and isolated zeros. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.BoundedSubclass 21 declarations This file records the determinate bounded statistical regime and its uniform first-stage ratio event.
Bounded Hölder subclass and first-stage contract
This file records the determinate bounded statistical regime and its uniform first-stage ratio event. The unresolved generated-rank estimator remains a descriptive payload rather than a fabricated construction.
Parameters of the bounded generated-rank regime.
Definition (Lean source)
An observed world generated by the latent mechanism through a shared C² diffeomorphism and one relabeled perfect intervention per latent node.
Definition (Lean source)
A bounded regime whose predecessor sets use exactly the ordering selected by the law-only population decoder.
Definition (Lean source)
Conditioning-coordinate domain induced by the log-ratios on K.
Definition (Lean source)
Maximum conditioning dimension of the selected ordering.
Definition (Lean source)
Minimum environment sample size at global index N.
Definition (Lean source)
Hölder-ball predicate of real order β: every derivative through ⌊β⌋ is bounded by M, and the top derivative has the corresponding fractional Hölder modulus.
Definition (Lean source)
All observational mechanisms, intervention densities, and unmixed log ratios lie in the common Hölder ball of order β and radius M.
Definition (Lean source)
Every observational and intervention density is uniformly bounded below by c.
Definition (Lean source)
Every signed own-coordinate observed log-ratio derivative is at least c.
Definition (Lean source)
The latent preimage of K is at least ρ from the boundary of the latent cube.
Definition (Lean source)
The Jacobian determinant of a Euclidean self-map relative to its stated domain.
Definition (Lean source)
Every observed log ratio has uniformly bounded value and first two derivatives on K.
Definition (Lean source)
For each environment, some density version of the law of its conditioning coordinates obeys the empty-predecessor convention and lies between c and M on its induced domain.
Definition (Lean source)
Membership evidence for the bounded Hölder subclass, indexed by a point of the full model stratum. Its extension is boundedSubclassSet.
Definition (Lean source)
The bounded Hölder subclass as a subset of the population stratum.
Definition (Lean source)
The uniform C¹ log-ratio error event, including C¹ membership of the fitted and true log-ratios rather than only pointwise derivative inequalities.
Definition (Lean source)
The common N-indexed first-stage contract over the bounded subclass. Each sampling world uses the regime's environment sample-size sequence, and the event is explicitly measurable.
Definition (Lean source)
The proposed uniform coordinate-rate expression.
Definition (Lean source)
@realizes (open generated-rank proof-strategy handle) @realizes (open second-stage cross-fitted rank estimator)
Definition (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.CitedGates 3 declarations These closed string payloads record cited scope facts.
Bibliographic comparator-scope records
These closed string payloads record cited scope facts. They are metadata only and are not logical hypotheses of any theorem.
Wendong, Kekić, von Kügelgen, Buchholz, Besserve, Gresele, and Schölkopf (2023), "Causal Component Analysis," Definition 3.2, Theorem 4.2, and Appendix E.2, NeurIPS paper handle WendongEtAl2023CauCA.
Definition (Lean source)
von Kügelgen, Besserve, Wendong, Gresele, Kekić, Bareinboim, Blei, and Schölkopf (2023), "Nonparametric Identifiability of Causal Representations from Unknown Interventions," Theorems 3.2 and 3.4 and Section 7, handle vonKugelgenEtAl2023UnknownInterventions.
Definition (Lean source)
Yao, Rancati, Cadei, Fumero, and Locatello (2025), "Unifying Causal Representation Learning with the Invariance Principle," Assumption D.1, Corollary D.1, and the following remark, arXiv handle 2409.02772v2.
Definition (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.CompactCondIndepBridge 12 declarations This file transports the paper's ambient, cube-supported coordinate conditional independence to the compact coordinate-product presentation used by positive finite-DAG factorizations.
Conditional-independence bridge to compact cube factorizations
This file transports the paper's ambient, cube-supported coordinate conditional independence to the compact coordinate-product presentation used by positive finite-DAG factorizations.
The finite-coordinate projection from latent states is measurable.
Formal statement
Proof (Lean source)
On compact coordinates, the real-valued coordinate projection generates the same sigma-algebra as the subtype-valued coordinate projection. the stated conclusion follows.
Formal statement
Proof (Lean source)
On compact coordinates, coercing one interval-valued coordinate to a real generates the same sigma-algebra as the original interval-valued coordinate. the stated conclusion follows.
Formal statement
Proof (Lean source)
The real-coordinate presentation on the compact cube is equivalent to the native subtype-coordinate presentation of a compact positive factorization. the stated conclusion follows.
Formal statement
Proof (Lean source)
If a compact positive factorization's observational measure includes to the paper's ambient observational law, then the two singleton-coordinate conditional-independence encodings are equivalent. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The paper and compact-factorization singleton conditional-independence encodings agree for an arbitrary mechanism whenever their observational measures agree. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
A positive normalized smooth paper mechanism restricts to a compact positive factorization on the product of unit-interval coordinate subtypes.
Definition (Lean source)
The compact factorization's local factor is the paper mechanism factor evaluated at the included compact assignment. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Uniform closeness of paper observational factors implies FactorSupClose for their compact positive factorizations. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Including the compact factorization's observational measure into the ambient latent space recovers the paper's cube-supported observational law. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
For a positive smooth mechanism, the paper's singleton-block conditional independence is exactly the compact positive factorization's coordinate conditional independence. the stated conclusion follows.
Formal statement
Proof (Lean source)
Every paper stratum point has one uniform compact-factor neighborhood in which causal minimality persists on all directed edges. the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.CompactCubeBridge 11 declarations This file identifies the ambient closed cube used by the paper with the product of compact interval coordinate types used by finite positive-density factorizations.
Compact cube carrier bridge
This file identifies the ambient closed cube used by the paper with the product of compact interval coordinate types used by finite positive-density factorizations.
The product of unit-interval coordinate types is measurably equivalent to the subtype of ambient latent vectors lying in the closed cube.
Definition (Lean source)
The cube equivalence carries the product of restricted coordinate volumes to the restricted ambient volume on the closed cube. the stated conclusion follows.
Formal statement
Proof (Lean source)
Compact coordinate assignments include into the ambient latent vector space.
Definition (Lean source)
Coordinatewise projection onto the unit interval retracts the ambient latent vector space onto compact coordinate assignments.
Definition (Lean source)
Inclusion of compact coordinate assignments into ambient latent vectors is measurable. the stated conclusion follows.
Formal statement
Proof (Lean source)
The coordinatewise compact-cube retraction is measurable. the stated conclusion follows.
Formal statement
Proof (Lean source)
Retraction after inclusion is exactly the identity on compact coordinate assignments. the stated conclusion follows.
Formal statement
Proof (Lean source)
Inclusion after retraction fixes every ambient point belonging to the latent cube. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Under a positive smooth mechanism's cube-supported observational law, inclusion after the compact-cube retraction is almost everywhere the ambient identity. the stated conclusion follows.
Formal statement
Proof (Lean source)
Pushing a cube-supported observational law to compact coordinates and including it back recovers the original ambient law. the stated conclusion follows.
Formal statement
Proof (Lean source)
For every compact-coordinate measure, inclusion followed by retraction also recovers the original measure. the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.CondIndepIntersection 10 declarations This file scaffolds the positivity-based graphoid intersection step and the finite-coordinate product bridge used with Causalean's generic weak-union lemma.
Conditional-independence bridges for parent pruning
This file scaffolds the positivity-based graphoid intersection step and the finite-coordinate product bridge used with Causalean's generic weak-union lemma.
The latent coordinate targeted by an environment label, expressed on observed space.
Definition (Lean source)
The support-restricted version of an observed latent coordinate is measurable; on the observed support it is exactly the corresponding coordinate of the inverse mixing map. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
On the latent cube, the measurable observed coordinate version recovers the targeted latent coordinate after applying the mixing map. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Conditional independence is equivalent before and after transporting the ambient law along a measurable map. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Pulling three measurable variables back along a measurable map preserves and reflects conditional independence when the target law is the corresponding pushforward. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Applying bimeasurable bijections separately to the two variables and the conditioning variable preserves conditional independence. the stated conclusion follows.
Formal statement
Proof (Lean source)
Replacing all three measurable coordinates by almost-everywhere equal versions preserves conditional independence. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Conditional independence is invariant under almost-everywhere replacement of each of its three measurable coordinates. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Positivity-based graphoid intersection for four disjoint latent-coordinate blocks on the paper's full product support. The disjointness hypotheses are the internal DAG bookkeeping used in equations (15)--(18); they are not assumptions of the delivered decoder theorem. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Coordinate-pair presentation of generic weak union for a finite family of measurable maps. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.ContrastIntegral 1 declarations This file isolates the density cancellation that rewrites a canonical second-moment contrast as the rational mechanism integral used by both the explicit sparse witness and the analytic perturbation argument.
Canonical second-moment contrast integral
This file isolates the density cancellation that rewrites a canonical second-moment contrast as the rational mechanism integral used by both the explicit sparse witness and the analytic perturbation argument.
For a positive normalized mechanism and distinct intervention and ratio targets, the canonical second-moment contrast equals the rational mechanism integral obtained by cancelling the observational child-density factor. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.Decoder 45 declarations The decoder is a function only of the observed probability laws.
Population ratio and conditional-rank decoder
The decoder is a function only of the observed probability laws. It selects a
topological ordering internally, constructs [0,1]-valued conditional ranks,
and prunes to the unique minimal admissible parent sets on the model domain.
A numerical linear extension of a directed relation. Injectivity excludes tied labels.
Labels preceding i in the explicitly selected ordering.
Projection of a coordinate family onto a finite index set.
A decoder input consists of genuine probability laws in all n+1 environments.
Definition (Lean source)
Turn a measure family into a probability-law family when it is one, using a fixed Dirac probability family only outside that domain. Model hypotheses prove that this fallback is never used by the exact-decoder theorem.
Definition (Lean source)
A continuous observed-ratio version for law family laws and environment i agrees almost everywhere with the canonical Radon--Nikodym ratio and is continuous on the support of the observational law.
Definition (Lean source)
The law-only continuous ratio selector for laws and environment i chooses a continuous version when one exists and otherwise retains the canonical Radon--Nikodym ratio.
Definition (Lean source)
Whenever a continuous observed-ratio version exists, the law-only selector returns one. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The law-selected continuous ratio is globally measurable: outside the observational support the selector uses the fixed zero extension. the stated conclusion follows.
Formal statement
Proof (Lean source)
Two continuous versions of the same almost-everywhere function agree throughout the measure's support. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The observable log ratio constructed from the law-selected continuous ratio version.
Definition (Lean source)
The law-selected logarithmic ratio is globally measurable. the stated conclusion follows.
Formal statement
Proof (Lean source)
Population MMD computed solely from the observed environment laws.
Definition (Lean source)
The ratio graph constructed solely from observed laws.
Definition (Lean source)
The predecessor log-ratio vector used as the conditioning variable.
Definition (Lean source)
The joint observed log-ratio and predecessor-log-ratio argument.
Definition (Lean source)
The joint log-ratio and predecessor-log-ratio argument is measurable. the stated conclusion follows.
Formal statement
Proof (Lean source)
Evaluation of an s-finite real kernel on a varying lower interval is jointly measurable in the endpoint and kernel parameter. the stated conclusion follows.
Formal statement
Proof (Lean source)
The law-derived domain on which a conditional-CDF version is required to be continuous: all thresholds over the support of the conditioning predecessor scores.
Definition (Lean source)
The raw regular-conditional-distribution representative, with the original zero fallback when the supplied environment laws are not finite.
Definition (Lean source)
The raw regular-conditional-distribution CDF is jointly measurable in threshold and conditioning argument. the stated conclusion follows.
Formal statement
Proof (Lean source)
A law-only conditional-CDF version: it is jointly measurable, agrees almost everywhere with the regular conditional distribution both at every fixed threshold and under the joint ratio/predecessor law, and is continuous on the joint model support.
Definition (Lean source)
The raw conditional-CDF representative as a unit-interval value, retaining it when it has the required range and using zero only as the range-check fallback.
Definition (Lean source)
The range-checked raw conditional CDF is jointly measurable. the stated conclusion follows.
Formal statement
Proof (Lean source)
The continuous conditional-CDF version selected from the observed laws alone. If no continuous version exists, this retains the raw condDistrib/zero fallback.
Definition (Lean source)
Whenever a continuous conditional-CDF version exists, the law-only selector returns one. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The selected conditional CDF is jointly measurable whether or not a continuous version exists: the fallback is the measurable range-checked raw conditional distribution. the stated conclusion follows.
Formal statement
Proof (Lean source)
Two continuous conditional-CDF versions agree everywhere on the support of the observed joint ratio/predecessor law. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Every continuous conditional-CDF version agrees on joint support with the law-only selected version. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The identified rank coordinate, constructed only from observed laws and an explicit ordering.
Definition (Lean source)
Every law-selected rank coordinate is measurable, including on the selector's raw fallback branch. the stated conclusion follows.
Formal statement
Proof (Lean source)
Every finite projection of the law-selected rank family is measurable. the stated conclusion follows.
Formal statement
Proof (Lean source)
Conditional independence of two measurable functions given a third.
Definition (Lean source)
A candidate parent set satisfies the observed-law conditional-independence test.
Definition (Lean source)
Inclusion-minimal admissibility for parent pruning.
Definition (Lean source)
The uniquely inclusion-minimal admissible set, defined only when it is genuinely unique. none records that the observed laws lie outside the decoder's parent-pruning domain.
Definition (Lean source)
The parent relation carried by a successful unique-minimum selection.
Definition (Lean source)
Every selected edge points forward in the supplied ordering. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The selected-parent relation is acyclic because every edge points forward in order. the stated conclusion follows.
Formal statement
Proof (Lean source)
The acyclic graph induced by all successful unique-minimum parent selections.
Definition (Lean source)
Compatibility restricts law-coherence comparisons to representations of the same observed law family on the same observed support.
Definition (Lean source)
Coherence uses almost-everywhere Radon--Nikodym representatives, but compares the selected continuous ranks pointwise on the full common observed support.
Definition (Lean source)
A topological ordering selected from the ratio graph using only the observed laws. The numeric label order is a total fallback outside the acyclic model domain.
Definition (Lean source)
If the observed ratio graph has a topological ordering, its law-only selected ordering is itself topological. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The law-only population recovery map. It forms the Gaussian-MMD graph, selects its own topological ordering, constructs unit-interval ranks, and returns the parent-pruned DAG.
Definition (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.DecoderCompProd 14 declarations This file separates one distinguished coordinate from a finite product-density measure.
Product-law assembly for decoder coordinates
This file separates one distinguished coordinate from a finite product-density measure. It supplies the measure-product step needed to assemble the equation-(11) conditional kernel.
Transporting a weighted measure through a measurable equivalence transports its density by the inverse equivalence. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
If a finite product density factors into a normalized density at one coordinate and a factor depending only on a disjoint coordinate set, that coordinate is independent of the projected set under the weighted measure. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Equation (10) as a product law: under intervention i, the target coordinate has its replacement-density law and is independent of all latent coordinates preceding i. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Mapping a product measure through a measurable fiber map gives a compositional product whenever the supplied kernel is the fiberwise pushforward of the second marginal. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Reindex and clamp retained latent predecessor coordinates into the compact decoder cube.
Definition (Lean source)
Reindexing and clamping the retained predecessor projection is measurable.
Formal statement
Proof (Lean source)
On the latent cube, the clamped retained projection is the actual predecessor restriction. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The globally measurable clamped predecessor restriction of an ambient latent state.
Definition (Lean source)
The clamped predecessor-coordinate restriction is measurable.
Formal statement
Proof (Lean source)
On the latent cube, clamped predecessor coordinates equal the genuine restriction. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Equation (10) transported to the compact predecessor cube: under intervention i, clamped predecessor coordinates and the target coordinate have a product law. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
On a triangular predecessor score, the ambient equation-(11) kernel is precisely the pushforward of the replacement coordinate law along the corresponding own-score fiber. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
On a latent cube point, the clamped equation-(11) fiber score equals the observed target log-ratio, because every target parent occurs among the reconstructed predecessors. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Under intervention i, the observed predecessor-score and target-score law is the predecessor marginal composed with the ambient equation-(11) Markov kernel. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.DecoderConditionalKernel 26 declarations This file supplies the factor-elimination identity underlying equation (10): when a parent-closed retained set contains the intervention target, its marginal density is the replacement density times the product of the re
Intervention marginal density for the decoder
This file supplies the factor-elimination identity underlying equation (10): when a parent-closed retained set contains the intervention target, its marginal density is the replacement density times the product of the remaining retained observational factors. It also constructs the equation-(11) Markov kernel on the compact predecessor cube and transports it through the triangular predecessor-score homeomorphism.
Eliminating all coordinates outside a parent-closed set containing the intervention target leaves the intervention density times the observational factors at the other retained nodes. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The latent-coordinate image of a decoder predecessor set, together with the current intervention target.
If the selected order respects the recovered ancestral order, the target and its decoder predecessors form a parent-closed latent set. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The predecessor-factor part of equation (10) is constant along the current target's own-coordinate fiber. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Equation (10) at the density-elimination level: under the current intervention, retaining the target and all predecessor coordinates leaves the replacement density times the remaining retained observational factors. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Equation (10) in explicit fiber-product form: after fixing predecessor coordinates, the retained intervention density is the own-coordinate replacement density times a factor that is constant along that coordinate's fiber. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The normalized replacement density, viewed as a probability measure on the target's scalar coordinate.
Definition (Lean source)
Normalization of the replacement density makes its coordinate measure a probability measure.
Definition (Lean source)
A globally measurable clamped extension of the target log-ratio score along a predecessor fiber. On the unit interval it is the score appearing in equation (11).
Definition (Lean source)
Smoothness on the compact cube makes the clamped equation-(11) score jointly measurable in predecessor coordinates and the target coordinate. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The equation-(11) Markov kernel on predecessor latent coordinates: draw the target from its replacement density and push it through the target log-ratio score.
Definition (Lean source)
The equation-(11) predecessor kernel has unit mass on every predecessor fiber.
Definition (Lean source)
Every lower-interval probability of the predecessor kernel is exactly the explicit equation-(11) conditional-CDF integral. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Transporting the predecessor kernel through the compact triangular inverse gives the equation-(11) kernel on the realized predecessor-score image.
Definition (Lean source)
The score-image transport of the equation-(11) kernel remains Markov.
Definition (Lean source)
On every realized predecessor score, the transported kernel's lower-interval probability is the explicit equation-(11) integral at the reconstructed predecessor coordinates. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
At every predecessor score realized by a latent cube point, the transported Markov kernel has exactly the equation-(11) lower-interval probability at that latent state. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
A measurable retraction of the ambient predecessor-score space onto the compact realized score image. Off the image it uses the score of the zero predecessor vector.
Definition (Lean source)
The compact-score retraction is measurable. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The equation-(11) kernel on the full predecessor-score space, obtained by a measurable retraction to the compact realized score image. Its off-support values are immaterial.
Definition (Lean source)
The ambient extension of the equation-(11) kernel remains Markov.
Definition (Lean source)
On every predecessor score realized by a latent cube point, the ambient kernel evaluates to the explicit equation-(11) conditional CDF. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Integrating out coordinates on which a measurable function is invariant leaves the function unchanged when every coordinate reference measure has unit mass. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The factorized retained density from equation (10) is invariant under every coordinate outside the target-plus-predecessor set. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Equation (10) as an equality of retained-coordinate measures: the actual intervention law has the same target-plus-predecessor marginal as the explicit replacement-density product. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
A candidate finite kernel whose compositional product is the observed predecessor/score law is the raw conditional-ratio CDF at every fixed threshold. This is the conditional-distribution uniqueness step used after equation (10). Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.DecoderContinuousVersion 11 declarations This file proves continuity of the equation-(11) fiber integral and packages the ambient Markov kernel as the continuous conditional-CDF version selected by the decoder.
Continuous equation-(11) conditional-CDF version
This file proves continuity of the equation-(11) fiber integral and packages the ambient Markov kernel as the continuous conditional-CDF version selected by the decoder.
The clamped equation-(11) score is jointly continuous in predecessor and target coordinates. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The equation-(11) fiber integral on the compact predecessor cube.
Definition (Lean source)
The equation-(11) fiber integral varies continuously with both its threshold and predecessor coordinates. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The compact fiber CDF is the explicit equation-(11) integral. the stated conclusion follows.
Formal statement
Proof (Lean source)
The ambient equation-(11) Markov kernel evaluated on lower intervals, packaged as a unit-interval-valued conditional CDF.
Definition (Lean source)
The ambient equation-(11) conditional CDF is jointly measurable. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
On the realized predecessor-score range, the ambient equation-(11) CDF is continuous. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The observed joint ratio/predecessor support has predecessor component in the compact triangular score range. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Conditional-kernel uniqueness holds jointly under the observed threshold/predecessor law, not merely separately at each fixed threshold. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The ambient equation-(11) CDF is a continuous conditional-distribution version for the observed intervention law. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
On every realized predecessor score, the continuous version evaluates to the explicit equation-(11) integral. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.DecoderCore 14 declarations This file collects paper-local consequences of the primitive observed-world assumptions that feed directly into the exact population decoder.
Structural pieces of the exact population decoder
This file collects paper-local consequences of the primitive observed-world assumptions that feed directly into the exact population decoder.
Strict positivity of every retained factor and the replacement density gives each latent single-target intervention law the full closed cube as its support. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The observational observed law has exactly the image of the latent cube as its support. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Normalized local factors make the observational latent law a probability measure. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Normalized local and replacement factors make every interventional latent law a probability measure. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The pushforward assumptions and normalized latent factors make every observed environment law a probability measure. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Transporting the latent canonical Radon--Nikodym ratio through the support diffeomorphism does not change its law under any latent base measure dominated by the observational law. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The observational latent law is concentrated on the closed latent cube. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Strict positivity of all latent factors makes the observational and target-intervention observed laws equivalent; this is the reverse direction not needed by the ratio-law bridge. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The supplied observed-world ratio agrees almost everywhere with the canonical law ratio, and the law-selected rank construction is unchanged by a compatible representation. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The smooth mechanism formula for an observed ratio, extended through the unmixing map.
Definition (Lean source)
Under the positive smooth mechanism assumptions, shared mixing assumptions, and perfect-intervention assumptions, the smooth mechanism ratio is a continuous observed-ratio version for world W and environment i.
Formal statement
Proof (Lean source)
Under positive smooth mechanisms, shared diffeomorphic mixing, and one perfect intervention per node, each observed ratio law has a continuous version.
Formal statement
Proof (Lean source)
The law-selected logarithmic ratio pulled back through the mixing map agrees pointwise on the latent cube with the smooth mechanism ratio, under the positive smooth mechanism assumptions, shared mixing assumptions, and perfect-intervention assumptions, for world W and environment i.
Formal statement
Proof (Lean source)
The observed-law logarithmic ratio pulled back through the mixing map agrees almost everywhere with the mechanism's scalar log ratio. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.DecoderGraph 19 declarations This file proves equations (4)--(6): nonancestor interventions cannot create ratio-law edges, ancestral covers generate the latent transitive closure, and every ratio-graph topological ordering places latent parents befo
Ratio-graph reconstruction for the exact decoder
This file proves equations (4)--(6): nonancestor interventions cannot create ratio-law edges, ancestral covers generate the latent transitive closure, and every ratio-graph topological ordering places latent parents before their children.
Environment-label parents obtained by pulling back the latent parent set.
A numeric order respects every latent edge after intervention-label relabeling.
Definition (Lean source)
Transitive-closure recovery makes every ratio-graph topological order respect latent edges. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The observational canonical-ratio law is invariant under the supplied support diffeomorphism. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Every intervention-base canonical-ratio law is likewise invariant under the supplied support diffeomorphism. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Hence the canonical-world discrepancy used by cover separation is exactly the observable discrepancy of the supplied law family. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Cover separation stated for the identity-mixing canonical world supplies exactly the cover edges required for the observed world. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
A non-ancestor intervention leaves the corresponding ratio law unchanged, hence has zero MMD. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Every strict ancestor relation in a finite DAG factors through ancestral covers. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Every observable ratio-graph edge points along the latent ancestral order. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Sound ratio edges plus all ancestral covers recover exactly the permuted latent transitive closure. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Once the ratio graph has the latent transitive closure, every topological ordering puts all environment-label parents before their child. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
In a two-vertex DAG every directed edge is automatically a cover of the ancestral order, since there is no third vertex that can lie strictly between its endpoints. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Cover separation supplies the bivariate Gaussian-MMD edge witness because every edge of a two-vertex DAG is an ancestral cover. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The intervention target of a node cannot be a parent of any earlier node in a valid ratio-graph topological ordering. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The triangular predecessor-score map recovers every predecessor's latent coordinate. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Positivity and the shared perfect-intervention representation make the observed ratio graph acyclic, witnessed by the latent DAG's topological order transported to environment labels. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Under the model assumptions, the decoder's internally selected ordering is a valid topological ordering of the observed ratio graph. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Equations (4)--(6) assemble into transitive-closure recovery, validity of the decoder's selected order, and containment of every true parent among every valid order's predecessors. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.DecoderOrderedLocalMarkov 7 declarations This module packages the finite-density ordered local Markov theorem in the paper's CondIndepGiven interface under its observational law.
Ordered local Markov bridge for decoder pruning
This module packages the finite-density ordered local Markov theorem in the
paper's CondIndepGiven interface under its observational law.
A numeric topological order for the ratio graph also orders every latent edge once their transitive closures agree. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
A topological order of the environment-label graph pulls back along the target permutation to a topological ranking of the latent graph.
Definition (Lean source)
Predecessors in the pulled-back latent ranking are exactly target-permutation images of the environment-label predecessors. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
A positive normalized paper mechanism makes a latent coordinate conditionally independent of the nonconditioned predecessors whenever the conditioning set contains all latent parents. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The ordered local-Markov property pulled back to environment labels: whenever an environment conditioning set contains the target's environment-label parents, the target latent coordinate is independent of all remaining predecessors. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Singleton-block conditional independence is equivalent to its scalar-coordinate presentation, with the same finite conditioning projection. the stated conclusion follows.
Formal statement
Proof (Lean source)
The decoder's weak-union independence and the ordered local-Markov independence combine, by strict-positive-density intersection, to remove every nonparent predecessor from the conditioning set of a putatively omitted parent. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.DecoderPruning 3 declarations This file packages the set-theoretic conclusion of equation (19): once the conditional-independence test characterizes exactly the supersets of the true parent set, that set is the unique inclusion-minimal admissible set
Exact parent pruning
This file packages the set-theoretic conclusion of equation (19): once the conditional-independence test characterizes exactly the supersets of the true parent set, that set is the unique inclusion-minimal admissible set and the decoder's selected graph is the permuted latent graph.
At one common order, the conditional-independence characterization makes the true parent set the unique inclusion-minimal admissible set. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
If admissibility is equivalent to containing the true environment-label parents for every valid ordering, parent pruning has that parent set as its unique minimum. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Exact unique parent pruning at the selected topological order makes the decoder's returned DAG equal to the environment-label pullback of the latent DAG. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.DecoderRank 16 declarations This file proves the one-dimensional integration step in equation (12): evaluating a conditional CDF at a strictly monotone score returns the intervention CDF, reflected when the score is decreasing.
Scalar conditional-rank identities
This file proves the one-dimensional integration step in equation (12): evaluating a conditional CDF at a strictly monotone score returns the intervention CDF, reflected when the score is decreasing.
Equation (11): conditional on predecessor ranks (hence on the parents), the target log-ratio CDF integrates the intervention density over own-coordinate values below the log-ratio threshold.
The normalized positive intervention density has a distribution function valued in the unit interval at every point of the unit interval. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The equation-(11) conditional kernel is a genuine unit-interval-valued CDF at every threshold and every latent state in the cube. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The equation-(11) kernel depends on the conditioning state only through the target's parent coordinates. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
On the unit interval, a score whose lower level set at z is [0,z] has conditional CDF equal to the integral of its density from zero to z. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
On the unit interval, a decreasing score has conditional CDF equal to one minus the integral of its normalized density from zero to z. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
A normalized density evaluated through a strictly increasing score produces its ordinary distribution function. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
A normalized density evaluated through a strictly decreasing score produces its reflected distribution function. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Equation (11), evaluated at the realized own-coordinate score, is the intervention CDF when that score is strictly increasing on the unit interval. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Equation (11), evaluated at the realized own-coordinate score, is the reflected intervention CDF when that score is strictly decreasing on the unit interval. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
A positive prescribed own-score derivative makes the own-coordinate score strictly increasing on the closed unit interval. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
A negative prescribed own-score derivative makes the own-coordinate score strictly decreasing on the closed unit interval. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
With parent coordinates fixed, equality of a node's log-ratio score is equivalent to equality of its own coordinate. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Equation (12) follows from equation (11) and the prescribed own-coordinate derivative sign: the recovered rank is the intervention CDF, reflected exactly for negative sign. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
At the realized score, the signed equation-(11) formula has the unit-interval range required by the decoder's conditional-CDF codomain. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Once the law-selected conditional CDF is identified with equation (11), evaluating it at the pointwise identified log ratio gives the signed intervention-CDF rank of equation (12). Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.DecoderRankAssembly 2 declarations This file assembles the support, continuous-version, explicit equation-(11), and signed-rank facts into the complete conditional-rank clause consumed by the exact population decoder theorem.
Continuous conditional-rank assembly
This file assembles the support, continuous-version, explicit equation-(11), and signed-rank facts into the complete conditional-rank clause consumed by the exact population decoder theorem.
A ratio-graph order that also respects the latent edges has the law-selected continuous conditional CDF, its equation-(11) realization, and the signed intervention-CDF rank. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Transitive-closure recovery supplies latent-edge compatibility for every valid ratio order. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.DecoderRankCondIndep 4 declarations This module records the measurable-embedding invariance used to pass between the decoder's signed CDF ranks and the corresponding latent coordinates.
Rank-coordinate conditional-independence transport
This module records the measurable-embedding invariance used to pass between the decoder's signed CDF ranks and the corresponding latent coordinates.
Applying measurable embeddings separately to both variables and the conditioning variable preserves and reflects conditional independence. the stated conclusion follows.
Formal statement
Proof (Lean source)
The signed intervention CDF restricted to the unit interval, with its range proof.
Definition (Lean source)
The signed intervention CDF chart is continuous on the closed unit interval. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The positive-density signed CDF chart is a measurable embedding of the unit interval. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.DecoderRankPruning 15 declarations This module transports conditional independence between law-selected signed-CDF ranks and measurable support-restricted latent coordinates, then combines ordered local Markov and positive-density intersection to characte
Rank-coordinate parent-pruning assembly
This module transports conditional independence between law-selected signed-CDF ranks and measurable support-restricted latent coordinates, then combines ordered local Markov and positive-density intersection to characterize the admissible parent sets exactly.
The support-restricted observed latent coordinate, bundled with its unit-interval range.
Definition (Lean source)
The unit-interval-valued observed latent coordinate is measurable. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Coordinatewise signed-CDF chart on a finite family of environment labels.
Definition (Lean source)
Applying the signed intervention CDF separately in finitely many coordinates is a measurable embedding. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Coordinatewise coercion from unit-interval-valued families to real-valued families.
Coordinatewise coercion from a finite product of unit intervals is a measurable embedding. the stated conclusion follows.
Formal statement
Proof (Lean source)
Pointwise identification of every selected rank with its signed intervention CDF transports the decoder's conditional-independence test exactly to the support-restricted latent coordinates. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
A globally measurable version of the mixing map, equal to it on the latent cube.
Definition (Lean source)
The support-restricted mixing-map version is measurable. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Conditional independence of support-restricted observed latent coordinates is equivalent to conditional independence of the target-permuted coordinates under the latent observational law. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Reindexing a finite coordinate family along the world's target permutation.
Definition (Lean source)
A one-coordinate finite family is measurably equivalent to its scalar coordinate.
Definition (Lean source)
Ordered local Markov in environment-label coordinates, reindexing the latent projection along the intervention-target permutation. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
For every valid ratio-graph ordering, rank-coordinate conditional independence holds exactly when the conditioning set contains all environment-label parents. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Transitive-closure recovery specializes the ordered characterization to every ratio order. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.DecoderRepresentation 11 declarations These lemmas isolate the law-support and graph-relabeling parts of the compatible- representation argument.
Compatible-representation bookkeeping
These lemmas isolate the law-support and graph-relabeling parts of the compatible- representation argument. The remaining analytic step is the componentwise coordinate identification from the common law-selected ranks.
The scalar rank chart selected by an intervention CDF and the prescribed ratio-score sign.
Definition (Lean source)
Strict positivity of the intervention density makes its CDF strictly increasing on the latent interval. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Reflection for a negative score sign preserves injectivity of the scalar intervention-CDF chart. Given the stated inputs and conditions, the stated conclusion follows.
Proof (Lean source)
The probability-family packaging, selected order, and rank coordinates are literally shared by representations whose supplied law families are equal. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Compatible smooth observed worlds with the same observational law have the same observed support. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Equality of environment-label graphs gives graph isomorphism under the intervention-target alignment permutation. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
If law-only exact pruning identifies both representations' parent relations, their latent graphs align by the target permutation. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
A topological order pulled back from a compatible competitor orders the common observable ratio graph and, once the reference transitive closure is identified, the reference graph too. No cover-separation premise is required for the competitor. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Two representations realizing the same law-only rank coordinate have equal signed scalar intervention-CDF coordinates at every common support point. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Equality of an aligned source coordinate forces equality of the competitor coordinate once both worlds realize the common law-only rank. This is the componentwise-dependence leaf of the representation argument. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Once the common law-selected order is known to be topological for both latent transitive closures, the assembled equation-(11)--(12) rank formula identifies their signed scalar CDF coordinates pointwise on the common support. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.DecoderSupport 5 declarations This file proves that every predecessor-score vector produced by a latent cube point lies in the support of its observed interventional predecessor law.
Realized predecessor-score support
This file proves that every predecessor-score vector produced by a latent cube point lies in the support of its observed interventional predecessor law. It is the support bridge needed to turn continuous-version uniqueness into the pointwise equation-(11) identity.
Every supplied observed single-target intervention law has the full observed model support, because its latent density is strictly positive on the full cube. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The law-selected log ratio is continuous on the common observed support. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The vector of predecessor log ratios is continuous on the common observed support. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
A function continuous on the support of a measure sends support points into the support of its pushforward. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Every predecessor-score vector realized by a latent cube point belongs to the support of the observed predecessor law under the current intervention. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.DecoderTriangularInverse 12 declarations This file packages equations (7)--(9): predecessor latent coordinates form a compact cube, their triangular log-ratio score map is a continuous injection, and hence it has a continuous inverse on its image.
Compact triangular predecessor-score inverse
This file packages equations (7)--(9): predecessor latent coordinates form a compact cube, their triangular log-ratio score map is a continuous injection, and hence it has a continuous inverse on its image.
The compact product cube of latent coordinates indexed by predecessors of i.
Definition (Lean source)
Embed predecessor coordinates into the full latent cube, filling nonpredecessors with zero.
Definition (Lean source)
Restrict a latent cube point to the coordinates indexed by decoder predecessors.
Definition (Lean source)
Embedding the predecessor restriction back into the ambient cube preserves every predecessor coordinate. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The triangular predecessor log-ratio map, written directly in latent coordinates.
Definition (Lean source)
The zero-filled predecessor-coordinate embedding always lies in the full latent cube. the stated conclusion follows.
Formal statement
Proof (Lean source)
On a latent cube point, the compact triangular score map is exactly the observed predecessor log-ratio projection pulled back through the mixing map. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Every predecessor log-ratio vector realized by a latent cube point belongs to the image of the compact triangular predecessor-score map. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Smooth positive mechanisms make the triangular predecessor score map continuous. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The prescribed own-score signs make the triangular predecessor score map injective. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The compact triangular predecessor score map is a homeomorphism onto its image.
Definition (Lean source)
The inverse predecessor-coordinate reconstruction is continuous on the score image. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.FiniteDensityBridge 13 declarations This file records the model-specific identification needed to instantiate the general finite-DAG nonancestor marginal theorem with the paper's observed laws.
Finite-density bridge for observed ratio laws
This file records the model-specific identification needed to instantiate the general finite-DAG nonancestor marginal theorem with the paper's observed laws.
A paper mechanism and observed world are represented by the reusable unit-cube factorization, including identification of the canonical observed ratio pushforwards.
Definition (Lean source)
A positive normalized smooth latent mechanism determines the reusable unit-cube factorization of its observational conditional densities.
Definition (Lean source)
A positive normalized smooth latent mechanism and observed target permutation determine the reusable unit-cube intervention density for an environment.
Definition (Lean source)
A positive normalized smooth mechanism has the same observational law as the observational measure of its clamped unit-cube factorization.
Formal statement
Proof (Lean source)
A positive normalized smooth mechanism has the same target-intervention law as the intervention measure of its clamped unit-cube factorization.
Formal statement
Proof (Lean source)
The positive normalized smooth mechanism and environment target determine the globally measurable clamped numerator used in the canonical target ratio.
Definition (Lean source)
On the latent unit cube, the real value of the clamped factor ratio is the paper's ordinary replacement-to-observational density ratio. With the stated inputs and conditions, the documented conclusion follows.
Formal statement
Proof (Lean source)
The clamped target ratio is globally measurable.
Formal statement
Proof (Lean source)
Every positive single-target latent intervention law is absolutely continuous with respect to the corresponding observational latent law. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Under positive latent densities, support-local shared mixing, and the supplied pushforward laws, every observed single-target intervention law is absolutely continuous with respect to the observed observational law.
Formal statement
Proof (Lean source)
The [primitive smooth-mechanism, support-local mixing, and observed-law hypotheses] (hyp:hpos,hmix,hone) construct the paper's finite-density observed-world bridge.
Definition (Lean source)
The finite-density bridge turns nonancestry into equality of the two canonical real-valued ratio laws. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The observational law of a positive normalized mechanism satisfies the ordered local Markov property for every topological ranking of its latent DAG. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.GaussianRecoveryBridge 4 declarations This file connects the paper's duplicated explicit Gaussian feature expansion and its canonical ratio laws to the neutral bounded-support recovery theorem.
Gaussian recovery bridge
This file connects the paper's duplicated explicit Gaussian feature expansion and its canonical ratio laws to the neutral bounded-support recovery theorem.
The identity-mixing canonical world satisfies the paper's perfect-intervention contract. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The paper and neutral Gaussian feature vectors are the same explicit ℓ² vector. the stated conclusion follows.
Formal statement
Proof (Lean source)
The paper's Gaussian mean embedding agrees with the neutral recovery embedding. the stated conclusion follows.
Formal statement
Proof (Lean source)
A nonzero canonical raw second-moment contrast forces positive paper-local Gaussian MMD. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.Inference 15 declarations This file defines the multi-environment evaluation sample, arbitrary training-fold ratio estimates, empirical MMDs, and the simultaneous threshold.
Independent sample-splitting and the confidence graph
This file defines the multi-environment evaluation sample, arbitrary training-fold ratio estimates, empirical MMDs, and the simultaneous threshold.
A sample-split experiment over a fixed observed environment family.
Definition (Lean source)
The complete training fold, retained rather than compressed to an arbitrary summary.
Definition (Lean source)
The σ-algebra generated by the complete training fold.
Definition (Lean source)
The fitted ratio, definitionally factored through the complete training fold.
Definition (Lean source)
The training-fold finite L¹ ratio-error event used by the confidence theorem.
Definition (Lean source)
All evaluation observations as a single dependent array.
Definition (Lean source)
Evaluation observations are independent within each environment, have the stated environment law, and the complete evaluation fold is independent of the training fold.
Definition (Lean source)
The part of the sample-splitting assumptions needed to condition an evaluation-sample concentration bound on the training fold. It deliberately omits the unused training-sample law and i.i.d. clauses and the measurability of the separate first-stage event.
Definition (Lean source)
The full independent-environment sampling contract supplies the smaller collection of assumptions needed for conditional evaluation-fold concentration. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Event E has conditional probability at least p, on event A, relative to m. The setwise formulation avoids selecting a conditional-expectation version.
Definition (Lean source)
The minimum sample size across observational and intervention environments.
Definition (Lean source)
Empirical mean embedding for ratio estimate i in environment e.
The sample-split empirical Gaussian-kernel MMD.
Definition (Lean source)
The paper's simultaneous confidence radius.
Definition (Lean source)
The graph selected by positive lower confidence bounds for population discrepancies.
Definition (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.Kernel 20 declarations This file defines the paper's explicit square-summable Gaussian feature map, kernel mean embeddings, population discrepancies, and the two genericity sets.
Gaussian feature embeddings and cover separation
This file defines the paper's explicit square-summable Gaussian feature map, kernel mean embeddings, population discrepancies, and the two genericity sets.
The Gaussian kernel exp (-(a-b)²).
Definition (Lean source)
A real Hilbert-space feature map of unit norm that realizes a specified kernel.
Definition (Lean source)
The mth coordinate of the paper's explicit Gaussian feature expansion.
The explicit coefficient sequence is square-summable. the stated conclusion follows.
Formal statement
Proof (Lean source)
The explicit Gaussian feature vector in real ℓ².
Definition (Lean source)
The inner product of two explicit Gaussian feature vectors equals the Gaussian kernel.
Formal statement
Proof (Lean source)
Every explicit Gaussian feature vector has unit norm.
Formal statement
Proof (Lean source)
The concrete unit-norm feature-map realization of the Gaussian kernel.
Definition (Lean source)
The Bochner kernel mean embedding of a real-valued law in a Hilbert space.
Definition (Lean source)
The observational law followed by the n interventional environment laws.
Definition (Lean source)
The canonical Radon--Nikodym ratio determined by the observed laws.
Definition (Lean source)
The canonical observed-law ratio is globally measurable. the stated conclusion follows.
Formal statement
Proof (Lean source)
The law of ratio i under the observational environment.
Definition (Lean source)
The law of ratio i under intervention environment j.
Definition (Lean source)
Population Gaussian-kernel MMD between the observational and environment-j ratio laws.
Definition (Lean source)
Equal observational and interventional ratio laws have zero population discrepancy. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The environment-j minus observational second-moment contrast of ratio i.
Definition (Lean source)
The observable directed ratio graph.
Definition (Lean source)
Mechanisms whose second-moment contrast is nonzero on every permuted direct edge.
Definition (Lean source)
Mechanisms whose Gaussian MMD is positive on every permuted ancestral cover.
Definition (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.OpenQuestions 1 declarations The second-stage procedure and sharp remainder criterion are intentionally left undefined by the paper, so the complete question is preserved as text.
Generated-rank frontier
The second-stage procedure and sharp remainder criterion are intentionally left undefined by the paper, so the complete question is preserved as text.
@realizes (open cross-fitted conditional-CDF estimator) @realizes (named nonassertive construction handle)
Definition (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.RkhsEmpiricalMean 5 declarations The statement is made against the local unit-norm feature-map interface and is designed for the reused scalar McDiarmid concentration engine.
Uniform Hilbert-valued empirical-mean deviation
The statement is made against the local unit-norm feature-map interface and is designed for the reused scalar McDiarmid concentration engine.
A training-measurable localization of the random-parameter product-law bound. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Every realization of the Gaussian kernel is sqrt 2-Lipschitz. the stated conclusion follows.
Formal statement
Proof (Lean source)
Gaussian mean embeddings are controlled by sqrt 2 times the input L¹ distance. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Conditional population embedding of the fitted ratio under environment e.
Definition (Lean source)
Conditional on training, all environment/ratio empirical feature means obey the stated unit-norm Hilbert-space deviation bound with probability at least 1-α. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.WitnessAssembly 14 declarations This file isolates the pointwise cancellations that turn the sparse and cancellation witness expectations into the low-dimensional integrals used by the certificate proof.
Explicit-witness density algebra
This file isolates the pointwise cancellations that turn the sparse and cancellation witness expectations into the low-dimensional integrals used by the certificate proof.
Fubini's theorem for a three-coordinate product measure, written in the explicit coordinate order used by the witness calculations. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
In the sparse observational law, one child-density factor cancels from the square of the explicit child ratio. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Under the sparse parent intervention, the same cancellation leaves the parent tilt multiplying the reduced child integrand. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The cancellation witness's parent-interventional minus observational test integrand factors into the parent tilt and the child test integrand. the stated conclusion follows.
Formal statement
Proof (Lean source)
Expanding the cancellation witness identifies its factored density difference with the reflected two-coordinate integrand from the FTC argument. the stated conclusion follows.
Formal statement
Proof (Lean source)
The full density difference against a ratio-law test function is exactly the reflected two-coordinate cancellation integrand. the stated conclusion follows.
Formal statement
Proof (Lean source)
Coordinate reflections preserve the complete cancellation integral, so it vanishes for every prescribed sign vector. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The reflected exponential intervention slots are globally measurable.
Formal statement
Proof (Lean source)
Every cancellation-witness observational mechanism slot is globally measurable.
Formal statement
Proof (Lean source)
The cancellation witness's observational joint density is globally measurable.
Formal statement
Proof (Lean source)
Every cancellation-witness interventional joint density is globally measurable.
Formal statement
Proof (Lean source)
The finite latent unit cube is measurable. the stated conclusion follows.
Formal statement
Proof (Lean source)
The cancellation witness has exactly the same child-ratio law before and after intervening on its parent. the stated conclusion follows.
Formal statement
Proof (Lean source)
Exact cancellation of the ratio laws makes the cancellation witness's Gaussian population discrepancy vanish. the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.WitnessCancellation 15 declarations This file isolates the fundamental-theorem-of-calculus identity behind equality of the cancellation witness's observational and parent-interventional ratio laws.
Cancellation-witness calculus
This file isolates the fundamental-theorem-of-calculus identity behind equality of the cancellation witness's observational and parent-interventional ratio laws.
In the canonical world, the law-defined Radon--Nikodym ratio agrees almost everywhere under the observational law with the explicit mechanism ratio. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The canonical observational ratio law is the pushforward of the observational latent law by the explicit mechanism ratio. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The canonical interventional ratio law is the pushforward of the corresponding latent interventional law by the same explicit mechanism ratio. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The second moment of the canonical observational ratio law is the latent observational integral of the square of the explicit mechanism ratio. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The second moment of a canonical interventional ratio law is the corresponding latent interventional integral of the square of the explicit mechanism ratio. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The cancellation primitive has derivative equal to the intervention-density tilt. the stated conclusion follows.
Formal statement
Proof (Lean source)
Integrating the cancellation tilt against any continuous function of the cancellation primitive gives zero. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Clamp a real argument to the range of the cancellation primitive.
If the argument already lies in the cancellation range, then clamping leaves it unchanged.
Formal statement
Proof (Lean source)
A globally continuous extension of the one-dimensional test integrand used to identify the cancellation ratio law.
Definition (Lean source)
The extended cancellation test integrand is continuous when the test function is continuous and the child coordinate lies in the unit interval. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The parent intervention tilt integrates to zero against the exact test integrand that appears after fixing the cancellation witness's child coordinate. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The complete two-coordinate cancellation integral vanishes for every continuous test function. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Two finite ratio laws coincide when every bounded continuous real test function has the same integral under both laws. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Equality of the observational and interventional ratio laws forces their kernel mean discrepancy to vanish. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.WitnessCancellationFaithfulness 9 declarations This file proves dependence of the cancellation witness's unique edge from a strictly positive covariance, and then invokes the three-node graph reduction.
Cancellation-witness faithfulness
This file proves dependence of the cancellation witness's unique edge from a strictly positive covariance, and then invokes the three-node graph reduction.
A fixed signed reflection followed by the cancellation primitive is continuous.
Formal statement
Proof (Lean source)
A continuous test function under the cancellation observational law is its explicit three-coordinate iterated density integral. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Integrating over the child leaves the cancellation coefficient unchanged. the stated conclusion follows.
Formal statement
Proof (Lean source)
Integrating the centered child coordinate gives one thirtieth of the parent coefficient. the stated conclusion follows.
Formal statement
Proof (Lean source)
The child-parent test-product integral is one thirtieth of the squared coefficient. the stated conclusion follows.
Formal statement
Proof (Lean source)
The reflected cancellation coefficient has strictly positive variance under unit Lebesgue law. the stated conclusion follows.
Formal statement
Proof (Lean source)
Positive coefficient-child covariance rules out independence of the cancellation edge. the stated conclusion follows.
Formal statement
Proof (Lean source)
The cancellation witness is causally minimal for the one-edge three-node DAG. the stated conclusion follows.
Formal statement
Proof (Lean source)
The cancellation witness is faithful to 0 → 1 with isolated node 2. the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.WitnessFaithfulness 9 declarations This file isolates the finite graph calculation used to reduce faithfulness of the explicit three-node witnesses to dependence of the unique adjacent pair.
Graph reduction for explicit-witness faithfulness
This file isolates the finite graph calculation used to reduce faithfulness of the explicit three-node witnesses to dependence of the unique adjacent pair.
Conditional independence given the trivial sigma algebra is ordinary independence on a probability space. This is the reverse of Causalean's existing trivial-conditioning bridge and is used to expose dependence of the explicit witness edge. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Coordinate-block conditional independence given the empty block implies ordinary independence whenever the observational law is a probability measure. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
For pairwise-disjoint blocks in the three-node witness DAG, d-separation fails exactly when the endpoints of its unique edge occur in opposite query blocks. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Conditional independence of two coordinate blocks descends to any chosen singleton coordinate from each block. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Coordinate-block conditional independence is symmetric in its two query blocks. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
For the three-node witness DAG, dependence of the unique adjacent pair under every admissible conditioning block suffices for full faithfulness. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
For the three-node witness DAG, unconditional dependence of the unique edge and independence of its first endpoint from the isolated node imply full faithfulness. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Every positive normalized mechanism factorizing over the three-node witness DAG makes the first endpoint of the unique edge independent of the isolated third coordinate. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
On the explicit three-node DAG, positivity and causal minimality already imply faithfulness because the only nontrivial d-connection is its unique edge. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.WitnessFaithfulnessAssembly 14 declarations This file turns the explicit sparse density calculation into dependence of the unique adjacent coordinate pair, and hence into faithfulness of the sparse three-node witness.
Explicit-witness faithfulness assembly
This file turns the explicit sparse density calculation into dependence of the unique adjacent coordinate pair, and hence into faithfulness of the sparse three-node witness.
The squared centered coordinate has unit-interval integral 1/3. the stated conclusion follows.
Formal statement
Proof (Lean source)
Coordinate reflection preserves the squared centered-coordinate integral. the stated conclusion follows.
Formal statement
Proof (Lean source)
Every sparse-witness observational mechanism slot is globally measurable.
Formal statement
Proof (Lean source)
The sparse witness's observational joint density is globally measurable.
Formal statement
Proof (Lean source)
A fixed signed reflection followed by centering is continuous.
Formal statement
Proof (Lean source)
A continuous test function under the sparse observational law can be evaluated as the explicit three-coordinate iterated density integral. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Integrating the sparse density times its centered parent coordinate over the child coordinate leaves the centered parent coordinate unchanged. the stated conclusion follows.
Formal statement
Proof (Lean source)
Integrating the sparse density times the centered child coordinate produces one thirtieth of the centered parent coordinate. the stated conclusion follows.
Formal statement
Proof (Lean source)
Integrating the sparse density times both centered edge coordinates over the child coordinate produces one thirtieth of the squared parent coordinate. the stated conclusion follows.
Formal statement
Proof (Lean source)
Each reflected centered endpoint has zero mean under the sparse observational law. the stated conclusion follows.
Formal statement
Proof (Lean source)
The two reflected centered edge coordinates have the exact positive sparse-law joint moment 1/90. the stated conclusion follows.
Formal statement
Proof (Lean source)
The exact nonzero centered cross-moment rules out independence of the sparse witness's unique adjacent coordinate pair. the stated conclusion follows.
Formal statement
Proof (Lean source)
The sparse witness is causally minimal for the one-edge three-node DAG. the stated conclusion follows.
Formal statement
Proof (Lean source)
The sparse witness is faithful to 0 → 1 with isolated node 2. the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.WitnessMomentMmdAssembly 10 declarations
For a parent coordinate, the sparse child-weight integral averages the squared intervention density against the sparse denominator.
Definition (Lean source)
At a point of the unit interval, the sparse child-weight integral has the stated derivative.
Formal statement
Proof (Lean source)
At a point of the unit interval, the derivative of the sparse child-weight integral equals its centered-weight formula.
Formal statement
Proof (Lean source)
The sparse child-weight integral is continuous on the unit interval.
Formal statement
Proof (Lean source)
The derivative of the sparse child-weight integral is interval-integrable.
Formal statement
Proof (Lean source)
The integral of the negated cancellation primitive equals its explicit centered mean.
Formal statement
Proof (Lean source)
The unreflected sparse construction has a strictly positive quantitative moment gap.
Formal statement
Proof (Lean source)
The sparse witness's second-moment contrast equals the negative analytic gap.
Formal statement
Proof (Lean source)
The explicit sparse witness has the required strictly positive observed-ratio moment gap.
Formal statement
Proof (Lean source)
The explicit sparse witness has the required strictly positive Gaussian-kernel discrepancy.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.WitnessPath 3 declarations This file records the elementary one-dimensional facts about the child-mechanism coefficient along the path from the cancellation witness to the sparse witness.
Explicit cancellation-to-sparse witness path
This file records the elementary one-dimensional facts about the child-mechanism coefficient along the path from the cancellation witness to the sparse witness.
The child-mechanism coefficient on the affine path from the cancellation witness (t = 0) to the sparse witness (t = 1).
Definition (Lean source)
Convex interpolation preserves the coefficient bound on the unit interval. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Every coefficient on the closed cancellation-to-sparse segment is nonconstant. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.WitnessPathRegularity 1 declarations This file records the positive, normalized, smooth part of stratum preservation along the closed affine path.
Affine witness-path regularity
This file records the positive, normalized, smooth part of stratum preservation along the closed affine path. Causal minimality and the fixed-sign cell are handled separately by the analytic perturbation argument.
Convex interpolation with the embedded sparse endpoint preserves positivity, normalization, and C³ smoothness throughout the closed unit interval. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.WitnessQuantitative 25 declarations This file isolates the elementary exponential and rational estimates used in the quantitative moment and Gaussian-MMD certificate.
Rational bounds for the explicit sparse witness
This file isolates the elementary exponential and rational estimates used in the quantitative moment and Gaussian-MMD certificate.
The one-dimensional weight appearing after differentiating the sparse second-moment integrand with respect to its parent coefficient.
Definition (Lean source)
The logarithmic derivative of the sparse weight has the explicit form used in the quantitative moment-gap argument. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
For every parent coefficient in [-1/10,1/10], the logarithmic derivative of the sparse weight is at least 68/9 on the unit interval. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The sparse weight derivative is its value times the explicit logarithmic derivative factor. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The exponential normalizer in the witness is strictly below 55. the stated conclusion follows.
Formal statement
The normalizing constant 4 / (exp 4 - 1) exceeds 2/27. the stated conclusion follows.
Formal statement
Proof (Lean source)
On the coefficient strip used by the witness, the sparse weight is strictly above the rational floor obtained from c > 2/27 and p₂ ≤ 11/10. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The derivative of the sparse weight has the uniform rational lower bound used in the moment certificate. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The derivative certificate integrates to a uniform secant lower bound on the unit interval. This is the monotonicity input for the covariance step in the sparse moment calculation. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Centering at the midpoint turns the secant estimate into the pointwise quadratic lower bound whose integral is the 1/6 covariance factor. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Integrating the centered secant estimate supplies the exact 1/6 factor used in the sparse second-moment certificate. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Convexity of the exponential puts the cancellation primitive in [-1,0] on the unit interval. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Reflection preserves the nonconstancy of the centered coordinate on the unit interval. the stated conclusion follows.
Formal statement
Proof (Lean source)
The cancellation primitive is strictly negative at the midpoint of the unit interval. the stated conclusion follows.
Formal statement
Proof (Lean source)
Reflection preserves the nonconstancy of the cancellation coefficient on the unit interval. the stated conclusion follows.
Formal statement
Proof (Lean source)
A nonconstant reflected parent coefficient makes the affine child conditional genuinely depend on that parent somewhere on the unit square. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Both explicit witness child conditionals genuinely depend on the reflected parent coordinate on the unit square. the stated conclusion follows.
Formal statement
Proof (Lean source)
The sparse child conditional lies between 9/10 and 11/10 on the latent cube. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
On the latent cube the sparse child ratio is strictly between zero and five. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The rational lower bound for the exponential-tilt mean excess used in the sparse moment calculation. the stated conclusion follows.
Formal statement
Proof (Lean source)
The product of rational lower bounds in the sparse moment argument is the stated exact certificate. the stated conclusion follows.
Formal statement
Proof (Lean source)
The exact rational lower certificate in the sparse moment calculation is strictly larger than 3 / 10000. the stated conclusion follows.
Formal statement
Proof (Lean source)
The integrated sparse-weight covariance and exponential-tilt mean gap combine to exceed the paper's 3 / 10000 moment threshold. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
After the coordinate and tail estimates, the remaining numerical MMD comparison is strictly larger than 5 / 10^8. the stated conclusion follows.
Formal statement
Proof (Lean source)
The geometric majorant for the factorial tail beyond degree one hundred is below 10⁻¹⁵. the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.WitnessSigns 6 declarations This file proves the elementary logarithmic-derivative bounds that give the sparse witness its prescribed own-coordinate signs after reflection.
Derivative signs for the explicit witnesses
This file proves the elementary logarithmic-derivative bounds that give the sparse witness its prescribed own-coordinate signs after reflection.
The normalized exponential intervention density has logarithmic slope four. the stated conclusion follows.
Formal statement
Proof (Lean source)
The unreflected child log ratio has slope 4 - K / (5p). Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Reflection reverses the child log-ratio derivative. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The reflected sparse witness has the prescribed strict own-coordinate derivative signs. the stated conclusion follows.
Formal statement
Proof (Lean source)
The reflected cancellation witness has the prescribed strict own-coordinate derivative signs. the stated conclusion follows.
Formal statement
Proof (Lean source)
Both explicit witnesses are positive, normalized, smooth to every finite order, and obey their prescribed own-coordinate derivative signs. the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.WitnessTransport 4 declarations This file records the distribution-function and first-moment calculations used to transport the sparse witness's derivative bound along the exponential tilt.
Exponential-tilt transport identities
This file records the distribution-function and first-moment calculations used to transport the sparse witness's derivative bound along the exponential tilt.
The exponential intervention density has its stated closed-form distribution function. the stated conclusion follows.
Formal statement
Proof (Lean source)
The exponential-tilt distribution function lies below the uniform distribution function. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The exponential intervention density has the exact first moment used in the sparse gap. the stated conclusion follows.
Formal statement
Proof (Lean source)
The exponential-tilt mean excess over the uniform mean has its exact closed form. the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.Helpers.Witnesses 46 declarations This file contains the elementary compact-cube mechanisms used by the genericity and cancellation arguments.
Explicit sparse, cancellation, and affine-path mechanisms
This file contains the elementary compact-cube mechanisms used by the genericity and cancellation arguments.
Reflection of a coordinate when its prescribed sign is negative.
Definition (Lean source)
The centered affine function 2z-1.
Definition (Lean source)
The normalized exponential intervention density.
The cancellation primitive H.
The three-node graph 0 → 1 with node 2 isolated.
Definition (Lean source)
The three-node edge relation has no directed cycle.
Formal statement
Proof (Lean source)
The fixed three-node witness DAG.
Definition (Lean source)
Reflected coordinate selected by a sign vector.
Definition (Lean source)
Sparse witness observational conditional mechanism.
Definition (Lean source)
Sparse witness intervention mechanism.
Definition (Lean source)
The sparse observational factor depends only on its own coordinate and graph parents.
Formal statement
Proof (Lean source)
The explicit reflected sparse witness on 0 → 1 plus an isolated node.
Definition (Lean source)
Cancellation witness observational conditional mechanism.
Definition (Lean source)
The cancellation observational factor depends only on its own coordinate and graph parents.
Formal statement
Proof (Lean source)
The explicit reflected faithful cancellation mechanism.
Definition (Lean source)
Edge-specific sparse endpoint embedded in an arbitrary DAG.
Definition (Lean source)
Given the selected directed edge, the embedded sparse factor depends only on its own coordinate and graph parents.
Formal statement
Proof (Lean source)
The edge-specific sparse endpoint used by the affine perturbation.
Definition (Lean source)
The affine interpolation of two mechanisms remains local to each node and its parents.
Formal statement
Proof (Lean source)
For a finite dimension, DAG, sign pattern, stratum point, directed edge endpoints, edge certificate, and real path parameter, the unrestricted affine mechanism path interpolates toward the embedded sparse witness.
Definition (Lean source)
Nodewise normalized affine interpolation, indexed exactly by t ∈ [0,1].
Definition (Lean source)
The exponential intervention density integrates to one on the unit interval.
Formal statement
Proof (Lean source)
The centered coordinate integrates to zero on the unit interval.
Formal statement
Proof (Lean source)
Reflection about the midpoint preserves integrals over the unit interval. the stated conclusion follows.
Formal statement
Proof (Lean source)
Every reflected exponential intervention density is normalized. the stated conclusion follows.
Formal statement
Proof (Lean source)
Every reflected centered coordinate has zero integral. the stated conclusion follows.
Formal statement
Proof (Lean source)
Every sparse observational conditional is normalized in its own coordinate. the stated conclusion follows.
Formal statement
Proof (Lean source)
Every cancellation observational conditional is normalized in its own coordinate. the stated conclusion follows.
Formal statement
Proof (Lean source)
The cancellation primitive vanishes at both endpoints of the unit interval.
Formal statement
Proof (Lean source)
The derivative of the cancellation primitive is the intervention density minus one.
Formal statement
Proof (Lean source)
The cancellation primitive genuinely varies, as witnessed by its nonzero derivative at zero. the stated conclusion follows.
Formal statement
Proof (Lean source)
On the unit interval the cancellation primitive lies between minus one and one. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
A prescribed coordinate reflection preserves the closed unit interval. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The centered coordinate has absolute value at most one on the unit interval. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The embedded sparse conditional stays uniformly between 9/10 and 11/10 on the latent cube. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Every embedded sparse observational conditional is normalized in its own coordinate. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The edge-specific sparse endpoint is positive, normalized, and smooth on every finite DAG, including DAGs with additional unused parents and edges. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The normalized exponential intervention density is strictly positive. the stated conclusion follows.
Formal statement
Proof (Lean source)
A rational lower bound on the exponential normalizing constant used by the quantitative sparse certificate. the stated conclusion follows.
Formal statement
Proof (Lean source)
On the unit interval the intervention density is strictly below 13/3. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Every sparse observational mechanism is strictly positive on the latent cube. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The sparse witness is positive, normalized, and C³ on every mechanism domain. the stated conclusion follows.
Formal statement
Proof (Lean source)
Every cancellation observational mechanism is strictly positive on the latent cube. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The cancellation witness is positive, normalized, and C³ on every mechanism domain. the stated conclusion follows.
Formal statement
Proof (Lean source)
Every sparse-witness mechanism component is smooth to every finite order. the stated conclusion follows.
Formal statement
Proof (Lean source)
Every cancellation-witness mechanism component is smooth to every finite order. the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.TExactRatioDecoder 11 declarations This file states the population transitive-closure, continuous conditional-rank, parent-pruning, ordering-independence, and representation-uniqueness conclusions.
Exact ratio decoder
This file states the population transitive-closure, continuous conditional-rank, parent-pruning, ordering-independence, and representation-uniqueness conclusions. Faithfulness is confined to a separate overlap corollary.
The componentwise C² ambiguity relating two compatible representations.
Definition (Lean source)
Common law-selected scalar ranks and aligned edges assemble the componentwise C² equivalence, including explicit inverse charts on the closed latent interval. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Exact law-only pruning for two compatible causal-minimal representations first aligns their graphs; their common selected rank coordinates then assemble the componentwise C² ambiguity. No cover-separation condition is imposed on the competitor. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
On the faithful overlap with von Kügelgen et al. (2023), the present law-only decoder uses one unknown-target intervention per node, strictly fewer than the comparator's two interventions per node in arbitrary dimension, while retaining representation uniqueness.
Definition (Lean source)
Explicit scope boundary for the comparison with von Kügelgen et al. (2023): the present result assumes positive C³ densities on the compact latent cube and C² mixing. In positive dimension that cube is strictly smaller than the full Euclidean latent space, and derivative order two is not the comparator's C¹ order.
Definition (Lean source)
Relative to Wendong et al. (2023) and Yao et al. (2025), the graph, topological order, and environment-to-coordinate alignment are outputs computed from the observed laws, rather than supplied structural inputs.
Definition (Lean source)
Formal scope/comparison payload: the frozen von-Kügelgen intervention-count and noncoverage clauses, recovery of the structure supplied by Wendong/Yao, and the bivariate MMD witness.
Definition (Lean source)
All mathematical conclusions of the exact population decoder theorem.
Definition (Lean source)
The formal comparator payload follows from exact graph recovery, representation uniqueness, the bivariate edge witness, and predecessor containment; target uniqueness is supplied by the world's target permutation. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Cover-separated positive smooth causal-minimal mechanisms are decoded exactly from their observed environment laws, up to relabeling and componentwise C² diffeomorphisms. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Faithful-overlap corollary; faithfulness is deliberately not a premise of the main theorem. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.TGenericCoverSeparation 27 declarations This file states the open-dense direct-edge result and its residual Gaussian-MMD ancestral-cover consequence, including the empty-graph case.
Generic cover separation
This file states the open-dense direct-edge result and its residual Gaussian-MMD ancestral-cover consequence, including the empty-graph case.
Relabelling the canonical intervention environments does not change the latent direct-edge contrast after transporting the two environment indices back through the permutation. the stated conclusion follows.
Formal statement
Proof (Lean source)
For each fixed direct edge, the corresponding canonical contrast-nonzero locus is dense in the mechanism stratum, independently of the target permutation. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The observational value coordinate is continuous on the mechanism stratum by construction of the induced product C² topology. the stated conclusion follows.
Formal statement
Proof (Lean source)
The intervention value coordinate is continuous on the mechanism stratum by construction of the induced product C² topology. the stated conclusion follows.
Formal statement
Proof (Lean source)
Uniform convergence of a continuous family, combined with continuous motion of the argument, gives joint continuity of evaluation. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Observational-factor evaluation is jointly continuous in a stratum mechanism and a compact latent state. the stated conclusion follows.
Formal statement
Proof (Lean source)
Intervention-factor evaluation is jointly continuous in a stratum mechanism and a unit coordinate. the stated conclusion follows.
Formal statement
Proof (Lean source)
Coordinatewise projection supplies a continuous ambient representative of a latent-cube point. the stated conclusion follows.
Formal statement
Proof (Lean source)
The coordinatewise compact-cube projection belongs to the latent cube.
Formal statement
Proof (Lean source)
The compact-cube rational contrast integrand, continuously extended to the ambient latent space by coordinatewise projection, is jointly continuous in the mechanism and latent state. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
A canonical direct-edge second-moment contrast varies continuously with the mechanism in the induced relative product C² topology. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The explicit Gaussian feature vector depends continuously on its scalar argument. the stated conclusion follows.
Formal statement
Proof (Lean source)
The observational Gaussian-embedding integrand is jointly continuous on the mechanism stratum and compact latent cube. the stated conclusion follows.
Formal statement
Proof (Lean source)
The target-interventional Gaussian-embedding integrand is jointly continuous on the mechanism stratum and compact latent cube. the stated conclusion follows.
Formal statement
Proof (Lean source)
The canonical observational ratio-law embedding is the explicit weighted cube integral. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The canonical interventional ratio-law embedding is the explicit weighted cube integral. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The canonical Gaussian population discrepancy varies continuously with the mechanism. the stated conclusion follows.
Formal statement
Proof (Lean source)
A finite intersection of open dense sets is dense, without any Baire-space assumption. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Direct-edge contrast separation is open in the stratum topology. the stated conclusion follows.
Formal statement
Proof (Lean source)
Direct-edge contrast separation is dense in the stratum topology. the stated conclusion follows.
Formal statement
Proof (Lean source)
Ancestral-cover Gaussian-MMD separation is open in the mechanism stratum. the stated conclusion follows.
Formal statement
Proof (Lean source)
An ancestral cover in a DAG is necessarily a direct edge. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
An edge-free DAG has no ancestral covers. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Both separation conditions are vacuous for an edge-free DAG. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
The complement of an open dense set is closed, nowhere dense, and meagre. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
Direct-edge raw second-moment separation implies Gaussian-MMD separation on every ancestral cover. the stated conclusion follows.
Formal statement
Proof (Lean source)
In every nonempty fixed-DAG sign stratum, direct-edge moment separation is open dense and implies an open dense residual ancestral-cover MMD region with closed nowhere-dense complement. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.TSimultaneousConfidenceEdges 2 declarations This file states the conditional and unconditional simultaneous MMD bounds, soundness of selected edges, and transitive-closure recovery under a cover margin.
Simultaneous confidence edges
This file states the conditional and unconditional simultaneous MMD bounds, soundness of selected edges, and transitive-closure recovery under a cover margin.
The event that every empirical MMD is within the simultaneous confidence radius.
Definition (Lean source)
Under the simultaneous first-stage event, sample splitting yields familywise MMD confidence bounds. Selected arrows are ancestral, and a two-radius cover margin recovers the true transitive closure. Given the stated inputs and conditions, the stated conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.ExactID.EID_CrlCoverratioMmdGenericity_Research.TSparseWitnessCertificate 2 declarations The theorem certifies both explicit three-node constructions, quantitative sparse separation, and the exact cancellation example.
Sparse and cancellation witness certificate
The theorem certifies both explicit three-node constructions, quantitative sparse separation, and the exact cancellation example.
The already established witness lemmas assemble both faithfulness assertions, all regularity, and exact cancellation. This leaves only the quantitative sparse moment/MMD estimates to the final assembly. the stated conclusion follows.
Formal statement
Proof (Lean source)
The reflected sparse and cancellation mechanisms satisfy the model atoms; the sparse witness has the certified moment and Gaussian-MMD gaps, while the cancellation ratio law is unchanged. the stated conclusion follows.