Provedattentionresidual-seriesexternal-review-4
Bucket total mass alone does not imply the uniform-share bound
What the notation means · or point at any symbol
- ∑Summation
- Add up 1/2 if j = 0, else 1/14 for every j in Fin(8). (
∑ j : Fin 8, (if j=0 then (1:ℝ)/2 else …) - 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 8. Lean writes f x; papers write f(x). (
Fin 8) - { a if c; b otherwiseCases (if … then … else)
- 1/2 when j = 0, and 1/14 otherwise. (
if j=0 then (1:ℝ)/2 else 1/14) - =Equality
- j and 0 are the same. (
j=0) - (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:ℝ)) - a/bDivision
- 1 divided by 2. In Lean, dividing by 0 gives 0. (
(1:ℝ)/2) - ∧And
- Both hold: (∑ j, 1/2 if j = 0, else 1/14^2/1/2 if j = 0, else 1/14) = 1, and 1 < (1/2)^2 · 8/1. (
(∑ j : Fin 8, (if j=0 then (1:ℝ)/2 else…) - aᵇPower
- 1/2 if j = 0, else 1/14 raised to the power 2. (
(if j=0 then (1:ℝ)/2 else 1/14)^2) - <Less than
- 1 is strictly smaller than (1/2)^2 · 8/1. (
(1:ℝ)<(1/2)^2*8/1) - ·Multiplication
- (1/2)^2 times 8. (
(1/2)^2*8)
theorem bucket-total-mass-insufficient :
(∑ j : Fin 8, (if j=0 then (1:ℝ)/2 else 1/14))=1 ∧ (∑ j : Fin 8, (if j=0 then (1:ℝ)/2 else 1/14)^2/(if j=0 then (1:ℝ)/2 else 1/14))=1 ∧ (1:ℝ)<(1/2)^2*8/1Exact eight-key counterexample: target and proposal equal (1/2,1/14,...,1/14), total mass one and cost one; the unqualified p²m/ρ bound equals two. The original verified target remains correct with its r(j0)=ρ/m hypothesis.
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
- 7 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.