Passivity-admissible couplings have dimension n² = dim u(n)

Proved

PassivityUn.admissible_finrank

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

linear-algebramatrices

Let $n$ be a natural number, and consider real $2n\times 2n$ matrices in $2\times 2$ block form with $n\times n$ blocks. Let

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

The set of real $2n\times 2n$ matrices $W$ that are

symmetric, $W^{\mathsf T} = W$ , and
commute with $J_n$ , $WJ_n = J_nW$ ,

is a real vector space $\mathcal{A}_n$ of dimension exactly $n^2$ :

\dim_{\mathbb{R}} \mathcal{A}_n = n^2 .

This is the dimension of the unitary Lie algebra $\mathfrak{u}(n)$ . At $n = 1, 2, 3$ it gives $1, 4, 9$ , the dimensions of $\mathfrak{u}(1)$ , $\mathfrak{u}(2) = \mathfrak{u}(1)\oplus\mathfrak{su}(2)$ and $\mathfrak{u}(3) = \mathfrak{u}(1)\oplus\mathfrak{su}(3)$ . The statement is pure linear algebra; it does not assert the physical premise that passivity forces a coupling to be symmetric.

Preamble

import Mathlib
import Definitions.Def_PassivityUn_admissible

Formal statement

namespace PassivityUn
theorem admissible_finrank (n : ℕ) :
    Module.finrank ℝ (admissible n) = n ^ 2 := 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): 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 admissible_finrank. For every natural number $n$ (including $n = 0$ ), the real vector space $\mathcal{A}_n$ defined below has dimension exactly $n^2$ over $\mathbb{R}$ :

\dim_{\mathbb{R}} \mathcal{A}_n = n^2 .

Setting. Rows and columns are indexed by the disjoint union $B_n = \{1,\dots,n\} \sqcup \{1,\dots,n\}$ , a set with $2n$ elements (a "first copy" and a "second copy" of $\{1,\dots,n\}$ ). The ambient space is $M_n = \mathbb{R}^{B_n \times B_n}$ , the real $2n \times 2n$ matrices written in $2 \times 2$ block form, where each block is $n \times n$ . The ambient space has dimension $4n^2$ .

The matrix $J_n$ . This is the fixed block matrix

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

The upper-left block (first copy × first copy) is $0$ . The upper-right block (first copy × second copy) is $-I_n$ . The lower-left block (second copy × first copy) is $I_n$ . The lower-right block is $0$ .

The subspace $\mathcal{A}_n$ . It is the intersection of two linear subspaces of $M_n$ :

Symmetric matrices: $S_n = \{X \in M_n : X^{\mathsf T} = X\}$ , the kernel of the linear map $X \mapsto X^{\mathsf T} - X$ .
Matrices commuting with $J_n$ : $C_n = \{X \in M_n : X J_n = J_n X\}$ , the kernel of the linear map $X \mapsto X J_n - J_n X$ .

\mathcal{A}_n = S_n \cap C_n = \{X \in \mathbb{R}^{2n \times 2n} : X^{\mathsf T} = X \text{ and } X J_n = J_n X\}.

This is a real linear subspace. The theorem says its dimension, as a real vector space, is $n^2$ .

Edge case. When $n = 0$ , the index set is empty. The ambient space is then the zero space, and the claim reads $0 = 0$ . "Dimension" here is Mathlib's Module.finrank, which returns $0$ for infinite-dimensional spaces. That convention never applies here, because $\mathcal{A}_n$ sits inside the finite-dimensional space $M_n$ .

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