The descent step of Schneider's method

The descent step — the analytic and arithmetic halves of Schneider's method, in one statement.

Under the standing hypotheses, if the auxiliary function has coefficients of size at most $e^{cLM}$ and vanishes at every lattice point $\sum_j m_j y_j$ with all $m_j < N$, for some $N \ge M$, then it vanishes at every such point with all $m_j < N+1$.

Iterating from the $M$ supplied by the Siegel step, the function vanishes on the whole lattice.

Why the two halves cannot be separate rungs. The analytic half says: an entire function with $N^l$ prescribed zeros is small on a disc, by dividing out the zeros and applying the maximum modulus principle. The arithmetic half says: the value at a new lattice point is an algebraic integer, so if it is non-zero its norm is at least 1. Each half is an inequality about a single value $F(w)$, and nothing links them except the balance of parameters, which is the body of the proof rather than a lemma. Stated apart they do not meet; stated together they are the induction step.

The balance is $N^l \log 2$ against $O(N^{l/d + 1})$, and it closes precisely when $dl > d + l$.

Where it anchors. Complex.norm_le_of_forall_mem_frontier_norm_le for the maximum modulus; NumberField.one_le_house_of_isIntegral and NumberField.norm_norm_le_norm_mul_house_pow for the arithmetic. The "many prescribed zeros implies small" estimate does not exist in Mathlib and has to be built — note that Analysis/Complex/Schwarz.lean is the ball-to-ball Schwarz lemma, which is a different statement. This is where essentially all the difficulty of the theorem lives.