Explicit bound on the uniform entropy modulus

Let $W$ be a finite set. For a function $p\colon W\to[0,1]$ write

the unnormalised natural-logarithm entropy used by the regional entropy rate data; no probability normalisation of $p$ is assumed. The uniform entropy modulus $\mathrm{mod}_W(\varepsilon)$ is the supremum of $|H(p)-H(q)|$ over all pairs $p,q\colon W\to[0,1]$ with $|p_w-q_w|\le\varepsilon$ for every $w\in W$. For every tolerance $0\le\varepsilon\le 1$,

The existing platform theorem mme_regional_entropy_uniform_modulus records only that the modulus is finite and tends to zero with $\varepsilon$. A finite regional certificate for the More Asymmetry construction has to bound the loss term $(\sum_r n_r)\cdot\mathrm{mod}_W(\varepsilon)$ inside the guaranteed copy count IntegerStep.entropyLower by an explicit number, which is what this bound supplies: the right-hand side is an elementary closed form in the tolerance fixed by the size test of the step and the cardinality $|W|$ of the parent-word alphabet.

Formalization Note The modulus is the platform constant entropyModulus W eps of Def_mme_regional_entropy_rate_data, a real supremum; the statement is therefore a bound on that supremum, and $h$ is Mathlib's Real.negMulLog.