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.
Interpolative cur and nystrom decompositions — Examples
1 · Prerequisites
- Algebraic Closure, Embeddings, and Separability
- Algebraic Extensions, Extension Degree, and Finite Fields
- Binary Operations, Monoids, Groups and Subgroups
- Composition Series, the Jordan–Hölder Theorem and Solvable Groups
- Congruences, the Integers Modulo n and the Chinese Remainder Theorem
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Cyclic Groups and Direct Products
- Determinants of Matrices over a Commutative Ring
- Diagonalisation and the Minimal Polynomial
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Eigenvalues, Eigenvectors and the Characteristic Polynomial
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Interpolative cur and nystrom decompositions
- Limits of Real Functions
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Polynomial Rings, the Division Algorithm and Roots
- Primes, Euclid's Lemma and the Fundamental Theorem of Arithmetic
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Simple Field Extensions and the Construction of the Complex Numbers
- Splitting Fields
- Suprema and Infima
- Sylow's Theorems, p-Groups and Nilpotent Groups
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Fundamental Theorem of Algebra
- The Fundamental Theorem of Finite Abelian Groups
- The Galois Correspondence
- The Moore--Penrose Pseudoinverse and Regularised Least Squares
- The Spectral Theorem, Positive Operators and Singular Value Decomposition
- The ZFC Axioms and the Basic Set Constructions
- Topology of ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
The examples compute an exact rank-two skeleton CUR reconstruction, exhibit a prescribed one-column interpolant that misses the dominant singular direction, and verify a positive-semidefinite Nyström residual on a two-dimensional matrix.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
A prescribed column can miss the dominant direction
Statement refuted
For every real matrix with , every integer , and every prescribed ordered list of distinct valid column indices, there is a matrix with , , and , where is the Euclidean operator norm and is the th singular value.
Facts & Assumptions
Given: The claimed universal bound above.
Consider , , and the prescribed index set .
Given: The matrix, rank parameter, and prescribed selected column in [A1].
Counterexample
Any matrix satisfying has the form . The coefficient condition gives , and direct multiplication gives . Its spectral norm is the Euclidean norm of its first column, .
The singular values of the diagonal matrix in [A1] are and , so the proposed upper bound is . Since , no such satisfies the claim.
An exact rank-two CUR reconstruction from a nonsingular cross
Example
Take , and select . The resulting skeleton CUR factors reconstruct exactly.
Facts & Assumptions
Given: The displayed matrix and ordered row and column selections .
The matrix and index lists are exactly those stated in the Example.
Skeleton and projected least-squares CUR cores: , , , and the skeleton reconstruction is .
Skeleton CUR is exact for a full-rank cross: if , then .
The Moore--Penrose pseudoinverse as the solution of the four Penrose equations: a Moore-Penrose inverse satisfies the four Penrose equations.
Every finite real or complex matrix has a unique Moore--Penrose pseudoinverse: every finite matrix has a unique Moore-Penrose inverse.
Given: and from [A1].
Verification
Direct extraction gives , , and . Since satisfies the four Penrose equations [F3], uniqueness [F4] gives ; [F1] therefore gives the reconstruction .
Multiplication yields . The identity satisfies the Penrose equations [F3], hence equals by uniqueness [F4]. The third row of is the sum of the first two, and the first two are independent, so . Hence [F2] also applies and confirms the exact skeleton CUR identity.
A PSD Nyström residual remains positive semidefinite
Example
For and , the Nyström approximation is and its residual is the positive-semidefinite matrix .
Facts & Assumptions
Given: and the one-column sketch .
The matrix and sketch are those stated in the Example.
Nyström is positive semidefinite, dominated by A, and exact when it captures the range: for every PSD and conformal sketch.
The Moore--Penrose pseudoinverse as the solution of the four Penrose equations: the Moore-Penrose inverse is characterized by the four Penrose equations.
Every finite real or complex matrix has a unique Moore--Penrose pseudoinverse: every finite matrix has a unique Moore-Penrose inverse.
Given: from [A1].
Verification
We have and . The scalar satisfies all four equations [F3], so it is the Moore-Penrose inverse by uniqueness [F4]. Substitution in [F1] gives .
Subtracting from gives , which is positive semidefinite by its nonnegative diagonal entries. The general order statement [F2] also gives in this instance.