What was already known
Gao and coauthors proved the threshold η^N(C₃³)=25 and gave extremal constructions, without classifying every length-24 extremal in this form.
AI involvement
John Fairfax-Ball directed the research and retains authorship responsibility. His disclosure credits AI with substantive lemma design and the Lean proof; the exact origin of each lemma is not apportioned. No independent human review of this classification is documented.
The project's AI disclosure explicitly covers mathematical research and lemma design for the retained classification, under a human-directed programme; exact per-lemma attribution remains a gap.
Importance
Classifies the extremal sequences one step below the known short-zero-sum threshold.
Limitations
The theorem is restricted to C₃³ and positional length 24. Its broader priority is supported only by the project’s bounded prior-art search.
Technical verification
The registered positional iff is reported checked by Lean and two independent kernels at the cited source. The formal check establishes the encoded claim, not historical novelty.
Formal checking
Statement comparison, proof export and independent kernel replay.
- Checker
- Palomar Comparator, Lean kernel, NanoDa and con-ron
- Scope
- InverseZeroSum.Candidate3.frozenClassification, the length-24 positional iff
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
A human-readable direct proof is archived, but no named human account of the central packing/residual mechanism or human proof check is documented; Few is the evidence-gap default.
Correction and publication history
Classifies the extremal sequences one step below the known short-zero-sum threshold.
Read this published revision