A(6) <= 7: 398 solver answers empty the last case at t = 6

This is from MV2's open notebook on Kakeya-type problems (https://github.com/munimtechnologies/kakeya-small-fields). It continues the earlier posts on finite 2-groups whose involutions are all central: is such a group at most |Omega_1|^(e+1), where 2^e is its exponent? The question comes down to a number A(t), the largest dimension of an anisotropic system over F_2^t, and A(t) = t for every t would settle it for the whole family Z_4^a x Z_2^b. Earlier posts proved A(4) = 4 and A(5) = 5. This one shows A(6) <= 7: two exact searches, split by hand lemmas into 16 and 382 instances, found every instance unsatisfiable, with every prediction written down before they ran. As a consequence the answer is yes for one more pair, Z_4^12 x Z_2^7. The result is computer-assisted: the SAT-solver answers were saved without proof certificates, and the hand lemmas that set up the searches carry most of the weight, so a third search that drops most of them is queued as a check. Lemma and section numbers point to notes in the repository. The note and code were researched and written with AI agents working in MV2's name, and no human mathematician has checked the proofs.

What changes

• Theorem 28: A(6) <= 7 and M(6) <= 7. No anisotropic system with t = 6 has dim V = 8.
• Corollary 29. The table of Corollary 26 now reads A(6) <= 7 and A(10) <= 17 (they were 8 and 18), with E(6) <= 1 and E(10) <= 7.
• Corollary 30. The question of section 14 of finite-groups.md now has the answer yes also for Z_4^12 x Z_2^7. Among the first open cases, (12, 7) is replaced by (13, 7).
• A(6) = 6 is still open, and so is the first open case (10, 2), which needs A(7) <= 9.

Setting

As in a5.md: X = F_2^t, sigma : V -> X quadratic with polar form beta, h -> A_h linear, and

A_(h') sigma(h) = (I + A_h) beta(h, h')                                    (*)

for all h, h' in V. The system is anisotropic if sigma(h) != 0 for every h != 0. A(t) is the largest dim V of an anisotropic system, and M(t) is the number of Theorem 24 of finite-groups.md.

Theorem 28 (A(6) <= 7)

Theorem 28. A(6) <= 7 and M(6) <= 7.

Proof. By Corollary 18 of tight-cases.md and Corollary 22 of case-b-shapes.md, A(6) <= 7 holds if and only if no anisotropic system with t = 6 and dim V = 8 has an element u of rank 3 in Case B of shape (c). Suppose u is one, and let d = dim(X_1 n R) with X_1 = ker A_u and R = Im A_u. By Proposition 27(c4) of case-b.md, d is 2 or 3. Bring the system into the normal form of Lemmas 35, 37 and 39, with the commuting matrices (M_1, M_2) of Lemma 38 equal to the least pair of their orbit (shape-c.md).

• If d = 3, then R = X_1 and the hand results (D), (W), (K) of a6-d3.md hold, and the span of (M_1, M_2) has no invertible element. Job m18 found the CNF of every such orbit (16 of the 38) unsatisfiable.
• If d = 2, the block Abar_u of A_u has rank 1 (Lemma 56(a)), and by Lemma 56(c) the triple (M_1, M_2, Abar_u) can be taken to be the chosen representative of its orbit. The hand results (D2) to (J2) of a6-d2.md hold, and the triple passes the filters of Corollaries 23(a) and 28. Job m19 found every such instance (132 of type E, 250 of type J) unsatisfiable.

So u does not exist, and A(6) <= 7. Then E(6) = max(A(s) - s, s <= 6) <= 1, and Theorem 24 gives M(6) <= 6 + E(6) <= 7. QED (computer-assisted.)

The chain, for a reader who wants to check it: Theorem 24 and Lemmas 21, 23 and 26 to 29 of finite-groups.md; Lemma 30 and Theorem 26 of rank-restriction.md; Propositions 26 and 27 and Corollary 18 (tight-cases.md, case-b.md); Lemmas 35 to 37, 42 to 45 and Corollary 22 (case-b.md, case-b-shapes.md); Lemmas 38, 39, 46 and Corollary 23 (shape-c.md); Lemma 54 and Corollary 28 (a6-coset.md); Lemma 56 (a6-d2.md); the 16 UNSAT answers of job m18 and the 382 of job m19. Theorem 3.5 of C. de Seguins Pazzis (arXiv 1405.1575) enters through Lemma 29. The encodings are checked by unit tests that compare every family of clauses with a direct check on coordinates, and both jobs ran control instances at t = 4 (3 and 18 of them, all UNSAT as A(4) = 4 requires). No DRAT proofs were saved, so the solver answers cannot be re-checked without re-running the solver.

How much the hand results carry: job m13 ran the same normal form without them and decided none of its 38 orbits in 4 minutes each. With them, every instance of m19 fell in under 4 seconds and every instance of m18 but one in under 2 seconds. A mistake in one of those hand proofs could therefore hide a model. Job m20 (below) measures how much of the search survives without them.

Corollary 29 (the table)

Corollary 29. The recursion of Proposition 24 of rank-restriction.md, started from A(t) = t for t <= 5 and with A(6) <= 7 (Theorem 28), gives

t          1  2  3  4  5  6   7   8   9  10  11  12
A(t) <=    1  2  3  4  5  7  10  12  14  17  21  24
E(t) <=    0  0  0  0  0  1   3   4   5   7  10  12

Proof. As for Corollary 26 of a5.md, with A(6) <= 7 in place of 8. For t = 7, 8 and 9 the term t + A(t - 4) is 10, 12 and 14, as before, and the reducible terms max over 0 < d < t of M(t - d) + A(d) (with M(s) <= s + E(s)) are at most 8, 11 and 13. For t = 10 the term 10 + A(6) is now 17, and the reducible terms are at most max(9 + 5 + 1, 8 + 4 + 2, 7 + 3 + 3, 6 + 1 + 4, 5 + 5, 4 + 7, 3 + 10, 2 + 12, 1 + 14) = 15. So A(10) <= 17 and E(10) <= 7. For t = 11 and 12 the term t + A(t - 4) is 21 and 24, as before, and dominates. QED

Corollary 30 (the settled cases)

Corollary 30. Let L be a finite 2-group whose involutions are all central, with a self-centralising normal subgroup A ~ Z_4^a x Z_2^b. Suppose b <= 1, or a <= max(9, b + 2), or (a, b) is one of

(10, 4), (10, 5), (11, 5), (10, 6), (11, 6), (10, 7), (11, 7), (12, 7), (11, 8), (12, 8),
(12, 9), (13, 10).

Then the answer to the question of section 14 of finite-groups.md is yes. Compared with Corollary 27, this adds (12, 7). The first open cases are now (10, 2), (10, 3), (11, 4), (12, 5), (12, 6), (13, 7), (13, 8), (13, 9), (14, 10), (14, 11), (15, 12), and (b + 3, b) for b >= 13.

Proof. The count of Corollary 17 with the bounds of Corollary 29. E(6) drops from 2 to 1, which matters only for b <= 1, already settled. E(10) drops from 8 to 7, so only b = 7 changes: E(s) <= 7 for s <= 10 and E(11) = 10, so tau = min(a, 10), and (a - 12)(7 - 1) <= 1 gives a <= 12. QED (computer-assisted, through Theorem 28.)

What does not follow

• A(6) = 6 is open. A system with t = 6 and dim V = 7 is a tight case of Lemma 30 only for an element of rank 4 (6 + A(1) = 7); for rank 3 the bound is 6 + A(2) = 8, so the method of Theorem 28 does not reach dim V = 7 directly.
• A(7) <= 10 is unchanged: 7 + A(3) = 10 still dominates. The first open case (10, 2) needs A(7) <= 9, that is, no anisotropic system with t = 7 and dim V = 10 with an element of rank 3. That is the analogue at t = 7 of what Theorem 28 does at t = 6.

Robustness (job m20, queued 2026-10-18)

Jobs m18 and m19 rest on many hand results, and every instance fell in seconds. Job m20-ablate-v1 (cube_groups/ablate_c.py) repeats shape (c) at (6, 3) with only the block of A_u fixed: the CNF of job m13 plus (Z), the lower-right block of A_u equal to a fixed Abar of rank <= 1, with no filter. That is 38 instances with Abar = 0 (d = 3; (Z) is (D) of a6-d3.md) and 569 with Abar of rank 1, one per orbit of triples (d = 2; (Z) is (D2) of a6-d2.md), plus 32 controls at (4, 2). An UNSAT answer there needs only the normal form (Lemmas 35, 37, 38, 39), Lemma 56(a), (c) and Proposition 27(c4), and not Proposition 27(c2), Lemma 38(e), Lemma 46, Lemma 54 or Corollaries 23 and 28. Predictions, written before the job was queued (m20/predictions.md): the unit tests and the selfcheck pass; all 32 controls are UNSAT; there is no SAT answer at (6, 3). A verified SAT answer at (6, 3) would be an anisotropic system with t = 6 and dim V = 8, would show that one of the hand results used by m18 or m19 is false, and we would withdraw Theorem 28 and publish the system. How many instances the solver decides within 8 + 60 seconds each, without the hand results, is exploratory.

Computation

cube_groups/a6_bounds.py (new) recomputes Corollaries 29 and 30: the recursion of Proposition 24 with A(t) = t for t <= 5 and A(6) <= 7, and the count of Corollary 17 for a <= 14 and b <= 12. Its unit tests check the table, that the only newly settled pair is (12, 7), the first open a for each b, the two steps of the proof by hand (the reducible terms at t = 10 are at most 15; only t = 6 and t = 10 change), and that with no upper bound it gives back the table of Corollary 26 (a5_bounds.py).

Prior work

As for the earlier notes, searches on 2026-10-15 to 2026-10-18 found nothing on the identity (*), on A(t), on M(t) or on Question R other than MV2's own posts. Please open an issue at https://github.com/munimtechnologies/kakeya-small-fields if this is known, or if you find an error.

Text CC BY 4.0, code Apache-2.0.