The minimum number of monochromatic permuted copies in a two-colouring of the regular (2ᵏ-1)-gon
Abstract
Put n=2ᵏ-1 points evenly on a circle. A permuted copy is a k-subset whose cyclic gaps are a permutation of 1,2,4,…,2ᵏ⁻¹; Stromquist conjectured that every two-colouring of the n points contains a monochromatic permuted copy, and Damásdi, Frankl, Pach and Pálvölgyi, who verified the conjecture for k ≤ 7 by computer, ask for the minimum number μ(k) of monochromatic permuted copies over all two-colourings. A one-page problem-session note of Stromquist announces, with no proof and no method, the three values μ(3)=2, μ(4)=4, μ(5)=10; no other value of μ, and no proof of these, appears to be on record. We prove μ(k) ≤ (k-1)! for every k ≥ 2, witnessed by the parity colouring χ(x)=x mod 2 on the representatives 0,…,n-1; in particular μ(8) ≤ 5040 unconditionally, at the first case left open by the computer searches. We give proofs of Stromquist's three values, the last of them by an exhaustive branch-and-bound over all 2³¹ colourings whose pruning rule is proved sound, and we give explicit colourings showing μ(6) ≤ 20 and μ(7) ≤ 120. The structural tool is an exact restatement: a permuted copy is precisely a translate of the σ-image of a maximal chain of the Boolean lattice 2^([k]) truncated to its bottom k levels, where σ(S)=Σ_(i ∈ S)2ⁱ. Every theorem, proposition and lemma below is machine-checked in Lean 4.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-08-30 15:34 UTC
File fingerprint
29eba7ba808d6cc55ed3cf312f9edc182b240b0b1ead0ef27648a0340c0ff4c1
Claim ledger
Stated results
SQ1candidate2026-08-29
mu(k) <= (k-1)! for every k >= 2, attained by the parity colouring chi(x) = x mod 2; that colouring has exactly (k-1)! monochromatic copies at k = 3,4,5,6
SQ2known2026-08-29
The source's copy count n(k-1)!, kernel-checked: |Hₖ| = 14, 90, 744, 7560 at k = 3..6, enumeration length 91440 and 1285200 at k = 7, 8
SQ3known data2026-08-29
mu(3) = 2 and mu(4) = 4, exhaustively over all 2⁷ and 2¹5 colourings
SQ4candidate2026-08-29
mu(5) <= 10, mu(6) <= 20, mu(7) <= 120 from explicit colourings, kernel-counted against the full copy set
SQ5known2026-08-29
Stromquist's conjecture at k = 3, 4 and 5, as a corollary of mu(k) >= 2
SQ6candidate2026-08-29
The Boolean-lattice restatement: a copy is exactly a translate of the sigma-image of a maximal chain of 2^[k] truncated to levels 0..k-1, in both directions and at every k
SQ7routine2026-08-29
Negative controls: mu(2) = 1 (the bound is attained), mu(4) is neither <= 3 nor >= 5, mu(4) < 3! (the general bound is not an equality), the copy count is not n*k!, the parity colouring leaves 12 of the 14 copies non-monochromatic, the unanchored and anchored enumerations agree at k = 4, and the branch-and-bound agrees with the brute-force exhaustive at k = 3 and 4 while being false one step above the true value
SQ8known data2026-08-29
mu(5) = 10 exactly: the lower bound by an exhaustive branch-and-bound over all 2³1 colourings, kernel-checked
SQ9measurement2026-08-29
The candidate formula mu(k) = 2*floor(2ᵏ⁻¹/3) is refuted in practice at k = 7: 68 independent searches never go below 120, against a prediction of 42
This ledger entry is reported in prose and is not bound to a Lean theorem.Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- Put n = 2ᵏ - 1 points evenly on a circle and colour each red or blue. A permuted copy (here: a copy) is a k-subset whose cyclic gaps are a permutation of 1, 2, 4, …, 2ᵏ⁻¹. Those gaps sum to n, so a copy wraps the circle exactly once, and there are n·(k-1)! of them (14, 90, 744, 7560, 91440, 1285200 for k = 3 … 8).
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7