No valid seven-node EML tree evaluates to 2

No valid closed EML tree with exactly seven nodes evaluates to $2$.

An EML tree is built from the leaf $1$ and the single binary operator $\mathrm{eml}(x,y) = e^{x} - \ln y$; it is valid when every logarithm in it is taken of a positive real. This closes size $7$ of the ladder for the constant $2$, in the same shape as the platform's not_attains_two_size_six.

Why it is a separate node. A tree of size $7$ is necessarily $\mathrm{node}(a,b)$ with $|a| + |b| = 6$, so the claim splits into the seven cases $(|a|,|b|) \in \{(0,6),(1,5),(2,4),(3,3),(4,2),(5,1),(6,0)\}$. Every one of those seven is already Proved on the platform as EmlComplexity.not_attains_two_pair_i_j. What is missing is the aggregation, and it does not come for free: it needs the observation that the size decomposition is exhaustive, which is omega on $|a| + |b| + 1 = 7$ after ruling out the leaf.

The seven splits are not symmetric. It is tempting to think $(i,j)$ and $(j,i)$ are mirror images, but $\mathrm{eval}(\mathrm{node}(a,b)) = e^{\mathrm{eval}(a)} - \ln(\mathrm{eval}(b))$ puts the left child through $\exp$ and the right through $\ln$, and validity constrains only the right child ($0 < \mathrm{eval}(b)$). The shape counts differ accordingly — the extreme splits $(0,6)$ and $(6,0)$ carry $132$ shape pairs each, far more than the balanced $(3,3)$ — and so do the sets of degenerate shapes killed exactly.

Role. With sizes $0$–$6$ closed (not_attains_two_upto_two, not_attains_two_size_three, not_attains_two_four_five, not_attains_two_size_six) and this node, the umbrella EmlComplexity.not_attains_two_below_nine needs only size $8$. That layer is not yet started: it is nine splits over $1430$ shape pairs, and it will have to be published as nine separate theorems, because a single-file proof does not fit — the verifier's source lexer caps input at $1\,048\,576$ bytes and the $132$-pair $(0,6)$ split alone already needs about $941$ KB after compression.