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.

Orthogonality of the full two-level factorial contrasts

Statement

For the design in Two-level full factorial designs and coded effects, let $c_{A} = (x_{A} (x))_{x \in X_{k}}$ be the column indexed by $A \subseteq [k]$ . Then $⟨ c_{A}, c_{B} ⟩ = {\begin{cases} 2^{k}, & A = B, \\ 0, & A \neq B . \end{cases}$ Thus the columns are pairwise orthogonal and $X^{T} X = 2^{k} I_{2^{k}}, 2^{- k} X^{T} X = I_{2^{k}} .$ This is a deterministic property of the design matrix.

Facts & Assumptions

Given: An integer $k \geq 1$ , the full run set $X_{k}$ , and the columns $c_{A}$ from the Statement.

[F1]

Two-level full factorial designs and coded effects: the runs are all sign vectors in ${- 1, + 1}^{[k]}$ , and the column indexed by $A$ has entries $x_{A} = \prod_{j \in A} x_{j}$ , with $x_{\emptyset} = 1$ .

[F2]

The standard formulas $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ and $\sum_{k < n} x_{k} \overline{y_{k}}$ on $C^{n}$ are inner products: the standard real coordinate pairing is $⟨ u, v ⟩ = \sum_{i} u_{i} v_{i}$ .

[F3]

Orthogonal vectors and subspaces, orthogonal and orthonormal sets, and orthonormal bases: two vectors are orthogonal exactly when their inner product is zero.

Proof

technique · direct sign cancellation over the symmetric difference

1.1givenF1F2algebra

For $A, B \subseteq [k]$ , every factor in $A \cap B$ occurs twice in $x_{A} x_{B}$ and has square $1$ , while factors outside $A △ B$ do not occur. Hence $x_{A} x_{B} = \prod_{j \in A △ B} x_{j}$ . By [F2], $⟨ c_{A}, c_{B} ⟩ = \sum_{x \in X_{k}} \prod_{j \in A △ B} x_{j}$ .

2.1step 1.1F1choosealgebra

If $A = B$ , then $A △ B = \emptyset$ and every summand in step 1.1 equals $1$ , so the sum is $2^{k}$ . If $A \neq B$ , choose $j \in A △ B$ and pair each run $x$ with the run obtained by reversing only $x_{j}$ . This is a fixed-point-free involution of $X_{k}$ and reverses the sign of the summand, so the terms cancel in pairs and the sum is $0$ .

3.1F1F3step 1.1step 2.1algebra∎

The matrix entry $(A, B)$ of $X^{T} X$ is $⟨ c_{A}, c_{B} ⟩$ . Step 2.1 therefore gives $X^{T} X = 2^{k} I_{2^{k}}$ and the scaled identity; [F3] gives pairwise orthogonality of distinct columns.

Depends on

Used by

Dependency tree · two levels

11 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.2 and 8.6 (standard reference, not scraped)
NIST/SEMATECH e-Handbook of Statistical Methods, §5.3.3.3.1, Two-level full factorial designs (standard reference, not scraped)