Tagewerk XIV

Independent kernel verification of Mafi–Naderi (2021): the integral closure of M_{3,t} gains an embedded prime

An independent kernel verification of a monomial-ideal result, on the general monomial-ideal instrument. Mafi and Naderi (2021, 'Integral closure and Hilbert series of a special monomial ideal', arXiv:2112.02921) study M_{n,t} = (x^{e_1},…,x^{e_n}), where x^{e_i} is the product of all variables except the i-th, each to the power t. Their Theorem 1.6 says the integral closure of M_{n,t} is a Veronese-type ideal; for three variables this is closure(M_{3,t}) = {x^u : min(a,t)+min(b,t)+min(c,t) ≥ 2t}. Their Corollary 1.7 says M_{n,t} is Cohen–Macaulay (unmixed), yet its integral closure has embedded associated primes. LLMs propose nothing here; the Lean 4.31 kernel decides. Using our exact integral-dependence instrument we confirm, for n = 3: (Theorem 1.6) the computed integral closure equals the Veronese cap-sum ideal, cross-checked for t = 1,2,3,4; and (Corollary 1.7) the closure has the embedded prime (x,y,z) for t ≥ 2 — witnessed by a monomial u that is not in the closure but whose product with each variable is (for t = 2 the witness is xyz) — while M_{3,t} itself has no such witness and is unmixed, so the integral closure GAINS an embedded prime the original ideal lacks. An honest detail our check surfaces: at t = 1 the ideal is the squarefree Veronese, already integrally closed and with no embedded prime, so the phenomenon begins at t = 2. Verdict: agreement — no erratum. Six theorems, kernel-decided by `decide`, standard axioms. This is a second independent verification on the general monomial-ideal instrument, after Ataka–Matsuoka.