Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-01
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.

Invertible preconditioners give equivalent linear systems, with the transformed residuals and errors written explicitly

Statement

Let Ax=b be a linear system. In the error formulas in parts 2 and 3, assume x∗ is a solution of Ax=b and put e:=x−x∗. The corresponding transformed exact solutions are denoted by y∗.

  1. If P∈GL⁡n(F) and P−1Ax=P−1b, then the left-preconditioned system has exactly the same solution set as Ax=b. Its residual is r~=P−1r, where r=b−Ax.
  2. If P∈GL⁡n(F) and y:=Px, then AP−1y=b is equivalent to Ax=b. Its residual is the same physical residual r^=b−AP−1y=r, and its error is e^=y−y∗=Pe, where y∗:=Px∗.
  3. If M=CC∗ is Hermitian positive definite and y:=C∗x, then C−1AC−∗y=C−1b is equivalent to Ax=b. Its residual is rsym=C−1r, and its error is esym=y−y∗=C∗e, where y∗:=C∗x∗.

Facts & Assumptions

Given: A linear system Ax=b, the left, right, and symmetric preconditioned forms from the definition, and, when an error formula is used, a solution x∗ of Ax=b.

[F1]

Left, right, and symmetric preconditioning are exactly the transformed systems P−1Ax=P−1b,AP−1y=b,C−1AC−∗y=C−1b with the accompanying variable changes (Left preconditioning, right preconditioning, and symmetric preconditioning of a linear system).

[L1]

An invertible matrix has a two-sided inverse (Invertible matrices and the general linear group GL⁡n(F)).

Proof

technique · direct
1.1

For left preconditioning, [L1] implies Ax=b  ⟺  P−1Ax=P−1b. For any trial vector x, the transformed residual is P−1b−P−1Ax=P−1(b−Ax)=P−1r.

F1L1algebra
1.2

For right preconditioning, put y=Px, so x=P−1y by [L1]. Then Ax=b  ⟺  AP−1y=b. The right-preconditioned residual is b−AP−1y=b−Ax=r, and if y∗=Px∗ then y−y∗=P(x−x∗)=Pe.

F1L1algebra
2.1

For symmetric preconditioning, [F1] writes x=C−∗y, equivalently y=C∗x. Therefore Ax=b  ⟺  C−1AC−∗y=C−1b. If y∗=C∗x∗, then C−1b−C−1AC−∗y=C−1(b−Ax)=C−1r, and y−y∗=C∗(x−x∗)=C∗e. Thus each transformed system is equivalent to the original one, with the displayed residual and error maps.

F1L1algebra∎

Depends on

Used by

Dependency tree · two levels

6 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