Alphabeta Math
TheoremStatement: Literature-sourcedProof: Literature-sourcedPipeline-generated
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.

Computed reduced QR least squares is backward stable for full column rank

Statement

Let A∈Rm×n, m≥n≥1, have full column rank. Successful scaled Householder QR gives the exactly orthonormal reduced representative Q^ and computed triangular R^ with A+ΔQ=Q^R^,∥ΔQ∥F≤βQ∥A∥F,βQ=(1+κm)n−1, where κm is the proved local-step coefficient. Apply the stored reflectors to b by rounded rank-one updates and let y^ be the first n coordinates. Set βb=βQ. Alternatively, if an explicitly supplied exactly orthonormal Q^ has entries admissible as arithmetic inputs and y^=fl⁡(Q^Tb) uses sequential rounded dots, set βb=n γm. Solve R^x^=y^ by successful rounded back substitution. Suppose mu<1 and γn+3<1/8. There exist δb and upper triangular ΔR with (R^+ΔR)x^=Q^T(b+δb),∥δb∥2≤βb∥b∥2,∥ΔR∥F≤γn+3∥R^∥F. If R^+ΔR is nonsingular, x^ is the unique least-squares solution for A~=Q^(R^+ΔR) and b~=b+δb. The relative matrix perturbation is at most βQ+γn+3(1+βQ); the right-hand perturbation is at most βb. For fixed m,n, both perturbation coefficients are O(u). If additionally βQ≤19γn+3/(1+γn+3) and βb≤20γn+3, both relative data perturbation bounds are at most 20γn+3. These two coefficient comparisons are additional checks; they do not follow from mu<1 and γn+3<1/8 alone. Success and nonsingularity are explicit hypotheses.

Facts & Assumptions

Given: The stated successful QR, right-hand-side evaluation, and triangular solve; all nonzero exact intermediates are normal.

[F1]

The scaled Householder QR implementation is backward stable supplies the proved QR bound and the stored-reflector application bound.

[F2]

Rounded triangular substitution has a componentwise matrix backward error supplies the rounded triangular matrix perturbation, including the zero-solution branch.

[F5]

Cauchy–Schwarz: ∣⟨x,y⟩∣≤∥x∥ ∥y∥, with equality exactly for dependent pairs: for real Euclidean vectors, ∣⟨v,w⟩∣≤∥v∥2∥w∥2.

Proof

1.1givenF1F4F5algebraconstruct

For stored-reflector evaluation, [F1] bounds ∥y^−Q^Tb∥2 by βQ∥b∥2. In the explicit admissible-input alternative, dot expansion by [F4] gives coordinate errors at most γm∑i∣q^ijbi∣≤γm∥b∥2 by Cauchy-Schwarz and unit column norms; combining coordinates gives nγm∥b∥2. In either case put z=y^−Q^Tb and δb=Q^z. Exact orthonormality gives Q^Tδb=z and ∥δb∥2=∥z∥2.

2.1F2step 1.1algebra

Apply [F2] to the actual rounded back substitution. It supplies upper triangular ΔR with (R^+ΔR)x^=y^ and the displayed Frobenius estimate. This holds also when x^=0, since the same row identities force y^=0. Combined with step 1.1 this proves the perturbed normal-coordinate equation.

3.1F1F3step 1.1step 2.1algebra∎

Under the stated nonsingularity hypothesis, A~=Q^(R^+ΔR) has full column rank, and [F3] identifies x^ as its unique least-squares minimizer for b+δb. Finally ∥R^∥F=∥A+ΔQ∥F≤(1+βQ)∥A∥F, and A~−A=ΔQ+Q^ΔR gives the stated relative matrix bound. At fixed dimensions, [F1] gives βQ=O(u), and γm=O(u) gives βb=O(u) in either right-hand-side branch, so the displayed coefficients are O(u). Under the additional coefficient checks, write g=γn+3; then βQ+g(1+βQ)=(1+g)βQ+g≤19g+g=20g, while the assumed βb≤20g gives the right-hand bound. No comparison between βQ and g is inferred from arithmetic success alone.

Depends on

Used by

Dependency tree · two levels

27 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