Pipeline-generated

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.

✓ 3 results · all verified · 3 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 3 also cleared it.

Potential outcomes and identification — Examples

1 · Prerequisites

2 · Summary

Finite worked models show how random assignment identifies a target contrast, how confounding changes an unadjusted comparison while standardization recovers the ATE, and how a positivity failure leaves two full-data laws with different effects compatible with the same observed law.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Randomized treatment identifies the target mean contrast

Example

Take $Ω = {u_{0}, u_{1}} \times {0, 1}$ with the uniform law. Let $U$ and $A$ be the first and second coordinates, let $L$ be constant, and set $Y^{0} = 0$ , $Y^{1} = 1_{{U = u_{1}}}$ , and $Y = Y^{A}$ . Then random assignment is independent of the potential outcomes, both treatment values have probability $1 / 2$ , and the target ATE is $1 / 2$ . The conditional means among the two treatment groups recover the same contrast.

Verification

Given: The finite probability space above; the definitions of potential outcomes and consistency, conditional exchangeability, positivity, and ATE; and the discrete-treatment identification theorem.

[A1] Choice is the axiom used by the library's conditional-expectation convention. The Axiom of Choice

[F1] Potential outcomes are indexed by treatment versions and consistency means $Y = Y^{A}$ almost surely. Potential outcomes and consistency

[F2] Conditional exchangeability is conditional independence of the potential-outcome family and $A$ given $L$ . Conditional exchangeability of potential outcomes

[F3] Conditional independence given the trivial sigma-algebra is ordinary independence, using the bounded-product identity. Conditional independence given a sigma-algebra

[F4] Positivity requires positive marginal and conditional probability for each treatment value in the contrast. Positivity for discrete treatment

[F5] The ATE is $E [Y^{1} - Y^{0}]$ . Average and conditional average treatment effects

[F6] Under consistency, conditional exchangeability and positivity, the potential-outcome mean equals the target-covariate integral of the observed treatment-stratum mean. Discrete-treatment potential-outcome means are identifiable

1.1givenF1algebra

Each of the four points $(u_{i}, a)$ has probability $1 / 4$ . By definition $Y = Y^{A}$ , so consistency [F1] holds; $Y^{0}, Y^{1}$ are bounded and hence integrable.

1.2A1F2F3F4algebra

For $i, a \in {0, 1}$ , $P (U = u_{i}, A = a) = 1 / 4 = P (U = u_{i}) P (A = a)$ . The pair $(Y^{0}, Y^{1})$ is a function of $U$ , so it is independent of $A$ ; since $L$ is constant, [F2] and [F3] give conditional exchangeability. Also $P (A = 0) = P (A = 1) = 1 / 2$ , and conditioning on constant $L$ leaves these probabilities unchanged, so [F4] holds.

2.1F5F6algebra∎

Under $P_{0}$ , $U$ remains uniform and $Y = Y^{0} = 0$ , so $m_{0} = 0$ . Under $P_{1}$ , $U$ remains uniform and $Y = Y^{1}$ , so $m_{1} = 1 / 2$ . As $P_{L}$ is a point mass, [F6] gives $E [Y^{0}] = 0$ and $E [Y^{1}] = 1 / 2$ ; hence the identified ATE is $1 / 2$ , agreeing with [F5].

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Binary confounding and standardization

Example

Let $Ω = {0, 1} \times {1, 2, 3, 4}$ with each point having probability $1 / 8$ , and write its coordinates as $(L, W)$ . Set $A = 1$ when $L = 0, W = 1$ or when $L = 1, W \in {1, 2, 3}$ , and set $A = 0$ otherwise. Let $Y^{0} = 10 L$ , $Y^{1} = 10 L + 1$ , and $Y = Y^{A}$ . Assignment depends on the prognostic covariate $L$ , but both treatment arms occur in both strata. The target ATE is $1$ ; the unadjusted treated-minus-untreated mean is $6$ ; standardization over the target law of $L$ returns $1$ .

Verification

Given: The finite probability space and variables above; the definitions of potential outcomes, conditional exchangeability, positivity, and ATE; and the discrete-treatment identification theorem.

[A1] Choice is assumed for the library's conditional-expectation classes. The Axiom of Choice

[F1] Consistency means that the observed outcome equals the potential outcome at the received treatment version. Potential outcomes and consistency

[F2] Conditional exchangeability is conditional independence of the full potential-outcome family and treatment given $L$ . Conditional exchangeability of potential outcomes

[F3] If one side of conditional independence is measurable with respect to the conditioning sigma-algebra, conditional independence holds. Conditional independence given a sigma-algebra

[F4] Positivity requires positive treatment probability in each target covariate stratum for every treatment in the contrast. Positivity for discrete treatment

[F5] The ATE is the target-population mean of $Y^{1} - Y^{0}$ . Average and conditional average treatment effects

[F6] Under consistency, conditional exchangeability and positivity, standardization identifies each potential-outcome mean. Discrete-treatment potential-outcome means are identifiable

1.1givenF1algebra

The point set has eight equally likely elements, $Y^{0}$ and $Y^{1}$ are bounded, and $Y = Y^{A}$ by construction, so all required integrability and consistency conditions hold by [F1].

1.2A1F2F3F4algebra

Given $L = l$ , $(Y^{0}, Y^{1}) = (10 l, 10 l + 1)$ is fixed, hence its sigma-algebra is contained in $σ (L)$ and [F3] gives conditional exchangeability [F2]. Direct counting gives $P (A = 1 ∣ L = 0) = 1 / 4$ , $P (A = 1 ∣ L = 1) = 3 / 4$ , and the complementary probabilities for $A = 0$ ; both marginal probabilities equal $1 / 2$ . Thus [F4] holds.

1.3F5F6algebra

In stratum $L = 0$ , the observed outcome means are $E [Y ∣ A = 1, L = 0] = 1$ and $E [Y ∣ A = 0, L = 0] = 0$ . In stratum $L = 1$ , they are $11$ and $10$ . Since $P (L = 0) = P (L = 1) = 1 / 2$ , [F6] standardizes the treatment means to $E [Y^{1}] = (1 + 11) / 2 = 6$ and $E [Y^{0}] = (0 + 10) / 2 = 5$ , so [F5] gives ATE $1$ .

2.1givenstep 1.2algebra∎

Bayes' rule gives $P (L = 1 ∣ A = 1) = 3 / 4$ and $P (L = 1 ∣ A = 0) = 1 / 4$ . Therefore $E [Y ∣ A = 1] = (1 / 4) 1 + (3 / 4) 11 = 8.5$ and $E [Y ∣ A = 0] = (3 / 4) 0 + (1 / 4) 10 = 2.5$ , whose difference is $6$ , not the ATE. The difference comes from the different target-covariate mixtures in the two treatment groups.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Positivity failure leaves the target unsupported

Example

Let $Ω = {0, 1}$ with each point having probability $1 / 2$ , and set $L = A = ω$ . Consider two full-data laws on this same observed space. In both, $Y^{0} = 0$ and $Y = Y^{A}$ . In law $Q_{1}$ , set $Y^{1} = 1$ everywhere; in law $Q_{2}$ , set $Y^{1} = L$ . Both laws give the same observed distribution: $(L, A, Y) = (0, 0, 0)$ or $(1, 1, 1)$ with probability $1 / 2$ each. Both satisfy consistency and conditional exchangeability given $L$ , but positivity fails. Their ATEs are respectively $1$ and $1 / 2$ , so the observed law and conditional exchangeability alone do not identify the ATE.

Verification

Given: The two full-data laws described above; the definitions of potential outcomes, conditional exchangeability, positivity, ATE and identifiability; and the theorem's positivity hypothesis.

[A1] Choice is assumed for the library's conditional-expectation classes. The Axiom of Choice

[F1] Consistency requires $Y = Y^{A}$ almost surely. Potential outcomes and consistency

[F2] Conditional exchangeability is conditional independence of potential outcomes and treatment given $L$ . Conditional exchangeability of potential outcomes

[F3] Conditional independence holds when one of its sigma-algebras is contained in the conditioning sigma-algebra. Conditional independence given a sigma-algebra

[F4] Positivity for a contrast requires positive treatment probability in each treatment arm almost surely on the target covariate law. Positivity for discrete treatment

[F5] The ATE is $E [Y^{1} - Y^{0}]$ . Average and conditional average treatment effects

[F6] Identifiability means the estimand is constant across parameter values with the same observed law. Identifiability of an estimand

[F7] The displayed standardization theorem assumes positivity for each treatment value in the contrast. Discrete-treatment potential-outcome means are identifiable

1.1givenF1algebra

In both laws, when $L = 0$ one has $A = 0, Y = Y^{0} = 0$ , and when $L = 1$ one has $A = 1, Y = Y^{1} = 1$ . Thus the observed law is identical in $Q_{1}, Q_{2}$ , and consistency [F1] holds in each.

1.2A1F2F3F4F7algebra

In each law the potential-outcome vector is $σ (L)$ -measurable and $A = L$ is $σ (L)$ -measurable. By [F3], conditional exchangeability [F2] holds. However, $P (A = 1 ∣ L = 0) = 0$ and $P (A = 0 ∣ L = 1) = 0$ , so [F4] fails despite $P (A = 0) = P (A = 1) = 1 / 2$ . Hence the hypotheses of [F7] are not met.

2.1F5F6step 1.1algebra∎

Under $Q_{1}$ , $E [Y^{1} - Y^{0}] = 1$ . Under $Q_{2}$ , $E [Y^{1} - Y^{0}] = E [L] = 1 / 2$ . The same observed law therefore corresponds to two target values, so [F6] says the ATE is not identifiable under consistency and conditional exchangeability without positivity.