# AI provenance: The minimum number of distinct abelian squares in a binary circular word

Author: Deep Bhattacharjee (sole author). No AI system is an author or contributor.

## How the work was produced

Deep Bhattacharjee chose the problem, Conjecture 0.6 of J. Simpson (arXiv:1802.04481), and directed the work. Claude (Anthropic), working through Claude Code, did the following:

- searched the literature;
- found and checked the proofs;
- wrote the Lean 4 formalization with Mathlib;
- wrote the verification programs in C, C++, Python, Julia and Bash;
- drafted the paper.

## How the results are checked

The proofs are complete by hand in the paper and fully formalized:

- `verification/lean/` contains Lean 4 with Mathlib, in 13 files. The theorems `min_distinct`, `extremal_odd`, `extremal_even`, `conjectureA` and `not_conjectureB` depend only on propext, Classical.choice and Quot.sound.
- `verification/c/circsq.c` checks every binary word of length n ≤ 22.
- `verification/cpp/necklaces.cpp` checks one word per necklace, n ≤ 28.
- `verification/python/verify_simpson.py` checks from the definitions (all rotations, all splits, Parikh vectors), n ≤ 12.
- `verification/julia/verify_lemmas.jl` checks every lemma of the proof on every word of length n ≤ 16.
- `verification/shell/check_small.sh` checks in Bash integer arithmetic only, n ≤ 10.

## What is claimed

Every binary circular word of length n ≥ 1 has at least floor((n−1)/2) distinct abelian squares. Equality holds exactly for the conjugates of the following words:

- when n is odd: a^n, b^n, a^(n−1)b and b^(n−1)a;
- when n is even: a^k b^(n−k) with k odd, together with (ab)^(n/2) when n ≡ 2 (mod 4).

So part (a) of Simpson's Conjecture 0.6 holds. In part (b) the minimum is correct, but the list of extremal words is incomplete exactly for n ≡ 2 (mod 4), n ≥ 6.

## Labels given on the Hexagon form

- Text of the contribution: a mix of human-written and AI-generated.
- Human understanding at submission: some parts, but not all, checked and understood by a human.

## Where everything is

Release v2.1.0: https://github.com/creelie/literate-octo-lamp/releases/tag/v2.1.0