Preimage trees of the nonzero even multiplicative digital roots: residue sieves, exclusion certificates, and open vertices

Let p(N) be the product of the decimal digits of N, and let Δ(N) be the digit at which iterating p stops. We study the preimage trees of the nonzero even roots Δ ∈ {2, 4, 6, 8}, the cases left open by Brier, Clavier, Gutsche, and Naccache. Subject to explicit enumeration and extraction premises stated with the result, we close 157 of the 177 tree vertices below 10^4000: their children are exactly the known ones. Under the same premises and the reported completeness of the corpus, this reduces persistence for roots 2 and 4 to two explicit integers: every N with Δ(N) = 4 and persistence at least 6 has an iterate that is a child of 128421199872 with more than 4000 digits, and every N with Δ(N) = 2 and persistence at least 7 has such an iterate for 1811939328. For root 6 and persistence at least 9, or root 8 and persistence at least 7, an iterate is such a child of one of the 18 named unresolved vertices of those trees. For 23 vertices, among them the four roots 2, 4, 6, 8 and every child of 2, the complete closure, enumeration included, is a Lean theorem with no external premise. The method turns a fixed digit inventory into finitely many exact two-dimensional exponent cosets, then excludes large realizations by decimal suffix congruences alone or by comparing a lattice lower bound with a two-sided logarithmic-form upper bound (Matveev's theorem and both the independent and dependent cases of Yu's 5-adic estimates); 96 of the 157 closures use no such upper bound. Under an explicit instantiation of the refined abc conjecture of Robert, Stewart, and Tenenbaum, together with the stated finite enumerations, the persistence of every integer with digital root 2, 4, 6, 8 is at most 6, 5, 8, 6, and at most 8 for every nonzero root. For vertices outside the 23 complete closures, Lean verifies the suffix-window exclusion, the lattice lower bound on the kernel-checked rows, and the connecting arithmetic for supplied cosets. Lean also verifies the listed final-stage arithmetic; its statement review is still pending. For realizations whose exponent of 2 is at most 60, Lean verifies the tabulated logarithmic upper bounds for at most 34 non-1 digits, conditional on the published inequalities; their link to the closure computations is not formalized. Completeness of the supplied cosets is not machine-checked. Below 10^96, direct enumeration finds exactly the 173 known children of the 177 vertices and no others. We state what remains: a bounded-anchor conjecture on the 177-vertex inventory, with supporting finite tests, a counterexample outside that inventory, and contrasting heuristic forecasts. In base 8, under premises of the same kind, all 70 nonzero-root vertices close and every integer with nonzero digital root has persistence at most 6; base 6 is partial. This record is the archive the paper cites: preprint-codex94.tar.gz (MD5 b26f09e1d87cea6adf0a0de34c91d602), holding the paper source and PDF, the Lean sources, the certificates and the replay records.