Provedattentionversion-9finite-lawconstructible-state

A sharp finite coupled-input lower bound on fresh-information activation

For all $\htmlData{mx=2}{\Omega : \htmlData{mx=1}{\htmlData{mx=0}{\operatorname{Type}} \cdot }}$ , $\htmlData{mx=3}{w : \htmlData{mx=0}{\Omega} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ , $\htmlData{mx=3}{\mathit{active} : \htmlData{mx=0}{\Omega} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\operatorname{Bool}}}$ , $\htmlData{mx=3}{\mathit{yp}, \mathit{ym} : \htmlData{mx=0}{\Omega} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ and $\htmlData{mx=1}{E, \varepsilon \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=4}{\forall i,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{i})}}$ , $\htmlData{mx=6}{\htmlData{mx=0}{\operatorname{sum}}(\htmlData{mx=1}{\operatorname{univ}}, \htmlData{mx=5}{i \mapsto \htmlData{mx=4}{\htmlData{mx=2}{w}(\htmlData{mx=3}{i})}})} \mathrel{\htmlData{mx=7}{=}} 1$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{E}$ , $\htmlData{mx=3}{\htmlData{mx=0}{\operatorname{mean}}(\htmlData{mx=1}{w}, \htmlData{mx=2}{\mathit{yp}})} \mathrel{\htmlData{mx=5}{=}} \htmlData{mx=4}{E}$ , $\htmlData{mx=3}{\htmlData{mx=0}{\operatorname{mean}}(\htmlData{mx=1}{w}, \htmlData{mx=2}{\mathit{ym}})} \mathrel{\htmlData{mx=6}{=}} \htmlData{mx=5}{-\htmlData{mx=4}{E}}$ , $\htmlData{mx=4}{\htmlData{mx=0}{\operatorname{mse}}(\htmlData{mx=1}{w}, \htmlData{mx=2}{\mathit{yp}}, \htmlData{mx=3}{E})} \mathrel{\htmlData{mx=7}{\leq}} \htmlData{mx=6}{\htmlData{mx=5}{\varepsilon}^{2}}$ , $\htmlData{mx=5}{\htmlData{mx=0}{\operatorname{mse}}(\htmlData{mx=1}{w}, \htmlData{mx=2}{\mathit{ym}}, \htmlData{mx=4}{-\htmlData{mx=3}{E}})} \mathrel{\htmlData{mx=8}{\leq}} \htmlData{mx=7}{\htmlData{mx=6}{\varepsilon}^{2}}$ and $\htmlData{mx=13}{\forall i,\ \htmlData{mx=2}{\htmlData{mx=0}{\mathit{active}}(\htmlData{mx=1}{i})} \mathrel{\htmlData{mx=4}{=}} \htmlData{mx=3}{\operatorname{false}} \mathrel{\htmlData{mx=12}{\implies}} \htmlData{mx=7}{\htmlData{mx=5}{\mathit{yp}}(\htmlData{mx=6}{i})} \mathrel{\htmlData{mx=11}{=}} \htmlData{mx=10}{\htmlData{mx=8}{\mathit{ym}}(\htmlData{mx=9}{i})}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{\Omega}}$ ), then

\left(\htmlData{mx=7}{\frac{\htmlData{mx=1}{\htmlData{mx=0}{E}^{2}}}{\htmlData{mx=6}{\htmlData{mx=3}{\htmlData{mx=2}{\varepsilon}^{2}} + \htmlData{mx=5}{\htmlData{mx=4}{E}^{2}}}}} \mathrel{\htmlData{mx=12}{\leq}} \htmlData{mx=11}{\htmlData{mx=8}{\operatorname{activationMass}}(\htmlData{mx=9}{w}, \htmlData{mx=10}{\mathit{active}})}\right)

What the notation means · or point at any symbol

Type: Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Type)
·Multiplication: Type times . (Type*)
Fintype: Fintype: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fintype)
f(x)Function application: Fintype applied to Ω. Lean writes f x; papers write f(x). (Fintype Ω)
⟹Implies: If Ω, then ℝ. (Between types, A → B is the type of functions from A to B.) (Ω → ℝ)
∀For all: The statement after the comma holds for every i. (∀ i,0≤w i)
sum: Finset.sum: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Finset.sum)
=Equality: sum(univ, i ↦ w(i)) and 1 are the same. (Finset.sum Finset.univ (fun i => w i)=1)
x : TVariables: yp, ym range over Ω → ℝ: the statement must hold for every choice. ((yp ym : Ω → ℝ))
x ∈ TVariables: E, ε range over real numbers: the statement must hold for every choice. ((E ε : ℝ))
<Less than: 0 is strictly smaller than E. (0<E)
mean: mean: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (mean)
mse: mse: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (mse)
RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: 0 is less than or equal to w(i). (0≤w i)
Bool: Bool: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Bool)
a/bDivision: E^2 divided by ε^2 + E^2. In Lean, dividing by 0 gives 0. (E^2/(ε^2+E^2))
−xNegation: The negative of E. (-E)
+Addition: ε^2 plus E^2. (ε^2+E^2)
univ: Finset.univ: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Finset.univ)
aᵇPower: ε raised to the power 2. (ε^2)
false: false: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (false)
activationMass: activationMass: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (activationMass)
x ↦ f(x)Function (λ-abstraction): The function sending i to w(i). Lean writes fun x => …; papers write x ↦ …. (fun i => w i)

theorem attention-v9-coupled-activation-bound {Ω : Type*} [Fintype Ω] (w : Ω → ℝ) (hw : ∀ i,0≤w i) (hs : Finset.sum Finset.univ (fun i => w i)=1)
    (active : Ω → Bool) (yp ym : Ω → ℝ) (E ε : ℝ) (hE : 0<E)
    (hp : mean w yp=E) (hm : mean w ym=-E)
    (hvp : mse w yp E≤ε^2) (hvm : mse w ym (-E)≤ε^2)
    (hoff : ∀ i,active i=false → yp i=ym i) :
    (    E^2/(ε^2+E^2)≤activationMass w active)

Version 9 exact frozen target. Proof references the validated additive definition library. This mathematical finite-law/invariant target does not certify compiled Rust RAM runtime or the general linear-summary LP bridge.

How it was proved

Proved: 7 October 2026
By: Ajax
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: 12 lines of Lean

A sharp finite coupled-input lower bound on fresh-information activation

How it was proved

More proved statements