LemmaStatement: 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.

A full-rank error-contrast matrix exists when n exceeds p

Statement

For every full-column-rank $X \in R^{n \times p}$ with $p < n$ , there exists an error-contrast matrix $K \in R^{n \times (n - p)}$ as defined in Error-contrast matrix for a full-rank fixed design.

Facts & Assumptions

Given: $X \in R^{n \times p}$ has full column rank and $p < n$ .

[F1]

For every subspace $W$ of finite-dimensional $R^{n}$ , $\dim W + \dim W^{⊥} = n$ . In finite dimension, $W^{⊥ ⊥} = W$ and $\dim W + \dim W^{⊥} = \dim V$ .

[F2]

Full column rank means the columns of $X$ are linearly independent; a basis is an independent spanning set, and finite dimension is the size of a finite basis. Fixed-design linear regression model, Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis, Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis.

[F3]

An error-contrast matrix has full-column-rank columns forming $col (X)^{⊥}$ . Error-contrast matrix for a full-rank fixed design.

[A1]

The columns of $X$ are linearly independent.

Proof

Given: A full-column-rank $X \in R^{n \times p}$ with $p < n$ .

1.1A1F1F2

Set $W = col (X)$ . By [A1] and [F2], the columns of $X$ form a basis of $W$ , so $\dim W = p$ . Applying [F1] gives $\dim W^{⊥} = n - p$ ; by [F2], this means $W^{⊥}$ has a basis with $n - p$ elements.

2.1F2step 1.1choose

Since $W^{⊥}$ has dimension $n - p$ , [F2] gives a basis $k_{1}, \dots, k_{n - p}$ of $W^{⊥}$ . Put these vectors into the columns of $K$ . The columns are independent and span $W^{⊥}$ , so $K$ has full column rank.

3.1F3step 2.1∎

Every column $k_{ℓ}$ is orthogonal to each column of $X$ , hence $X^{T} k_{ℓ} = 0$ . Thus $X^{T} K = 0$ and $K$ satisfies the error-contrast definition [F3]. This proves existence.

Depends on

Used by

Restricted maximum likelihood from error contrasts Definition

Cited to discharge well-definedness by Error-contrast matrix for a full-rank fixed design.

Dependency tree · two levels

38 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

Fan Li, STA610 Lecture 4: Maximum Likelihood Estimation and Inference for the Hierarchical Normal Model, PDF pp. 4–5 (standard reference, not scraped)
Duchateau, Janssen, and Rowlands, Linear Mixed Models, Chapter 2 §2.4.2 (standard reference, not scraped)