slug: chervov-2026-cayleypy4-conjecture-fifteen-refutation bibkey: chervov2026cayleypy4 doi: 10.48550/arXiv.2603.22195 url: https://arxiv.org/abs/2603.22195v1 triage: theorem motivation_gids:

• D5/S3/Combinatorics/ShrunkenGrassmannianConjectureFifteenRefutation.result

CayleyPy-4 Conjecture 15 fails at k = 5, L = 4, N = 13

Problem

CayleyPy-4 (arXiv:2603.22195v1) studies the Schreier coset graph S_N / (S_L × S_{N−L}) on binary words with L zeros and N − L ones, generated by the consecutive k-cycles (i, …, i + k − 1). Conjecture 15 treats generators without their inverses and gives the diameters as quasipolynomials in n and t = n − (l + 1); its k = 5 clause reads:

For $k=5$ with period~$4$ (again $t=n-(l+1)$, for all $L\ge 4$, starting from $t+1\ge 9$ that is, $N\ge L+9$): $D(L,N)=L\lfloor \frac{t+1}{4}\rfloor +1_{(t+1)\equiv 0(\mathrm{mod}4)}$.

Issue #10253 fixes the readings: vertices and the central state as in #10230; a directed move rotates a window of five consecutive letters one place, to the left in one convention for the action of a cycle on a word and to the right in the other; the diameter is read both as the largest directed distance from the central state and as the largest directed distance between two vertices. The formal claim is that the clause holds for some convention and some reading.

Motivation

A false clause makes Conjecture 15 false as printed. D5/S3/Combinatorics/ShrunkenGrassmannianConjectureFifteenRefutation.result refutes the clause under both conventions and both readings.

Gap

Issue #10253 preregisters the refutation and its literature check. arXiv lists only version 1 (2026-03-23); the two citing papers reported by Semantic Scholar, arXiv:2607.13219 and arXiv:2607.12026, do not concern these coset graphs. These readings are not-found-in-searched-scope.

Route

The inversion count of a word is the number of positions p < q holding a one at p and a zero at q. By the frozen D5/S1/Digit/Carry/ListInversions.inv_window, rotating five consecutive letters changes only the inversions inside the window, and a rotation by one place carries one letter past the other four, so one move changes the count by at most 4, in either direction. The central state 0^4 1^9 has no inversion and its reversal 1^9 0^4 has 36, so reaching the reversal takes at least 9 moves. If the central eccentricity or the diameter were 8 at L = 4, N = 13, the least element of its defining set would be 8, and the reversal would be within 8 moves of the central state. The clause gives 4 ⌊9/4⌋ + 0 = 8.

Falsifier

The refutation would fail if a rotation of five consecutive letters could change the inversion count by more than 4, or if the clause gave more than 8 at L = 4, N = 13.

Evidence

Exact breadth-first search over the 715 vertices at L = 4, N = 13 gives central eccentricity 12 in both conventions; the reversal is at distance 12 with left rotations and 9 with right rotations. With ⌈(t + 1)/4⌉ in place of ⌊(t + 1)/4⌋ the clause matches the central eccentricity under left rotations for L = 4, 13 ≤ N ≤ 18 (12, 12, 12, 13, 16, 16), which points to a misprint in the source. It does not match the other readings: under right rotations the central eccentricity is 13 at N = 14 against 12, and the largest directed distance between two vertices at L = 4, N = 13 is 15 in both conventions. Independently, the k = 4 clause of Conjecture 15 disagrees at (l, n) = (2, 7): 5 with left rotations, 6 with right rotations, formula 4.

The canonical source is D5/S3/Combinatorics/ShrunkenGrassmannianConjectureFifteenRefutation.lean. Its public declarations are StepDir, ReachDir, eccDir, diamDir, clauseFive, claim, and result. The frozen module state has statement identity sha256:6ecad692fa348cd171637de850505aa020a7cd1e77693602765d21fa3d89eddc. The result declaration has statement identity sha256:182d805d958d08e11824dc654994424b065f466a61477fce7329e3df435999e2. The Freeze event is sha256:3d6eda4ddacaeb2b074f7dd3946665472b134f0f37b05ac15b5838939066d2e3. Its project-level frozen prerequisite is D5/S3/Combinatorics/ShrunkenGrassmannianThreeCycleDiameter. The proof uses only the standard axioms propext, Classical.choice and Quot.sound; no sorry, native_decide, or new axiom.

Triage

Tier 1 external named conjecture, preregistered in issue #10253 before the probe. theorem (a refutation); resolution refuted. Utility kind=certified-instance; basis=refutes, with typed claim and result. The public theorem has proof_shape: content: the per-move inversion bound and its accumulation along directed paths are new propositions on the live proof path. Its admission basis is open-problem-resolution.

ASSUMED-UNVERIFIED

Whether the ceiling form of the k = 5 clause holds, for the central eccentricity under left rotations, for all L ≥ 4, N ≥ L + 9 is not settled here. The bounded literature check does not establish exhaustive worldwide novelty, priority, or the absence of an independent proof.