CayleyPy-4 Conjecture 16 fails at k = 4, L = 2, N = 5

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) for N > k. Conjecture 16 treats the inverse-closed case, in which a move rotates k consecutive letters one place in either direction:

For $k=3$ from $L\ge 2$(?): $D(L, N) = \left\lceil \frac{L (N - L)}{2} \right\rceil$ For $k=4$ from $L\ge 2$: $D(L, N) = \frac{L}{3}(N - L)$ if $3 \mid L$, $\left\lfloor \frac{L(N - L) + 2}{3} \right\rfloor$ if $3 \nmid L$. For $k=5$ for $N,L,N-L$ large enough: $D(L, N) = \left\lfloor \frac{LN + 2}{4} \right\rfloor - 2\left\lfloor \frac{L^2}{8} \right\rfloor - \mathbf{1}{L \equiv 2 \pmod{4}} , \mathbf{1}{N \equiv 2 \pmod{4}}$

Issue #10252 fixes the readings as in #10230: words are List Bool, and the diameter is read both as the largest distance from the central state [0]^L + [1]^{N−L} and as the largest distance between two vertices; the k = 5 range reads "for some constant C, all L ≥ C and N − L ≥ C".

The formal claim is the conjunction of the three clauses under either reading of the diameter, and D5/S3/Combinatorics/ShrunkenGrassmannianConjectureSixteenRefutation.result refutes it under both. The k = 3 clause alone holds: D5/S3/Combinatorics/ShrunkenGrassmannianThreeCycleDiameter.result proves it.

Issue #10252 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.

At k = 4, L = 2, N = 5 the ten vertices lie at distances 0, 1, 1, 1, 1, 2, 2, 2, 2, 3 from 00111, and 11010 is the only vertex at distance 3. The proof lists every word reached within m moves: starting from [x], each step appends all rotations of all listed words, and every word reached within m moves is in the list, by induction on m. The kernel evaluates the list for m = 2 from 00111 and finds that 11010 is absent. If the central eccentricity or the diameter were 2, the least element of its defining set would be 2, and 11010, which has two zeros, would be within two moves of 00111, which is also a vertex. Since 3 does not divide 2, the k = 4 formula gives ⌊8/3⌋ = 2.

The refutation would fail if 11010 were within two moves of 00111 under rotations of four consecutive letters in either direction, or if the k = 4 formula gave 3 at L = 2, N = 5.

Exact breadth-first search for 5 ≤ N ≤ 11 and 2 ≤ L ≤ N finds the k = 4 clause wrong at 13 pairs. At (L, N) = (2, 5), (3, 5), (3, 6), (5, 6), (6, 7), (2, 8), (6, 8), (8, 9), (9, 10), (2, 11), (9, 11) both the central eccentricity and the diameter exceed the formula by one. At (3, 9) and (6, 9) the central eccentricity equals the formula value 6 and the diameter is 7. Every mismatch has min(L, N − L) ≤ 3, and every pair with L ≥ 4 and N − L ≥ 4 in this range agrees under both readings.

The canonical source is D5/S3/Combinatorics/ShrunkenGrassmannianConjectureSixteenRefutation.lean. Its public declarations are formulaFour, formulaFive, conjSixteen, claim, and result. The frozen module state has statement identity sha256:d4efb9b91f4f74202d8789187fef8f6e3e111969aaeb081382f701d58fec3370. The result declaration has statement identity sha256:bacb17b09e6e0da67076f7e6e8be374d632a61ad01db65990a8c2c4df6a39563. The Freeze event is sha256:34620c527700187f5670eb299dab35022829f54ca91ed4742d8686daa8742a8d. 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.

Tier 1 external named conjecture, preregistered in issue #10252 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 containment of the m-move reachable set in the listed ball is a new proposition on the live proof path. Its admission basis is open-problem-resolution.

The failures lie at the boundary min(L, N − L) ≤ 3; whether the formula holds for all L ≥ 4, N − L ≥ 4 is not settled here. The k = 5 clause is not settled here. The bounded literature check does not establish exhaustive worldwide novelty, priority, or the absence of an independent proof.