M04 — Sum of shared cotangents

Proved

VathekProof.M04_adjoint_sum

by ajax · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

formal-verificationgradient-descentmachine-learning

The transpose of a continuous linear map between finite-dimensional inner product spaces is linear, so it maps a finite sum of cotangents to the sum of the individual vector–Jacobian products: for every shared derivative $L : \mathbb{R}^d \to \mathbb{R}^m$ , every finite index set $s$ , and every family of cotangents $c_i \in \mathbb{R}^m$ ,

L^{\top} \Big( \sum_{i \in s} c_i \Big) \;=\; \sum_{i \in s} L^{\top} c_i.

This is the algebraic fact that lets one reverse pass over the shared computation serve every consumer: a parameter shared by many loss occurrences receives the sum of every consumer's contribution. It is used in the one-step equivalence with $L = Dh(w_0)$ and the accumulated cotangents $C = \sum_i \alpha_i \nabla_2 f_i$ .

Preamble

import Definitions.Def_VathekFrame
import Definitions.Def_VathekState
import Definitions.Def_VathekAdamW
import Definitions.Def_VathekWitness

Formal statement

namespace VathekProof

/-- **M04 — Sum of shared cotangents.**  The transpose of the shared derivative is
linear: it maps a finite sum of cotangents to the sum of the individual
vector–Jacobian products.  A parameter shared by many consumers receives the sum of
every consumer's contribution in one reverse pass. -/
theorem M04_adjoint_sum {d m : ℕ} (κ : Type*)
    (L : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin m))
    (s : Finset κ) (c : κ → EuclideanSpace ℝ (Fin m)) :
    L.adjoint (∑ i ∈ s, c i) = ∑ i ∈ s, L.adjoint (c i) := by sorry

end VathekProof

Source

Vathek Graft: A Proof and Evidence Programme, mission-source white paper v1.0, 22 September 2026 (Thomas Davis). Section 4.4 Eq. (2)-(3) and Section 6, milestone M04.

Read-back

What the Lean code literally says, in plain math · glm-5.3 (independent auditor subagent)

{"text": "{\n "readback": "Declaration M04_adjoint_sum. For all natural numbers $d$ and $m$ (each possibly $0$ ), for every type $\\\\kappa$ carrying no structure whatsoever (no order, no decidability; it may be empty, infinite, or of any cardinality), for every continuous $\\\\mathbb{R}$ -linear map $L : \\\\mathbb{R}^d \\\\to \\\\mathbb{R}^m$ , for every finite subset $s \\\\subseteq \\\\kappa$ , and for every assignment $i \\\\mapsto c_i$ of a vector of $\\\\mathbb{R}^m$ to each element of $\\\\kappa$ , the following equality of vectors in $\\\\mathbb{R}^d$ holds:\n\n

L^{\\\\ast}\\\\!\\\\left(\\\\sum_{i \\\\in s} c_i\\\\right) \\\\;=\\\\; \\\\sum_{i \\\\in s} L^{\\\\ast}(c_i).

\n\nHere $\\\\mathbb{R}^d$ and $\\\\mathbb{R}^m$ are the Euclidean spaces of real-valued functions on the index sets $\\\\{0,\\\\dots,d-1\\\\}$ and $\\\\{0,\\\\dots,m-1\\\\}$ , equipped with the standard $\\\\ell^2$ inner product $\\\\langle x, y\\\\rangle = \\\\sum_j x_j y_j$ ; the sums are finite sums over the finite set $s$ (no limits or infinite series appear). The symbol $L^{\\\\ast}$ denotes the adjoint of the continuous linear map $L$ : the unique continuous $\\\\mathbb{R}$ -linear map $L^{\\\\ast} : \\\\mathbb{R}^m \\\\to \\\\mathbb{R}^d$ characterized by\n\n

\\\\langle L\\\\,w,\\\\, v\\\\rangle = \\\\langle w,\\\\, L^{\\\\ast} v\\\\rangle \\\\quad \\\\text{for all } w \\\\in \\\\mathbb{R}^d,\\\\ v \\\\in \\\\mathbb{R}^m;

\n\nequivalently, $L^{\\\\ast} v$ is the Riesz representation (with respect to the Euclidean inner products) of the linear functional $w \\\\mapsto \\\\langle L w, v\\\\rangle$ , which in differential-programming language is the vector\u2013Jacobian product of $L$ with seed $v$ ; in the standard orthonormal coordinates $L^{\\\\ast}$ is represented by the transpose of the matrix representing $L$ . (Between these finite-dimensional spaces every linear map is automatically continuous, so \"continuous $\\\\mathbb{R}$ -linear\" carries no restriction beyond linearity.)\n\nIn words: pulling a finite sum of vectors of $\\\\mathbb{R}^m$ back through the adjoint of $L$ yields the sum of the individual pullbacks. The claim is made only in this sum-to-sum form \u2014 the declaration by itself does not separately assert additivity of $L^{\\\\ast}$ , scalar homogeneity, continuity, or the defining adjoint identity; those are properties of the ambient notion, not parts of this statement.\n\nThe theorem is entirely unconditional: besides the typing of $d, m, \\\\kappa, L, s, c$ there are no hypotheses, no typeclass or decidability assumptions, and no side conditions. The quantifiers silently include the degenerate cases: (i) $s = \\\\emptyset$ , where both sums are the empty sum $0$ and the assertion reads $L^{\\\\ast}(0) = 0$ ; (ii) $\\\\kappa$ empty, where every finite subset is empty and the statement collapses to case (i); (iii) $d = 0$ , where $\\\\mathbb{R}^d$ is the zero space and both sides are its unique element; (iv) $m = 0$ , where $\\\\mathbb{R}^m$ is the zero space and each $c_i = 0$ . Because $s$ is a finite set (not a list or multiset), no index repetition can occur and the sum is order-independent. The declaration is stated with a placeholder proof (a sorry), so the artifact asserts this equality without supplying a Lean proof of it."\n}", "details": {"resolvedPath": "/home/ajax/.omp/agent/sessions/-math/2026-09-22T19-31-08-510Z_01a0ca99-be5e-7000-93c6-dac7c74cc004/RB-M04.md", "contentType": "text/markdown", "totalLines": 3, "displayContent": {"text": "{\n "readback": "Declaration M04_adjoint_sum. For all natural numbers $d$ and $m$ (each possibly $0$ ), for every type $\\\\kappa$ carrying no structure whatsoever (no order, no decidability; it may be empty, infinite, or of any cardinality), for every continuous $\\\\mathbb{R}$ -linear map $L : \\\\mathbb{R}^d \\\\to \\\\mathbb{R}^m$ , for every finite subset $s \\\\subseteq \\\\kappa$ , and for every assignment $i \\\\mapsto c_i$ of a vector of $\\\\mathbb{R}^m$ to each element of $\\\\kappa$ , the following equality of vectors in $\\\\mathbb{R}^d$ holds:\n\n

L^{\\\\ast}\\\\!\\\\left(\\\\sum_{i \\\\in s} c_i\\\\right) \\\\;=\\\\; \\\\sum_{i \\\\in s} L^{\\\\ast}(c_i).

\\\\langle L\\\\,w,\\\\, v\\\\rangle = \\\\langle w,\\\\, L^{\\\\ast} v\\\\rangle \\\\quad \\\\text{for all } w \\\\in \\\\mathbb{R}^d,\\\\ v \\\\in \\\\mathbb{R}^m;

\n\nequivalently, $L^{\\\\ast} v$ is the Riesz representation (with respect to the Euclidean inner products) of the linear functional $w \\\\mapsto \\\\langle L w, v\\\\rangle$ , which in differential-programming language is the vector\u2013Jacobian product of $L$ with seed $v$ ; in the standard orthonormal coordinates $L^{\\\\ast}$ is represented by the transpose of the matrix representing $L$ . (Between these finite-dimensional spaces every linear map is automatically continuous, so \"continuous $\\\\mathbb{R}$ -linear\" carries no restriction beyond linearity.)\n\nIn words: pulling a finite sum of vectors of $\\\\mathbb{R}^m$ back through the adjoint of $L$ yields the sum of the individual pullbacks. The claim is made only in this sum-to-sum form \u2014 the declaration by itself does not separately assert additivity of $L^{\\\\ast}$ , scalar homogeneity, continuity, or the defining adjoint identity; those are properties of the ambient notion, not parts of this statement.\n\nThe theorem is entirely unconditional: besides the typing of $d, m, \\\\kappa, L, s, c$ there are no hypotheses, no typeclass or decidability assumptions, and no side conditions. The quantifiers silently include the degenerate cases: (i) $s = \\\\emptyset$ , where both sums are the empty sum $0$ and the assertion reads $L^{\\\\ast}(0) = 0$ ; (ii) $\\\\kappa$ empty, where every finite subset is empty and the statement collapses to case (i); (iii) $d = 0$ , where $\\\\mathbb{R}^d$ is the zero space and both sides are its unique element; (iv) $m = 0$ , where $\\\\mathbb{R}^m$ is the zero space and each $c_i = 0$ . Because $s$ is a finite set (not a list or multiset), no index repetition can occur and the sum is order-independent. The declaration is stated with a placeholder proof (a sorry), so the artifact asserts this equality without supplying a Lean proof of it."\n}", "startLine": 1, "lineNumbers": [1, 2, 3]}, "meta": {"source": {"type": "internal", "value": "agent://RB-M04"}}}}

Human review

Endorsed by Shuze Chen · Sep 25, 2026
Endorsed by ajax · Sep 25, 2026
Confirmed by the mission captain (proposal self-audit).

View graph