Provedattentionresidual-seriesexternal-review-4

Residual series: finite normalized residual and reward means

For all $\htmlData{mx=1}{J \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=3}{r, a, b, v : \htmlData{mx=0}{J} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ and $\htmlData{mx=1}{B, p, M, o, c \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=0}{B} \mathrel{\htmlData{mx=1}{\neq}} 0$ , $\htmlData{mx=7}{\sum_{j} \htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{r}(\htmlData{mx=1}{j})} \cdot \htmlData{mx=5}{\htmlData{mx=3}{b}(\htmlData{mx=4}{j})}}} \mathrel{\htmlData{mx=9}{=}} \htmlData{mx=8}{B}$ , $\htmlData{mx=7}{\sum_{j} \htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{r}(\htmlData{mx=1}{j})} \cdot \htmlData{mx=5}{\htmlData{mx=3}{a}(\htmlData{mx=4}{j})}}} \mathrel{\htmlData{mx=9}{=}} \htmlData{mx=8}{p}$ , $\htmlData{mx=11}{\sum_{j} \htmlData{mx=10}{\htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{r}(\htmlData{mx=1}{j})} \cdot \htmlData{mx=5}{\htmlData{mx=3}{b}(\htmlData{mx=4}{j})}} \cdot \htmlData{mx=9}{\htmlData{mx=7}{v}(\htmlData{mx=8}{j})}}} \mathrel{\htmlData{mx=13}{=}} \htmlData{mx=12}{M}$ , $\htmlData{mx=11}{\sum_{j} \htmlData{mx=10}{\htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{r}(\htmlData{mx=1}{j})} \cdot \htmlData{mx=5}{\htmlData{mx=3}{a}(\htmlData{mx=4}{j})}} \cdot \htmlData{mx=9}{\htmlData{mx=7}{v}(\htmlData{mx=8}{j})}}} \mathrel{\htmlData{mx=15}{=}} \htmlData{mx=14}{\htmlData{mx=12}{p} \cdot \htmlData{mx=13}{o}}$ and $\htmlData{mx=2}{\htmlData{mx=0}{B} \cdot \htmlData{mx=1}{c}} \mathrel{\htmlData{mx=4}{=}} \htmlData{mx=3}{M}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{J}}$ ), then

\begin{aligned} & \left(\htmlData{mx=14}{\sum_{j} \htmlData{mx=13}{\htmlData{mx=3}{\htmlData{mx=1}{r}(\htmlData{mx=2}{j})} \cdot \left(\htmlData{mx=12}{\frac{\htmlData{mx=10}{\htmlData{mx=6}{\htmlData{mx=4}{b}(\htmlData{mx=5}{j})} - \htmlData{mx=9}{\htmlData{mx=7}{a}(\htmlData{mx=8}{j})}}}{\htmlData{mx=11}{B}}}\right)}}\right) \mathrel{\htmlData{mx=19}{=}} \htmlData{mx=18}{1 - \htmlData{mx=17}{\frac{\htmlData{mx=15}{p}}{\htmlData{mx=16}{B}}}} \\ & \htmlData{mx=0}{\land} \left(\htmlData{mx=41}{\sum_{j} \htmlData{mx=40}{\htmlData{mx=23}{\htmlData{mx=21}{r}(\htmlData{mx=22}{j})} \cdot \left(\htmlData{mx=39}{\htmlData{mx=33}{-\htmlData{mx=32}{\frac{\htmlData{mx=30}{\htmlData{mx=26}{\htmlData{mx=24}{b}(\htmlData{mx=25}{j})} - \htmlData{mx=29}{\htmlData{mx=27}{a}(\htmlData{mx=28}{j})}}}{\htmlData{mx=31}{B}}}} \cdot (\htmlData{mx=38}{\htmlData{mx=36}{\htmlData{mx=34}{v}(\htmlData{mx=35}{j})} - \htmlData{mx=37}{c}})}\right)}}\right) \\ & \quad \htmlData{mx=20}{=} \htmlData{mx=48}{\htmlData{mx=44}{\frac{\htmlData{mx=42}{p}}{\htmlData{mx=43}{B}}} \cdot (\htmlData{mx=47}{\htmlData{mx=45}{o} - \htmlData{mx=46}{c}})} \end{aligned}

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)
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 J. Lean writes f x; papers write f(x). (Fintype J)
⟹Implies: If J, then ℝ. (Between types, A → B is the type of functions from A to B.) (J → ℝ)
x : TVariables: r, a, b, v range over J → ℝ: the statement must hold for every choice. ((r a b v : J → ℝ))
x ∈ TVariables: B, p, M, o, c range over real numbers: the statement must hold for every choice. ((B p M o c : ℝ))
≠Not equal: B and 0 are different. (B ≠ 0)
∑Summation: Add up r(j) · b(j) for every j. (∑ j,r j*b j)
=Equality: ∑ j, r(j) · b(j) and B are the same. (∑ j,r j*b j=B)
∧And: Both hold: (∑ j, r(j) · ((b(j) − a(j))/B)) = 1 − p/B, and (∑ j, r(j) · (−((b(j) − a(j))/B) · (v(j) − c))) = p/B · (o…. ((∑ j,r j*((b j-a j)/B))=1-p/B ∧ (∑ j,r …)
RReal numbers: The real numbers: every point on the number line. (ℝ)
·Multiplication: r(j) times b(j). (r j*b j)
a/bDivision: b(j) − a(j) divided by B. In Lean, dividing by 0 gives 0. ((b j-a j)/B)
-Subtraction: b(j) minus a(j). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (b j-a j)
−xNegation: The negative of (b(j) − a(j))/B. (-((b j-a j)/B))

theorem residual-series-reward-mean {J : Type} [Fintype J] (r a b v : J → ℝ) (B p M o c : ℝ) (hB : B ≠ 0) (hb : ∑ j,r j*b j=B) (ha : ∑ j,r j*a j=p) (hM : ∑ j,r j*b j*v j=M) (ho : ∑ j,r j*a j*v j=p*o) (hc : B*c=M) :
    (∑ j,r j*((b j-a j)/B))=1-p/B ∧ (∑ j,r j*(-((b j-a j)/B)*(v j-c)))=(p/B)*(o-c)

Finite scalar aggregate identity connects h=(b-a)/B and R=-h(v-c) to the original normalized attention discrepancy. This is the attention-specific algebra used by the full finite sampler, not an infinite probability-space theorem.

How it was proved

Proved: 6 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: 15 lines of Lean

Residual series: finite normalized residual and reward means

How it was proved

More proved statements