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.
Every Euclidean linear map has a unique matrix and satisfies for some
Statement
For every linear there is a unique matrix such that . Moreover there is with for every .
Facts & Assumptions
Given: A Euclidean linear map .
The coordinate list of with respect to the ordered basis is its ordinary coordinate list, and (The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension ).
The Euclidean norm of is , and it is a norm (The Euclidean inner product on ).
Proof
Put . By [L1] and linearity, , so .
The columns determine every value in step 1.1, and evaluating the displayed formula at shows that every representing matrix has exactly these entries; thus the matrix is unique.
Let . Cauchy--Schwarz [L3] in each row and summing gives , hence .
Depends on
- A linear map $L:\mathbb{R}^m\to\mathbb{R}^n$ in Euclidean coordinates
- The standard list $e : n \to F^{n}$ with $e_i(i) = 1_F$ and $e_i(j) = 0_F$ for $j \ne i$ is an ordered basis of $F^{n}$; hence $\dim_F F^{n} = n$, and $F^{0}$ is the zero space with basis $\varnothing$ and dimension $0$
- The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$
- A norm on a real vector space, the induced metric, and the dictionary with the metric axioms
- Finite sums and finite products, by recursion
- Laws of finite sums and finite products
- Cauchy-Schwarz $\lvert\langle x,y\rangle\rvert \le \lVert x\rVert_2\lVert y\rVert_2$ with its equality case, the triangle inequality for $\lVert\cdot\rVert_2$, the parallelogram law and polarisation
Used by
- The Jordan content of the parallelepiped spanned by the columns of a square real matrix is the absolute value of its determinant Corollary
- Newton maps are uniform contractions near a point with invertible derivative Lemma
- A linear endomorphism of ℝⁿ sends bounded Jordan sets to bounded Jordan sets and scales their content by the absolute determinant Theorem
- A total derivative computes every directional derivative, and its matrix is the Jacobian Theorem
- The chain rule for total derivatives: D(g∘ f)(a)=Dg(f(a))∘ Df(a) Theorem
- The Euclidean implicit function theorem with derivative formula Theorem
- Total differentiability gives a local O(‖h‖₂) increment bound and therefore continuity Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 113 results over 24 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- J. Lebl, Basic Analysis I, §8.3 (standard reference, not scraped)