Theorem 5.3 from the attained same-marginal minimum

Davie--Stothers Theorem 5.3 with the same-marginal minimum supplied as a hypothesis rather than through the algebraic description of where it sits.

Let $K$ be a field, $\tfrac23\le\tau\le1$, and let $a,b\in Z$ be strictly positive with $a-b\in Y$. Suppose $b$ minimises the Lemma 5.2 weight over the whole affine slice:

Then for every $V$ with

the literal fourth power $\mathrm{CW}_6^{\otimes4}$ has $\tau$-value at least $V$.

Role. This is the extraction half of Theorem 5.3, separated from its arithmetic half. Equation (3.4) of the source bounds the star count of the hashing step by $\prod_jA_j^{-A_j}$ times $\inf_{D\in\Lambda_E}\prod_\mu D_\mu^{D_\mu}\big/\prod_\mu E_\mu^{E_\mu}$, an infimum over the profiles sharing the marginals of the profile $E=a$ that is actually used. What the extraction consumes is only that the displayed $b$ attains that infimum — the extremal property stated above. Lemma 5.2 is what identifies the attaining point: it shows that the stationary set $\mathcal N$, cut out by $b_3b_8^2=b_5b_6b_{10}$ and $b_4b_8b_9=b_5b_7b_{10}$, consists exactly of the slice minimisers, because those two equations say precisely that the gradient of $\sum_in_ib_i\log b_i$ vanishes along the two kernel directions $\sigma$ and $\tau$.

Splitting the theorem this way keeps the algebraic characterisation of $\mathcal N$ — already proved — out of the combinatorial argument, which needs only the inequality.