Linear algebra

Motivation

Singular value thresholding (SVT) is a first-order method introduced by Cai, Candès and Shen (SIAM J. Optim. 20 (2010)) for recovering a low-rank matrix from incomplete or indirect information. Its basic form, for matrix completion, alternates a soft-thresholding of singular values with a gradient step on a dual variable, and needs only one sparse singular value decomposition per iteration. That is what made nuclear-norm heuristics usable on matrices with tens of thousands of rows and columns, where interior-point methods for the equivalent semidefinite program do not fit in memory.

Matrix completion is only one constraint set. In applications the data are noisy linear measurements $b = \mathcal A(M) + z$, and the constraint takes the form of componentwise error bounds or norm balls around the data (§3.3 of the paper). Section 3.2 of the paper extends the method to a general finite family of convex constraints, and §4.2 proves that the extended iteration converges. This mission formalizes that extension and its convergence theorem, Theorem 4.4.

Setting

Let $n_1, n_2, m$ be natural numbers and $\mathbb R^{n_1\times n_2}$ the real $n_1\times n_2$ matrices, with the Frobenius inner product $\langle X, Y\rangle = \sum_{i,j} X_{ij}Y_{ij}$ and norm $\|X\|_F = \sqrt{\langle X, X\rangle}$. The nuclear norm $\|X\|_*$ is the sum of the singular values of $X$. For a fixed $\tau > 0$ the objective is

$$f_\tau(X) = \tau\|X\|_* + \tfrac12\|X\|_F^2 .$$

A matrix $Z$ is a subgradient of a function $g$ at $X_0$, written $Z\in\partial g(X_0)$, if $g(X)\ge g(X_0) + \langle Z, X - X_0\rangle$ for all $X$.

Let $f_1,\dots,f_m:\mathbb R^{n_1\times n_2}\to\mathbb R$ be convex and put $\mathcal F(X) = (f_1(X),\dots,f_m(X))\in\mathbb R^m$. On $\mathbb R^m$, $\langle u, v\rangle = \sum_i u_iv_i$ and $\|v\|$ is the Euclidean norm. The constrained problem is

$$\text{(3.4)}\qquad \text{minimize } f_\tau(X)\quad\text{subject to } f_i(X)\le 0,\ i=1,\dots,m,$$

with Lagrangian $\mathcal L(X, y) = f_\tau(X) + \langle y, \mathcal F(X)\rangle$ for $y\ge 0$. A pair $(X^\star, y^\star)$ with $y^\star\ge0$ is primal-dual optimal if it is a saddle point:

$$\mathcal L(X^\star, y)\le \mathcal L(X^\star, y^\star)\le \mathcal L(X, y^\star)\qquad\text{for all } y\ge 0,\ X .$$

The paper's standing assumption "strong duality holds" is the existence of such a pair.

The iteration (3.5) starts from $y^0 = 0$ and, for step sizes $\delta_k$, sets for $k = 1, 2, \dots$

$$X^k = \arg\min_X\{f_\tau(X) + \langle y^{k-1}, \mathcal F(X)\rangle\},\qquad y^k = [\,y^{k-1} + \delta_k\mathcal F(X^k)\,]_+ ,$$

where $x_+$ has entries $\max(x_i, 0)$. It is Uzawa's method for (3.4): an exact minimization in the primal variable followed by a projected ascent step on the dual. When $\mathcal F(X) = b - \mathcal A(X)$ is affine, the minimization is a singular value thresholding step, which gives the algorithm its name.

The analysis of §4.2 assumes $\mathcal F$ is Lipschitz in the sense

$$\text{(4.2)}\qquad \|\mathcal F(X) - \mathcal F(Y)\|\le L\,\|X - Y\|_F\quad\text{for all } X, Y,$$

for a constant $L\ge 0$.

Formalization targets

Goal: Theorem 4.4 (p. 1969)

If $0 < \inf_k\delta_k\le\sup_k\delta_k < 2/L^2$ and strong duality holds, then the sequence $X^k$ of (3.5) converges to the unique solution of (3.4):

$$\exists!\,X^\star\ \text{solving (3.4)},\qquad \lim_{k\to\infty} X^k = X^\star .$$

Milestones, in the order the proof uses them

• Lemma 4.1 (p. 1968): $\langle Z - Z', X - X'\rangle\ge\|X - X'\|_F^2$ for $Z\in\partial f_\tau(X)$, $Z'\in\partial f_\tau(X')$.
• Lemma 4.3 (p. 1969): for a primal-dual optimal pair and each $\delta > 0$, $y^\star = [y^\star + \delta\mathcal F(X^\star)]_+$.
• Eq. (4.4) (p. 1969): there are $Z^k\in\partial f_\tau(X^k)$ and $Z^\star\in\partial f_\tau(X^\star)$ with $\langle Z^k, X - X^k\rangle + \langle y^{k-1}, \mathcal F(X) - \mathcal F(X^k)\rangle\ge 0$ and $\langle Z^\star, X - X^\star\rangle + \langle y^\star, \mathcal F(X) - \mathcal F(X^\star)\rangle\ge 0$ for all $X$.
• Eq. (4.5) (p. 1969): $\langle y^{k-1} - y^\star, \mathcal F(X^k) - \mathcal F(X^\star)\rangle\le -\|X^k - X^\star\|_F^2$.
• Contraction step (p. 1969): $\|y^k - y^\star\|\le\|y^{k-1} - y^\star + \delta_k(\mathcal F(X^k) - \mathcal F(X^\star))\|$.
• Eq. (4.6) (p. 1970): if $2\delta_k - \delta_k^2L^2\ge\beta > 0$ for $k\ge1$, then $\|y^k - y^\star\|^2\le\|y^{k-1} - y^\star\|^2 - \beta\|X^k - X^\star\|_F^2$.

Significance

The result. Theorem 4.4 is the convergence guarantee for SVT beyond matrix completion. The componentwise error bounds of (3.8), whose SVT iteration is (3.9), are finitely many affine constraints and fall under it directly, as does any finite family of Lipschitz convex constraints, for instance a Frobenius-norm ball around the data. The conic variants of §3.3 ((3.11)–(3.13)) project the dual variable onto a cone rather than onto the nonnegative orthant and are not covered by the theorem as stated. Together with Theorem 3.1 of the same paper, which says that the solution of (3.4) tends to the minimum-nuclear-norm solution as $\tau\to\infty$, it justifies using SVT as a solver for nuclear-norm minimization under general convex constraints.

Formalizing it. The theorem is proved in the paper, with two steps delegated to the literature: Lemma 4.3 cites [31], and the concluding step reads "the conclusion is as before". Its proof is short but relies on convex-analytic facts that are standard on paper and missing, in this form, from Mathlib: subgradients of the nuclear norm, the subdifferential sum rule for finite convex functions, and nonexpansiveness of the projection onto the nonnegative orthant. No machine-checked proof of this theorem or of Uzawa-type convergence for nuclear-norm objectives is known to exist. The mission produces a complete, checked version of the argument, including the omitted closing step.

Difficulty

The obvious approach is to view (3.5) as projected gradient ascent on the dual function $g(y) = \min_X\mathcal L(X, y)$ and quote the standard convergence theorem for gradient methods with Lipschitz gradients. That does not apply directly: for general convex $f_i$ the dual function need not be differentiable, $\mathcal F(X^k)$ is only a supergradient, and the Lipschitz hypothesis (4.2) is on $\mathcal F$, not on a dual gradient. The proof instead works with the primal-dual pair: it needs first-order optimality conditions (4.4), which require a subdifferential sum rule for $f_\tau + \sum_i y_i f_i$ with nonsmooth $f_i$, and it needs the strong monotonicity of $\partial f_\tau$ (Lemma 4.1), which depends on the description of subgradients of the nuclear norm. A second subtlety is that the theorem asserts convergence of the whole primal sequence to the unique solution, not to some solution along a subsequence, while nothing is claimed about convergence of the dual sequence.

Formalization scope

Matrices are Matrix (Fin n₁) (Fin n₂) ℝ, vectors in $\mathbb R^m$ are Fin m → ℝ, and convergence of matrices is in Mathlib's product topology, which coincides with the Frobenius topology. The nuclear norm is the sum of Mathlib's LinearMap.singularValues of the matrix viewed as a map between Euclidean spaces. Each $f_i$ is a real-valued function with ConvexOn ℝ Set.univ. The iteration is a predicate on sequences indexed by ℕ: the paper's step $k$ produces X (k+1) and y (k+1) from y k with step size δ (k+1), and y 0 = 0. $X^k$ is required to minimize $\mathcal L(\cdot, y^{k-1})$; for $\tau>0$ and convex $f_i$ this minimizer exists and is unique, so the predicate is satisfiable and determines the sequence. The step-size condition is stated as $a\le\delta_k\le C$ for $k\ge1$ with $a>0$ and $C L^2 < 2$, which avoids the division $2/L^2$ (evaluated as $0$ in Lean when $L=0$); for $L=0$ it requires only bounded steps, matching the convention $2/0 = \infty$. Strong duality is the hypothesis that a saddle point exists; Slater's condition is not assumed. The paper's standing assumptions ($\tau>0$, convex $f_i$, and (4.2) where $L$ enters) appear as explicit hypotheses in every statement.

A formalization that assumes convergence or boundedness of the dual iterates, replaces the primal minimization by a closed-form thresholding step (valid only for affine $\mathcal F$), or states only subsequential convergence would not be this theorem; each of these is excluded by the statements above.

A complete development needs: subgradients of the nuclear norm and strong monotonicity of $\partial f_\tau$; existence and characterization of minimizers of strongly convex continuous functions on a finite-dimensional space; the subdifferential sum rule for finite convex functions; complementary slackness from the saddle-point inequalities; and nonexpansiveness of the entrywise positive part. These are reusable beyond this mission, especially for other Uzawa and augmented Lagrangian analyses. Contributions of any of these pieces as separate lemmas are welcome.

Selected references

• J.-F. Cai, E. J. Candès, Z. Shen, A Singular Value Thresholding Algorithm for Matrix Completion, SIAM J. Optim. 20(4):1956–1982, 2010. https://doi.org/10.1137/080738970
• E. J. Candès, B. Recht, Exact Matrix Completion via Convex Optimization, Found. Comput. Math. 9:717–772, 2009. https://doi.org/10.1007/s10208-009-9045-5
• K. J. Arrow, L. Hurwicz, H. Uzawa, Studies in Linear and Nonlinear Programming, Stanford University Press, 1958.
• S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511804441

Motivation

Matrix completion asks to recover an $n_1\times n_2$ matrix $M$ from a subset $\Omega$ of its entries. When $M$ has low rank, a standard convex surrogate is to minimize the nuclear norm $\|X\|_*$ (the sum of the singular values) subject to agreeing with $M$ on $\Omega$; Candès and Recht showed that this recovers $M$ exactly under incoherence and sampling conditions (Candès–Recht 2009). Generic interior-point solvers for this semidefinite program do not scale beyond matrices of a few hundred rows.

Cai, Candès and Shen (SIAM J. Optim. 2010) proposed the singular value thresholding (SVT) algorithm: a first-order iteration whose only nonlinear step is a soft-thresholding of singular values, and whose other iterate is a sparse matrix supported on $\Omega$. The algorithm has become a standard baseline in low-rank matrix recovery and a model example of dual (Uzawa-type) methods for nuclear-norm problems. This mission formalizes its convergence theorem.

Setting

All matrices are real. For $X,Y\in\mathbb R^{n_1\times n_2}$ write $\langle X,Y\rangle=\operatorname{trace}(X^*Y)=\sum_{i,j}X_{ij}Y_{ij}$ and $\|X\|_F^2=\langle X,X\rangle$. The nuclear norm $\|X\|_*$ is the sum of the singular values of $X$.

For an index set $\Omega$, the sampling projector $P_\Omega$ keeps the entries with indices in $\Omega$ and sets the others to zero.

A reduced singular value decomposition of a matrix $Y$ of rank $r$ is $Y=U\Sigma V^*$ with $U$ ($n_1\times r$) and $V$ ($n_2\times r$) having orthonormal columns and $\Sigma=\operatorname{diag}(\sigma_1,\dots,\sigma_r)$ with $\sigma_i>0$. For $\tau\ge0$ the singular value shrinkage operator is

$$\mathcal D_\tau(Y)=U\operatorname{diag}\big((\sigma_i-\tau)_+\big)V^*,\qquad t_+=\max(0,t).$$

Fix $\tau>0$, a sequence of step sizes $\{\delta_k\}_{k\ge1}$ and data $M$. The SVT iteration (2.7) starts from $Y^0=0$ and sets, for $k=1,2,\dots$,

$$X^k=\mathcal D_\tau(Y^{k-1}),\qquad Y^k=Y^{k-1}+\delta_k P_\Omega(M-X^k).$$

The proximal problem (2.8) is

$$\text{minimize}\ \ f_\tau(X)=\tau\|X\|_*+\tfrac12\|X\|_F^2\quad\text{subject to}\ \ P_\Omega(X)=P_\Omega(M).$$

More generally, for a linear map $\mathcal A:\mathbb R^{n_1\times n_2}\to\mathbb R^m$ with adjoint $\mathcal A^*$ and spectral norm $\|\mathcal A\|=\sup\{\|\mathcal A(X)\|_{\ell_2}:\|X\|_F=1\}$, and $b\in\mathbb R^m$, problem (3.1) is to minimize $f_\tau(X)$ subject to $\mathcal A(X)=b$, and Uzawa's iteration (3.3) starts from $y^0=0$ and sets $X^k=\mathcal D_\tau(\mathcal A^*(y^{k-1}))$, $y^k=y^{k-1}+\delta_k(b-\mathcal A(X^k))$.

Formalization targets

Goal: Theorem 4.2, second sentence (p. 1968)

If $0<\inf_k\delta_k\le\sup_k\delta_k<2$, then (2.8) has a unique solution $X^\star$ and the SVT iterates satisfy

$$\lim_{k\to\infty}X^k=X^\star .$$

Theorem 4.2, first sentence (p. 1968)

If (3.1) is feasible and $0<\inf_k\delta_k\le\sup_k\delta_k<2/\|\mathcal A\|^2$, then (3.1) has a unique solution and the iterates $X^k$ of (3.3) converge to it.

Supporting results (milestones, in attack order)

1. Well-definedness of $\mathcal D_\tau$ (§2.1, p. 1960): the output does not depend on the chosen SVD.
2. Theorem 2.1 (p. 1960): $\mathcal D_\tau(Y)=\arg\min_X \tfrac12\|X-Y\|_F^2+\tau\|X\|_*$.
3. Sparsity of the iterates (§2.2, p. 1961): since $Y^0=0$, every $Y^k$ vanishes outside $\Omega$.
4. Eq. (2.14) (p. 1964): the minimizers of the Lagrangian $f_\tau(X)+\langle Y,P_\Omega(M-X)\rangle$ are those of $\tau\|X\|_*+\tfrac12\|X-P_\Omega Y\|_F^2$.
5. Lemma 4.1 (p. 1968): for $Z\in\partial f_\tau(X)$, $Z'\in\partial f_\tau(X')$, $\langle Z-Z',X-X'\rangle\ge\|X-X'\|_F^2$.
6. The §3.1 reduction (p. 1964): for a sampling operator, $\mathcal A^*\mathcal A=P_\Omega$ and (3.3) becomes (2.7) under $Y^k=\mathcal A^*(y^k)$.
7. Theorem 4.2, first sentence, as above.

Significance

The theorem certifies that SVT, run with any step sizes in a fixed interval $(0,2)$, computes the unique minimizer of the strongly convex surrogate (2.8). Together with the separate fact that the solution of (2.8) tends to the minimum nuclear norm completion as $\tau\to\infty$ (the paper's Theorem 3.1, a companion mission), this is what justifies using SVT as a solver for nuclear-norm matrix completion. Theorem 2.1, the proximal characterization of singular value soft-thresholding, is used throughout the literature on proximal methods for low-rank problems.

The paper's proof of Theorem 4.2 consists of the reduction to Uzawa's method and a citation of a general convergence theorem for projected gradient methods on the dual. The formalization produces a self-contained, machine-checked chain: the proximal characterization of $\mathcal D_\tau$, the Lagrangian identity, strong monotonicity of $\partial f_\tau$, and the convergence argument itself. To our knowledge none of these results has a machine-checked proof; Mathlib at the pinned revision has singular values of linear maps but no SVD structure, no nuclear norm and no subgradient calculus.

Difficulty

Nothing in the iteration is a gradient step of a smooth function in $X$: the $X$-update is a nonsmooth proximal map, and the convergence of $X^k$ is not visible from the recursion itself. The paper's argument cites a general theorem on projected gradient methods ([25, Theorem 2.1]) and takes for granted that "strong duality holds" for (2.8) (p. 1963), so the existence of a Lagrange multiplier is part of what must be formalized. Theorem 2.1 depends on the subdifferential of the nuclear norm, which Mathlib does not provide, and therefore on the singular value decomposition and the duality between the nuclear and spectral norms. Convergence of objective values or of a subsequence would not suffice: the target is convergence of the whole sequence $X^k$ to the unique solution.

Formalization scope

Matrices are Matrix (Fin n₁) (Fin n₂) ℝ; convergence is Mathlib's topology on matrices, which coincides with the Frobenius-norm topology. $\langle\cdot,\cdot\rangle$ and $\|\cdot\|_F$ are defined entrywise; $\|X\|_*$ is the sum of Mathlib's LinearMap.singularValues of $X$ viewed as a map $\mathbb R^{n_2}\to\mathbb R^{n_1}$. The shrinkage operator is a relation IsShrink τ Y X defined, as in (2.1)–(2.2), through some reduced SVD of $Y$; well-definedness is a milestone. It is not defined as the minimizer of (2.3), which would make Theorem 2.1 definitional. Linear maps $\mathcal A$ are given by matrices $A_1,\dots,A_m$ with $\mathcal A(X)_i=\langle A_i,X\rangle$, and a sampling operator by an injective enumeration of $\Omega$. Subgradients are those of (2.4).

Sequences are indexed by $\mathbb N$: Lean's step $k+1$ is the paper's step $k$, so $X^0$ and $\delta_0$ are unused. Committed conventions:

• $Y^0=0$ and $y^0=0$ are hypotheses; with a start that is nonzero outside $\Omega$ the iterates converge to a different matrix.
• The standing $\tau>0$ is kept, except in Theorem 2.1 and the well-definedness statement, which are printed for $\tau\ge0$.
• The step-size conditions are explicit bounds $a>0$, $C$ with $a\le\delta_k\le C$ for $k\ge1$, together with $C<2$, respectively $C\|\mathcal A\|^2<2$. The multiplicative form avoids Lean's $x/0=0$: for $\mathcal A=0$ the condition does not become unsatisfiable.
• Feasibility of (3.1) is an added hypothesis of Theorem 4.2's first sentence, since "the unique solution" presupposes it.
• "Converges to the unique solution" is stated as existence and uniqueness of the solution together with convergence of the whole sequence to it.

A small unprinted helper, $\|\mathcal A\|\le1$ for sampling operators, is included to pass from the first sentence of Theorem 4.2 to the second; it is not a milestone. The subdifferential formula (2.6) of the nuclear norm and the Fejér-type condition of §5.1.2 are not stated. Reusable infrastructure welcome from solvers: existence and uniqueness properties of the reduced SVD, the nuclear/spectral norm duality, the subdifferential of the nuclear norm, and a general convergence theorem for Uzawa's method with a strongly convex objective.

Selected references

• J.-F. Cai, E. J. Candès, Z. Shen, A Singular Value Thresholding Algorithm for Matrix Completion, SIAM J. Optim. 20(4):1956–1982, 2010. https://doi.org/10.1137/080738970
• E. J. Candès, B. Recht, Exact Matrix Completion via Convex Optimization, Found. Comput. Math. 9:717–772, 2009. https://doi.org/10.1007/s10208-009-9045-5
• K. J. Arrow, L. Hurwicz, H. Uzawa, Studies in Linear and Non-Linear Programming, Stanford University Press, 1958.

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):

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). 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). 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

Why initialization matters for transfer learning

Transfer learning starts with a representation learned on an earlier task and adapts it to a new one. Two common choices are linear probing, which changes only the final linear predictor, and fine-tuning, which changes the representation as well. These procedures optimize related training objectives, but their behavior away from the training data can differ. Kumar and coauthors study this distinction through two-layer linear networks, alongside experiments with nonlinear networks. This mission formalizes their perfect-feature LP-FT result, rather than the empirical claims or the general imperfect-feature comparison. See Section 3.4, Proposition 3.7, PDF p. 10.

LP-FT first learns a head by linear probing and then uses that head to initialize full fine-tuning. The perfect-feature setting isolates the effect of head initialization: the representation already contains exactly the features needed to predict the labels, but the head initially need not use them correctly. The mathematical question is whether joint training preserves or loses the representation's ability to predict outside the observed training subspace.

Linear predictors, training data, and OOD loss

An input is a vector $x\in\mathbb R^d$. A feature extractor is a matrix $B\in\mathbb R^{k\times d}$, and a head is a vector $v\in\mathbb R^k$. Together they predict $v^\top Bx$, with effective weight vector $B^\top v$. The fixed matrix $X\in\mathbb R^{n\times d}$ contains the $n$ training inputs as rows. Their span is $S=\operatorname{rowspace}(X)$, with dimension $m$.

The ground truth has orthonormal-row features $B_\star$ and a nonzero head $v_\star$. Write $w_\star=B_\star^\top v_\star$ and $Y=Xw_\star$. Perfect pretrained features mean $B_0=UB_\star$ for an orthogonal matrix $U$. The corresponding aligned head is $u=Uv_\star$. The dimensions satisfy $1\le k\le m$ and $m+k<d$.

The two geometric assumptions require the orthogonal projections from $R_0=\operatorname{rowspace}(B_0)$ into $S$ and into $S^\perp$ to be injective. In this dimension regime these are exactly the positive largest-principal-angle cosine conditions used by the paper. They demand more than two subspaces having some nonorthogonal directions. The Lean definition spells out injectivity of $v\mapsto\Pi_T B_0^\top v$ for each $T\in\{S,S^\perp\}$. See Definition 3.2 and Appendix A.1, PDF pp. 7 and 22-23.

An out-of-distribution law $\mu$ is any probability measure on $\mathbb R^d$ with a finite second moment and positive-definite uncentered second-moment matrix $\Sigma=\mathbb E_\mu[xx^\top]$. Its mean need not be zero. Define

$$L_{\rm OOD}(v,B)=\mathbb E_{x\sim\mu} [(v^\top Bx-w_\star^\top x)^2].$$

Both training methods use the unnormalized loss $\widehat L(v,B)=\|XB^\top v-Y\|_2^2$. Fine-tuning follows its gradient flow in both parameters; linear probing keeps $B=B_0$. Time is real and nonnegative. These are the paper's equations (3.2)-(3.3), PDF p. 6.

Formalization targets

The goal is Proposition 3.7 in an explicit nonzero-signal regime. For $\sigma>0$, initialize an FT head with independent Gaussian coordinates, $v_0\sim\mathcal N(0,\sigma^2I_k)$. Establish

$$\Pr\!\left[\forall t\ge0,\quad L_{\rm OOD}(v_{\rm FT}(t),B_{\rm FT}(t))>0\right]=1.$$

Linear probing, from any initial head, must converge to $u$. Fine-tuning initialized at its limit must satisfy

$$v_{\rm LP}(t)\longrightarrow u,\qquad \forall t\ge0,\quad L_{\rm OOD}(v_{\rm LP\text{-}FT}(t),B_{\rm LP\text{-}FT}(t))=0.$$

The probability-one event applies to all times simultaneously. The goal also asserts existence of the relevant global flows; a conditional claim about a possibly nonexistent trajectory would not suffice. The statement does not assert a numerical error lower bound or a positive time-infimum.

Seven milestones supply the supporting results: global flow existence and FT uniqueness; unchanged features orthogonal to the training span; the balancedness invariant; the second-moment identity for OOD risk; almost-sure Gaussian head misalignment; exact LP recovery; and stationarity after LP initialization. The principal source is Appendices A.2 and A.7, PDF pp. 23-31 and 45-47.

What the result establishes

The result distinguishes two initializations of the same joint-training procedure. In this idealized setting, a head obtained by linear probing gives zero OOD loss throughout subsequent fine-tuning, while a Gaussian head almost surely has positive OOD loss at every finite time. The conclusion concerns population squared prediction error, not classification accuracy or a finite test-set estimate.

The paper establishes the mathematical claim; this mission asks for a Lean proof of the stated model and result. The scope is deliberately limited to perfect pretrained features. It does not claim an LP-FT upper bound for imperfect features, which the authors identify as a further challenge in Section 3.4, PDF p. 10. A completed development would also provide reusable components for finite dimensional gradient flows, factorized linear models, and population risk.

Why the proof needs the training dynamics

The training loss alone does not select a unique effective predictor in an overparameterized problem. Knowing that a predictor fits the observed examples therefore does not determine its OOD loss. Formalization must track the head and feature extractor together, and it must distinguish parameter stationarity from a claim that a derivative happens to vanish at one time. The Gaussian conclusion also requires one event controlling an uncountable set of times; separate probability-one statements for individual times would be weaker.

Formalization scope and conventions

Vectors use Mathlib's finite dimensional real Euclidean spaces. Matrices are represented as continuous linear maps, with Euclidean adjoints and operator norms. The feature update is written explicitly as the Frobenius-gradient equation; it is not a gradient with respect to the operator norm. Differentiability is imposed within $[0,\infty)$, including the right derivative at zero.

The dimensions, nonzero target, positive Gaussian scale, finite second moments, and projection injectivity are explicit. The nonzero target restricts the formalization to the regime of the Gaussian alignment argument in Lemma A.12; $k\le m$ makes the identifiability condition used in Proposition A.20 precise. The random-head law is the scaled standard Gaussian measure. No randomness of the fixed training matrix or independence from an additional data draw is assumed.

The model contains no assumed convergence, invariant, or desired risk bound. Each of those is a theorem obligation. The well-posedness milestone makes explicit an analytic prerequisite of the source's flow notation. The risk milestone uses the identity in (A.29)-(A.32), avoiding the reversed inequality printed in (A.28). The quantitative constant in Theorem 3.3 is outside this mission. Source-aligned proofs and the supporting analysis infrastructure are welcome; changing the learning rule or assuming a milestone inside the model would change the task.

Selected references

• Ananya Kumar, Aditi Raghunathan, Robbie Jones, Tengyu Ma, and Percy Liang, Fine-Tuning can Distort Pretrained Features and Underperform Out-of-Distribution, ICLR 2022, arXiv:2202.10054v1. Main target: Section 3.4, Proposition 3.7, PDF p. 10, equations (3.10)-(3.11); proof: Appendix A.7, PDF pp. 45-47, Proposition A.20 and (A.208)-(A.218). Supporting invariants: Appendix A.2, PDF p. 24, Lemmas A.3-A.4, equations (A.15)-(A.20). Gaussian alignment: Appendix A.3, PDF pp. 34-35, Lemmas A.11-A.12.

Motivation

This mission is pure mathematics about objects it defines itself: an octonion multiplication built from the Fano plane of the companion mission The role postulates force exactly seven points, and the matrix of the linear map

$$p \;\mapsto\; p\,a + b\,p$$

for two unit imaginary octonions $a, b$. It is motivated by the two-generator D8 flow $\dot\psi = \psi a + b\psi$ in the Shape Zero derivation (00_START_HERE/MODEL_SPEC.md §1b; 02_synthesis/D8_SYNTHESIS.md). The statements below do not depend on that motivation.

Result. For $a = e_1$ and $b = c\,e_1 + s\,e_2$ with $c^2 + s^2 = 1$, the characteristic polynomial of $M = R_a + L_b$ is

$$X^2\,(X^2 + 4)\,\bigl(X^2 + (2 - 2c)\bigr)^2 .$$

With $c = \cos\theta$, $2 - 2c = 4\sin^2(\theta/2)$, so the eigenvalues are $0, 0, \pm 2i$ and $\pm 2i\sin(\theta/2)$ (each twice), and the ratio of the two nonzero frequencies is $1/\sin(\theta/2)$.

What this mission does NOT prove.

• Only the canonical pair. It proves the result for $a = e_1$, $b = \cos\theta\, e_1 + \sin\theta\, e_2$. That every pair of unit imaginary octonions at angle $\theta$ gives the same spectrum follows from the classical fact that $G_2$ acts transitively on such pairs — not formalized here.
• Nothing about any model. It says nothing about which angle, if any, a physical model selects, or whether the D8 flow plays a role in one.
• One orientation. The octonion table uses one orientation of the Fano lines; all valid orientations give isomorphic algebras, and the spectrum is basis-independent, but only this table is formalized.

Setting

Write $e_0 = 1, e_1, \dots, e_7$ for the standard basis of $\mathbb{R}^8$. The imaginary unit $e_u$ ($u = 1, \dots, 7$) is labelled by the Fano point $u - 1$. For each line $\{l, l+1, l+3\}$ (mod $7$) of the companion mission's Fano plane RolesForceSeven.fanoLine, the product is oriented cyclically along the ordered triple $(l, l+1, l+3)$:

$$e_{l+1}\,e_{l+2} = e_{l+4}, \qquad e_{l+2}\,e_{l+4} = e_{l+1}, \qquad e_{l+4}\,e_{l+1} = e_{l+2}$$

(unit indices mod $7$, shifted into $1, \dots, 7$), with the reversed products negative, $e_u^2 = -1$, and $e_0$ the identity. This defines OctonionD8.octTable and the bilinear product OctonionD8.omul on $\mathbb{R}^8$.

For $a, b \in \mathbb{R}^8$, Rmat a is the matrix of $p \mapsto p\,a$ and Lmat b the matrix of $p \mapsto b\,p$ (column $j$ is the image of $e_j$). The flow matrix is

$$M = \texttt{flowMat}\;c\;s = R_{e_1} + L_{c e_1 + s e_2}.$$

The Fano plane is imported from the companion mission, not restated. The reordering blockEquiv and the two blocks blockA c s, blockB c s are defined explicitly for the milestones.

Formalization targets

Goal: the characteristic polynomial

$$c^2 + s^2 = 1 \;\Longrightarrow\; \chi_M(X) = X^2\,(X^2 + 4)\,\bigl(X^2 + (2 - 2c)\bigr)^2 .$$

This is OctonionD8.flow_charpoly. The hypothesis $c^2 + s^2 = 1$ is the only one, and it is needed: without it the characteristic polynomial differs.

Milestones — the proof outline

The proof goes through an invariant-subspace decomposition. Reorder the basis as $(e_0, e_1, e_2, e_4 \mid e_3, e_5, e_6, e_7)$ (OctonionD8.blockEquiv).

1. M1 (block-diagonal form). For all real $c, s$, in the reordered basis $M$ is block diagonal: $M = \begin{pmatrix} A & 0 \\ 0 & B \end{pmatrix}$, with explicit $4\times4$ blocks $A$ on $(e_0, e_1, e_2, e_4)$ and $B$ on $(e_3, e_5, e_6, e_7)$ (OctonionD8.blockA, OctonionD8.blockB).
2. M2 (block $A$). If $c^2 + s^2 = 1$, then $\chi_A(X) = X^2\,(X^2 + 4)$.
3. M3 (block $B$). If $c^2 + s^2 = 1$, then $\chi_B(X) = \bigl(X^2 + (2 - 2c)\bigr)^2$.

The goal follows: the characteristic polynomial is unchanged by reordering the basis, and that of a block-diagonal matrix is the product of the blocks' characteristic polynomials.

Further results (after the goal)

• It is the octonions: the norm is multiplicative. For all $p, q \in \mathbb{R}^8$, $\sum_k (pq)_k^2 = \bigl(\sum_i p_i^2\bigr)\bigl(\sum_j q_j^2\bigr)$ — the eight-square identity, which certifies that the table defines a normed (composition) algebra, the octonions, rather than some other algebra.
• The flow conserves the norm. $M^{\mathsf T} = -M$.
• An annihilating polynomial. If $c^2 + s^2 = 1$, then $M\,(M^2 + 4)\,\bigl(M^2 + (2 - 2c)\bigr) = 0$.

Corollary: the frequencies

For $0 < \theta < \pi$, with $c = \cos\theta$ and $s = \sin\theta$, the roots over $\mathbb{C}$ of the characteristic polynomial, with multiplicity, are exactly

$$0,\ 0,\ \pm 2i,\ \pm 2i\sin(\theta/2),\ \pm 2i\sin(\theta/2),$$

and $0 < \sin(\theta/2) < 1$. So the two nonzero frequencies $2$ and $2\sin(\theta/2)$ are distinct, and their ratio is $1/\sin(\theta/2)$. Uses $2 - 2\cos\theta = 4\sin^2(\theta/2)$.

Significance

The result itself. It gives the spectrum of the two-generator flow for the canonical pair in closed form, for every angle, from an octonion table built on the formalized Fano plane.

Formalizing it. The spectrum had been checked numerically and symbolically only.

Numerical and symbolic cross-check (independent code)

check	result
table from the companion mission's Fano lines is a normed algebra (200 random pairs)	true
eigenvalue magnitudes $\{0 \times 2,\ 2\sin(\theta/2) \times 4,\ 2 \times 2\}$ at 5°, 30°, 60°, 76.3°, 90°, 120°, 150°	max error $1.8\times10^{-15}$
symbolic characteristic polynomial (sympy, $s^2 = 1 - c^2$)	$X^2(X^2 + 4)(X^2 + 2 - 2c)^2$

These agree with the repository's shape_zero_tests/d8_closed_form.py (frequencies $\{0, 2\sin(\theta/2), 2\}$ to $5\times10^{-11}$), which uses a different octonion table.

Difficulty

Moderate. The goal needs the characteristic polynomial of an $8\times8$ matrix with symbolic entries; a direct determinant expansion is expensive. The milestones take the invariant-subspace route: the block-diagonal form (M1) is an entrywise computation from the octonion table, and each $4\times4$ block's characteristic polynomial (M2, M3) is a small determinant, reduced with $c^2 + s^2 = 1$. The further results are large but mechanical polynomial identities (the eight-square identity; the annihilating polynomial), where the risk is performance, not ideas.

Formalization scope

• Vectors are Fin 8 → ℝ; matrices are Matrix (Fin 8) (Fin 8) ℝ, with column $j$ the image of the basis vector $e_j$.
• The characteristic polynomial is Mathlib's Matrix.charpoly over $\mathbb{R}$; the corollary maps it to $\mathbb{C}$ and uses Polynomial.roots, a multiset, so multiplicities are part of the statement.
• The table is one fixed orientation of the Fano lines; $G_2$-invariance and other orientations are out of scope.

Selected references

• Wikipedia, Octonion. https://en.wikipedia.org/wiki/Octonion
• Wikipedia, Fano plane. https://en.wikipedia.org/wiki/Fano_plane
• Shape Zero repository (motivation only). https://github.com/ShapeZeroSZ/shape-zero

Motivation

The Shape Zero model (Shape Zero LLC, unpublished) couples neighbouring nodes through a velocity-dependent force, one coupling matrix per link. The companion mission Zero net power forces every link coupling to be symmetric (rings of ≥ 3 sites) proves that a coupling doing no net work (a passive coupling) must have every link matrix symmetric — but only on a one-dimensional ring. The model's base is three-dimensional. This mission extends the result to a periodic cubic lattice with any number q of spatial axes, so it covers q = 3 directly and reduces exactly to the ring result at q = 1.

What this mission does NOT prove. As with the companion missions, commuting with the complex structure $J$ is not derived here; it remains a modelling premise. This mission shows only that passivity forces symmetry on every link in every direction.

Setting

Fix natural numbers $q$ (number of axes), $L$ (sites along each axis) and $d$. A site is a point $x \in (\mathbb{Z}/L\mathbb{Z})^q$ of the periodic cubic lattice; $x \pm e_a$ is the site one step forward or back along axis $a$, wrapping around. Each link — a site $x$ together with an axis $a$ — carries its own real $d\times d$ matrix $W(x,a)$, and each site carries a velocity $v(x) \in \mathbb{R}^d$. The force on site $x$ is

$$F(x) = \sum_{a} \Bigl( W(x,a)\, v(x+e_a) - W(x-e_a,a)\, v(x-e_a) \Bigr),$$

where the second term uses the matrix of the link behind $x$. The total power is

$$P_W(v) = \sum_{x} v(x) \cdot F(x).$$

In Lean, sites are Site q L = Fin q → Fin L, the step is shift x a s (update coordinate $a$ by $s$ in Fin L), and the power is PassivityTorus.power q L d W v. The coupling is passive when $P_W(v) = 0$ for every $v$.

Formalization targets

Goal: passive if and only if every link is symmetric ($L \ge 3$)

$$L \ge 3 \;\Longrightarrow\; \Bigl(\forall v,\; P_W(v) = 0\Bigr) \iff \Bigl(\forall x, a,\; W(x,a)^{\mathsf T} = W(x,a)\Bigr).$$

This is PassivityTorus.passive_iff_symm, for every $q$ and $d$.

Milestones

1. M1. Stepping back then forward along an axis returns to the start.
2. M2 (power identity, every $q$, $L$). $P_W(v) = \sum_x \sum_a v(x) \cdot \bigl((W(x,a) - W(x,a)^{\mathsf T})\, v(x+e_a)\bigr)$.
3. M3 (symmetric links are passive, every $L$).
4. M4 (passive forces symmetric, $L \ge 3$).

Significance

The result itself. It is the dimension-independent form of the passivity theorem: whatever the number of spatial axes, a per-link coupling does no net work for every motion exactly when every link matrix is symmetric. It removes the one-dimensional restriction from the step that justifies restricting the model's coupling class to symmetric matrices.

Formalizing it. The ring result has been machine-checked; the lattice extension had been checked numerically only (identity error $\le 3.6\times10^{-14}$ at $(q,L) = (1,3), (2,3), (3,3), (3,4)$). A proof covers every $q$, $L \ge 3$ and $d$.

Difficulty

The algebra is the ring argument; the difficulty is bookkeeping. The incoming term must be reindexed by the one-step shift, which is a bijection of the torus, and the converse needs a test motion supported on two neighbouring sites $x$ and $x+e_a$ together with a proof that no other link joins them.

The hypothesis $L \ge 3$ is necessary. At $L = 2$ the step forward and the step back along an axis reach the same site. This is proved (in Lean, locally): for every $q \ge 1$, putting the same non-symmetric matrix $\begin{pmatrix} 0 & 1 \\ 0 & 0 \end{pmatrix}$ on every link of the $L = 2$ lattice gives exactly zero power for every velocity field, so passivity does not force symmetry there. Weakening the hypothesis makes the goal false.

Formalization scope

• The lattice is periodic in every axis, with the same $L$ along each; [NeZero L] is needed for the literal $1$ in Fin L and is implied by $L \ge 3$ in the goal.
• There is one matrix per site per axis, with no relation assumed between links.
• Passivity is quantified over all velocity fields; everything is real.
• $q = 0$ (a single site, no links) and $d = 0$ are included; both sides of the goal hold trivially there, and this is not a trivialization since the statement is quantified over all $q$ and $d$.

Selected references

• Wikipedia, Symmetric matrix. https://en.wikipedia.org/wiki/Symmetric_matrix
• Wikipedia, Passivity (engineering). https://en.wikipedia.org/wiki/Passivity_(engineering)
• Mathlib, Mathlib.Data.Matrix.Mul (dot product ⬝ᵥ, matrix–vector product *ᵥ). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Mul.html

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).

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