Provedattentioninformation-complexityadaptive-probes

Finite attention probe frontier for arbitrary linear summaries

For all $\htmlData{mx=2}{\kappa : \htmlData{mx=1}{\htmlData{mx=0}{\operatorname{Type}} \cdot }}$ , $\htmlData{mx=1}{B, m, r \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=1}{F, t, \mathit{epsilon} \in \htmlData{mx=0}{\mathbb{R}}}$ and $\htmlData{mx=20}{S : (\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{B}} \mathrel{\htmlData{mx=9}{\to}} \htmlData{mx=6}{\htmlData{mx=3}{\operatorname{Fin}}\,\htmlData{mx=5}{\htmlData{mx=4}{m} + 1}} \mathrel{\htmlData{mx=8}{\to}} \htmlData{mx=7}{\mathbb{R}}) \mathrel{\htmlData{mx=19}{\to}} \htmlData{mx=18}{\htmlData{mx=10}{_{l}}\,\htmlData{mx=12}{\left[ \htmlData{mx=11}{\mathbb{R}} \right]}\,\htmlData{mx=15}{\htmlData{mx=13}{\operatorname{Fin}}\,\htmlData{mx=14}{r}} \mathrel{\htmlData{mx=17}{\to}} \htmlData{mx=16}{\mathbb{R}}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{B}$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{F}$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{t}$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\mathit{epsilon}}$ and $\htmlData{mx=3}{\htmlData{mx=0}{\operatorname{finrank}}(\htmlData{mx=1}{\mathbb{R}}, \htmlData{mx=2}{\operatorname{range}})} \mathrel{\htmlData{mx=5}{\leq}} \htmlData{mx=4}{m}$ , then

\begin{aligned} & \htmlData{mx=0}{\exists} z : \htmlData{mx=3}{\htmlData{mx=1}{\operatorname{Fin}}\,\htmlData{mx=2}{B}} \mathrel{\htmlData{mx=10}{\to}} \htmlData{mx=7}{\htmlData{mx=4}{\operatorname{Fin}}\,\htmlData{mx=6}{\htmlData{mx=5}{m} + 1}} \mathrel{\htmlData{mx=9}{\to}} \htmlData{mx=8}{\mathbb{R}}, \\ & \quad \htmlData{mx=11}{\exists} i : \htmlData{mx=15}{\htmlData{mx=12}{\operatorname{Fin}}\,\htmlData{mx=14}{\htmlData{mx=13}{m} + 1}}, \\ & \quad \quad (\htmlData{mx=25}{\forall u,\ \htmlData{mx=23}{\htmlData{mx=17}{S}(\htmlData{mx=22}{\htmlData{mx=18}{\operatorname{blockValues}}(\htmlData{mx=19}{F}, \htmlData{mx=20}{z}, \htmlData{mx=21}{u})})} \mathrel{\htmlData{mx=24}{=}} 0}) \\ & \quad \quad \htmlData{mx=16}{\land} (\htmlData{mx=36}{\forall u, b, j,\ \htmlData{mx=33}{\left\lvert \htmlData{mx=32}{\htmlData{mx=26}{\operatorname{blockValues}}(\htmlData{mx=27}{F}, \htmlData{mx=28}{z}, \htmlData{mx=29}{u}, \htmlData{mx=30}{b}, \htmlData{mx=31}{j})} \right\rvert} \mathrel{\htmlData{mx=35}{\leq}} \htmlData{mx=34}{F}}) \\ & \quad \quad \htmlData{mx=16}{\land} \htmlData{mx=37}{\forall} A : \htmlData{mx=40}{\htmlData{mx=38}{\operatorname{Finset}}\,\htmlData{mx=39}{\kappa}},\ w : \htmlData{mx=41}{\kappa} \mathrel{\htmlData{mx=43}{\to}} \htmlData{mx=42}{\mathbb{R}},\ T : \htmlData{mx=44}{\kappa} \mathrel{\htmlData{mx=51}{\to}} \htmlData{mx=50}{\htmlData{mx=45}{\operatorname{RevealTree}}\,\htmlData{mx=48}{\htmlData{mx=46}{\operatorname{Fin}}\,\htmlData{mx=47}{B}}\,\htmlData{mx=49}{\operatorname{univ}}},\ Y : \htmlData{mx=52}{\kappa} \mathrel{\htmlData{mx=60}{\to}} (\htmlData{mx=55}{\htmlData{mx=53}{\operatorname{Fin}}\,\htmlData{mx=54}{B}} \mathrel{\htmlData{mx=57}{\to}} \htmlData{mx=56}{\mathbb{R}}) \mathrel{\htmlData{mx=59}{\to}} \htmlData{mx=58}{\mathbb{R}}, \\ & \quad \quad \quad (\htmlData{mx=67}{\forall s \in \htmlData{mx=66}{A},\ 0 \mathrel{\htmlData{mx=65}{\leq}} \htmlData{mx=64}{\htmlData{mx=62}{w}(\htmlData{mx=63}{s})}}) \\ & \quad \quad \quad \htmlData{mx=61}{\implies} \left(\htmlData{mx=72}{\sum_{s \in \htmlData{mx=68}{A}} \htmlData{mx=71}{\htmlData{mx=69}{w}(\htmlData{mx=70}{s})}}\right) \mathrel{\htmlData{mx=73}{=}} 1 \\ & \quad \quad \quad \htmlData{mx=61}{\implies} \left(\right. \htmlData{mx=74}{\forall} u \in \htmlData{mx=79}{\operatorname{powerset}\left(\htmlData{mx=78}{\htmlData{mx=77}{\operatorname{univ}}}\right)}, \\ & \quad \quad \quad \quad \left(\htmlData{mx=95}{\sum_{s \in \htmlData{mx=81}{A}} \htmlData{mx=94}{\htmlData{mx=84}{\htmlData{mx=82}{w}(\htmlData{mx=83}{s})} \cdot \htmlData{mx=93}{\htmlData{mx=85}{Y}(\htmlData{mx=86}{s}, \htmlData{mx=92}{\htmlData{mx=87}{\operatorname{execute}}(\htmlData{mx=90}{\htmlData{mx=88}{T}(\htmlData{mx=89}{s})}, \htmlData{mx=91}{u})})}}}\right) \\ & \quad \quad \quad \quad \quad \htmlData{mx=80}{=} \htmlData{mx=104}{\htmlData{mx=96}{\operatorname{blockAttention}}(\htmlData{mx=97}{t}, \htmlData{mx=98}{i}, \htmlData{mx=103}{\htmlData{mx=99}{\operatorname{blockValues}}(\htmlData{mx=100}{F}, \htmlData{mx=101}{z}, \htmlData{mx=102}{u})})} \left.\right) \\ & \quad \quad \quad \htmlData{mx=61}{\implies} \left(\right. \htmlData{mx=105}{\forall} u \in \htmlData{mx=110}{\operatorname{powerset}\left(\htmlData{mx=109}{\htmlData{mx=108}{\operatorname{univ}}}\right)}, \\ & \quad \quad \quad \quad \left(\htmlData{mx=163}{\sum_{s \in \htmlData{mx=138}{A}} \htmlData{mx=162}{\htmlData{mx=141}{\htmlData{mx=139}{w}(\htmlData{mx=140}{s})} \cdot \htmlData{mx=161}{(\htmlData{mx=160}{\htmlData{mx=150}{\htmlData{mx=142}{Y}(\htmlData{mx=143}{s}, \htmlData{mx=149}{\htmlData{mx=144}{\operatorname{execute}}(\htmlData{mx=147}{\htmlData{mx=145}{T}(\htmlData{mx=146}{s})}, \htmlData{mx=148}{u})})} - \htmlData{mx=159}{\htmlData{mx=151}{\operatorname{blockAttention}}(\htmlData{mx=152}{t}, \htmlData{mx=153}{i}, \htmlData{mx=158}{\htmlData{mx=154}{\operatorname{blockValues}}(\htmlData{mx=155}{F}, \htmlData{mx=156}{z}, \htmlData{mx=157}{u})})}})^{2}}}}\right) \\ & \quad \quad \quad \quad \quad \htmlData{mx=111}{\leq} \htmlData{mx=165}{\htmlData{mx=164}{\mathit{epsilon}}^{2}} \left.\right) \\ & \quad \quad \quad \htmlData{mx=61}{\implies} \htmlData{mx=189}{\frac{\htmlData{mx=174}{\htmlData{mx=168}{\htmlData{mx=167}{F}^{2}} \cdot \htmlData{mx=173}{(\htmlData{mx=172}{\htmlData{mx=169}{\operatorname{gridAmplitude}}(\htmlData{mx=170}{m}, \htmlData{mx=171}{t})})^{2}}}}{\htmlData{mx=188}{\htmlData{mx=179}{\htmlData{mx=178}{\htmlData{mx=177}{\htmlData{mx=176}{\htmlData{mx=175}{m} + 1}}}^{2}} \cdot \left(\htmlData{mx=187}{\htmlData{mx=181}{\htmlData{mx=180}{\mathit{epsilon}}^{2}} + \htmlData{mx=186}{\frac{\htmlData{mx=183}{\htmlData{mx=182}{F}^{2}}}{\htmlData{mx=185}{\htmlData{mx=184}{B}}}}}\right)}}} \\ & \quad \quad \quad \quad \htmlData{mx=166}{\leq} \htmlData{mx=200}{\sum_{s \in \htmlData{mx=190}{A}} \htmlData{mx=199}{\htmlData{mx=193}{\htmlData{mx=191}{w}(\htmlData{mx=192}{s})} \cdot \htmlData{mx=198}{\htmlData{mx=194}{\operatorname{revealCount}}(\htmlData{mx=197}{\htmlData{mx=195}{T}(\htmlData{mx=196}{s})})}}} \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)
·Multiplication: Type times . (Type*)
NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
x ∈ TVariables: B, m, r range over natural numbers: the statement must hold for every choice. ((B m r : ℕ))
<Less than: 0 is strictly smaller than B. (0<B)
RReal numbers: The real numbers: every point on the number line. (ℝ)
finrank: Module.finrank: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Module.finrank)
≤At most: finrank(ℝ, range) is less than or equal to m. (Module.finrank ℝ S.range≤m)
Fin: Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fin)
f(x)Function application: Fin applied to B. Lean writes f x; papers write f(x). (Fin B)
⟹Implies: If Fin(m + 1), then ℝ. (Between types, A → B is the type of functions from A to B.) (Fin (m+1) → ℝ)
+Addition: m plus 1. (m+1)
range: S.range: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (S.range)
[a, b]List: The list of ℝ, in order. ([ℝ])
∃There exists: At least one i makes the statement after the comma true. (∃ i : Fin (m+1), (∀ u, S (blockValues F…)
∀For all: The statement after the comma holds for every u. (∀ u, S (blockValues F z u)=0)
=Equality: S(blockValues(F, z, u)) and 0 are the same. (S (blockValues F z u)=0)
blockValues: blockValues: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (blockValues)
∧And: Both hold: ∀ u, b, j, |blockValues(F, z, u, b, j)| ≤ F, and ∀ A, w, T, Y, (∀ s, 0 ≤ w(s)) → ((∑ s, w(s)) = 1 → ((∀ u, …. ((∀ u b j, |blockValues F z u b j|≤F) ∧ …)
|x|Absolute value: The size of blockValues(F, z, u, b, j) without its sign. (|blockValues F z u b j|)
Finset: Finset: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Finset)
RevealTree: RevealTree: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (RevealTree)
∑Summation: Add up w(s) for each s in A. (∑ s ∈ A, w s)
(x : T)Type ascription: univ read as a Finset(Fin(B)). Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((Finset.univ : Finset (Fin B)))
e.fpowerset: powerset of univ: Lean's dot notation e.powerset means powerset applied to e. ((Finset.univ : Finset (Fin B)).powerset)
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)
execute: execute: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (execute)
blockAttention: blockAttention: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (blockAttention)
aᵇPower: Y(s, execute(T(s), u)) − blockAttention(t, i, blockValues(… raised to the power 2. ((Y s (execute (T s) u)-blockAttention t…)
-Subtraction: Y(s, execute(T(s), u)) minus blockAttention(t, i, blockValues(F, z, u)). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (Y s (execute (T s) u)-blockAttention t …)
gridAmplitude: gridAmplitude: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (gridAmplitude)
(x : T)As real numbers: m + 1 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (((m+1 : ℕ) : ℝ))
(x : T)As natural numbers: m + 1 read as an element of natural numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((m+1 : ℕ))
a/bDivision: F^2 divided by B. In Lean, dividing by 0 gives 0. (F^2/(B : ℝ))
revealCount: revealCount: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (revealCount)

theorem attention-frontier-arbitrary-summary-softmax-probes {κ : Type*}
    (B m r : ℕ) (hB : 0<B) (F t epsilon : ℝ)
    (hF : 0<F) (ht : 0<t) (he : 0<epsilon)
    (S : (Fin B → Fin (m+1) → ℝ) →ₗ[ℝ] (Fin r → ℝ))
    (hrank : Module.finrank ℝ S.range≤m) :
    ∃ z : Fin B → Fin (m+1) → ℝ, ∃ i : Fin (m+1),
      (∀ u, S (blockValues F z u)=0) ∧
      (∀ u b j, |blockValues F z u b j|≤F) ∧
      ∀ (A : Finset κ) (w : κ → ℝ)
        (T : κ → RevealTree (Fin B) Finset.univ)
        (Y : κ → (Fin B → ℝ) → ℝ),
        (∀ s ∈ A, 0≤w s) → (∑ s ∈ A, w s)=1 →
        (∀ u ∈ (Finset.univ : Finset (Fin B)).powerset,
          (∑ s ∈ A, w s*Y s (execute (T s) u))=blockAttention t i (blockValues F z u)) →
        (∀ u ∈ (Finset.univ : Finset (Fin B)).powerset,
          (∑ s ∈ A, w s*(Y s (execute (T s) u)-blockAttention t i (blockValues F z u))^2)≤epsilon^2) →
        F^2*(gridAmplitude m t)^2 /
          (((m+1 : ℕ) : ℝ)^2*(epsilon^2+F^2/(B : ℝ))) ≤
          ∑ s ∈ A, w s*revealCount (T s)

Actual global rank-m summaries, original one-dimensional exponential-softmax grid, constructed indistinguishable bounded value families, and adaptive finite independent-seed execution. This theorem is a complete finite lower composition, not an arbitrary-RAM lower bound.

How it was proved

Proved: 8 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 attention probe frontier for arbitrary linear summaries

How it was proved

More proved statements