Provedattentioninnovationexternal-review-3

Surrogate innovation: mean and residual reward bound

For all $\htmlData{mx=1}{J \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=3}{r, b, v, a : \htmlData{mx=0}{J} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ and $\htmlData{mx=1}{B, c, F, \eta \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=4}{\forall j,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{r}(\htmlData{mx=1}{j})}}$ , $\htmlData{mx=4}{\forall j,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{b}(\htmlData{mx=1}{j})}}$ , $\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}$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{B}$ , $\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=15}{=}} \htmlData{mx=14}{\htmlData{mx=12}{B} \cdot \htmlData{mx=13}{c}}$ , $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{F}$ , $\htmlData{mx=6}{\forall j,\ \htmlData{mx=3}{\left\lvert \htmlData{mx=2}{\htmlData{mx=0}{v}(\htmlData{mx=1}{j})} \right\rvert} \mathrel{\htmlData{mx=5}{\leq}} \htmlData{mx=4}{F}}$ , $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{\eta}$ and $\htmlData{mx=10}{\forall j,\ \htmlData{mx=7}{\left\lvert \htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{a}(\htmlData{mx=1}{j})} - \htmlData{mx=5}{\htmlData{mx=3}{b}(\htmlData{mx=4}{j})}} \right\rvert} \mathrel{\htmlData{mx=9}{\leq}} \htmlData{mx=8}{\eta}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{J}}$ ), then

\htmlData{mx=1}{\left\lvert \htmlData{mx=0}{c} \right\rvert} \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{F} \mathbin{\htmlData{mx=24}{\land}} \htmlData{mx=23}{\forall j,\ \htmlData{mx=17}{\left\lvert \htmlData{mx=16}{(\htmlData{mx=10}{\htmlData{mx=6}{\htmlData{mx=4}{a}(\htmlData{mx=5}{j})} - \htmlData{mx=9}{\htmlData{mx=7}{b}(\htmlData{mx=8}{j})}}) \cdot (\htmlData{mx=15}{\htmlData{mx=13}{\htmlData{mx=11}{v}(\htmlData{mx=12}{j})} - \htmlData{mx=14}{c}})} \right\rvert} \mathrel{\htmlData{mx=22}{\leq}} \htmlData{mx=21}{\htmlData{mx=19}{2\htmlData{mx=18}{F}} \cdot \htmlData{mx=20}{\eta}}}

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, b, v, a range over J → ℝ: the statement must hold for every choice. ((r b v a : J → ℝ))
x ∈ TVariables: B, c, F, η range over real numbers: the statement must hold for every choice. ((B c F η : ℝ))
∀For all: The statement after the comma holds for every j. (∀ j, 0 ≤ r j)
∑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)
<Less than: 0 is strictly smaller than B. (0 < B)
∧And: Both hold: |c| ≤ F, and ∀ j, |(a(j) − b(j)) · (v(j) − c)| ≤ 2 · F · η. (|c| ≤ F ∧ ∀ j, |(a j - b j) * (v j - c)…)
RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: 0 is less than or equal to r(j). (0 ≤ r j)
·Multiplication: r(j) times b(j). (r j * b j)
|x|Absolute value: The size of v(j) without its sign. (|v j|)
-Subtraction: a(j) minus b(j). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (a j - b j)

theorem innov-surrogate-reward-bound {J : Type} [Fintype J] (r b v a : J → ℝ) (B c F η : ℝ) (hr : ∀ j, 0 ≤ r j) (hb : ∀ j, 0 ≤ b j) (hB : ∑ j, r j * b j = B) (hB0 : 0 < B) (hc : ∑ j, r j * b j * v j = B * c) (hF : 0 ≤ F) (hv : ∀ j, |v j| ≤ F) (hη : 0 ≤ η) (hab : ∀ j, |a j - b j| ≤ η) :
    |c| ≤ F ∧ ∀ j, |(a j - b j) * (v j - c)| ≤ 2 * F * η

Nonnegative finite reference and surrogate weights, positive surrogate mass and bounded scalar values imply a bounded surrogate mean and reward. Vector and stopped-process bounds are paper steps.

How it was proved

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

Surrogate innovation: mean and residual reward bound

How it was proved

More proved statements