Alphabeta MathHow 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 least squares problem where rounded normal equations lose the pivot
Example
In binary64 RNE take A=((1,1),(0,2^-27)). Its determinant 2^-27 is nonzero. The exact Gram matrix is A^T A=((1,1),(1,1+2^-54)). The spacing above 1 is 2^-52, so the midpoint is 1+2^-53; 1+2^-54 lies strictly below it and rounds to 1. Thus the formed Gram matrix has equal rows and is singular. Reduced QR works directly on A and avoids forming this rounded Gram matrix; the computed stability statement remains conditional on its own hypotheses.
Facts & Assumptions
Given: binary64 RNE and A=((1,1),(0,2^-27)).
Reduced QR over the reals solves full-column-rank least squares without squaring the condition number: exact reduced QR solves full-rank least squares without forming the Gram matrix.
Computed reduced QR least squares is backward stable for full column rank: the computed guarantee is conditional on the listed QR and solve premises.
Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add: binary64 operations use round-to-nearest, ties-to-even.
Verification
The determinant is 2^-27, while direct multiplication gives (A^T A)_22=1+2^-54.
Since 2^-54<2^-53, the exact entry is strictly below the RNE midpoint above 1 and rounds to 1. The rounded Gram matrix has equal rows and is singular.
The exact result [F1] acts on the full-rank A without a Gram formation. The computed conclusion [F2] applies only if its separate successful-step hypotheses hold.
Depends on
Used by
Nothing in the library uses this result yet.
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
- Fundamentals of Numerical Computation, normal equations (standard reference, not scraped)
- Fundamentals of Numerical Computation, QR factorization and least squares (standard reference, not scraped)
- Stuart and Voss, Matrix Analysis and Algorithms, Warwick lecture notes (standard reference, not scraped)