proofs
Provedattentioninnovationexternal-review-3

Bayesian envelope: exact two-row optimum 81 over 50

For all x∈R\htmlData{mx=1}{x \in \htmlData{mx=0}{\mathbb{R}}}, if 0<x0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{x} and x<1\htmlData{mx=0}{x} \mathrel{\htmlData{mx=1}{<}} 1, then

8150≤45⋅max⁡(910x,1101−x)+15⋅max⁡(110x,9101−x)∧45⋅max⁡(91023,1101−23)+15⋅max⁡(11023,9101−23)=8150\begin{aligned} & \htmlData{mx=3}{\htmlData{mx=2}{\frac{81}{50}}} \\ & \quad \htmlData{mx=1}{\leq} \htmlData{mx=24}{\htmlData{mx=13}{\htmlData{mx=4}{\frac{4}{5}} \cdot \htmlData{mx=12}{\max(\htmlData{mx=7}{\frac{\htmlData{mx=5}{\frac{9}{10}}}{\htmlData{mx=6}{x}}}, \htmlData{mx=11}{\frac{\htmlData{mx=8}{\frac{1}{10}}}{\htmlData{mx=10}{1 - \htmlData{mx=9}{x}}}})}} + \htmlData{mx=23}{\htmlData{mx=14}{\frac{1}{5}} \cdot \htmlData{mx=22}{\max(\htmlData{mx=17}{\frac{\htmlData{mx=15}{\frac{1}{10}}}{\htmlData{mx=16}{x}}}, \htmlData{mx=21}{\frac{\htmlData{mx=18}{\frac{9}{10}}}{\htmlData{mx=20}{1 - \htmlData{mx=19}{x}}}})}}} \\ & \htmlData{mx=0}{\land} \htmlData{mx=47}{\htmlData{mx=36}{\htmlData{mx=27}{\htmlData{mx=26}{\frac{4}{5}}} \cdot \htmlData{mx=35}{\max(\htmlData{mx=30}{\frac{\htmlData{mx=28}{\frac{9}{10}}}{\htmlData{mx=29}{\frac{2}{3}}}}, \htmlData{mx=34}{\frac{\htmlData{mx=31}{\frac{1}{10}}}{\htmlData{mx=33}{1 - \htmlData{mx=32}{\frac{2}{3}}}}})}} + \htmlData{mx=46}{\htmlData{mx=37}{\frac{1}{5}} \cdot \htmlData{mx=45}{\max(\htmlData{mx=40}{\frac{\htmlData{mx=38}{\frac{1}{10}}}{\htmlData{mx=39}{\frac{2}{3}}}}, \htmlData{mx=44}{\frac{\htmlData{mx=41}{\frac{9}{10}}}{\htmlData{mx=43}{1 - \htmlData{mx=42}{\frac{2}{3}}}}})}}} \\ & \quad \htmlData{mx=25}{=} \htmlData{mx=48}{\frac{81}{50}} \end{aligned}
What the notation means · or point at any symbol
RReal numbers
The real numbers: every point on the number line. (ℝ)
<Less than
0 is strictly smaller than x. (0 < x)
(x : T)As real numbers
81/50 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((81 / 50 : ℝ))
≤At most
81/50 is less than or equal to 4/5 · max(9/10/x, 1/10/(1 − x)) + 1/5 · max(1/10/x, 9/10/(…. ((81 / 50 : ℝ) ≤ (4 / 5) * max ((9 / 10)…)
∧And
Both hold: 81/50 ≤ 4/5 · max(9/10/x, 1/10/(1 − x)) + 1/5 · max(1/10/x…, and 4/5 · max(9/10/(2/3), 1/10/(1 − 2/3)) + 1/5 · max(1/10/(2/…. ((81 / 50 : ℝ) ≤ (4 / 5) * max ((9 / 10)…)
a/bDivision
81 divided by 50. In Lean, dividing by 0 gives 0. (81 / 50)
·Multiplication
4/5 times max(9/10/x, 1/10/(1 − x)). ((4 / 5) * max ((9 / 10) / x) ((1 / 10) …)
+Addition
4/5 · max(9/10/x, 1/10/(1 − x)) plus 1/5 · max(1/10/x, 9/10/(1 − x)). ((4 / 5) * max ((9 / 10) / x) ((1 / 10) …)
maxMaximum
The larger of 9/10/x and 1/10/(1 − x). (max ((9 / 10) / x) ((1 / 10) / (1-x)))
-Subtraction
1 minus x. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (1-x)
=Equality
4/5 · max(9/10/(2/3), 1/10/(1 − 2/3)) + 1/5 · max(1/10/(2/… and 81/50 are the same. ((4 / 5 : ℝ) * max ((9 / 10) / (2/3)) ((…)

Proves a global lower bound and attainment at (2/3,1/3) for the stated two positive posterior rows and prior (4/5,1/5). General finite-prior convex duality remains a paper proof.

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
22 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements