Exhaustive Formal Verification of Elementary Lambert W W Identities up to Size 7

We present a complete, mechanically verified enumeration of all elementary expression trees involving the Lambert W function with size ≤ 7 and depth ≤ 4, built from the alphabet {z,0,1,+,−,×,÷,exp,ln,sin,cos,W}. A normalization procedure applying only the three known identities (exp(W(z)) = z/W(z), ln(W(z)) = ln z − W(z), and W(z·e^z) = z) together with standard algebraic simplifications eliminates W from every eliminable expression in this search space. The entire verification – comprising 819 453 expression trees, of which 386 442 contain W and 34 411 are W‑eliminable – was carried out in the Lean 4 theorem prover with the Mathlib library, providing a machine‑checked certificate that no new independent elementary Lambert W identity exists at size ≤ 7. All encountered eliminable expressions are consequences of the three classical identities; the only nontrivial ones arise from W(0)=0. The Lean source code is provided for full reproducibility.