What was already known
Joshi and Rust posed these three first-occurrence identities as Conjecture 3.8. Earlier work by Parshina and Aedo–Grimm–Nagai–Staynova established maximal-length results and block-recognition methods, but not the three earliest-start formulas.
AI involvement
The source package credits dot, an OpenAI agent, with the all-start argument, Lean formalization and proof audit. The underlying model is unspecified, and human mathematical direction is not itemized.
The pinned package credits dot, an OpenAI agent, with the uniform all-start argument, complete Lean proof and proof audit. The source identifies Joshi and Rust’s conjecture and earlier maximal-length work separately. It does not itemize human mathematical input; AI-led involvement is supported by the project’s direct credit of the central proof.
Importance
Resolves the three stated first-occurrence families of Joshi–Rust Conjecture 3.8 and supplies all-start classifications for two families.
Limitations
The first formula excludes n=1, where i(3)=45. The result concerns three specified difference families, not all differences. The build receipt is project supplied; there is no public CI or outside expert endorsement.
Technical verification
The pinned package reports fresh compilation of seven Lean modules and a full audit of 323 source-owned declarations. The completed Headline.lean theorems state all three earliest-start formulas with their exact small-index ranges and global maximum definitions. This is a source-reported Lean check; AIProofWatch did not rebuild it, and no public CI or outside expert endorsement is claimed.
Formal checking
The pinned package reports a fresh compilation of seven Lean modules and an audit of 323 source-owned declarations. Headline.lean states all three formulas with exact index ranges and completed proofs.
- Checker
- Lean 4 kernel, as reported by the source package
- Scope
- For Thue–Morse digit-sum parity t, maximum monochromatic progression length A(d), and earliest maximizing start i(d): i(2^n+1)=3·2^(2n)−2^n−1 for n≥2; i(2^(2n)−1)=3·2^(4n)−2^(2n)+1 for n≥1; and i(2^(2n+1)−1)=2^(2n+1)−1 for n≥0.
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Few is the default when evidence for a higher level is insufficient. No named person is documented explaining the central argument. Editorial reading or a separate AI review does not establish human understanding. Few is the default from missing evidence, not a finding that people cannot explain it.
Correction and publication history
Pinned primary claim, prior baseline, AI attribution and checking scope reviewed for local inclusion without notification.
Read this published revision