Mutation-acyclicity in rank four is decidable but not semialgebraic

AI involvement AI-centered

The authors explicitly credit GPT-Astra with discovering the family $Q(t)$ and the main results after extensive prompting. The human team generalized the results, simplified the proofs and organized the exposition. This supports AI-centered work for the alternating family and its polynomial-sign obstruction.

• Armstrong-Williams, Hirst, Jackson and Lee: mutation-acyclicity in rank four — Introduction, Theorem 1.2, Section 3 and Use of AI

Importance Notable

Gives a concrete barrier to a natural algebraic classification method beyond rank three. It rules out fixed polynomial-sign criteria, while leaving arithmetic tests, general mutation invariants and input-dependent algorithms available.

Technical verification Partial

The manuscript gives a proof through the alternating integer family and eventual constancy of polynomial signs. The pinned artifact reports successful exact-arithmetic checks of 300 claims and the finite census, but its clean Lean audit completed only 135 of 573 modules. The Lean obstruction covers rational coefficients in rank four; real coefficients, higher ranks and connected extensions use separate manuscript arguments. These records support Partial, not a completed check of the entire assessed claim.

• Exact checks, retained Lean scope and incomplete clean build — Introduction, Theorem 1.2, Section 3 and Use of AI

Human understanding Explained

The authors explain the central mechanism: mutation-acyclicity alternates along the positive integers in an affine family, while each fixed polynomial restricted to that line has eventually constant sign. A path attachment carries the obstruction to connected higher-rank quivers. Their discussion distinguishes this obstruction from the separate rank-four decision algorithm and preserves the earlier human criteria.