TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Coefficient and factorial-effect variances under equal replication

Statement

Let $r \geq 1$ be an integer. For every run $x \in X_{k}$ and replicate $s \in {1, \dots, r}$ , suppose $Y_{x, s} = \sum_{B \subseteq [k]} β_{B} x_{B} + ϵ_{x, s},$ where the coefficients $β_{B}$ are fixed and the errors are mutually independent real random variables on one probability space, with $E [ϵ_{x, s}^{2}] < \infty$ and common variance $σ^{2} < \infty$ . Define ${\overline{Y}}_{x} = r^{- 1} \sum_{s = 1}^{r} Y_{x, s}$ and ${\hat{β}}_{A} = 2^{- k} \sum_{x \in X_{k}} x_{A} {\overline{Y}}_{x} .$ Then for every $A \subseteq [k]$ , $Var ({\hat{β}}_{A}) = \frac{σ^{2}}{r 2^{k}} .$ For nonempty $A$ , define ${\hat{τ}}_{A}$ as the difference of the mean run responses ${\overline{Y}}_{x}$ over $G_{A, +}$ and $G_{A, -}$ from Two-level full factorial designs and coded effects. Then ${\hat{τ}}_{A} = 2 {\hat{β}}_{A}, Var ({\hat{τ}}_{A}) = \frac{4 σ^{2}}{r 2^{k}} .$

The variance calculation assumes equal replication at every run and independence across all run-replicate errors. It requires neither Gaussian errors nor zero interactions. A zero-mean assumption is additionally needed if $β_{B}$ is to denote coefficients of the mean response; it is not needed for these variance identities.

Facts & Assumptions

Given: The full factorial design and coefficient convention in Two-level full factorial designs and coded effects, the model and error hypotheses in the Statement, and the contrast identity in Orthogonality of the full two-level factorial contrasts.

[F1]

Two-level full factorial designs and coded effects: each column is $x_{A} = \prod_{j \in A} x_{j}$ , and the normalized coefficient of a response table $y$ is $2^{- k} \sum_{x} x_{A} y_{x}$ ; for nonempty $A$ , the factorial effect is the difference of the two $x_{A}$ group means.

[F2]

Orthogonality of the full two-level factorial contrasts: $2^{- k} \sum_{x} x_{A} x_{B} = 1$ when $A = B$ and $0$ otherwise.

[F3]

Random elements and real random variables: a real random variable is a measurable map from a probability space to $R$ with its Borel sigma-algebra.

[F4]

Independent random elements: a family of random elements on one probability space is independent when their generated sigma-algebras are independent.

[F5]

Expectation of a nonnegative or integrable random variable: for a nonnegative measurable random variable $U$ , $E [U] = \int U d P$ .

[F6]

Moments, variance, and covariance on a probability space: for a square-integrable real random variable $Z$ , $Var (Z) = E [(Z - E Z)^{2}]$ .

[F7]

Variance and covariance identities for random variables: covariance is symmetric and bilinear on finite linear combinations of square-integrable real random variables.

[F8]

Variance adds for every finite pairwise-independent family: the variance of a finite sum of pairwise-independent square-integrable real random variables is the sum of their variances.

Proof

technique · isolate each coefficient by the contrast Gram identity, then add the variances of the signed independent errors

1.1givenF1F2algebra

Substitute the model and the run averages into the definition of ${\hat{β}}_{A}$ . This gives ${\hat{β}}_{A} = \sum_{B \subseteq [k]} β_{B} (2^{- k} \sum_{x \in X_{k}} x_{A} x_{B}) + \frac{1}{r 2^{k}} \sum_{x \in X_{k}} \sum_{s = 1}^{r} x_{A} ϵ_{x, s} .$ By [F2], the parenthesized factor is $1$ for $B = A$ and $0$ otherwise. Thus ${\hat{β}}_{A} - β_{A} = (r 2^{k})^{- 1} \sum_{x, s} x_{A} ϵ_{x, s}$ .

1.2givenF3F4F5F6F7algebra

Fix $A$ and put $Z_{x, s} = x_{A} ϵ_{x, s}$ . Each $x_{A}$ is $+ 1$ or $- 1$ , so multiplication by $x_{A}$ is a Borel bijection whose inverse is itself; consequently $σ (Z_{x, s}) = σ (ϵ_{x, s})$ . By [F3] and [F4] these variables remain mutually, hence pairwise, independent. Their second moments are finite by the hypothesis, and $2 ∣ z ∣ \leq 1 + z^{2}$ gives $E ∣ Z_{x, s} ∣ < \infty$ , so their variances are defined. By [F6], variance is covariance with both arguments equal; then [F7] gives $Var (Z_{x, s}) = x_{A}^{2} Var (ϵ_{x, s}) = σ^{2}$ .

2.1F7F8step 1.1step 1.2algebra

There are $r 2^{k}$ variables $Z_{x, s}$ . By [F8], their sum has variance $r 2^{k} σ^{2}$ . Applying the scalar rule from [F7] to step 1.1 yields $Var ({\hat{β}}_{A}) = (r 2^{k})^{- 2} r 2^{k} σ^{2} = σ^{2} / (r 2^{k})$ .

3.1F1F7step 2.1choosealgebra∎

For nonempty $A$ , choose $j \in A$ . Reversing coordinate $x_{j}$ bijects $G_{A, +}$ with $G_{A, -}$ , so each group has $2^{k - 1}$ runs. The difference of their run-average means is therefore $2^{1 - k} \sum_{x} x_{A} {\overline{Y}}_{x} = 2 {\hat{β}}_{A}$ by [F1]. Its variance is four times the coefficient variance from step 2.1, giving $4 σ^{2} / (r 2^{k})$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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

Gary W. Oehlert, A First Course in Design and Analysis of Experiments, Chapter 8, §§8.5–8.6 (standard reference, not scraped)
NIST/SEMATECH e-Handbook of Statistical Methods, §5.3.3.3.2, Full factorial example (standard reference, not scraped)