Blind read-back of Milestone3.lean

mme_stothers_lemma52_same_marginal

The theorem is the conjunction of two assertions over real $10$-coordinate vectors and has no field, tensor, or $\tau$ parameter. First, for every $x=(x_0,\ldots,x_9)\in\mathbb R^{10}$, the following nine equations hold simultaneously, $2x_0+2x_1+2x_2+2x_3+x_4=0$, $2x_1+2x_5+2x_6+2x_7=0$, $2x_2+2x_6+2x_8+x_9=0$, $2x_3+2x_7+2x_9=0$, $2x_4+2x_7+x_8=0$, $2x_3+2x_6=0$, $2x_2+x_5=0$, $2x_1=0$, and $x_0=0$, if and only if there exist real numbers $s,t$ such that $x=(0,0,s,t,-2s-2t,-2s,-t,2s+t,2t,-2s-2t)$; both directions of the equivalence are asserted, while uniqueness of $s,t$ is not part of the stated right-hand side. Second, for every pair $a=(a_0,\ldots,a_9)$ and $b=(b_0,\ldots,b_9)$ of real vectors, if (i) every $a_i\ge0$ and $a_0+2a_1+2a_2+2a_3+a_4+a_5+2a_6+2a_7+a_8+a_9=1$; (ii) every $b_i\ge0$, $b_0+2b_1+2b_2+2b_3+b_4+b_5+2b_6+2b_7+b_8+b_9=1$, $b_2b_7^2=b_4b_5b_9$, and $b_3b_7b_8=b_4b_6b_9$; (iii) in addition, every coordinate of $b$ is strictly positive; and (iv) there exist real $s,t$ such that $a-b=(0,0,s,t,-2s-2t,-2s,-t,2s+t,2t,-2s-2t)$, then $F(b)\le F(a)$, where, writing $R(x,r)=\operatorname{Real.rpow}(x,r)$, $F(x)=R(x_0,x_0)R(x_1,2x_1)R(x_2,2x_2)R(x_3,2x_3)R(x_4,x_4)R(x_5,x_5)R(x_6,2x_6)R(x_7,2x_7)R(x_8,x_8)R(x_9,x_9)$. The conclusion is non-strict; $a$ is required only to be nonnegative, not strictly positive and not to satisfy the two polynomial equations, so zero coordinates of $a$ are included and contribute $R(0,0)=1$ under the total real-power operation; strict positivity is imposed only on $b$, in addition to all of the nonnegativity, normalization, and polynomial conditions already contained in its second premise. Because the premises form an implication chain, the second assertion imposes no comparison when any one of them fails.