Provedproposal-principleattentionunifiedcrux
The oracle is an attention call: on key subset S with indicator values 1[j ∈ T] (T ⊆ S), the exact attention output equals the conditional mass Σ_T e^s / Σ_S e^s
For all , and , if , then
What the notation means · or point at any symbol
- NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - 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 n. Lean writes f x; papers write f(x). (
Fin n) - ⟹Implies
- If Fin(n), then ℝ. (Between types, A → B is the type of functions from A to B.) (
Fin n → ℝ) - 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) - x ∈ TVariables
- S, T range over Finset (Fin n): the statement must hold for every choice. (
(S T : Finset (Fin n))) - ⊆Subset
- Every element of T is also in S. (
T ⊆ S) - a/bDivision
- ∑ j, exp(s(j)) · 1 if j ∈ T, else 0 divided by ∑ j, exp(s(j)). In Lean, dividing by 0 gives 0. (
(∑ j ∈ S, Real.exp (s j) * (if j ∈ T th…) - =Equality
- (∑ j, exp(s(j)) · 1 if j ∈ T, else 0)/(∑ j, exp(s(j))) and (∑ j, exp(s(j)))/(∑ j, exp(s(j))) are the same. (
(∑ j ∈ S, Real.exp (s j) * (if j ∈ T th…) - ∑Summation
- Add up exp(s(j)) · 1 if j ∈ T, else 0 for each j in S. (
∑ j ∈ S, Real.exp (s j) * (if j ∈ T the…) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - eˣExponential function
- e raised to the power s(j), where e ≈ 2.718. (
Real.exp (s j)) - ·Multiplication
- exp(s(j)) times 1 if j ∈ T, else 0. (
Real.exp (s j) * (if j ∈ T then (1 : ℝ)…) - { a if c; b otherwiseCases (if … then … else)
- 1 when j ∈ T, and 0 otherwise. (
if j ∈ T then (1 : ℝ) else 0) - ∈Element of
- j is a member of T. (
j ∈ T) - (x : T)As real numbers
- 1 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(1 : ℝ))
theorem cv-indicator-output-is-conditional-mass {n : ℕ} (s : Fin n → ℝ) (S T : Finset (Fin n)) (hTS : T ⊆ S) :
(∑ j ∈ S, Real.exp (s j) * (if j ∈ T then (1 : ℝ) else 0)) / (∑ j ∈ S, Real.exp (s j)) = (∑ j ∈ T, Real.exp (s j)) / (∑ j ∈ S, Real.exp (s j))Closes the last modelling remark of the Conversion Theorem: an attention algorithm that is additively ε-accurate on arbitrary key subsets, queried with indicator values for a node's child, returns exactly the branch-mass estimate phat that cv-conversion-theorem consumes. Part of 'The Proposal Principle: attention complexity is proposal complexity'.
How it was proved
- Proved
- 4 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
- 21 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.