Zero net power forces every link coupling to be symmetric (rings of ≥ 3 sites)Textbook
## Motivation
The **Shape Zero model** (Shape Zero LLC, unpublished) couples neighbouring nodes on a ring through a velocity-dependent force, with one coupling matrix per link. A companion mission, *The passivity-admissible couplings have dimension n² = dim u(n)*, shows that real matrices which are symmetric and commute with a complex structure $J$ form a space of dimension $n^2 = \dim \mathfrak{u}(n)$. That mission deliberately takes symmetry as given. This mission supplies the reason for it: a coupling that never does net work (a **passive** coupling) must have every link matrix symmetric, provided the ring has at least three sites.
Together the two missions give the chain
$$
\text{passive} \;\Longrightarrow\; \text{every } W_i \text{ symmetric} \qquad\text{(this mission)},
$$
$$
\text{symmetric} + \text{commutes with } J \;\Longrightarrow\; \dim = n^2 \qquad\text{(companion mission)}.
$$
**What these two missions do NOT prove.** Commuting with $J$ is not derived here. It is the requirement that the coupling respect each node's complex structure, and in the model it is imposed, not forced by passivity. After both missions the proved content is: passivity forces symmetry, and symmetric $J$-compatible couplings have the dimension of $\mathfrak{u}(n)$. The $J$-compatibility step remains a modelling premise. In addition, the coupling space consists of the **Hermitian** matrices, which match $\mathfrak{u}(n)$ in dimension; the Lie algebra $\mathfrak{u}(n)$ itself appears only after multiplying by $i$ ([Unitary group](https://en.wikipedia.org/wiki/Unitary_group)).
## Setting
Let $N$ and $d$ be natural numbers with $N \ge 1$. A **ring** has $N$ sites labelled by $\mathbb{Z}/N\mathbb{Z} = \{0, \dots, N-1\}$, so site $N-1$ is next to site $0$; indices $i + 1$ and $i - 1$ are taken modulo $N$. Each site carries a velocity vector $v_i \in \mathbb{R}^d$, and each link $i \to i+1$ carries a real $d \times d$ **link matrix** $W_i$. The force on site $i$ is
$$
F_i = W_i\, v_{i+1} - W_{i-1}\, v_{i-1},
$$
where the second term uses the **previous** link's matrix $W_{i-1}$. The **total power** delivered by the coupling is
$$
P_W(v) = \sum_{i \in \mathbb{Z}/N\mathbb{Z}} v_i \cdot \bigl( W_i\, v_{i+1} - W_{i-1}\, v_{i-1} \bigr).
$$
In the Lean development this is `PassivityRing.power N d W v`, with sites indexed by `Fin N` (whose addition and subtraction wrap around modulo $N$), vectors in `Fin d → ℝ`, and $\cdot$ the dot product `⬝ᵥ`. The coupling is **passive** when $P_W(v) = 0$ for every choice of velocities $v$.
## Formalization targets
### Goal: passive if and only if every link is symmetric (rings of at least 3 sites)
$$
N \ge 3 \;\Longrightarrow\; \Bigl( \forall v,\; P_W(v) = 0 \Bigr) \iff \Bigl( \forall i,\; W_i^{\mathsf T} = W_i \Bigr).
$$
This is `PassivityRing.passive_iff_symm`. It holds for every $d$ and every family of link matrices, with no assumption relating different links.
### Milestones
1. **M1 (power identity, every $N$).** $P_W(v) = \sum_i v_i \cdot \bigl((W_i - W_i^{\mathsf T})\, v_{i+1}\bigr)$.
2. **M2 (symmetric links are passive, every $N$).** If every $W_i$ is symmetric, then $P_W(v) = 0$ for all $v$.
3. **M3 (passive forces symmetric, $N \ge 3$).** If $P_W(v) = 0$ for all $v$, then every $W_i$ is symmetric.
## Significance
*The result itself.* The goal turns a physical requirement — no net work for any motion — into an exact algebraic condition on each link separately. It is the step that justifies restricting the companion mission's coupling class to symmetric matrices, so that the dimension count $n^2$ applies to the passive couplings of the model rather than to an assumed class.
*Formalizing it.* The model's claim has so far been checked numerically at ring sizes $1, 2, 3, 4, 7$. A machine-checked proof covers every $N \ge 3$ and every $d$, makes the role of the hypothesis $N \ge 3$ explicit, and separates what is proved (passivity forces symmetry) from what remains a modelling premise ($J$-compatibility).
## Difficulty
The forward direction and the power identity are finite-sum bookkeeping. The central difficulty is the converse: the hypothesis constrains a single scalar quantity summed around the ring, and it must be shown to constrain each link matrix individually. On small rings this fails because distinct terms of the sum coincide, so the argument depends on the ring being large enough that neighbouring sites are genuinely distinct, and in Lean that is modular arithmetic on `Fin N`.
The hypothesis $N \ge 3$ is necessary, not a convenience:
- **$N = 1$:** the site is its own neighbour on both sides, so the force is $W_0 v_0 - W_0 v_0 = 0$ and the power vanishes for every $W_0$, symmetric or not.
- **$N = 2$:** the power reduces to $v_0 \cdot (D - D^{\mathsf T})\, v_1$ with $D = W_0 - W_1$, so it depends only on the difference of the two link matrices. Taking both links equal to the same non-symmetric matrix, for example $\begin{pmatrix} 0 & 1 \\ 0 & 0 \end{pmatrix}$, gives zero power for all velocities.
Weakening the hypothesis to $2 \le N$, or dropping it, makes the goal false.
## Formalization scope
- Sites are `Fin N` with its wrap-around arithmetic, so $i + 1$ and $i - 1$ go around the ring; `[NeZero N]` is required for the literal $1$ in `Fin N` and is implied by $N \ge 3$ in the goal.
- There is one matrix per link, `W : Fin N → Matrix (Fin d) (Fin d) ℝ`, not a single shared matrix, and no relation between different links is assumed.
- Passivity is quantified over **all** velocity configurations `v : Fin N → (Fin d → ℝ)`.
- Everything is real (`ℝ`); symmetry is `(W i)ᵀ = W i`.
- $d = 0$ is included; there both sides of the goal hold trivially. This is not a trivialization, since the statement is quantified over all $d$.
M1 and M2 hold for every $N \ge 1$ and carry no ring-size hypothesis; M3 and the goal require $N \ge 3$. The development needs only Mathlib's finite sums, dot products, matrix–vector products and `Fin` arithmetic.
## 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, *Symmetric matrix*. https://en.wikipedia.org/wiki/Symmetric_matrix
- Mathlib, `Mathlib.Data.Matrix.Mul` (dot product `⬝ᵥ`, matrix–vector product `*ᵥ`). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Mul.html
5 thms1 active userReviewed
🏆Completed
Captain: ShapeZero
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