Proved

General-source attention frontier on a fixed hard input

For all $\htmlData{mx=2}{\alpha : \htmlData{mx=1}{\htmlData{mx=0}{\operatorname{Type}} \cdot }}$ , $\htmlData{mx=3}{\mu \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Measure}}\,\htmlData{mx=1}{\alpha}}}$ , $\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}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{MeasurableSpace}}\,\htmlData{mx=1}{\alpha}}$ and $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{IsProbabilityMeasure}}\,\htmlData{mx=1}{\mu}}$ ), then

\htmlData{mx=132}{\left(\htmlData{mx=131}{\exists z : \htmlData{mx=123}{\htmlData{mx=121}{\operatorname{Fin}}\,\htmlData{mx=122}{B}} \mathrel{\htmlData{mx=130}{\to}} \htmlData{mx=127}{\htmlData{mx=124}{\operatorname{Fin}}\,\htmlData{mx=126}{\htmlData{mx=125}{m} + 1}} \mathrel{\htmlData{mx=129}{\to}} \htmlData{mx=128}{\mathbb{R}},\ \htmlData{mx=120}{\exists i : \htmlData{mx=119}{\htmlData{mx=116}{\operatorname{Fin}}\,\htmlData{mx=118}{\htmlData{mx=117}{m} + 1}},\ (\htmlData{mx=8}{\forall u,\ \htmlData{mx=6}{\htmlData{mx=0}{S}(\htmlData{mx=5}{\htmlData{mx=1}{\operatorname{blockValues}}(\htmlData{mx=2}{F}, \htmlData{mx=3}{z}, \htmlData{mx=4}{u})})} \mathrel{\htmlData{mx=7}{=}} 0}) \mathbin{\htmlData{mx=115}{\land}} (\htmlData{mx=19}{\forall u, b, j,\ \htmlData{mx=16}{\left\lvert \htmlData{mx=15}{\htmlData{mx=9}{\operatorname{blockValues}}(\htmlData{mx=10}{F}, \htmlData{mx=11}{z}, \htmlData{mx=12}{u}, \htmlData{mx=13}{b}, \htmlData{mx=14}{j})} \right\rvert} \mathrel{\htmlData{mx=18}{\leq}} \htmlData{mx=17}{F}}) \mathbin{\htmlData{mx=114}{\land}} \htmlData{mx=113}{\forall T : \htmlData{mx=96}{\alpha} \mathrel{\htmlData{mx=103}{\to}} \htmlData{mx=102}{\htmlData{mx=97}{\operatorname{RevealTree}}\,\htmlData{mx=100}{\htmlData{mx=98}{\operatorname{Fin}}\,\htmlData{mx=99}{B}}\,\htmlData{mx=101}{\operatorname{univ}}},\ Y : \htmlData{mx=104}{\alpha} \mathrel{\htmlData{mx=112}{\to}} (\htmlData{mx=107}{\htmlData{mx=105}{\operatorname{Fin}}\,\htmlData{mx=106}{B}} \mathrel{\htmlData{mx=109}{\to}} \htmlData{mx=108}{\mathbb{R}}) \mathrel{\htmlData{mx=111}{\to}} \htmlData{mx=110}{\mathbb{R}},\ (\htmlData{mx=38}{\forall u \in \htmlData{mx=37}{\operatorname{powerset}\left(\htmlData{mx=36}{\htmlData{mx=35}{\operatorname{univ}}}\right)},\ \htmlData{mx=32}{\htmlData{mx=20}{\operatorname{Integrable}}\,\htmlData{mx=30}{s \mapsto \htmlData{mx=29}{\htmlData{mx=21}{Y}(\htmlData{mx=22}{s}, \htmlData{mx=28}{\htmlData{mx=23}{\operatorname{execute}}(\htmlData{mx=26}{\htmlData{mx=24}{T}(\htmlData{mx=25}{s})}, \htmlData{mx=27}{u})})}}\,\htmlData{mx=31}{\mu}}}) \mathrel{\htmlData{mx=95}{\implies}} (\htmlData{mx=58}{\forall u \in \htmlData{mx=57}{\operatorname{powerset}\left(\htmlData{mx=56}{\htmlData{mx=55}{\operatorname{univ}}}\right)},\ \htmlData{mx=52}{\htmlData{mx=39}{\operatorname{Integrable}}\,\htmlData{mx=50}{s \mapsto \htmlData{mx=49}{(\htmlData{mx=48}{\htmlData{mx=40}{Y}(\htmlData{mx=41}{s}, \htmlData{mx=47}{\htmlData{mx=42}{\operatorname{execute}}(\htmlData{mx=45}{\htmlData{mx=43}{T}(\htmlData{mx=44}{s})}, \htmlData{mx=46}{u})})})^{2}}}\,\htmlData{mx=51}{\mu}}}) \mathrel{\htmlData{mx=94}{\implies}} (\htmlData{mx=76}{\forall u \in \htmlData{mx=75}{\operatorname{powerset}\left(\htmlData{mx=74}{\htmlData{mx=73}{\operatorname{univ}}}\right)},\ \htmlData{mx=70}{\forall j,\ \htmlData{mx=69}{\htmlData{mx=59}{\operatorname{AEStronglyMeasurable}}\,\htmlData{mx=67}{s \mapsto \htmlData{mx=66}{\htmlData{mx=60}{\operatorname{execute}}(\htmlData{mx=63}{\htmlData{mx=61}{T}(\htmlData{mx=62}{s})}, \htmlData{mx=64}{u}, \htmlData{mx=65}{j})}}\,\htmlData{mx=68}{\mu}}}}) \mathrel{\htmlData{mx=93}{\implies}} \left(\htmlData{mx=92}{\forall u \in \htmlData{mx=91}{\operatorname{powerset}\left(\htmlData{mx=90}{\htmlData{mx=89}{\operatorname{univ}}}\right)},\ \left(\htmlData{mx=86}{\int \htmlData{mx=85}{\htmlData{mx=77}{Y}(\htmlData{mx=78}{s}, \htmlData{mx=84}{\htmlData{mx=79}{\operatorname{execute}}(\htmlData{mx=82}{\htmlData{mx=80}{T}(\htmlData{mx=81}{s})}, \htmlData{mx=83}{u})})} \, ds}\right)}\right)}}}\right)(\mathtt{\text{∂}{\mu})=blockAttention\ t\ i\ (blockValues\ F\ z\ u))\ \to \ \ \ \ \ \ \ \ \ (\forall \ u\ \in \ (Finset.univ\ :\ Finset\ (Fin\ B)).powerset,\ \ \ \ \ \ \ \ \ \ \ (\text{∫}\ s,(Y\ s\ (execute\ (T\ s)\ u)-blockAttention\ t\ i\ (blockValues\ F\ z\ u))\^2\ \text{∂}{\mu})\leq epsilon\^2)\ \to \ \ \ \ \ \ \ \ \ \exists \ u\ \in \ (Finset.univ\ :\ Finset\ (Fin\ B)).powerset,\ \ \ \ \ \ \ \ \ F\^2*(gridAmplitude\ m\ t)\^2\ /\ \ \ \ \ \ \ \ \ \ \ (((m+1\ :\ \text{ℕ})\ :\ \text{ℝ})\^2*(epsilon\^2+F\^2/(B\ :\ \text{ℝ})))\ \leq \ \ \ \ \ \ \ \ \ \ \ \text{∫}\ s,originalReadCount\ Finset.univ\ (execute\ (T\ s)\ u)\ \text{∂}{\mu})})}

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*)
MeasurableSpace: MeasurableSpace: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (MeasurableSpace)
f(x)Function application: MeasurableSpace applied to α. Lean writes f x; papers write f(x). (MeasurableSpace α)
Measure: Measure: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Measure)
IsProbabilityMeasure: IsProbabilityMeasure: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (IsProbabilityMeasure)
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)
⟹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 ∀ T, Y, (∀ u, Integrable(s ↦ Y(s, execute(T(s), 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|)
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)
(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)
Integrable: Integrable: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Integrable)
x ↦ f(x)Function (λ-abstraction): The function sending s to Y(s, execute(T(s), u)). Lean writes fun x => …; papers write x ↦ …. (fun s => Y s (execute (T s) u))
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)
aᵇPower: Y(s, execute(T(s), u)) raised to the power 2. ((Y s (execute (T s) u))^2)
AEStronglyMeasurable: AEStronglyMeasurable: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (AEStronglyMeasurable)
∫Integral: The integral of Y(s, execute(T(s), u)) over s: the signed area under it. (∫ s,Y s (execute (T s) u))

theorem attention-precision-general-source-fixed-input {α : Type*} [MeasurableSpace α]
    (μ : Measure α) [IsProbabilityMeasure μ]
    (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) ∧
      ∀ (T : α → RevealTree (Fin B) Finset.univ)
        (Y : α → (Fin B → ℝ) → ℝ),
        (∀ u ∈ (Finset.univ : Finset (Fin B)).powerset,
          Integrable (fun s => Y s (execute (T s) u)) μ) →
        (∀ u ∈ (Finset.univ : Finset (Fin B)).powerset,
          Integrable (fun s => (Y s (execute (T s) u))^2) μ) →
        (∀ u ∈ (Finset.univ : Finset (Fin B)).powerset,∀ j,
          AEStronglyMeasurable (fun s => execute (T s) u j) μ) →
        (∀ u ∈ (Finset.univ : Finset (Fin B)).powerset,
          (∫ s,Y s (execute (T s) u) ∂μ)=blockAttention t i (blockValues F z u)) →
        (∀ u ∈ (Finset.univ : Finset (Fin B)).powerset,
          (∫ s,(Y s (execute (T s) u)-blockAttention t i (blockValues F z u))^2 ∂μ)≤epsilon^2) →
        ∃ u ∈ (Finset.univ : Finset (Fin B)).powerset,
        F^2*(gridAmplitude m t)^2 /
          (((m+1 : ℕ) : ℝ)^2*(epsilon^2+F^2/(B : ℝ))) ≤
          ∫ s,originalReadCount Finset.univ (execute (T s) u) ∂μ)

Actual global rank-m linear summaries, original exponential softmax, arbitrary independent probability sources, measurable finite adaptive revelation and L1/L2 outputs. Constructs a fixed hard input; fresh block-sign probes, not arbitrary RAM runtime.

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

General-source attention frontier on a fixed hard input

How it was proved

More proved statements