ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

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].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

25 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.