Provedattentionresidual-seriesexternal-review-4
Uniform within a tile can increase the full chi-square cost
What the notation means · or point at any symbol
- aᵇPower
- 9/10 raised to the power 2. (
((9:ℝ)/10)^2) - +Addition
- (9/10)^2/(9/10) plus (1/10)^2/(1/10). (
((9:ℝ)/10)^2/(9/10)+(1/10)^2/(1/10)) - =Equality
- (9/10)^2/(9/10) + (1/10)^2/(1/10) and 1 are the same. (
((9:ℝ)/10)^2/(9/10)+(1/10)^2/(1/10)=1) - (x : T)As real numbers
- 9 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(9:ℝ)) - a/bDivision
- 9 divided by 10. In Lean, dividing by 0 gives 0. (
(9:ℝ)/10) - ∧And
- Both hold: (9/10)^2/(1/2) + (1/10)^2/(1/2) = 41/25, and 1 < 41/25. (
((9:ℝ)/10)^2/(1/2)+(1/10)^2/(1/2)=41/25…) - <Less than
- 1 is strictly smaller than 41/25. (
(1:ℝ)<41/25)
theorem tile-uniform-conditional-counterexample :
((9:ℝ)/10)^2/(9/10)+(1/10)^2/(1/10)=1 ∧ ((9:ℝ)/10)^2/(1/2)+(1/10)^2/(1/2)=41/25 ∧ (1:ℝ)<41/25Exact two-key counterexample: pi=r=(9/10,1/10) has full and one-tile marginal cost one; changing to uniform within that tile raises full cost to 41/25.
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.