ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge 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.

Nonadditive direct effects create positive variance-estimator bias

Example

Take four groups of four units, select exactly two groups for $ψ$ , and use $K_{i}^{ϕ} = K_{i}^{ψ} = 2$ in every group. Let $a_{1} = 1$ and $a_{2} = a_{3} = a_{4} = 0$ , and define the full potential-outcome schedule by $Y_{i j} (z_{i}) = a_{j} z_{i j} .$ The design has two groups per strategy and two units per treatment arm within each group, so every sample variance in the direct-effect variance estimator is defined.

Verification

Given: The design-based direct-effect variance estimator and theorem in Stratified interference and source design-based variance estimators and Stratified-interference variance estimators are conservative.

[F1] Stratified interference and source design-based variance estimators: the direct-effect point estimator is the mean of the group control-minus-treatment sample means; its source variance estimator combines a sample variance across selected groups with the two within-group arm sample variances.

[F2] Stratified-interference variance estimators are conservative: the expected source variance estimator exceeds the design variance by $N^{- 2} \sum_{i} S_{i D}^{2} / n_{i}$ .

1.1givenF1constructalgebra

For any fixed group assignment, $Y_{i j} (z_{i})$ depends only on $z_{i j}$ . Hence changing peer assignments while holding the unit's treatment and the treated count fixed leaves its outcome unchanged, so stratified interference holds. The unit direct effects are $d_{i j} = Y_{i j} (0) - Y_{i j} (1) = - a_{j} = (- 1, 0, 0, 0)$ , which are not constant.

1.2givenF1algebra

The finite-population mean direct effect in each group is $- 1 / 4$ , and its finite-population variance is $S_{i D}^{2} = (3 / 4) / 3 = 1 / 4$ . Within a group, the estimated direct effect is $- 1 / 2$ if unit 1 is treated and $0$ otherwise, each with probability $1 / 2$ . Its variance is therefore $1 / 16$ . The within-group variance component ${\hat{v}}_{i} = s_{i 0}^{2} / 2 + s_{i 1}^{2} / 2$ is $1 / 4$ when unit 1 is treated and $0$ otherwise, so $E [{\hat{v}}_{i}] = 1 / 8$ .

1.3givenF1algebra

Two groups are selected for $ψ$ , and their within-group assignments are independent. The population direct-effect estimator is their mean. Its values are $- 1 / 2, - 1 / 4, 0$ with probabilities $1 / 4, 1 / 2, 1 / 4$ , respectively, so its mean is $- 1 / 4$ and its design variance is $1 / 32$ . For two selected groups, the between-group sample variance of their direct-effect estimates is $1 / 8$ when their outcomes differ and $0$ otherwise; the outcomes differ with probability $1 / 2$ , giving expected sample variance $1 / 16$ .

2.1givenF1step 1.2step 1.3algebra

The expected between-group term in the source variance estimator is $(1 - C / N) s_{D, ψ}^{2} / C = (1 / 4) s_{D, ψ}^{2}$ , hence its expectation is $1 / 64$ . The expected within-group term is $(C N)^{- 1}$ times the sum over the two selected groups' ${\hat{v}}_{i}$ values, giving $(1 / 8) (2 \cdot 1 / 8) = 1 / 32$ . Therefore the complete variance estimator has expectation $1 / 64 + 1 / 32 = 3 / 64$ .

3.1F2step 1.1step 2.1algebra∎

The positive bias is $3 / 64 - 1 / 32 = 1 / 64$ . It also equals the theorem's correction $N^{- 2} \sum_{i} S_{i D}^{2} / n_{i} = 16^{- 1} \cdot 4 \cdot (1 / 4) / 4 = 1 / 64$ . Thus the nonadditive individual effects give a strict conservative bias despite stratified interference and all required sample sizes.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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

Sources

Michael G. Hudgens and M. Elizabeth Halloran, Toward Causal Inference With Interference, Theorem 6 and Corollary (standard reference, not scraped)