Commuting with $J$ forces the block form $\begin{pmatrix} A & -B \\ B & A \end{pmatrix}$

Proved

PassivityUn.commJ_iff_blocks

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

linear-algebramatrices

Let $n$ be a natural number, let $A, B, C, D$ be real $n\times n$ matrices, and let $J_n = \begin{pmatrix} 0 & -I_n \\ I_n & 0 \end{pmatrix}$ . Then

\begin{pmatrix} A & B \\ C & D \end{pmatrix} J_n = J_n \begin{pmatrix} A & B \\ C & D \end{pmatrix} \quad\Longleftrightarrow\quad D = A \ \text{ and } \ B = -C.

So a real $2n\times 2n$ matrix commutes with $J_n$ exactly when its top-left and bottom-right blocks agree and its top-right block is the negative of its bottom-left block, i.e. it is the real form of a complex $n\times n$ matrix.

Preamble

import Mathlib
import Definitions.Def_PassivityUn_stdJ

Formal statement

namespace PassivityUn
theorem commJ_iff_blocks (n : ℕ) (A B C D : Matrix (Fin n) (Fin n) ℝ) :
    Matrix.fromBlocks A B C D * stdJ n = stdJ n * Matrix.fromBlocks A B C D
      ↔ D = A ∧ B = -C := 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

Theorem commJ_iff_blocks. Fix a natural number $n$ (any $n \ge 0$ ) and four real $n \times n$ matrices $A, B, C, D$ , whose rows and columns are indexed by $\{0, \dots, n-1\}$ . No other hypotheses are assumed.

Auxiliary definitions, expanded. Let $\mathrm{Blk}_n$ be the disjoint union of two copies of $\{0,\dots,n-1\}$ : a "first" copy and a "second" copy, so it has $2n$ elements. Matrices indexed by $\mathrm{Blk}_n \times \mathrm{Blk}_n$ are real $2n \times 2n$ matrices written in $2 \times 2$ block form. The first copy indexes the top/left blocks and the second copy indexes the bottom/right blocks. The matrix $J_n$ (stdJ n) is defined as the real block matrix

J_n \;=\; \begin{pmatrix} 0 & -I_n \\ I_n & 0 \end{pmatrix},

where $0$ is the $n\times n$ zero matrix and $I_n$ is the $n \times n$ identity matrix. The top-left block is $0$ , the top-right block is $-I_n$ , the bottom-left block is $I_n$ and the bottom-right block is $0$ . Write $M$ for the $2n \times 2n$ real block matrix built from the four given matrices, indexed the same way:

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

Here $A$ is the top-left block, $B$ the top-right, $C$ the bottom-left and $D$ the bottom-right.

Assertion. For every $n$ and every choice of $A, B, C, D$ , the following biconditional holds:

M\,J_n \;=\; J_n\,M \quad\Longleftrightarrow\quad \big(D = A \ \text{ and } \ B = -C\big).

The products are ordinary real matrix products, and the equality on the left is entrywise equality of $2n \times 2n$ matrices. The equalities on the right are entrywise equalities of $n \times n$ matrices. So $M$ commutes with $J_n$ exactly when its bottom-right block equals its top-left block and its top-right block is the negative of its bottom-left block. Both directions of the equivalence are asserted.

Degenerate case. When $n = 0$ , all of $A, B, C, D$ , $M$ and $J_n$ are empty matrices. Both sides of the biconditional then hold automatically.

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

Commuting with JJJ forces the block form (A−BBA)\begin{pmatrix} A & -B \\ B & A \end{pmatrix}(AB​−BA​)

Commuting with $J$ forces the block form $\begin{pmatrix} A & -B \\ B & A \end{pmatrix}$