Provedunbiased-attentionchi-squareheadline-theoremreview-response
Sharp uniform-proposal cost: score range ≤ R ⇒ n·Σπ_j² ≤ cosh²(R/2) = (1+e^R)²/(4e^R) ≤ e^R
For all , and , if and , then
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 n. (
0 < n) - 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 → ℝ) - ∀For all
- The statement after the comma holds for every i, j. (
∀ i j, s i - s j ≤ R) - (x : T)As real numbers
- n read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(n : ℝ)) - ·Multiplication
- n times ∑ j, (exp(s(j))/(∑ k, exp(s(k))))^2. (
(n : ℝ) * ∑ j, (Real.exp (s j) / ∑ k, R…) - -Subtraction
- s(i) minus s(j). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
s i - s j) - ≤At most
- s(i) − s(j) is less than or equal to R. (
s i - s j ≤ R) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - aᵇPower
- exp(s(j))/(∑ k, exp(s(k))) raised to the power 2. (
(Real.exp (s j) / ∑ k, Real.exp (s k)) …) - eˣExponential function
- e raised to the power s(j), where e ≈ 2.718. (
Real.exp (s j)) - a/bDivision
- exp(s(j)) divided by ∑ k, exp(s(k)). In Lean, dividing by 0 gives 0. (
Real.exp (s j) / ∑ k, Real.exp (s k)) - ∑Summation
- Add up exp(s(k)) for every k. (
∑ k, Real.exp (s k)) - coshHyperbolic cosine
- (eˣ + e⁻ˣ)/2 at R/2. (
Real.cosh (R / 2)) - =Equality
- cosh(R/2)^2 and (1 + exp(R))^2/(4 · exp(R)) are the same. (
Real.cosh (R / 2) ^ 2 = (1 + Real.exp R…) - ∧And
- Both hold: cosh(R/2)^2 = (1 + exp(R))^2/(4 · exp(R)), and cosh(R/2)^2 ≤ exp(R). (
Real.cosh (R / 2) ^ 2 = (1 + Real.exp R…) - +Addition
- 1 plus exp(R). (
1 + Real.exp R)
theorem ua-uniform-proposal-cosh-bound {n : ℕ} (hn : 0 < n) (s : Fin n → ℝ) (R : ℝ) (hR : ∀ i j, s i - s j ≤ R) :
(n : ℝ) * ∑ j, (Real.exp (s j) / ∑ k, Real.exp (s k)) ^ 2 ≤ Real.cosh (R / 2) ^ 2 ∧ Real.cosh (R / 2) ^ 2 = (1 + Real.exp R) ^ 2 / (4 * Real.exp R) ∧ Real.cosh (R / 2) ^ 2 ≤ Real.exp RSharpens ua-uniform-proposal-chi-square-bound (e^R) by a factor of about 4 at large R and shows second-order degradation near R = 0 (cosh²(R/2) = 1 + R²/4 + O(R⁴)). Proof: Kantorovich range bound on x_j = e^{s_j} ∈ [a, a e^R] with uniform weights. Raised in an external review, 2026-10-05.
How it was proved
- Proved
- 5 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
- 61 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.