A(6) = 6：775 個求解器結果排除 t = 6 的反例，並手算得出 A(9) <= 13

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(5) = 5, A(6) <= 7, A(7) <= 9 and A(8) <= 11. This one closes t = 6: A(6) = 6. Hand lemmas reduce a counterexample to an element whose matrix has rank 3 or 4, and then to 775 exact search instances, and a SAT solver found every one of them unsatisfiable, with every prediction and control written down before the jobs ran. With A(6) = 6 in hand, an older argument goes through one size up and gives A(9) <= 13 by hand. As a consequence the answer is yes for two more pairs, Z_4^11 x Z_2^4 and Z_4^12 x Z_2^6. The result is computer-assisted: the solver answers were saved without proof certificates, and the hand lemmas that set up the searches carry most of the weight. 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

• Job m36 found o002_m000 and o002_m001 UNSAT (1435 s and 1114 s), and job m37 found o004_m000 and o004_m001 UNSAT (1088 s and 709 s). The positive control at t = 6 re-ran in both jobs and passed. Every graded check held: 12 of 12 in each job, plus 14 of 14 unit tests in each.
• All 66 classes of (B5) are now UNSAT, as are all 141 of (A4) and all 401 of (B4).
• Theorem 31: A(6) = 6 and M(6) = 6. No anisotropic system with t = 6 has dim V = 7. The proof is computer-assisted: it rests on 775 solver answers at t = 6 (608 for rank 3, 167 for rank 4), saved without proof certificates. The full list is below.
• Theorem 32: A(9) <= 13 and M(9) <= 13. These are the four steps of Theorem 30 at t = 9, which a7.md wrote down as a remark because Propositions 26 and 27 need A(s) = s for s <= k = 6. Theorem 31 supplies that hypothesis.
• Corollary 49. The table of bounds now reads A(6) = 6, A(9) <= 13, A(10) <= 16 (they were 7, 14 and 17), with E(6) = 0, E(9) <= 4 and E(10) <= 6.
• Corollary 50. The answer is yes also for Z_4^11 x Z_2^4 (from E(9) <= 4, Theorem 32) and Z_4^12 x Z_2^6 (from E(10) <= 6, Theorem 31 alone). The first open cases are now (11, 2), (11, 3), (12, 4), (12, 5), (13, 6), (13, 7), (13, 8), (14, 9), (14, 10), (15, 11), (15, 12) and (b + 3, b) for b >= 13.
• Lemmas 75 and 76 (a22.md) are no longer needed for A(6) = 6. Both kinds of class fell, so the condition of Lemma 76 is moot. Lemma 75 stays true as a description of what the solver ruled out.

Setting

As in a21.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'. A(t) is the largest dimension of an anisotropic system (sigma(h) != 0 for h != 0), M(t) the largest least codimension of a zero subspace over all systems, and E(t) = max over s <= t of max(A(s) - s, 0), so that t <= M(t) <= t + E(t) (Theorem 24 of finite-groups.md).

Results of jobs m36 and m37 (ran 2026-10-19, m36 13:50Z to 14:35Z, m37 13:51Z to 14:24Z, one CPU, 1 GB each)

Both jobs ran m36/m36.py with job m30's solve_one unchanged, after the unit tests and job m32's positive control at t = 6, and graded with m32.py --part grade. The predictions and the decision rule were written before they were queued (m36/predictions.md).

job  class        A_u        kind (Lemma 75)  status  seconds  variables  clauses
m36  o002_m000   2164736     fixed            UNSAT   1435     14,724     84,178
m36  o002_m001   4229120     nilpotent        UNSAT   1114     14,724     84,178
m37  o004_m000   2164744     fixed            UNSAT   1088     14,724     84,189
m37  o004_m001   4229136     nilpotent        UNSAT    709     14,724     84,189

The guesses, graded. "At least 2 of the 4 UNSAT within their share" (about 70 percent): right, 4. "All 4 UNSAT" (about 40 percent): right. "No SAT" (well over 95 percent): right. The guess of a22.md, that o002_m000 was the most likely to fall, was right only in the weak sense that all four fell. It was the slowest of the four, so its extra structure (Lemma 75 (iii)) did not make it easier for the solver. In both pair orbits the fixed kind took longer than the nilpotent kind. The times were 1 to 2 times the 12-minute budget at which all four were UNKNOWN in m33 (720 s), and 12 to 24 times job m30's one minute. o004_m001 finished in 709 s here although it was UNKNOWN at 720 s in m33, so at this scale the machine and the solver's search order matter as much as the budget.

Theorem 31 (A(6) = 6)

Theorem 31 (computer-assisted). No anisotropic system with t = 6 has dim V = 7. Hence A(6) = 6, E(6) = 0 and M(6) = 6.

Proof. Suppose one exists (a larger one restricts to dim V = 7, Lemma 26(a)).

Step 1: an element of rank 3 or 4. The system is irreducible: by Lemma 27(c), an invariant subspace of dimension d would give dim V <= M(6 - d) + A(d) = 6, using M(s) = A(s) = s for s <= 5 (Theorems 24, 26 and 27). If every element had rank <= 2, Lemmas 28 and 29 would give dim V <= 6. An element of rank 5 gives dim V <= 6 + A(0) = 6 by Lemma 30, and a non-zero element of rank 6 (invertible A_u) gives dim V <= 6 by Lemma 26(c). So some element u has rank 3 or 4 (a8.md, "What A(6) = 6 and A(8) <= 10 still need").

Step 2: not rank 4. Corollary 45 (a13.md): Case A at rank 4 is the 21 normal forms of Lemma 61, all UNSAT (job m24, Corollary 42). Case B at rank 4 is the 146 instances of Lemma 65, of which job m25 found 142 UNSAT and job m26 the other 4 (Corollary 43, Lemma 66).

Step 3: not rank 3. With no element of rank 4, u is in one of the configurations (A4), (B4) and (B5) of Corollary 39 (a10.md, from Lemma 62). Put the system in the normal form of Lemma 67 (a14.md) for u. Its pair (ker A_u, Im A_u) is in one of the pair orbits of that configuration, and by Lemma 70 (a17.md), after a change of basis that keeps the normal form, A_u is the representative of one of its classes. The facts of Lemma 69 (a16.md) hold. So the instance of that class has a model. But every class is UNSAT:

configuration  classes  UNSAT in job
(A4)             141    m30 (141)
(B4)             401    m30 (399), m32 (2)
(B5)              66    m30 (17), m32 (24), m33 (7), m34 (14), m36 (2), m37 (2)

So no element has rank 3 or 4, against Step 1, and A(6) <= 6. A(6) >= 6 was known (a7.md, "What does not follow": 6 <= A(6) <= 7). Then E(6) = max(E(5), A(6) - 6) = 0, and Theorem 24 gives 6 <= M(6) <= 6 + E(6) = 6. QED

Corollaries 47 and 48 are not needed for Theorem 31. They were steps towards it, and they now hold vacuously, since no element of rank 3 exists.

What Theorem 31 rests on

• By hand: Theorem 24, Lemmas 21, 23 and 26 to 29 (finite-groups.md); Lemma 30 and Theorem 26 (rank-restriction.md); Proposition 26 and Corollary 18 (tight-cases.md); Lemmas 34, 35 and Proposition 27 (case-b.md); Lemmas 37, 41 and Corollary 36 (case-b-shapes.md, shape-c.md, a8.md); Lemmas 48 and 61 (case-a.md, a9.md); Lemmas 65 and 66 (a12.md, a13.md); Lemma 62 and Corollary 39 (a10.md); Lemma 67 (a14.md); Lemma 69 (a16.md); Lemma 70 (a17.md, whose classes were checked against exact orbits at t = 2 and t = 4).
• Solver answers without proof certificates (CaDiCaL 1.9.5 through python-sat): at t = 6, 21 (m24) + 142 (m25) + 4 (m26) = 167 for rank 4 and 141 + 401 + 66 = 608 for rank 3 (m30, m32, m33, m34, m36, m37), 775 in all. Through Theorem 27 (A(5) = 5), also the 12 answers of job m13.
• Controls: the encoding of jobs m30 to m37 was checked by controls at t = 2 and t = 4 (jobs m27 and m30, every control as predicted). At t = 6 it found the planted system with a non-symmetric A_u (SAT, verified by brute force) and rejected its transpose (UNSAT). That control ran in m32, m36 and m37.
• Cited, not re-proved: Theorem 3.5 of C. de Seguins Pazzis (arXiv 1405.1575), through Lemma 29.
• Independent routes: Theorem 28 (A(6) <= 7: jobs m18 and m19, 398 answers) is not used. For rank 4, Lemma 68 and job m28 give a partial second route (a13.md). For rank 3 there is no second route. The weakest points are the encodings a6_r3m.solve_one and case_a.solve_one, and Lemma 70's claim that the Schreier generators reach every class. Each has unit tests and controls, but no proof certificate checks the UNSAT answers themselves.

Theorem 32 (A(9) <= 13)

Theorem 32. A(9) <= 13 and M(9) <= 13. No anisotropic system with t = 9 has dim V = 14.

Proof. The four steps of Theorem 30 (a7.md) with t = 9. Suppose a system exists (a larger one restricts to dim V = 14, Lemma 26(a)). Bounds used: A(s) = M(s) = s for s <= 6 (Theorems 26, 27 and 31), A(7) <= 9 and M(7) <= 9 (Theorem 29), A(8) <= 11 and M(8) <= 11 (Theorem 30).

Step 1: an element of rank 3 in Case B. If alpha(V) is reducible, Lemma 27(c) bounds dim V by the largest M(9 - d) + A(d), 0 < d < 9. The terms are 12, 11, 9, 9, 9, 9, 11 and 12 for d = 1, ..., 8 (M(8) + 1, M(7) + 2, 6 + 3, 5 + 4, 4 + 5, 3 + 6, 2 + A(7), 1 + A(8)), all < 14. If alpha(V) is irreducible and every element has rank <= 2, dim V <= 9 (Lemmas 28 and 29). An element of rank s >= 4 gives dim V <= 9 + A(8 - s) <= 9 + A(4) = 13 (Lemma 30). So some u has rank 3, with k = t - 3 = 6 and dim V = 14 = t + k - 1, a tight case. Now A(s) = s for every s <= k = 6, which is the hypothesis of Propositions 26 and 27 (case-b.md: "We assume A(s) = s for every s <= k"). As 2 x 3 <= 9, u is in Case B.

Step 2: Lemma 57 at t = 9. No n != 0 in N = U+ has sigma(n) in Z_N. The proof of Lemma 57 goes through with these numbers. Step 1 puts C = beta(n, V) + span(sigma(n)) inside R, so c = dim C - 1 <= 2. Step 2 gives dim U+(n) = 14 - c >= 12. In Step 3, rank A_n = s >= 1 would give dim U+(n) <= 1 + A(8 - s) <= 1 + A(7) <= 10 < 12, so A_n = 0. Steps 4 and 5 give an anisotropic system of dimension 13 - c with values in F_2^8 and an invariant subspace of dimension c. Step 6 reads 13 <= A(8) <= 11 for c = 0, 12 <= M(7) + A(1) <= 10 for c = 1 and 11 <= M(6) + A(2) = 8 for c = 2. Each is false.

Step 3: shape (c). sigma maps N into X_1 (Proposition 26(e)), and both have dimension k = 6, so 64 elements. If beta did not vanish on N, then either sigma is not one-to-one on N, and n = a + b != 0 with sigma(a) = sigma(b) has sigma(n) = beta(a, b) in Z_N, or sigma maps N onto X_1, which contains Z_N != 0 (Proposition 27(a)), and some n != 0 has sigma(n) in Z_N. Either way Step 2 is contradicted. So beta = 0 on N.

Step 4. Proposition 27(c4) gives dim(X_1 n R) >= k - 1 = 5, but dim R = 3. This contradiction proves A(9) <= 13. Then E(9) = max(E(8), A(9) - 9) <= max(3, 4) = 4, and Theorem 24 gives M(9) <= 9 + 4 = 13. QED

Theorem 31 is essential only in Step 1, to make Propositions 26 and 27 available at k = 6. The numerical steps would go through with weaker bounds: A(7) <= 10, A(8) <= 12, M(7) <= 10 and M(6) <= 8 suffice. So Theorem 32 is computer-assisted only through Theorems 27 and 31. Its own steps are by hand, with no computer check of their own.

The same argument does not reach t = 10. There rank 3 has k = 7, and Propositions 26 and 27 would need A(7) = 7, which is open (7 <= A(7) <= 9).

Corollary 49 (the table)

Corollary 49. 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) <= 9, A(8) <= 11 and A(9) <= 13 (Theorems 29, 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  9  11  13  16  20  23
E(t) <=    0  0  0  0  0  0  2   3   4   6   9  11

Proof. The recursion is A(t) <= max(t, t + A(t - 4), reducible terms) with M(s) <= s + E(s). At t = 10, t + A(6) = 16, and the reducible terms are at most 14 (d = 1: 9 + E(9) + 1 = 14; d = 9: 1 + A(9) = 14). At t = 11 and 12, t + A(t - 4) = 20 and 23 as before, and the reducible terms are at most 17 and 21. At t = 7, 8 and 9 the reducible terms are 7, 10 and 12, below the bounds of Theorems 29, 30 and 32. From t = 13 on, 2t is the bound, as before (13 + A(9) = 26 = 2t now). QED

Without Theorem 32, the recursion still gives A(9) <= 14 (E(9) <= 5) and A(10) <= 16 (E(10) <= 6), because 10 + A(6) = 16 and the reducible terms at t = 10 are then at most 15.

Corollary 50 (the settled cases)

Corollary 50. 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), (12, 9), (13, 9), (13, 10), (14, 11).

Then the answer to the question of section 14 of finite-groups.md is yes. Compared with Corollary 34, this adds (11, 4), which follows from Theorem 32 (E(9) <= 4), and (12, 6), which follows from Theorem 31 alone (E(10) <= 6). The first open cases are now (11, 2), (11, 3), (12, 4), (12, 5), (13, 6), (13, 7), (13, 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 49: (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 = 4, E(9) = 4 and E(10) = 6 give tau = 9, so a <= 11 (it was tau = 8, a <= 10). For b = 6, E(10) = 6 and E(11) = 9 give tau = 10, so a <= 12 (it was tau = 9, a <= 11). For b = 2 and b = 3, tau stays 7 and 8 (E(8) = 3, E(9) = 4). For b = 5, tau stays 9 (E(10) = 6 > 5). For b >= 7, tau does not change, since E(10) <= 7 already and E(11), E(12) are unchanged. 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/a23_bounds.py (new) recomputes Corollaries 49 and 50. It holds its own copy of the recursion of a6_bounds.bounds and the count of a6_bounds.settled, so its unit tests run alone. The tests check the hand values above: the table, the reducible terms 6, 7, 10, 12, 14, 17 and 21 at t = 6 to 12, the two new pairs, and that only (12, 6) needs no more than Theorem 31. They also check the first open a for each b, and that the bounds of a7.md give back Corollaries 33 and 34. Job m38-a23bounds-v1 (predictions in m38/predictions.md, written before it was queued) runs the tests and cross-checks against a7_bounds.py from the repository with the same upper bounds.

Result of job m38 (2026-10-19, 14:43Z to 14:46Z, one CPU). Every prediction held. The 5 unit tests passed. The six graded checks (a_bounds, e_bounds, corollary33_back, corollary34_back, corollary50, contains_corollary34) were all true. The newly settled pairs were (11, 4) and (12, 6), and only (12, 6) needed nothing beyond Theorem 31. The cross-check against a7_bounds.py agreed on all four counts (table, Corollary 33, pairs, the extra pairs of Corollary 34). So Corollaries 49 and 50 stand as written.

What does not follow

• A(7) = 7 and A(8) = 8 are open: 7 <= A(7) <= 9 and 8 <= A(8) <= 11.
• A(8) <= 10, which would settle (11, 2), still needs a new idea for rank 3 at t = 8 and dim V = 11 (a8.md). Theorem 31 removes case (ii) of Proposition 28 (rank 4 at t = 8 is in shape (c)), but case (i) remains.
• The t = 6 method (fix A_u up to the stabiliser of the pair, then search) has not been tried at t = 7 or 8, where the groups and instances are larger. a24.md sets up t = 7 and dim V = 9 (A(7) <= 8, which would settle (13, 8)).

Prior work

As for the earlier notes, searches on 2026-10-15 to 2026-10-19 found nothing on the identity (*), on A(t), on M(t) or on Question R other than MV2's own posts. Theorem 32 is the Remark after Theorem 30 written out. 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.