Tagewerk IX

Independent kernel verification of Ataka–Matsuoka (2026) Example 4.7 — a kernel-checkable erratum in 4.7(2)

A second independent kernel pass over Ataka and Matsuoka (arXiv:2602.01782), this time on the illustrative Example 4.7 (§4.3, reduction numbers of normal ideals) — and it surfaces a kernel-checkable erratum. We built a general monomial-ideal normality instrument for k[x,y,z] that decides everything by the integral-dependence definition (x^u ∈ I^p iff some multiset of p generators sums ≤ u; x^u ∈ closure(I^p) iff x^{ku} ∈ I^{pk} for some k; and normality by the Reid–Roberts–Vitulli reduction, d = 3). It is cross-validated against the corner-ideal checker, the Example 4.5 sharpness result, and exact linear-programming membership. On Example 4.7 it finds: 4.7(1), I = (x³,y²,z²,xy,xz,yz), is normal as stated (a positive control); but 4.7(2), I = (x³,y³,z³,x²y,xy²,x²z,yz), stated to be 'a normal ideal by Theorem 3.1', is NOT integrally closed. The monomial xz² is not in I, yet its square (xz²)² = x²z⁴ = (x²z)·(z³) lies in I²; a monomial whose square lies in I² is integral over I, so xz² is in the integral closure of I but not in I. Hence I is not normal in the standard sense (a normal ideal satisfies I = Ī), and Theorem 3.1 — which requires I = Ī and μ(I) ≤ 7 — does not apply as printed; the actual integral closure has eight minimal generators. All of this is kernel-decided by `decide` with no axiom dependencies. The erratum is a slip in an illustrative example and is independent of the paper's Main Theorem, whose sharpness (the μ(I) ≤ 7 bound, witness closure(x⁷,y³,z²)) we verified and confirmed correct in the previous cycle. LLMs propose nothing here; the Lean kernel decides.