The passivity-admissible couplings have dimension n² = dim u(n)Textbook
## Motivation The **Shape Zero model** (Shape Zero LLC, unpublished) aims to obtain all three factors of the Standard Model gauge structure — $U(1)$, $SU(2)$ and $SU(3)$ — from a single linear-algebra statement applied at three node sizes. A node carrying $n$ oscillator pairs has a $2n$-dimensional real state space with a **complex structure** $J$. Within the model, the couplings that do no net work (**passive** couplings) are the symmetric matrices, and those that respect $J$ are the ones commuting with it. The claim is that the couplings satisfying both conditions form a real vector space of dimension exactly $n^2$, which is the dimension of the unitary Lie algebra $\mathfrak{u}(n)$ ([Unitary group](https://en.wikipedia.org/wiki/Unitary_group)): | node size $n$ | admissible dimension | Lie algebra | |---|---|---| | 1 | 1 | $\mathfrak{u}(1)$ | | 2 | 4 | $\mathfrak{u}(2) = \mathfrak{u}(1) \oplus \mathfrak{su}(2)$ | | 3 | 9 | $\mathfrak{u}(3) = \mathfrak{u}(1) \oplus \mathfrak{su}(3)$ | The dimension count has so far been checked numerically for $n = 1, \dots, 5$ only, giving $1, 4, 9, 16, 25$. A machine-checked proof covers every $n$, and it is the claim a physicist examining the model would check first. **What this mission does NOT prove.** This mission proves the **linear algebra**: symmetric matrices commuting with $J$ form a space of dimension $n^2$. It does **not** prove the physics step that passivity forces a coupling to be symmetric. That step is a separate premise of the model, and a completed mission must not be read as establishing it. ## Setting Fix a natural number $n$. Consider real $2n \times 2n$ matrices, with rows and columns indexed by two copies of $\{0, \dots, n-1\}$, so that each matrix is written in $2 \times 2$ block form with $n \times n$ blocks: $$ W = \begin{pmatrix} A & B \\ C & D \end{pmatrix}. $$ Let $I$ be the $n \times n$ identity matrix and define the **standard complex structure** $$ J = \begin{pmatrix} 0 & -I \\ I & 0 \end{pmatrix}, $$ which satisfies $J^2 = -1$. In the Lean development this matrix is `PassivityUn.stdJ n`, and the index type is `PassivityUn.Blk n`, the disjoint union of two copies of `Fin n`. Two real linear subspaces of the $4n^2$-dimensional space of such matrices are defined: 1. `symm n`: the **symmetric** matrices, $W^{\mathsf T} = W$; 2. `commJ n`: the matrices **commuting with $J$**, $WJ = JW$. The **admissible coupling class** `admissible n` is their intersection: $$ \mathcal{A}_n = \{\, W \in \mathbb{R}^{2n \times 2n} : W^{\mathsf T} = W \ \text{and}\ WJ = JW \,\}. $$ ## Formalization targets ### Goal: the admissible class has dimension $n^2$ $$ \dim_{\mathbb{R}} \mathcal{A}_n = n^2 \qquad \text{for every } n \in \mathbb{N}. $$ This is `PassivityUn.admissible_finrank`. It asserts the exact dimension for all $n$ at once, not for a particular node size. ### Milestones 1. **M1.** $J \cdot J = -1$, so $J$ is a complex structure. 2. **M2.** A block matrix $\begin{pmatrix} A & B \\ C & D \end{pmatrix}$ commutes with $J$ exactly when $D = A$ and $B = -C$. 3. **M3.** A block matrix $\begin{pmatrix} A & -B \\ B & A \end{pmatrix}$ is symmetric exactly when $A^{\mathsf T} = A$ and $B^{\mathsf T} = -B$. 4. **M4.** The dimension counts of symmetric and antisymmetric $n \times n$ matrices add to $n^2$: $\tfrac{n(n+1)}{2} + \tfrac{n(n-1)}{2} = n^2$. ## Significance *The result itself.* The goal identifies the admissible coupling class with the real form of the $n \times n$ Hermitian matrices, the space whose dimension is that of $\mathfrak{u}(n)$ ([Hermitian matrix](https://en.wikipedia.org/wiki/Hermitian_matrix)). Applied at $n = 1, 2, 3$ it gives the dimensions $1$, $4$ and $9$, which the Shape Zero model matches with $\mathfrak{u}(1)$, $\mathfrak{u}(2) = \mathfrak{u}(1) \oplus \mathfrak{su}(2)$ and $\mathfrak{u}(3) = \mathfrak{u}(1) \oplus \mathfrak{su}(3)$. Without a proof for general $n$, the model rests on a finite numerical check. *Formalizing it.* The underlying fact is standard linear algebra, a special case of the correspondence between real matrices commuting with a complex structure and complex-linear maps ([Linear complex structure](https://en.wikipedia.org/wiki/Linear_complex_structure)). No machine-checked statement of this exact dimension count was found in the platform library. The mission produces a verified, general-$n$ statement whose hypotheses are fully explicit, and it separates the verified linear algebra from the unverified physical premise. ## Difficulty Every step is standard linear algebra, so the difficulty is in the formal bookkeeping rather than the mathematics. The dimension of a subspace defined by equations is not computed by any Mathlib tactic. It has to be obtained by exhibiting an explicit linear equivalence with spaces of known dimension, and that requires moving between the $2n \times 2n$ matrix indexed by a disjoint union and its four $n \times n$ blocks. Checking small cases numerically, as has already been done, does not extend to a statement about every $n$. ## Formalization scope - Matrices are real (`ℝ`), not complex. The complex structure enters only through the fixed real matrix $J$. - Matrices are indexed by `Fin n ⊕ Fin n` (`PassivityUn.Blk n`) rather than `Fin (2n)`, so that block decomposition via Mathlib's `Matrix.fromBlocks` is direct. The first copy of `Fin n` indexes the upper/left blocks. - Each condition is defined as the kernel of a linear map: symmetry as the kernel of $W \mapsto W^{\mathsf T} - W$, and commuting with $J$ as the kernel of $W \mapsto WJ - JW$. Both are therefore subspaces by construction, with no hand-written closure proofs. - Dimension is `Module.finrank ℝ`. The ambient space is finite-dimensional, so the convention that `finrank` of an infinite-dimensional space is $0$ never applies. - The case $n = 0$ is included, and there the statement reads $0 = 0$. This is not a trivialization: the claim is quantified over all $n$, and every $n \ge 1$ is a nontrivial instance. - M4 is stated with natural-number division and truncated subtraction. Both are exact here, because $n(n \pm 1)$ is always even and $n \cdot (n - 1) = 0$ when $n = 0$. The development needs only Mathlib's block matrices, transpose, linear maps and `finrank`. The block-characterization lemmas (M2, M3) are reusable for any statement relating real matrices commuting with $J$ to complex matrices. Contributions are welcome on the milestones and on the assembling isomorphism. ## Selected references - B. C. Hall, *Lie Groups, Lie Algebras, and Representations: An Elementary Introduction*, 2nd ed., Graduate Texts in Mathematics 222, Springer, 2015. https://doi.org/10.1007/978-3-319-13467-3 - Wikipedia, *Unitary group*. https://en.wikipedia.org/wiki/Unitary_group - Wikipedia, *Linear complex structure*. https://en.wikipedia.org/wiki/Linear_complex_structure - Wikipedia, *Hermitian matrix*. https://en.wikipedia.org/wiki/Hermitian_matrix - Mathlib, `Mathlib.Data.Matrix.Block` (block matrices, `Matrix.fromBlocks`). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Block.html