The borderline case of the Migliore–Miró-Roig–Nagel conjecture for level monomial almost complete intersections: complete integer eliminations up to a=13
Abstract
Let Bbbk have characteristic zero, let R=Bbbk[x,y,z], and let I be generated by x^(a₁+t), y^(a₂+t), z^(a₃+t) and x^(a₁)y^(a₂)z^(a₃), so that R/I is a level monomial almost complete intersection. Migliore, Miró-Roig and Nagel conjectured a characterisation of when such an algebra fails the weak Lefschetz property; in the form Cook and Nagel restated it, failure occurs — apart from the two quadruples (2,9,13,9) and (3,7,14,9), which are exceptions — exactly when t is even, a₁+a₂+a₃ is odd and a₁,a₂,a₃ are not all distinct. One implication is a theorem and the other is open. Booth and Vraciu reduce the first unresolved value t=(a₁+a₂+a₃)/3+1 to the integer zeros of an explicit polynomial Fₐ(a₁,a₂), where a is defined by a₃=2(a₁+a₂)-3a. They settle a ≤ 3, report a textsl(Macaulay2) verification for a ≤ 6 under the extra hypothesis a₁ ≥ a, and stop: for a ≥ 7, "the list of values that need to be checked is too large to be practical." We determine the zero set of Fₐ on the admissible region 0<a₁ ≤ a₂ ≤ a₃ completely, for 2 ≤ a ≤ 13 and in both regimes. In the regime a ≤ a₁ the zeros are the diagonal a₁=a₂ for odd a and none for even a, apart from the single triple (3,7,14) at a=2; the levels 7 ≤ a ≤ 13 are new. In the regime a₁=r<a — which the published textsl(Macaulay2) code excludes by construction — the zeros are a₂=a₃=3a-2r for odd r and none for even r, apart from the single triple (2,9,13) at a=3; this is new for 4 ≤ a ≤ 13, and all 78 pairs (a,r) are settled without any appeal to compiled evaluation. The two exceptions are exactly the two quadruples the conjecture already excepts, and every remaining zero is a triple on which failure of the weak Lefschetz property is already a theorem: no analogue of the exceptional quadruples appears at any level above a=3 in this range. Granting Booth and Vraciu's reduction, the conjecture therefore holds at t=(a₁+a₂+a₃)/3+1 for every admissible triple with 2 ≤ a ≤ 13, and no exceptional quadruple beyond the two known ones occurs at that t in that range. Up to a=8 the method replaces divisor lists by a scan reaching only √(N(a)) together with one modulus certificate per surviving value of S=a₁+a₂; past a=8 the scan is itself the obstruction — it would need 1.5 · 10¹⁰ trial divisions at a=12 — and is replaced by a divisor list built from the factorisation of N(a), with each certificate evaluated at S reduced modulo its own modulus. Two small corrections to the source are recorded. Every theorem below about the polynomials Fₐ is machine-checked in Lean 4; the consequence for the conjecture, being a statement about Lefschetz properties, is not.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 2 · current (opens in a new tab)
Source snapshot 2026-09-07 03:53 UTC
File fingerprint
59566a92a525252ce5d694c5336ae6cbe9606167f8c3e3c78dfd2e5896631024
Claim ledger
Stated results
W1known2026-09-03
The source's Theorem borderline for a <= 3, rebuilt from its own definitions: tau¹ D, tau² D, tau³ D in both regimes, the polynomial F (a = 2), G (a = 3), the boundary polynomials at (a,a1) = (2,1), (3,1), (3,2), and the complete zero sets – (3,7,14), (1,4,4), (1,7,7), (2,9,13)
W2known2026-09-03
Generic regime a <= a1 complete for a = 4, 5, 6: on 0 < a1 <= a2 <= a3 the only zeros of Fₐ are the diagonal a1 = a2 (odd a), and none at all for even a
W3candidate2026-09-03
Generic regime a <= a1 complete for a = 7 and a = 8: Fₐ = 0 has no admissible solution except the diagonal a1 = a2 (a = 7) and no solution at all (a = 8)
W4candidate2026-09-03
Boundary regime a1 = r < a complete for 4 <= a <= 8 and every 1 <= r < a: the only admissible zero is a2 = a3 = 3a - 2r, present exactly when r is odd. Entirely kernel-clean – no native_decide
W5routine2026-09-03
The normalisation is faithful: over 1 <= a <= 8, 1 <= a1 <= a2 <= 40, the raw coefficient (real binomial coefficients, no denominators cleared) vanishes exactly where the normalised polynomial does, and its complete zero set is a1 = a2 (odd a), (r, 3a-2r) for odd r < a, and the two rogue triples
W6routine2026-09-03
Negative controls, including two corrections to the source: the hypotheses do not imply a <= a1 (counterexample (1,4,4) at a = 2), and the printed tau branch condition 1 <= k <= a1+1 must be read as k <= a1
W7prose2026-09-03
The same complete answer for 9 <= a <= 13, both regimes, in exact integer arithmetic outside Lean: the zeros of Fₐ are a1 = a2 (odd a) and (r, 3a-2r, 3a-2r) for odd r < a, and nothing else
This ledger entry is reported in prose and is not bound to a Lean theorem.W8known2026-09-03
The source's experimentally observed shape of Fₐ – constant term in P equal to the printed product P(S), every higher P-coefficient divisible by 2S - c(a) as an integer polynomial – verified for 2 <= a <= 8 by ring and for a <= 11 in exact arithmetic
W9candidate2026-09-03
Generic regime a ≤ a₁ complete for a = 9, 10, 11, 12, 13: on a ≤ a₁ ≤ a₂ ≤ a₃ the only zeros of Fₐ are the diagonal a₁ = a₂ (odd a), and none at all for even a — the levels the source states it could not reach
W10candidate2026-09-03
Boundary regime a₁ = r < a complete for 9 ≤ a ≤ 13 and every 1 ≤ r < a — all 50 pairs: the only admissible zero is a₂ = a₃ = 3a − 2r, present exactly when r is odd. Entirely kernel-clean — no native_decide
W11routine2026-09-03
The normalisation is faithful at the new levels: over 9 ≤ a ≤ 13 the raw coefficient (real binomial coefficients, nothing cleared) vanishes exactly where Fgen does on a ≤ a₁ ≤ a₂ ≤ 40, and exactly where Fbdry does on the 50 boundary pairs with a₂ ≤ 60
W12candidate2026-09-03
The complete zero set of the raw coefficient for 9 ≤ a ≤ 13 over 1 ≤ a₁ ≤ a₂ ≤ 40: exactly the diagonal a₁ = a₂ (odd a) together with (r, 3a−2r) for odd r < a, and nothing else — so no analogue of the rogue quadruples (2,9,13,9), (3,7,14,9) exists at any of these levels
W13routine2026-09-03
Negative controls for the extension: the built divisor list stops being complete if one prime is dropped; memₚrodList genuinely needs primality (2 ∣ 4¹, 2 ∉ powers 4 1); a modulus certificate is per-S (71 clears S = 53 at a = 9 but not S = 134); too-small, too-large and boundary-parity refutations at the new levels; c(9) = 25, not 26; both regimes inhabited
W14routine2026-09-03
The divisor list of N(a) built from its factorisation rather than found by a √N scan, with completeness from the multiplicative structure (d ∣ mn ⟹ d = d₁d₂), plus modulus certificates evaluated at S % m; both kernel-clean, and together they remove one native_decide axiom per level
W15measurement2026-09-03
Measured: unfolding the τ recursion in one simp costs 3ᵃ copies of the base because tau1 names its argument three times — 6 561 at a = 8, 59 049 at a = 10. Naming the intermediate lists is 8× in CPU and takes peak RSS from 10.7 GB to 6.8 GB on the same declaration
This ledger entry is reported in prose and is not bound to a Lean theorem.Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- Source. M. D. Booth, A. Vraciu, *The generators of a colon ideal with an application to the weak Lefschetz property for monomial almost complete intersections in three variables*, arXiv:2603.11491 v2 (12 Mar 2026, revised 6 Jul 2026); *Experimental Mathematics*, DOI 10.1080/10586458.2026.2709599. v2 is the live version (checked 2026-09-03); 0 citations on OpenAlex, Semantic Scholar.
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7