Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-08-29
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.

Exact rank is locally constant at full-rank matrices and discontinuous at nonmaximal-rank matrices

Statement

Let m,n∈N with m≥1 and n≥1, let A∈Mm×n(R), let k:=min⁡(m,n), and let ∥⋅∥2 be the spectral norm.

  1. Locally constant at full rank. If rank⁡A=k and σk is the smallest singular value of A (which is positive), then every B∈Mm×n(R) with ∥B−A∥2<σk satisfies rank⁡B=k.
  2. Discontinuous at nonmaximal rank. If rank⁡A=r<k, then for every ε>0 there is B∈Mm×n(R) with ∥B−A∥2<ε and rank⁡B=r+1.

Facts & Assumptions

Given: Natural numbers m,n≥1, a matrix A∈Mm×n(R) with rank r and singular values σ1≥⋯≥σr>0, and k=min⁡(m,n).

[L1]

There is a singular value decomposition A=UΣVT with orthogonal U,V and diagonal Σ; likewise every matrix B∈Mm×n(R) admits one (Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition).

[L2]

The rank of a matrix is the number of its positive singular values (The rank of a linear map is the number of its nonzero singular values).

[L3]

The spectral norm of a matrix equals its largest singular value, and ∥My∥2≤∥M∥2∥y∥2 for every vector y (Spectral and Frobenius norms are unitarily invariant, are given by singular values, and satisfy the sharp rank comparison).

Proof

technique · direct
1.1L2

If rank⁡A=k, then by [L2] there are exactly k positive singular values, so the smallest one, σk, is positive.

1.2L1algebra

Full-column-rank lower bound. Suppose n≤m and B∈Mm×n(R) has singular values τ1≥⋯≥τn. Writing a unit vector x in the right-singular basis of the decomposition from [L1] gives ∥Bx∥22=∑j<nτj2∣(VTx)j∣2≥τn2, attained at the last right-singular vector. Hence τn=min⁡∥x∥2=1∥Bx∥2.

1.3L1givenalgebra

Suppose rank⁡A=r<k; then both r<m and r<n, so the decomposition of [L1] has a left singular vector ur+1∈Rm and a right singular vector vr+1∈Rn beyond the positive singular values.

1.4L1L2algebraconstruct

For ε>0 put Bε:=A+ε ur+1vr+1T. Then Bε=U(Σ+ε er+1er+1T)VT is a singular value decomposition of Bε with positive singular values σ1,…,σr,ε, so by [L2] rank⁡Bε=r+1.

2.1step 1.2L2L3algebra

Assume first that rank⁡A=k and n≤m. Applying step 1.2 to A gives ∥Ax∥2≥σk for every unit vector x, and [L3] gives ∥Ex∥2≤∥E∥2 for E:=B−A; so ∥Bx∥2=∥Ax+Ex∥2≥∥Ax∥2−∥Ex∥2≥σk−∥E∥2. If ∥E∥2<σk, then ∥Bx∥2>0 for every unit vector x, so step 1.2 applied to B gives its smallest singular value τn>0. Therefore [L2] gives rank⁡B=n=k.

2.2step 1.4L3algebra

Fix ε>0 and set η:=ε/2. Step 1.4 gives rank⁡Bη=r+1. By [L3], the spectral norm of η ur+1vr+1T is η times the largest singular value of the rank-one matrix ur+1vr+1T, whose only positive singular value is 1; hence ∥Bη−A∥2=η<ε. This proves the discontinuity claim.

3.1L1L3step 2.1algebra

Assume next that rank⁡A=k and m<n. Then AT has full column rank m and the same positive singular values as A by [L1], so its smallest singular value is again σk. The same transpose relation holds for BT, and [L3] gives ∥BT−AT∥2=∥B−A∥2. Applying step 2.1 to AT and BT yields rank⁡BT=m, hence rank⁡B=m=k.

4.1step 2.1step 3.1

Steps 2.1 and 3.1 prove the local-constancy claim.

5.1step 4.1step 2.2∎

Claim 1 is step 4.1 and claim 2 is step 2.2.

Depends on

Used by

Dependency tree · two levels

16 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