ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Positivity failure prevents standardization and IPW identification

Example

Let $L \in {0, 1}$ with $P (L = 0) = P (L = 1) = 1 / 2$ . In both full-data models, set $P (A = 1 ∣ L = 0) = 0$ and $P (A = 1 ∣ L = 1) = 1 / 2$ , and set $Y^{0} = 0$ everywhere and $Y^{1} = 1$ when $L = 1$ . In model $P_{0}$ , also set $Y^{1} = 0$ when $L = 0$ ; in model $P_{2}$ , set $Y^{1} = 2$ when $L = 0$ . Treatment assignment at $L = 1$ is independent of these deterministic potential outcomes, so conditional exchangeability holds in each model. Define the observed outcome by consistency, $Y = Y^{A}$ .

Facts & Assumptions

Given: The two specified full-data laws, consistency, and the potential-outcome conventions of Potential outcomes and consistency. The target is the population mean $E [Y^{1}]$ .

[A1]

Treatment assignment has zero probability of treatment $1$ at $L = 0$ in both models; the point-treatment setup is as in Potential outcomes and consistency.

[F1]

The standardization and IPW functionals require the conditional probability $e_{1} (L)$ to be positive almost surely. (Standardization for a causal mean, Inverse probability weighting for a causal mean)

[F2]

Conditional treatment-indicator factorization gives $E [1_{{A = 1}} Y^{1} ∣ σ (L)] = e_{1} (L) E [Y^{1} ∣ σ (L)]$ under conditional exchangeability. (Conditional treatment-indicator factorization)

[F3]

Identifiability requires equal observed laws to imply equal target values. (Identifiability of an estimand)

Verification

1.1givenA1construct

In both models the observed law assigns probability $1 / 2$ to $(L, A, Y) = (0, 0, 0)$ , probability $1 / 4$ to $(1, 1, 1)$ , and probability $1 / 4$ to $(1, 0, 0)$ . The unobserved value of $Y^{1}$ at $L = 0$ does not enter any observed outcome because $A = 0$ there.

2.1F3step 1.1algebra

The target means differ: $E_{P_{0}} [Y^{1}] = \frac{1}{2}$ while $E_{P_{2}} [Y^{1}] = \frac{3}{2}$ . Since the observed laws in step 1.1 coincide, [F3] shows that $E [Y^{1}]$ is not identified in this model class.

3.1A1F1F2step 2.1∎

Here $e_{1} (0) = 0$ , so the observed treated conditional mean at $L = 0$ is unavailable and both $q_{1} (0) / e_{1} (0)$ and the treated weight $I_{1} / e_{1} (L)$ are undefined. Also [F2] gives $E [I_{1} Y^{1} ∣ L = 0] = 0 \cdot E [Y^{1} ∣ L = 0] = 0$ in both models, leaving the differing target-stratum means unrecovered.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.