$J^2 = -1$

Proved

PassivityUn.stdJ_sq

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

linear-algebramatrices

Let $J_n = \begin{pmatrix} 0 & -I_n \\ I_n & 0 \end{pmatrix}$ be the standard complex structure on real $2n\times 2n$ block matrices. Then, for every natural number $n$ ,

J_n \, J_n = -I_{2n}.

This confirms that $J_n$ is a complex structure, which is what makes "commuting with $J_n$ " the condition of being complex-linear.

Preamble

import Mathlib
import Definitions.Def_PassivityUn_stdJ

Formal statement

namespace PassivityUn
theorem stdJ_sq (n : ℕ) : stdJ n * stdJ n = -1 := 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

Read-back of PassivityUn.stdJ_sq. Let $n$ be any natural number. The claim is universally quantified over $n$ , and $n = 0$ is included. There are no other hypotheses.

Index set. The rows and columns are indexed by the disjoint union $\mathrm{Fin}\,n \sqcup \mathrm{Fin}\,n$ : a "left" copy and a "right" copy of $\{0,\dots,n-1\}$ . This set has $2n$ elements. It is not $\{0,\dots,2n-1\}$ . Indices are tagged as belonging to the first or the second block.

The matrix $J_n$ . The definition stdJ gives a real square matrix $J_n$ over this index set. It is built from four $n\times n$ real blocks:

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

The upper-left block (left row, left column) is the zero matrix.
The upper-right block (left row, right column) is $-I_n$ .
The lower-left block (right row, left column) is the identity $I_n$ .
The lower-right block (right row, right column) is the zero matrix.

Written out entry by entry:

$(J_n)_{\mathrm{L}i,\,\mathrm{R}j} = -\delta_{ij}$
$(J_n)_{\mathrm{R}i,\,\mathrm{L}j} = \delta_{ij}$
every other entry is $0$ .

Assertion. The ordinary matrix product of $J_n$ with itself equals the negative of the identity matrix on the full $2n$ -element index set:

J_n \, J_n \;=\; -I_{2n} \qquad \text{for every } n \in \mathbb{N}.

In other words, $(J_n J_n)_{a,b} = -1$ if $a = b$ and $0$ otherwise, for all indices $a, b$ in $\mathrm{Fin}\,n \sqcup \mathrm{Fin}\,n$ .

Edge case $n = 0$ . The index set is empty, so both sides are the unique empty $0 \times 0$ matrix and the equation holds trivially.

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

J2=−1J^2 = -1J2=−1

$J^2 = -1$