Provedalphabaguettenoether-checksumlinear

Checksum E1 (Euler homogeneity): for y = Wx, Σₜ⟨dyₜ, yₜ⟩ = ⟨dW, W⟩ = Σₜ⟨dxₜ, xₜ⟩

For all $\htmlData{mx=1}{N, \mathit{Din}, \mathit{Dout} \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=9}{W : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{\mathit{Dout}}} \mathrel{\htmlData{mx=8}{\to}} \htmlData{mx=5}{\htmlData{mx=3}{\operatorname{Fin}}\,\htmlData{mx=4}{\mathit{Din}}} \mathrel{\htmlData{mx=7}{\to}} \htmlData{mx=6}{\mathbb{R}}}$ , $\htmlData{mx=9}{x : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{N}} \mathrel{\htmlData{mx=8}{\to}} \htmlData{mx=5}{\htmlData{mx=3}{\operatorname{Fin}}\,\htmlData{mx=4}{\mathit{Din}}} \mathrel{\htmlData{mx=7}{\to}} \htmlData{mx=6}{\mathbb{R}}}$ and $\htmlData{mx=9}{\mathit{dy} : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{N}} \mathrel{\htmlData{mx=8}{\to}} \htmlData{mx=5}{\htmlData{mx=3}{\operatorname{Fin}}\,\htmlData{mx=4}{\mathit{Dout}}} \mathrel{\htmlData{mx=7}{\to}} \htmlData{mx=6}{\mathbb{R}}}$ :

\begin{aligned} & \left(\right. \htmlData{mx=18}{\sum_{t} \htmlData{mx=17}{\sum_{o} \htmlData{mx=16}{\htmlData{mx=5}{\htmlData{mx=2}{\mathit{dy}}(\htmlData{mx=3}{t}, \htmlData{mx=4}{o})} \cdot \left(\htmlData{mx=15}{\sum_{c} \htmlData{mx=14}{\htmlData{mx=9}{\htmlData{mx=6}{W}(\htmlData{mx=7}{o}, \htmlData{mx=8}{c})} \cdot \htmlData{mx=13}{\htmlData{mx=10}{x}(\htmlData{mx=11}{t}, \htmlData{mx=12}{c})}}}\right)}}} \\ & \quad \htmlData{mx=1}{=} \htmlData{mx=35}{\sum_{o} \htmlData{mx=34}{\sum_{c} \htmlData{mx=33}{\left(\htmlData{mx=28}{\sum_{t} \htmlData{mx=27}{\htmlData{mx=22}{\htmlData{mx=19}{\mathit{dy}}(\htmlData{mx=20}{t}, \htmlData{mx=21}{o})} \cdot \htmlData{mx=26}{\htmlData{mx=23}{x}(\htmlData{mx=24}{t}, \htmlData{mx=25}{c})}}}\right) \cdot \htmlData{mx=32}{\htmlData{mx=29}{W}(\htmlData{mx=30}{o}, \htmlData{mx=31}{c})}}}} \left.\right) \\ & \htmlData{mx=0}{\land} \left(\right. \htmlData{mx=53}{\sum_{t} \htmlData{mx=52}{\sum_{o} \htmlData{mx=51}{\htmlData{mx=40}{\htmlData{mx=37}{\mathit{dy}}(\htmlData{mx=38}{t}, \htmlData{mx=39}{o})} \cdot \left(\htmlData{mx=50}{\sum_{c} \htmlData{mx=49}{\htmlData{mx=44}{\htmlData{mx=41}{W}(\htmlData{mx=42}{o}, \htmlData{mx=43}{c})} \cdot \htmlData{mx=48}{\htmlData{mx=45}{x}(\htmlData{mx=46}{t}, \htmlData{mx=47}{c})}}}\right)}}} \\ & \quad \htmlData{mx=36}{=} \htmlData{mx=70}{\sum_{t} \htmlData{mx=69}{\sum_{c} \htmlData{mx=68}{\left(\htmlData{mx=63}{\sum_{o} \htmlData{mx=62}{\htmlData{mx=57}{\htmlData{mx=54}{W}(\htmlData{mx=55}{o}, \htmlData{mx=56}{c})} \cdot \htmlData{mx=61}{\htmlData{mx=58}{\mathit{dy}}(\htmlData{mx=59}{t}, \htmlData{mx=60}{o})}}}\right) \cdot \htmlData{mx=67}{\htmlData{mx=64}{x}(\htmlData{mx=65}{t}, \htmlData{mx=66}{c})}}}} \left.\right) \end{aligned}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
x ∈ TVariables: N, Din, Dout range over natural numbers: the statement must hold for every choice. ((N Din Dout : ℕ))
Fin: Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fin)
f(x)Function application: Fin applied to Dout. Lean writes f x; papers write f(x). (Fin Dout)
∧And: Both hold: (∑ t, ∑ o, dy(t, o) · (∑ c, W(o, c) · x(t, c))) = (∑ o, ∑ …, and (∑ t, ∑ o, dy(t, o) · (∑ c, W(o, c) · x(t, c))) = (∑ t, ∑ …. ((∑ t, ∑ o, dy t o * (∑ c, W o c * x t c…)
=Equality: ∑ t, ∑ o, dy(t, o) · (∑ c, W(o, c) · x(t, c)) and ∑ o, ∑ c, (∑ t, dy(t, o) · x(t, c)) · W(o, c) are the same. (∑ t, ∑ o, dy t o * (∑ c, W o c * x t c)…)
⟹Implies: If Fin(Din), then ℝ. (Between types, A → B is the type of functions from A to B.) (Fin Din → ℝ)
RReal numbers: The real numbers: every point on the number line. (ℝ)
∑Summation: Add up W(o, c) · x(t, c) for every c. (∑ c, W o c * x t c)
·Multiplication: W(o, c) times x(t, c). (W o c * x t c)

theorem nc-linear-euler-identity {N Din Dout : ℕ} (W : Fin Dout → Fin Din → ℝ) (x : Fin N → Fin Din → ℝ) (dy : Fin N → Fin Dout → ℝ) :
    (∑ t, ∑ o, dy t o * (∑ c, W o c * x t c) = ∑ o, ∑ c, (∑ t, dy t o * x t c) * W o c) ∧ (∑ t, ∑ o, dy t o * (∑ c, W o c * x t c) = ∑ t, ∑ c, (∑ o, W o c * dy t o) * x t c)

A linear layer is homogeneous of degree one in its weights and in its input. Euler's identity ties the forward output, the weight-gradient kernel (dW = Σₜ dyₜxₜᵀ) and the data-gradient kernel (dxₜ = Wᵀdyₜ) together: three scalars that must agree. In the experiment a weight-gradient kernel reading input rows in the wrong order is flagged at ≈ 4·10⁶× the clean residual. Part of 'Noether checksums for Baguette's backward kernels'.

How it was proved

Proved: 3 October 2026
By: Ajax, with the agent “Baguette math & proofs (Claude Code, 2026-10-03)”
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: Classical.choice, Quot.sound, propext
Proof: 24 lines of Lean

Checksum E1 (Euler homogeneity): for y = Wx, Σₜ⟨dyₜ, yₜ⟩ = ⟨dW, W⟩ = Σₜ⟨dxₜ, xₜ⟩

How it was proved

More proved statements