TheoremStatement: AI-adaptedProof: 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.

Rank capacity and factorization ambiguity of a low-rank adapter

Statement

Fix positive integers $d, k$ , an integer $1 \leq r \leq \min (d, k)$ , a nonzero real number $c$ , and a base matrix $W_{0} \in R^{d \times k}$ . For every pair $B \in R^{d \times r}$ and $A \in R^{r \times k}$ , the adapter update $Δ = c B A$ has matrix rank at most $r$ , where rank is the dimension of the image of the associated linear map. Conversely, every target update $Δ \in R^{d \times k}$ of rank at most $r$ has at least one representation $Δ = c B A$ with these factor shapes. For any such factors and any invertible matrix $M \in R^{r \times r}$ , the transformed factors $B M$ and $M^{- 1} A$ represent the same update. Thus the factorization is not identifiable: every target update of rank at most $r$ has more than one factor pair. A target update of rank greater than $r$ cannot be represented.

Statement references

Axler, Linear Algebra Done Right, §7E, Theorem 7.70: singular value decomposition for finite-dimensional inner-product spaces

Axler, Linear Algebra Done Right, §7E, Theorem 7.80: matrix factorization from the singular value decomposition

Facts & Assumptions

Given: The factor dimensions and nonzero scale in the statement.

[F1]

Low-rank adaptation of a linear layer: the update matrix is $c B A$ , with $A \in R^{r \times k}$ , $B \in R^{d \times r}$ , and $c \neq 0$ .

[F2]

Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition: every linear map between finite-dimensional real or complex inner-product spaces has an SVD with positive singular values and orthonormal domain and range vectors; its proof shows the range vectors span the image, so their number equals the rank.

Proof

1.1givenF1algebra

The image of $B A$ is contained in the image of $B$ , whose dimension is at most the number $r$ of columns of $B$ . Multiplication by the nonzero scalar $c$ preserves image dimension, so $rank (c B A) \leq r$ .

1.2givenF2choosealgebra

Let $Δ \in R^{d \times k}$ have rank $q \leq r$ . If $q = 0$ , then $Δ = 0$ and the zero factors give $Δ = c B A$ . If $q > 0$ , apply [F2] to the real linear map $Δ / c : R^{k} \to R^{d}$ . Since $c \neq 0$ , this map has rank $q$ , so its SVD has exactly $q$ positive terms: $Δ / c = \sum_{j = 1}^{q} s_{j} u_{j} v_{j}^{T}$ , with $s_{j} > 0$ and orthonormal vectors $u_{j} \in R^{d}$ , $v_{j} \in R^{k}$ .

1.3F1givenalgebra

If $M \in R^{r \times r}$ is invertible, associativity gives $(B M) (M^{- 1} A) = B (M M^{- 1}) A = B A$ , so the transformation preserves $c B A$ .

2.1F1step 1.2constructalgebra

For $j \leq q$ , set the $j$ th column of $B$ to $\sqrt{s_{j}} u_{j}$ and the $j$ th row of $A$ to $\sqrt{s_{j}} v_{j}^{T}$ ; fill the remaining columns of $B$ and rows of $A$ with zero. These matrices have the required shapes and $B A = \sum_{j = 1}^{q} s_{j} u_{j} v_{j}^{T} = Δ / c$ , hence $c B A = Δ$ .

3.1givenstep 1.1step 2.1step 1.3algebra∎

If $rank (Δ) > r$ , step 1.1 rules out a factor representation. If $Δ \neq 0$ has rank at most $r$ , step 2.1 gives a representation with $B \neq 0$ ; the matrix $M = 2 I_{r}$ , where $I_{r}$ is the identity on $R^{r}$ , is invertible with inverse $\frac{1}{2} I_{r}$ , and $B M = 2 B \neq B$ , so step 1.3 gives a distinct factor pair with the same product. If $Δ = 0$ , let $A^{'}$ have entry $1$ in position $(1, 1)$ and all other entries $0$ ; then $(B, A) = (0, 0)$ and $(B, A) = (0, A^{'})$ are distinct factor pairs for the zero update. Thus every representable target update has multiple factor pairs.

Depends on

Used by

Dependency tree · two levels

8 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

Edward Hu et al., LoRA: Low-Rank Adaptation of Large Language Models, arXiv:2106.09685v2, §4.1 (standard reference, not scraped)
Sheldon Axler, Linear Algebra Done Right, fourth edition, §7E, Theorems 7.70 and 7.80 (standard reference, not scraped)