Tagewerk VIII

Independent kernel verification of Ataka–Matsuoka (2026): closure(x⁷,y³,z²) is the sharp non-normal monomial ideal

An independent kernel verification of a February-2026 result. Ataka and Matsuoka (arXiv:2602.01782) prove that an integrally closed monomial ideal I in k[x,y,z] with at most seven minimal generators is normal (every power integrally closed), and that the bound seven is sharp. Their sharpness witness (Example 4.5) is I = the integral closure of (x⁷,y³,z²): it has eight minimal generators and fails to be normal. LLMs propose nothing here — the paper's claim is the object, and the Lean 4.31 kernel decides. From the Newton polyhedron (weights (6,14,21), L = lcm = 42) we reproduce BOTH load-bearing facts and cross-check them verbatim against Example 4.5: the eight minimal generators (x⁷, y³, z², x⁵y, x³y², x⁴z, y²z, x²yz), and the non-normality witness x⁶y²z, which lies in the integral closure of I² (weighted degree 85 ≥ 2L = 84) but not in I² itself, so by the Reid–Roberts–Vitulli reduction (in three variables, normal ⇔ I and I² integrally closed) the ideal is not normal. All three theorems are decided by `decide` with no axiom dependencies at all. A built-in erratum guard refuses to emit the certificate unless the generator count, the generator set, the verdict, the witness monomial, and the weight vector all match the transcribed paper — the same discipline that caught a real erratum in the SS-RS-GD COLT refutation. Verification-amplification on the flagship Problem-41 instrument; no trust surface is touched. A companion research pass (paper-grounded, adversarially faithfulness-checked) records that the three resolved commutative-ring candidates 30a, 30b, and 9 are NOT finite-decidable counterexamples — 30a (Secord 2023) and 30b (Choi–Walker 2016) were resolved positively, and Problem 9 (Haotian Ma 2026) has an intrinsically infinite counterexample — so the domain's growth runs through open monomial questions, not the resolved n-absorbing ones.