Provedentropy-cost-lawattention-entropystabilitylaw

An entropy gain Δ in H₂ divides the cost factor by e^Δ: n·S' = n·S·e^{−Δ} when −log S' = −log S + Δ

For all $\htmlData{mx=1}{n, S, S', \Delta \in \htmlData{mx=0}{\mathbb{R}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{n}$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{S}$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{S'}$ and $\htmlData{mx=2}{-\htmlData{mx=1}{\log \htmlData{mx=0}{S'}}} \mathrel{\htmlData{mx=8}{=}} \htmlData{mx=7}{\htmlData{mx=5}{-\htmlData{mx=4}{\log \htmlData{mx=3}{S}}} + \htmlData{mx=6}{\Delta}}$ , then

\htmlData{mx=2}{\htmlData{mx=0}{n} \cdot \htmlData{mx=1}{S'}} \mathrel{\htmlData{mx=10}{=}} \htmlData{mx=9}{\htmlData{mx=5}{\htmlData{mx=3}{n} \cdot \htmlData{mx=4}{S}} \cdot \htmlData{mx=8}{e^{\htmlData{mx=7}{-\htmlData{mx=6}{\Delta}}}}}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: n, S, S', Δ range over real numbers: the statement must hold for every choice. ((n S S' Δ : ℝ))
<Less than: 0 is strictly smaller than n. (0 < n)
−xNegation: The negative of log(S'). (- Real.log S')
=Equality: −log(S') and −log(S) + Δ are the same. (- Real.log S' = - Real.log S + Δ)
·Multiplication: n times S'. (n * S')
logNatural logarithm: The logarithm of S' to base e: the power e must be raised to to give S'. (Real.log S')
+Addition: −log(S) plus Δ. (- Real.log S + Δ)
eˣExponential function: e raised to the power −Δ, where e ≈ 2.718. (Real.exp (-Δ))

theorem ec-entropy-gain-divides-cost (n S S' Δ : ℝ) (hn : 0 < n) (hS : 0 < S) (hS' : 0 < S') (hΔ : - Real.log S' = - Real.log S + Δ) :
    n * S' = (n * S) * Real.exp (-Δ)

The Flatness–Speed Alignment quantifier: every nat of Rényi-2 entropy gained per head (e.g. from σReparam-style entropy preservation) cuts that head's unbiased sampling cost by e. Part of 'Entropy–Cost Law: attention compute cost is n e^{-H2}, so stability regularizers also buy speed'.

How it was proved

Proved: 4 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: 13 lines of Lean

An entropy gain Δ in H₂ divides the cost factor by e^Δ: n·S' = n·S·e^{−Δ} when −log S' = −log S + Δ

How it was proved

More proved statements