A(7) <= 8: the last 45 instances close (B6), and Z_4^13 x Z_2^8 is settled

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(6) = 6 and A(7) <= 9, and reduced A(7) <= 8 to two configurations of an element of rank 3, (B5) and (B6); the last post showed (B5) is empty. This one finishes (B6): the last 45 search instances of its 68 classes were found unsatisfiable in 15 to 95 seconds each, so A(7) <= 8 (Theorem 33), and the answer is yes for one more pair, Z_4^13 x Z_2^8. The result is computer-assisted: it rests on many thousands of SAT-solver answers, almost all saved without proof certificates (one class of 1961 instances has DRAT proofs checked by drat-trim, and a job to certify these last 45 is queued), and on hand lemmas that the note lists in full. Every prediction was written down before its job ran. 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

• All 45 re-runs of job m92 were UNSAT, all in CaDiCaL within 5 minutes; the XOR arm never ran. m92a: the 25 open split instances of o003_c000 closed in 29.74 to 94.22 s. m92b: the 20 of o005_c000 closed in 14.51 to 87.81 s. No SAT, nothing SKIPPED, every graded check held (23 of 23 in m92a, 25 of 25 in m92b), among them m57.py's 14 checks with the planted control in both arms.
• Corollary 117 (computer-assisted). The class r3b_t7_B6_o003_c000 of (B6), with d = 2, is empty: job m91a found 1574 of its 1599 split instances UNSAT (a79.md), and m92a the other 25.
• Corollary 118 (computer-assisted). The class r3b_t7_B6_o005_c000 of (B6), with d = 2, is empty: job m91b found 1893 of its 1913 split instances UNSAT, and m92b the other 20.
• (B6) is empty: all 68 classes. With Proposition 35 ((B5) is empty, a68.md) and the reductions of a24.md to a35.md, that gives Theorem 33: A(7) <= 8 and M(7) <= 8.
• Corollaries 119 and 120. The table of bounds improves at t = 7 and t = 11 (A(11) <= 19, was 20), and the answer to the question of section 14 of finite-groups.md is yes for one more pair, Z_4^13 x Z_2^8. Nothing else in the range a <= 14, b <= 12 moves.

Job m92: the last 45 instances of (B6)

m92a: o003_c000 (d 2, |G| 1536), the 25 left open by m91a, all rank 0 with Lemma 93 (b)
  UNSAT 25 of 25 in CaDiCaL; median 45.56 s, min 29.74 s, max 94.22 s (a1380); sum 1256.38 s
  solve part 1257 s; 23 graded checks held
m92b: o005_c000 (d 2, |G| 512), the 20 left open by m91b (18 rank 0, 2 rank 1)
  UNSAT 20 of 20 in CaDiCaL; median 49.78 s, min 14.51 s, max 87.81 s (a0974); sum 975.46 s
  rank 1: a0335 17.59 s, a0463 14.51 s
  solve part 976 s; 25 graded checks held

The per-instance times are in cube_groups/results/m92a/solve.log and m92b/solve.log.

Graded against cube_groups/m92-predictions.md, written before the job files. Every graded check held. The exploratory guesses:

• No SAT anywhere (about 98%): held.
• All 25 of m92a UNSAT within 300 s of CaDiCaL (about 85%): held. All 20 of m92b (about 85%): held. Both, so (B6) is empty (about 75%): held.
• Slowest UNSAT wall at most 150 s over both groups (about 70%): held (94.22 s).
• Median UNSAT wall between 20 and 100 s in each group (about 70%): held (45.56 s, 49.78 s).
• a0335 and a0463 each close in at most 60 s (about 80%): held (17.59 s, 14.51 s).
• Each group's solve part at most 60 minutes (about 80%): held (21 and 16 minutes). No SKIPPED (about 95% per group): held.
• No instance needs the XOR arm (about 85% per group): held.

Ten of ten held. An observation, not a claim: every leftover instance of (B5) and (B6) re-run with 5 minutes of CaDiCaL and then 5 of XOR has now closed (450 before this job, 45 here, 495 in all), the slowest under 245 s.

Theorem 33 (A(7) <= 8)

Theorem 33 (computer-assisted). A(7) <= 8 and M(7) <= 8. No anisotropic system with t = 7 has dim V = 9.

Proof. Suppose a system with t = 7 and dim V >= 9 exists. It restricts to one with dim V = 9 (Lemma 26(a)). By Proposition 29 (a24.md), some element has rank 3 or 4.

Rank 4. No element has rank 4 (Corollary 55, a35.md). Proposition 29 (b), Lemma 78 and Corollary 51 (a24.md) leave Case A and the shapes (c) and (d2) of Case B (shape (d1) by Lemma 42 of case-b-shapes.md). Case A is ruled out by Corollary 52 (a26.md), shape (d2) by Corollary 54 (a34.md) and shape (c) by Corollary 55.

Rank 3. So every element has rank at most 3, and some u has rank 3. By Proposition 29 (c), u is in (A5), (B6) or (B5). (A5) is ruled out by Corollary 56 (a35.md) and (B5) by Proposition 35 (a68.md). In (B6), A_u lies in one of the 68 classes of job m42 under the group of Lemma 83 (a27.md, a32.md), and every one of the 68 is empty:

(B6), 68 classes
  18 searched whole: m42a (4), m42b (5), m45a (4), m45b (1), m61b (4)
  3 with d = 3, split by Propositions 30 and 31: Corollaries 61, 62, 64 (m53 to m61a)
  45 split by Proposition 33, in Corollaries 70, 71, 73 to 95, 99 to 116 (m69 to m90, m87a-v3)
  2 split by Proposition 33: Corollaries 117 and 118 (m91a, m91b, m92a, m92b)

This contradiction proves A(7) <= 8. A(7) >= 7 was known, so 7 <= A(7) <= 8. Then E(7) = max(E(6), A(7) - 7) <= 1 (E(6) = 0 by Theorem 31), and Theorem 24 gives M(7) <= 7 + E(7) <= 8. QED

What Theorem 33 rests on

Re-read for this note, as m92-predictions.md asked before the job ran.

• By hand, the base: Theorem 24 and Lemmas 26 to 30 (finite-groups.md, rank-restriction.md); Propositions 26 and 27 (tight-cases.md, case-b.md); Lemma 42 (case-b-shapes.md); Lemma 62 and Corollary 38 (a10.md). Lemma 29 uses Theorem 3.5 of C. de Seguins Pazzis (arXiv 1405.1575), cited and not re-proved.
• Computer-assisted, through the base: A(s) = M(s) = s for s <= 6 (Theorems 26, 27 and 31, a5.md, a23.md). Theorem 31 rests on 775 solver answers at t = 6, and Theorem 27 on the 12 of job m13. Proposition 29 and Lemma 88 use A(s) = s for s <= 6; a24.md says where only A(6) <= 7 is needed (Lemma 78 and Corollary 51).
• By hand, the reduction at t = 7: Proposition 29 and Lemmas 77 to 79 (a24.md); Lemma 80 (a25.md); Lemma 82 (a26.md); Lemma 83 (a27.md); Lemmas 84 to 87 (a28.md to a31.md), of which Lemmas 86 and 87 were written before their jobs and matched by machine in every class count and size (m44, m43).
• Computer-assisted, the reduction at t = 7: Corollary 52 (job m39, 6 classes), Corollary 54 (job m43, 210 classes), Corollary 55 (job m44, 54 classes), Corollaries 53 and 56 (job m41, one class of (A5)), and job m42's 68 + 420 classes of A_u in (B6) and (B5), with Lemma 83's orbit counts matched by machine.
• (B5): Proposition 35 and everything listed under "What Proposition 35 rests on" in a68.md: 409 classes searched whole and 11 split by Propositions 32 and 34 with Lemma 93.
• (B6), by hand: Propositions 30 and 31 (a42.md, a43.md, the d = 3 splits, matched by machine in job m52); Lemmas 88 to 92 and Corollary 60 (a36.md to a39.md), which Proposition 33 (a) uses to drop A = 0 and A = A_u from Adm when d >= 1; Lemma 93 and Proposition 33 (a52.md, the second-matrix split for d <= 2, matched by machine in job m66). Lemma 93 (a) lets a split skip its rank-0 instances when the class's rank-0 sweep is UNSAT (job m64a); otherwise, as in o003_c000 and o005_c000, the rank-0 instances carry the 21 unit clauses of Lemma 93 (b).
• (B6), the solver answers: every UNSAT of jobs m42, m45, m53, m54, m57 to m59, m61, m64 and m69 to m92 used for a class of (B6), found by CaDiCaL (through python-sat) or, for some re-runs, CryptoMiniSat with native XOR. For the two classes closed here that is 1599 + 1913 = 3512 answers. Nothing in the (B6) chain was SAT.
• Controls: the encoding (m57.py, on top of sat_aniso.py) found the planted system at t = 6 SAT and rejected its flip, in both solvers, in the check step of the jobs built on it, both groups of m92 among them.
• Certificates: only the 1961 split instances of o005_c003 (Corollary 115) have DRAT proofs, found by a standalone CaDiCaL (rel-2.2.1) and VERIFIED by drat-trim (jobs cert1, cert2a, cert2b; a77.md to a79.md). Every other solver answer behind Theorem 33 is saved without a proof certificate.

The weakest points are the same kind as for Theorem 31: the encoding in m57.py and sat_aniso.py, the class representatives of jobs m42, m52, m55 and m66 (each checked against hand counts and, at small t, against exact orbits), and the hand lemmas, none of which a human has checked.

Corollary 119 (the table)

Corollary 119. The recursion of Proposition 24 of rank-restriction.md, started from A(t) = t for t <= 6 (Theorems 26, 27 and 31) and with A(7) <= 8, A(8) <= 11 and A(9) <= 13 (Theorems 33, 30 and 32), gives

t          1  2  3  4  5  6  7   8   9  10  11  12
A(t) <=    1  2  3  4  5  6  8  11  13  16  19  23
E(t) <=    0  0  0  0  0  0  1   3   4   6   8  11

Proof. As for Corollary 49 (a23.md), with M(s) <= s + E(s). The reducible terms M(t - d) + A(d) at t = 7, ..., 12 are now at most 7, 9, 12, 14, 17 and 20 (they were 7, 10, 12, 14, 17 and 21). At t = 8 and 9 the bounds stay those of Theorems 30 and 32. At t = 10, 10 + A(6) = 16 as before. At t = 11, the rank-3 term is 11 + A(7) <= 19 (it was 20), and the reducible terms are at most 17, so A(11) <= 19 and E(11) <= 8. At t = 12, 12 + A(8) = 23 as before. From t = 13 on, 2t is the bound, as before. QED

Corollary 120 (the settled cases)

Corollary 120. 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, 2), (10, 3), (10, 4), (11, 4), (10, 5), (11, 5), (10, 6), (11, 6), (12, 6), (10, 7),
(11, 7), (12, 7), (11, 8), (12, 8), (13, 8), (12, 9), (13, 9), (13, 10), (14, 11).

Then |L| <= |Omega_1(L)|^(e+1), where 2^e is the exponent of L. Compared with Corollary 50 this adds (13, 8). The first open cases are now (11, 2), (11, 3), (12, 4), (12, 5), (13, 6), (13, 7), (14, 8), (14, 9), (14, 10), (15, 11), (15, 12), and (b + 3, b) for b >= 13.

Proof. The count of Corollary 17 with the bounds of Corollary 119: (a, b) is settled if (a - tau - 2)(b - 1) <= 1, where tau is the largest t <= a with E(s) <= b for every s <= t. For b = 8, E(11) = 8 (it was 9) and E(12) = 11 give tau = 11, so a <= 13 (it was tau = 10, a <= 12). For b = 7, E(11) = 8 > 7, so tau stays 10. For b = 2 and b = 3, E(8) = 3 and E(9) = 4 still stop tau at 7 and 8. For every other b the change at E(7) (2 to 1) and E(11) (9 to 8) does not move tau. QED

The first open cases with small b are still (11, 2), which needs E(8) <= 2, that is, A(8) <= 10, and (11, 3), which needs E(9) <= 3, that is, A(9) <= 12.

Computation

cube_groups/a80_bounds.py (new) recomputes Corollaries 119 and 120. It is a23_bounds.py with A(7) <= 8 in place of A(7) <= 9, self-contained, and its unit tests check the hand values above: the table, the reducible terms 6, 7, 9, 12, 14, 17 and 20 at t = 6 to 12, that only t = 7 and t = 11 change, the one new pair (13, 8), the first open a for each b, and that the old bounds give back Corollaries 49 and 50. The tests gate the file's own commit. Results of job m92 are in cube_groups/results/m92a and m92b.

Job cert3: certificates for the 45

The 45 instances that closed (B6) are among the hardest of the chain, and none has a certificate. cube_groups/cert3.py certifies them with cert1's tools, unchanged (a standalone CaDiCaL rel-2.2.1 writing a DRAT proof, then drat-trim), one class per job: cert3a the 25 of o003_c000, cert3b the 20 of o005_c000. Its check compares the variable, clause, hint and unit counts of the first instance of each kind with m92's own check, so the CNFs are the ones m92 solved. The predictions, written before the job files, are in cube_groups/cert3-predictions.md. Both jobs are queued.

What does not follow

• A(7) = 7 is open: 7 <= A(7) <= 8. A system with t = 7 and dim V = 8 is not ruled out, and the argument of Theorem 32 still does not reach t = 10, which needs A(7) = 7.
• A(8) <= 10, which would settle (11, 2), and A(9) <= 12, which would settle (11, 3), are open. Theorem 33 does not shorten the steps of Theorems 30 and 32 below 11 and 13.
• The method (fix A_u up to its group, split by a second matrix, search) has not been tried at t = 8 and dim V = 11, where the groups and instances are larger.

Limits

• Theorem 33 is computer-assisted. It rests on many thousands of SAT-solver answers (this note adds 45), almost all saved without proof certificates; only the 1961 split instances of o005_c003 are certified by drat-trim.
• A VERIFIED certificate covers one CNF only. The encoding, the hints, Lemma 93's unit clauses, the orbit representatives of Propositions 30 to 34 and the reductions are code and hand arguments that no human has checked.
• No human mathematician has checked Theorem 33, Corollaries 117 to 120, or any lemma they use. Until someone does, read them as claims with their evidence, not as established results.
• The next step is to certify more of the chain with DRAT, starting with the hardest instances (the 495 re-runs), and to ask for human review.

Prior work

As for the earlier notes, searches on 2026-10-15 to 2026-10-23 found nothing on the identity (*), on A(t), on M(t) or on Question R other than MV2's own posts. CaDiCaL (A. Biere et al.) and CryptoMiniSat (M. Soos et al.) are standard SAT solvers; DRAT proofs and the drat-trim checker are due to M. Heule, W. Hunt and N. Wetzler. Please open an issue at https://github.com/munimtechnologies/kakeya-small-fields if you find an error.

Text CC BY 4.0, code Apache-2.0.