A Four-Letter Refutation of the Abelian-Square Equality Claim

Abstract

The binary word abab refutes the equality conclusion in Conjecture 4 on abelian squares.

Definition 1.1 (Binary abelian squares).

$$\forall u\in \mathrm{List}\left(Bool\right),(\mathrm{IsAbelianSquare}\left(u\right))\iff (\mathrm{let}p:=\mathrm{NatDiv}\left(\mathrm{length}\left(u\right),2\right),(0<p)\wedge \left((\mathrm{length}\left(u\right)=2\cdot p)\wedge \left((\mathrm{count}\left(false,\mathrm{take}\left(p,u\right)\right)=\mathrm{count}\left(false,\mathrm{drop}\left(p,u\right)\right))\wedge (\mathrm{count}\left(true,\mathrm{take}\left(p,u\right)\right)=\mathrm{count}\left(true,\mathrm{drop}\left(p,u\right)\right))\right)\right))$$

Formalization. D5/S1/Words/Powers/FazekasAbelianSquareEqualityRefutation.IsAbelianSquare (✓ std3).

Citation. Szilárd Zsolt Fazekas, Adam Mammoliti, Robert Mercaş, Jamie Simpson (2026). Binary Words Containing Few Abelian Squares. DOI: 10.48550/arXiv.2604.23188. URL: https://arxiv.org/abs/2604.23188v1.

Commentary.

The binary alphabet is encoded by a=false and b=true. NatDiv is floor division on natural numbers. The midpoint p is NatDiv(length(u),2), and both letter counts are equal across take(p,u) and drop(p,u).

Definition 1.2 (Distinct abelian-square factors).

$$\forall w\in \mathrm{List}\left(Bool\right),\mathrm{abelianSquares}\left(w\right)=\mathrm{filter}\left(IsAbelianSquare,\mathrm{toFinset}\left(\mathrm{flatMap}\left(inits,\mathrm{tails}\left(w\right)\right)\right)\right)$$

Formalization. D5/S1/Words/Powers/FazekasAbelianSquareEqualityRefutation.abelianSquares (✓ std3).

Citation. Szilárd Zsolt Fazekas, Adam Mammoliti, Robert Mercaş, Jamie Simpson (2026). Binary Words Containing Few Abelian Squares. DOI: 10.48550/arXiv.2604.23188. URL: https://arxiv.org/abs/2604.23188v1.

Commentary.

The factors are prefixes of suffixes, formed by inits and tails. Converting them to a finite set removes repeated occurrences before filtering for abelian squares.

Definition 1.3 (Trivial abelian squares).

$$\forall u\in \mathrm{List}\left(Bool\right),(\mathrm{IsTrivial}\left(u\right))\iff (\exists m\in \mathbb{N},(0<m)\wedge ((u=\mathrm{replicate}\left(2\cdot m,false\right))\vee (u=\mathrm{replicate}\left(2\cdot m,true\right))))$$

Formalization. D5/S1/Words/Powers/FazekasAbelianSquareEqualityRefutation.IsTrivial (✓ std3).

Citation. Szilárd Zsolt Fazekas, Adam Mammoliti, Robert Mercaş, Jamie Simpson (2026). Binary Words Containing Few Abelian Squares. DOI: 10.48550/arXiv.2604.23188. URL: https://arxiv.org/abs/2604.23188v1.

Commentary.

A trivial abelian square is a positive even power of exactly one binary letter.

Definition 1.4 (Conjecture 4).

$$(claim)\iff (\forall w\in \mathrm{List}\left(Bool\right),(\mathrm{NatDiv}\left(\mathrm{length}\left(w\right),4\right)\le |\mathrm{abelianSquares}\left(w\right)|)\wedge ((|\mathrm{abelianSquares}\left(w\right)|=\mathrm{NatDiv}\left(\mathrm{length}\left(w\right),4\right))\Rightarrow (\forall u\in \mathrm{abelianSquares}\left(w\right),\mathrm{IsTrivial}\left(u\right))))$$

Formalization. D5/S1/Words/Powers/FazekasAbelianSquareEqualityRefutation.claim (✓ std3).

Citation. Szilárd Zsolt Fazekas, Adam Mammoliti, Robert Mercaş, Jamie Simpson (2026). Binary Words Containing Few Abelian Squares. DOI: 10.48550/arXiv.2604.23188. URL: https://arxiv.org/abs/2604.23188v1.

Commentary.

Conjecture 4 (printed page 1) reads verbatim: “A binary word of length n contains at least ⌊n/4⌋ abelian squares and if it contains exactly ⌊n/4⌋ abelian squares then all the abelian squares are trivial.” The word is a list over the letters a ↦ false and b ↦ true; the number of abelian squares is the number of distinct abelian-square factors, as in the paper’s example abaababa with six such factors. For every binary word w, NatDiv(length(w),4) is at most that number, and if equality holds, every such factor is asserted to be trivial.

Theorem 1.5 (The equality conclusion fails).

$$\neg claim$$

Proof. Machine-checked in Lean as D5/S1/Words/Powers/FazekasAbelianSquareEqualityRefutation.result (✓ std3). ∎

Resolves. Problems/fazekas-abelian-square-equality-refutation (refuted) by D5/S1/Words/Powers/FazekasAbelianSquareEqualityRefutation.result.

Source. Repository-derived.

Commentary.

For abab the distinct abelian-square factor set is the singleton containing abab, so its cardinality is NatDiv(4,4)=1. The factor abab contains both letters and is not a positive even power of either one. This refutes the conjunction through its equality conclusion and does not refute the lower bound.

References

• Truth anchor: D5/S1/Words/Powers/FazekasAbelianSquareEqualityRefutation.IsAbelianSquare
• Truth anchor: D5/S1/Words/Powers/FazekasAbelianSquareEqualityRefutation.IsTrivial
• Truth anchor: D5/S1/Words/Powers/FazekasAbelianSquareEqualityRefutation.abelianSquares
• Truth anchor: D5/S1/Words/Powers/FazekasAbelianSquareEqualityRefutation.claim
• Truth anchor: D5/S1/Words/Powers/FazekasAbelianSquareEqualityRefutation.result