The parameter regime of thm:qld #
Stage 4 of the appendix runs at the padded dimension 4m, so it needs 4m | q; the theorem is
stated for every tuple with m | q. The paper closes the gap in a \cnote of qld-combining.tex
("admissibility makes m a power of two") and its stage-4 setup lists 4m | q beside the regime
16md <= q as though it were a further hypothesis; blueprint lem:qld-global-setup states the
derivation, and lists the lemmas below. Neither says what the derivation uses,
and the derivation is short enough to be worth getting exactly right, because the obvious reading
of it is false.
m | q and q a power of two do not give 4m | q. Take m = q. What they give is that m
is itself a power of two, m = 2^j with 2^j | 2^n; 4m = 2^{j+2} then divides 2^n exactly when
j + 2 <= n, which is 4m <= q. So the size condition is load-bearing, and it is the regime
that supplies it: 48 m d <= q with d >= 1 gives 4m <= q. Outside the regime the theorem takes
the trivial bound and never needs 4m | q, which is why the derivation is only ever made inside it.
And "admissible" is not needed at all. The paper's admissible sizes are q = 2^t with t
odd; the oddness is for the self-dual basis. What this step uses is only that q is a power of
two, and a finite field of characteristic two has that for free (FiniteField.card). The
characteristic-two hypothesis [Algebra (ZMod 2) F] is already on every declaration of the
appendix, so the step costs no hypothesis the theorem does not already carry.
A divisor of the field size is a power of two. This is the content of the paper's
\cnote that admissibility makes m a power of two, and it needs characteristic two only.
4m | q from m | q and 4m <= q. The size condition cannot be dropped: at m = q the
divisibility holds and the conclusion fails.
Inside the regime, stage 4's divisibility holds. 48 m d <= q with d >= 1 gives
4m <= q, which is the size condition four_mul_dvd_card needs. MIPRE.QLD.exists_mirrorSimul
derives 4m | q this way, from 48 m d <= q together with m | q.