Symmetric block form $\iff$ $A$ symmetric, $B$ antisymmetric

Proved

PassivityUn.symm_blocks_iff

by ShapeZero · Sep 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-algebramatrices

Let $n$ be a natural number and let $A, B$ be real $n\times n$ matrices. Then

\begin{pmatrix} A & -B \\ B & A \end{pmatrix}^{\mathsf T} = \begin{pmatrix} A & -B \\ B & A \end{pmatrix} \quad\Longleftrightarrow\quad A^{\mathsf T} = A \ \text{ and } \ B^{\mathsf T} = -B.

In complex terms, the real form of $A + iB$ is symmetric exactly when $A + iB$ is Hermitian.

Preamble

import Mathlib

open Matrix

Formal statement

namespace PassivityUn
theorem symm_blocks_iff (n : ℕ) (A B : Matrix (Fin n) (Fin n) ℝ) :
    (Matrix.fromBlocks A (-B) B A)ᵀ = Matrix.fromBlocks A (-B) B A
      ↔ Aᵀ = A ∧ Bᵀ = -B := by sorry
end PassivityUn

Source

Shape Zero LLC, "Formal Proofs of the C1 Verification Package" (August 2026), §6, Theorem 6.1: https://github.com/ShapeZeroSZ/shape-zero/blob/main/01_source/proofs/ShapeZero_C1_Formal_Proofs.pdf ; corrected in "Errata — C1 Formal Proofs (Sections 3 and 6)", Corrected Theorem 6.1(b) (block form): https://github.com/ShapeZeroSZ/shape-zero/blob/main/01_source/proofs/ERRATUM_Theorem_6.1.md

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Read-back of PassivityUn.symm_blocks_iff.

Let $n$ be any natural number, including $n = 0$ . Let $A$ and $B$ be any two real $n \times n$ matrices, with rows and columns indexed by $\{0, 1, \dots, n-1\}$ . The statement places no other conditions on $A$ or $B$ . From them it builds the real $2n \times 2n$ block matrix

M \;=\; \begin{pmatrix} A & -B \\ B & A \end{pmatrix}.

Its rows and columns are indexed by the disjoint union of two copies of $\{0, \dots, n-1\}$ : the first copy gives the top/left blocks and the second gives the bottom/right blocks. In $M$ , the top-left block is $A$ , the top-right block is $-B$ , the bottom-left block is $B$ and the bottom-right block is $A$ .

The theorem claims a two-way equivalence ("if and only if"):

M^{\mathsf T} = M \quad\Longleftrightarrow\quad \bigl(A^{\mathsf T} = A \ \text{ and } \ B^{\mathsf T} = -B\bigr).

Here $^{\mathsf T}$ is the ordinary matrix transpose. The left side says the block matrix $M$ is symmetric. The right side says both of the following hold together:

$A$ is symmetric.
$B$ is skew-symmetric.

Both directions of the equivalence are asserted. The claim is made for every $n$ and every pair $A, B$ .

Edge case $n = 0$ : $A$ , $B$ and $M$ are all empty matrices. Every equality between them holds trivially, so both sides of the equivalence are true.

Human review

Endorsed by Shuze Chen · Sep 24, 2026
Confirmed by the moderator at approval.
Endorsed by ShapeZero · Sep 24, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Symmetric block form ⟺ \iff⟺AAA symmetric, BBB antisymmetric

Symmetric block form $\iff$ $A$ symmetric, $B$ antisymmetric