Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)
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 Schur solve for a full-row-rank symmetric saddle system

Statement

Under the hypotheses of Symmetric saddle-point system, Schur complement, and block preconditioners, S=BA−1BT is positive definite and hence invertible. For every f∈Rn and g∈Rm, the unique solution of (ABTB0)(up)=(fg) is p=S−1(BA−1f−g),u=A−1(f−BTp). The factorization used in this solve is the published block-LU factorization An invertible leading block yields block LU through its Schur complement.

Facts & Assumptions

Given: A symmetric positive definite, B full row rank, and the finite-dimensional symmetric saddle equations with right-hand side (f,g).

[F1]

The saddle matrix, pressure Schur matrix S=BA−1BT, and the two equations are defined in Symmetric saddle-point system, Schur complement, and block preconditioners.

[F2]

If a square block matrix has an invertible leading block, it factorizes through the Schur complement as (A11A12A21A22)=(I0A21A11−1I)(A11A120A22−A21A11−1A12) (An invertible leading block yields block LU through its Schur complement).

[F3]

For a linear map between finite-dimensional spaces, dim⁡V=dim⁡ker⁡T+dim⁡im⁡T (Rank-nullity: dim⁡FV=nullity⁡T+rank⁡T).

Proof

1.1givenF1F3algebra

Positive definiteness of A makes its kernel zero: if Ax=0, then xTAx=0, so the positivity hypothesis forces x=0. Since A is a square matrix on a finite-dimensional space, [F3] makes its image full-dimensional; thus A is invertible. For nonzero q∈Rm, full row rank gives BTq≠0. Put y=A−1BTq, which is nonzero. Then qTSq=(BTq)TA−1(BTq)=(Ay)Ty=yTAy>0. Therefore S is symmetric positive definite.

2.1F1F2step 1.1algebra

Apply [F2] to K with leading block A, upper-right block BT, lower-left block B, and lower-right block 0. Its trailing Schur complement is 0−BA−1BT=−S. Hence K=(I0BA−1I)(ABT0−S), and both diagonal blocks of the upper factor are invertible by the hypotheses and step 1.1.

3.1F1step 2.1algebra∎

Solve the lower-triangular factor against (f,g) first. It gives the intermediate vector (f,g−BA−1f). The second block row of the upper solve is −Sp=g−BA−1f, so p=S−1(BA−1f−g). The first row gives u=A−1(f−BTp). Substitution verifies Au+BTp=f and Bu=BA−1f−Sp=g. Invertibility of the diagonal blocks in step 2.1 makes both triangular solves unique, so this is the unique solution.

Depends on

Used by

Nothing in the library uses this result yet.

Cited to discharge well-definedness by Symmetric saddle-point system, Schur complement, and block preconditioners.

Dependency tree · two levels

17 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