Provedattentionformal-verificationfinite-sampler

Restricted original-coordinate attention frontier

For all $\htmlData{mx=1}{B \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=2}{\Omega : \htmlData{mx=1}{\htmlData{mx=0}{\operatorname{Type}} \cdot }}$ , $\htmlData{mx=3}{\nu \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Measure}}\,\htmlData{mx=1}{\Omega}}}$ , $\htmlData{mx=8}{p : \htmlData{mx=0}{\Omega} \mathrel{\htmlData{mx=7}{\to}} \htmlData{mx=6}{\htmlData{mx=1}{\operatorname{Policy}}\,\htmlData{mx=4}{\htmlData{mx=2}{\operatorname{Fin}}\,\htmlData{mx=3}{B}}\,\htmlData{mx=5}{\operatorname{univ}}}}$ , $\htmlData{mx=1}{F, z, \varepsilon \in \htmlData{mx=0}{\mathbb{R}}}$ , $\htmlData{mx=18}{\mathit{hY} : \htmlData{mx=17}{\forall \sigma,\ \htmlData{mx=16}{\htmlData{mx=0}{\operatorname{Integrable}}\,\htmlData{mx=14}{\omega \mapsto \htmlData{mx=13}{\operatorname{answer}\left(\htmlData{mx=12}{\htmlData{mx=7}{\operatorname{run}}(\htmlData{mx=10}{\htmlData{mx=8}{p}(\htmlData{mx=9}{\omega})}, \htmlData{mx=11}{\sigma})}\right)}}\,\htmlData{mx=15}{\nu}}}}$ , $\htmlData{mx=19}{\mathit{hYY} : \htmlData{mx=18}{\forall \sigma,\ \htmlData{mx=17}{\htmlData{mx=0}{\operatorname{Integrable}}\,\htmlData{mx=15}{\omega \mapsto \htmlData{mx=14}{\htmlData{mx=13}{\operatorname{answer}\left(\htmlData{mx=12}{\htmlData{mx=7}{\operatorname{run}}(\htmlData{mx=10}{\htmlData{mx=8}{p}(\htmlData{mx=9}{\omega})}, \htmlData{mx=11}{\sigma})}\right)}^{2}}}\,\htmlData{mx=16}{\nu}}}}$ , $\htmlData{mx=32}{\mathit{hYS} : \htmlData{mx=31}{\forall \sigma,\ \htmlData{mx=30}{\htmlData{mx=0}{\operatorname{Integrable}}\,\htmlData{mx=28}{\omega \mapsto \htmlData{mx=27}{\htmlData{mx=13}{\operatorname{answer}\left(\htmlData{mx=12}{\htmlData{mx=7}{\operatorname{run}}(\htmlData{mx=10}{\htmlData{mx=8}{p}(\htmlData{mx=9}{\omega})}, \htmlData{mx=11}{\sigma})}\right)} \cdot \htmlData{mx=26}{\operatorname{observed}\left(\htmlData{mx=25}{\htmlData{mx=20}{\operatorname{run}}(\htmlData{mx=23}{\htmlData{mx=21}{p}(\htmlData{mx=22}{\omega})}, \htmlData{mx=24}{\sigma})}\right)}}}\,\htmlData{mx=29}{\nu}}}}$ , $\htmlData{mx=19}{\mathit{hSS} : \htmlData{mx=18}{\forall \sigma,\ \htmlData{mx=17}{\htmlData{mx=0}{\operatorname{Integrable}}\,\htmlData{mx=15}{\omega \mapsto \htmlData{mx=14}{\htmlData{mx=13}{\operatorname{observed}\left(\htmlData{mx=12}{\htmlData{mx=7}{\operatorname{run}}(\htmlData{mx=10}{\htmlData{mx=8}{p}(\htmlData{mx=9}{\omega})}, \htmlData{mx=11}{\sigma})}\right)}^{2}}}\,\htmlData{mx=16}{\nu}}}}$ , $\htmlData{mx=19}{\mathit{hN} : \htmlData{mx=18}{\forall \sigma,\ \htmlData{mx=17}{\htmlData{mx=0}{\operatorname{Integrable}}\,\htmlData{mx=15}{\omega \mapsto \htmlData{mx=14}{\htmlData{mx=13}{\operatorname{probes}\left(\htmlData{mx=12}{\htmlData{mx=7}{\operatorname{run}}(\htmlData{mx=10}{\htmlData{mx=8}{p}(\htmlData{mx=9}{\omega})}, \htmlData{mx=11}{\sigma})}\right)}}}\,\htmlData{mx=16}{\nu}}}}$ , $\htmlData{mx=16}{\mathit{hunbiased} \in \htmlData{mx=15}{\htmlData{mx=14}{\forall \sigma,\ \left(\htmlData{mx=13}{\int \htmlData{mx=12}{\operatorname{answer}\left(\htmlData{mx=11}{\htmlData{mx=6}{\operatorname{run}}(\htmlData{mx=9}{\htmlData{mx=7}{p}(\htmlData{mx=8}{\omega})}, \htmlData{mx=10}{\sigma})}\right)} \, d\omega}\right)}\,\mathtt{\text{∂}{\nu})=familyOutput\ F\ z\ {\sigma}}}}$ and $\htmlData{mx=23}{\mathit{herror} \in \htmlData{mx=22}{\htmlData{mx=21}{\forall \sigma,\ \left(\htmlData{mx=20}{\int \htmlData{mx=19}{(\htmlData{mx=18}{\htmlData{mx=12}{\operatorname{answer}\left(\htmlData{mx=11}{\htmlData{mx=6}{\operatorname{run}}(\htmlData{mx=9}{\htmlData{mx=7}{p}(\htmlData{mx=8}{\omega})}, \htmlData{mx=10}{\sigma})}\right)} - \htmlData{mx=17}{\htmlData{mx=13}{\operatorname{familyOutput}}(\htmlData{mx=14}{F}, \htmlData{mx=15}{z}, \htmlData{mx=16}{\sigma})}})^{2}} \, d\omega}\right)}\,\mathtt{\text{∂}{\nu})\leq {\varepsilon}\^2}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{B}$ and $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\varepsilon}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{MeasurableSpace}}\,\htmlData{mx=1}{\Omega}}$ and $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{IsProbabilityMeasure}}\,\htmlData{mx=1}{\nu}}$ ), then

\htmlData{mx=26}{\left(\htmlData{mx=25}{\exists \sigma,\ \htmlData{mx=8}{\frac{\htmlData{mx=7}{\min(\htmlData{mx=1}{\htmlData{mx=0}{B}}, \htmlData{mx=6}{\htmlData{mx=2}{\operatorname{blockKappa}}(\htmlData{mx=3}{F}, \htmlData{mx=4}{z}, \htmlData{mx=5}{\varepsilon})})}}{2}} \mathrel{\htmlData{mx=24}{\leq}} \htmlData{mx=23}{\int \htmlData{mx=22}{\htmlData{mx=21}{\operatorname{probes}\left(\htmlData{mx=20}{\htmlData{mx=15}{\operatorname{run}}(\htmlData{mx=18}{\htmlData{mx=16}{p}(\htmlData{mx=17}{\omega})}, \htmlData{mx=19}{\sigma})}\right)}} \, d\omega}}\right)(\mathtt{\text{∂}{\nu}\ \ \ )})}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
<Less than: 0 is strictly smaller than B. (0<B)
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)
⟹Implies: If Ω, then Policy(Fin(B), univ). (Between types, A → B is the type of functions from A to B.) (Ω → Policy (Fin B) Finset.univ)
RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: F, z, ε range over real numbers: the statement must hold for every choice. ((F z ε : ℝ))
∀For all: The statement after the comma holds for every σ. (∀ σ,Integrable (fun ω => (run (p ω) σ).…)
Policy: Policy: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Policy)
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)
∫Integral: The integral of answer(run(p(ω), σ)) over ω: the signed area under it. (∫ ω,(run (p ω) σ).answer)
∃There exists: At least one σ makes the statement after the comma true. (∃ σ,min (B : ℝ) (blockKappa F z ε)/2≤∫ …)
-Subtraction: answer(run(p(ω), σ)) minus familyOutput(F, z, σ). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. ((run (p ω) σ).answer-familyOutput F z σ)
minMinimum: The smaller of B and blockKappa(F, z, ε). (min (B : ℝ) (blockKappa F z ε))
a/bDivision: min(B, blockKappa(F, z, ε)) divided by 2. In Lean, dividing by 0 gives 0. (min (B : ℝ) (blockKappa F z ε)/2)
≤At most: min(B, blockKappa(F, z, ε))/2 is less than or equal to ∫ ω, probes(run(p(ω), σ)). (min (B : ℝ) (blockKappa F z ε)/2≤∫ ω,((…)
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)
x ↦ f(x)Function (λ-abstraction): The function sending ω to answer(run(p(ω), σ)). Lean writes fun x => …; papers write x ↦ …. (fun ω => (run (p ω) σ).answer)
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)
blockKappa: blockKappa: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (blockKappa)
e.fanswer: answer of run(p(ω), σ): Lean's dot notation e.answer means answer applied to e. ((run (p ω) σ).answer)
aᵇPower: answer(run(p(ω), σ)) raised to the power 2. ((run (p ω) σ).answer^2)
(x : T)As real numbers: probes(run(p(ω), σ)) read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (((run (p ω) σ).probes : ℝ))
run: run: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (run)
e.fprobes: probes of run(p(ω), σ): Lean's dot notation e.probes means probes applied to e. ((run (p ω) σ).probes)
familyOutput: familyOutput: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (familyOutput)
e.fobserved: observed of run(p(ω), σ): Lean's dot notation e.observed means observed applied to e. ((run (p ω) σ).observed)

theorem attention-e2e-restricted-probe-lower (B : ℕ) (hB : 0<B) {Ω : Type*} [MeasurableSpace Ω]
    (ν : Measure Ω) [IsProbabilityMeasure ν] (p : Ω → Policy (Fin B) Finset.univ)
    (F z ε : ℝ) (hε : 0<ε)
    (hY : ∀ σ,Integrable (fun ω => (run (p ω) σ).answer) ν)
    (hYY : ∀ σ,Integrable (fun ω => (run (p ω) σ).answer^2) ν)
    (hYS : ∀ σ,Integrable (fun ω => (run (p ω) σ).answer*(run (p ω) σ).observed) ν)
    (hSS : ∀ σ,Integrable (fun ω => (run (p ω) σ).observed^2) ν)
    (hN : ∀ σ,Integrable (fun ω => ((run (p ω) σ).probes : ℝ)) ν)
    (hunbiased : ∀ σ,(∫ ω,(run (p ω) σ).answer ∂ν)=familyOutput F z σ)
    (herror : ∀ σ,(∫ ω,((run (p ω) σ).answer-familyOutput F z σ)^2 ∂ν)≤ε^2) :
    (
    ∃ σ,min (B : ℝ) (blockKappa F z ε)/2≤∫ ω,((run (p ω) σ).probes : ℝ) ∂ν
  )

Fixed hard member for finite nonrepeating original-coordinate policies after prescribed affine information, arbitrary independent seed with explicit integrability and pointwise mean/MSE contracts. This is not an unrestricted preprocessing lower bound.

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

Restricted original-coordinate attention frontier

How it was proved

More proved statements