Provedattentioncertified-onlineaffine-information-frontier

Finite calibrated access moments imply the sharp probe bound

For all $\htmlData{mx=1}{J \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=3}{w, y, s : \htmlData{mx=0}{J} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ and $\htmlData{mx=1}{N, \mathit{lambda}, \mathit{eps}_{2}, B \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=4}{\forall j,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{j})}}$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{B}$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\mathit{eps}_{2}}$ , $\htmlData{mx=11}{\sum_{j} \htmlData{mx=10}{\htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{j})} \cdot \htmlData{mx=5}{\htmlData{mx=3}{y}(\htmlData{mx=4}{j})}} \cdot \htmlData{mx=9}{\htmlData{mx=7}{s}(\htmlData{mx=8}{j})}}} \mathrel{\htmlData{mx=13}{=}} \htmlData{mx=12}{\mathit{lambda}}$ , $\htmlData{mx=8}{\sum_{j} \htmlData{mx=7}{\htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{j})} \cdot \htmlData{mx=6}{\htmlData{mx=5}{\htmlData{mx=3}{s}(\htmlData{mx=4}{j})}^{2}}}} \mathrel{\htmlData{mx=10}{=}} \htmlData{mx=9}{N}$ and $\htmlData{mx=8}{\sum_{j} \htmlData{mx=7}{\htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{j})} \cdot \htmlData{mx=6}{\htmlData{mx=5}{\htmlData{mx=3}{y}(\htmlData{mx=4}{j})}^{2}}}} \mathrel{\htmlData{mx=15}{\leq}} \htmlData{mx=14}{\htmlData{mx=9}{\mathit{eps}_{2}} + \htmlData{mx=13}{\frac{\htmlData{mx=11}{\htmlData{mx=10}{\mathit{lambda}}^{2}}}{\htmlData{mx=12}{B}}}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{J}}$ ), then

\left(\htmlData{mx=10}{\frac{\htmlData{mx=3}{\htmlData{mx=0}{B} \cdot \htmlData{mx=2}{\htmlData{mx=1}{\mathit{lambda}}^{2}}}}{\htmlData{mx=9}{\htmlData{mx=6}{\htmlData{mx=4}{B} \cdot \htmlData{mx=5}{\mathit{eps}_{2}}} + \htmlData{mx=8}{\htmlData{mx=7}{\mathit{lambda}}^{2}}}}} \mathrel{\htmlData{mx=12}{\leq}} \htmlData{mx=11}{N}\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)
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: w, y, s range over J → ℝ: the statement must hold for every choice. ((w y s : J → ℝ))
x ∈ TVariables: N, lambda, eps2, B range over real numbers: the statement must hold for every choice. ((N lambda eps2 B : ℝ))
∀For all: The statement after the comma holds for every j. (∀ j, 0 ≤ w j)
<Less than: 0 is strictly smaller than B. (0 < B)
∑Summation: Add up w(j) · y(j) · s(j) for every j. (∑ j, w j*y j*s j)
=Equality: ∑ j, w(j) · y(j) · s(j) and lambda are the same. (∑ j, w j*y j*s j = lambda)
RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: 0 is less than or equal to w(j). (0 ≤ w j)
·Multiplication: w(j) times y(j). (w j*y j)
aᵇPower: s(j) raised to the power 2. (s j^2)
+Addition: eps2 plus lambda^2/B. (eps2+lambda^2/B)
a/bDivision: lambda^2 divided by B. In Lean, dividing by 0 gives 0. (lambda^2/B)

theorem affine-information-frontier {J : Type} [Fintype J] (w y s : J → ℝ) (N lambda eps2 B : ℝ) (hw : ∀ j, 0 ≤ w j) (hB : 0 < B) (he : 0 < eps2) (hcal : ∑ j, w j*y j*s j = lambda) (haccess : ∑ j, w j*s j^2 = N) (hsecond : ∑ j, w j*y j^2 ≤ eps2+lambda^2/B) :
    (B*lambda^2/(B*eps2+lambda^2) ≤ N)

Weighted finite Cauchy-Schwarz and the second-moment cap give Blambda^2/(Beps2+lambda^2) <= N. Calibration and access identities are explicit hypotheses; this is NOT a full formalization of the attention lower bound. The actual adaptive access invariant is proved separately.

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: 30 lines of Lean

Finite calibrated access moments imply the sharp probe bound

How it was proved

More proved statements