Provedattentioninnovationexternal-review-3

Constrained optimum: zero-objective normalization counterexample

For all $\htmlData{mx=1}{\gamma \in \htmlData{mx=0}{\mathbb{R}}}$ :

\begin{aligned} & \left(\htmlData{mx=4}{\htmlData{mx=2}{\htmlData{mx=1}{\frac{1}{2}}} + \htmlData{mx=3}{\frac{1}{2}}} \mathrel{\htmlData{mx=5}{=}} 1\right) \\ & \htmlData{mx=0}{\land} \left(\htmlData{mx=7}{\htmlData{mx=6}{\frac{1}{2}}} \mathrel{\htmlData{mx=10}{\geq}} \htmlData{mx=9}{\frac{\htmlData{mx=8}{\frac{1}{2}}}{2}}\right) \\ & \htmlData{mx=0}{\land} \left(\htmlData{mx=16}{\htmlData{mx=13}{\frac{\htmlData{mx=11}{0}}{\htmlData{mx=12}{\frac{1}{2}}}} + \htmlData{mx=15}{\frac{0}{\htmlData{mx=14}{\frac{1}{2}}}}} \mathrel{\htmlData{mx=17}{=}} 0\right) \\ & \htmlData{mx=0}{\land} \left(\htmlData{mx=32}{\htmlData{mx=24}{\max(\htmlData{mx=20}{\frac{\htmlData{mx=19}{\htmlData{mx=18}{\frac{1}{2}}}}{2}}, \htmlData{mx=23}{\htmlData{mx=21}{\gamma} \cdot \htmlData{mx=22}{\sqrt{0}}})} + \htmlData{mx=31}{\max(\htmlData{mx=27}{\frac{\htmlData{mx=26}{\htmlData{mx=25}{\frac{1}{2}}}}{2}}, \htmlData{mx=30}{\htmlData{mx=28}{\gamma} \cdot \htmlData{mx=29}{\sqrt{0}}})}} \mathrel{\htmlData{mx=34}{=}} \htmlData{mx=33}{\frac{1}{2}}\right) \\ & \htmlData{mx=0}{\land} \left(\htmlData{mx=49}{\htmlData{mx=41}{\max(\htmlData{mx=37}{\frac{\htmlData{mx=36}{\htmlData{mx=35}{\frac{1}{2}}}}{2}}, \htmlData{mx=40}{\htmlData{mx=38}{\gamma} \cdot \htmlData{mx=39}{\sqrt{0}}})} + \htmlData{mx=48}{\max(\htmlData{mx=44}{\frac{\htmlData{mx=43}{\htmlData{mx=42}{\frac{1}{2}}}}{2}}, \htmlData{mx=47}{\htmlData{mx=45}{\gamma} \cdot \htmlData{mx=46}{\sqrt{0}}})}} \mathrel{\htmlData{mx=50}{\neq}} 1\right) \end{aligned}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
(x : T)As real numbers: 1/2 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((1 / 2 : ℝ))
+Addition: 1/2 plus 1/2. ((1 / 2 : ℝ) + 1 / 2)
=Equality: 1/2 + 1/2 and 1 are the same. ((1 / 2 : ℝ) + 1 / 2 = 1)
a/bDivision: 1 divided by 2. In Lean, dividing by 0 gives 0. (1 / 2)
≥At least: 1/2 is greater than or equal to 1/2/2. ((1 / 2 : ℝ) ≥ (1 / 2) / 2)
∧And: Both hold: max(1/2/2, γ · √(0)) + max(1/2/2, γ · √(0)) = 1/2, and max(1/2/2, γ · √(0)) + max(1/2/2, γ · √(0)) ≠ 1. ((max ((1 / 2 : ℝ) / 2) (γ * Real.sqrt 0…)
maxMaximum: The larger of 1/2/2 and γ · √(0). (max ((1 / 2 : ℝ) / 2) (γ * Real.sqrt 0))
·Multiplication: γ times √(0). (γ * Real.sqrt 0)
√Square root: The non-negative number whose square is 0. (Real.sqrt 0)
≠Not equal: max(1/2/2, γ · √(0)) + max(1/2/2, γ · √(0)) and 1 are different. (max ((1 / 2 : ℝ) / 2) (γ * Real.sqrt 0)…)

theorem vcl-zero-objective-waterfill-counterexample (γ : ℝ) :
    ((1 / 2 : ℝ) + 1 / 2 = 1) ∧ ((1 / 2 : ℝ) ≥ (1 / 2) / 2) ∧ ((0 : ℝ) / (1 / 2) + 0 / (1 / 2) = 0) ∧ (max ((1 / 2 : ℝ) / 2) (γ * Real.sqrt 0) + max ((1 / 2 : ℝ) / 2) (γ * Real.sqrt 0) = 1 / 2) ∧ (max ((1 / 2 : ℝ) / 2) (γ * Real.sqrt 0) + max ((1 / 2 : ℝ) / 2) (γ * Real.sqrt 0) ≠ 1)

Proves the printed water-filling normalization formula fails when all objective coefficients vanish, while a positive feasible proposal exists.

How it was proved

Proved: 6 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: 9 lines of Lean

Constrained optimum: zero-objective normalization counterexample

How it was proved

More proved statements