Kakeya 型問題： (B5) 的 420 個類別均不可滿足，A(7) ≤ 8 現只取決於 (B6)

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, A(7) <= 9 and A(8) <= 11. The next step, A(7) <= 8, would settle the pair Z_4^13 x Z_2^8, and hand lemmas plus earlier searches reduce it to two configurations of an element of rank 3, called (B5) and (B6). This note closes the first: all 420 classes of (B5) are unsatisfiable (Proposition 35), the last 7 search instances closing in 11 to 38 seconds each. So A(7) <= 8 is now exactly the statement that (B6) is empty, and 20 of its 68 classes are left. The result is computer-assisted: it rests on many SAT-solver answers saved without proof certificates, and on hand lemmas listed in the note. Every prediction was written down before its job ran, including two that missed. 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

Every graded check of the three jobs held (23 of 23 in m80r, 26 of 26 in m79a, 24 of 24 in m79b), among them m57.py's own 14 checks with the planted control in both arms, and the structure, |G|, |Adm| and class or orbit counts by rank on X_1 of every class split, equal to jobs m74 and m66. No SAT.
Corollary 98 (computer-assisted). The class r3b_t7_B5_o005_c005 of (B5), with d = 2, is empty. Jobs m78a and m78b found 6713 of its 6720 split instances of rank 1 and 2 on X_1 UNSAT (a67.md). Job m80r found the other 7, all of rank 1, UNSAT in CaDiCaL within 5 minutes: the slowest took 37.13 s, the median 20.94 s. The XOR arm never ran. The class's rank-0 sweep was UNSAT in job m64b, so by Lemma 93 (a) the instances of rank 1 and 2 are all that is needed.
Proposition 35 (computer-assisted). At t = 7 and dim V = 9, (B5) is empty: no anisotropic system with t = 7 and dim V = 9 has an element of rank 3 in the configuration (B5). All 420 classes of A_u in (B5) are now UNSAT (below). With Corollaries 55 and 56, A(7) <= 8 is now exactly the statement that (B6) is empty.
(B6) is unchanged at 48 of 68. Jobs m79a and m79b split three of its 20 open classes and left 42 instances open (below). Job m82 re-runs them.

What Proposition 35 rests on

Re-read for this note, as m80-predictions.md asked before m80 ran:

The configuration and its classes. Proposition 29 (a24.md, by hand) puts every element of rank 3 in (A5), (B6) or (B5) when there is none of rank 4. Corollary 55 (a35.md, computer-assisted) rules out rank 4. Lemma 83 (a27.md, by hand) gives (B5)'s 49 orbits of (ker A_u, Im A_u), and job m42 its 420 classes of A_u, with Lemma 83's orbit count matched by machine (a32.md).
The direct searches. Jobs m42 to m59 searched the classes of (B5) whole, one class per instance, and closed 409 of 420 (job m59b, a49.md). The steps are in the status paragraph of README.md and in notes a32.md to a49.md.
The split classes. Proposition 32 (a45.md, by hand, matched by machine in job m55) splits the classes with d = 3, and Proposition 34 (a58.md, by hand, matched by machine in job m74) the three left with d = 2, by the orbit of the second matrix A_(h_1). Lemma 93 (a52.md, by hand) lets the later splits drop their instances of rank 0 on X_1 when the class's rank-0 sweep is UNSAT (part (a); job m64b), and adds unit clauses to them otherwise (part (b)); the splits before it (jobs m59b, m60, m62) ran their rank-0 instances plain. The last eleven classes closed this way: Corollary 63 (two classes, a51.md), Corollaries 65 and 66 (a55.md), 67 (a56.md), 68 (a57.md), 69 (a58.md), 72 (a60.md), 96 and 97 (a67.md) and 98 (here): 409 + 11 = 420.
Solver answers. Every UNSAT is a CaDiCaL or CryptoMiniSat answer saved without a proof certificate. Nothing in the (B5) chain was SAT.

Job m80r: the last 7 instances of (B5)

instance (rank 1)   m55 index   CaDiCaL     cap
a1774               12342       11.50 s     300 s
a3821               262198      20.94 s     300 s
a3845               262534      13.21 s     300 s
a4910               546834      20.68 s     300 s
a4982               560182      22.34 s     300 s
a5005               561206      37.13 s     300 s
a5032               564278      27.50 s     300 s

The solve part took 153 s. The guesses of m80-predictions.md, written before it ran: all 7 UNSAT within 5 minutes of CaDiCaL (about 80%), held; all within 60 s (about 65%), held; no XOR arm needed (about 80%), held. An observation, not a claim: each of the 7 closed in 11 to 38 s, just past the 10 s budget that left them open, which matches what a1240 did in m78r (9.89 s after an UNKNOWN at 10.01 s).

Jobs m79a and m79b: three (B6) classes with an open sweep

CaDiCaL, 10 to 20 s   planned   UNSAT   open            median wall   slowest   job
o008_c000 (d = 1)     2023      2002    21 (19 r0, 2 r1)   1.12 s     9.64 s    m79a
o008_c001 (d = 1)     1287      1280    7 (r0)             1.07 s     17.77 s   m79a
o008_c003 (d = 1)     1975      1961    14 (r0)            1.12 s     18.93 s   m79b

The rank-0 instances carried the 21 unit clauses of Lemma 93 (b), since the three sweeps were open in job m64a. No instance was SKIPPED. The solve parts took 4810 s for 3310 instances (m79a) and 2866 s for 1975 (m79b), about 1.45 s per instance with overhead. The open instances, by position k in m66's order:

o008_c000 r0: a0028 a0110 a0196 a0282 a0325 a0594 a0671 a0758 a1047 a1144 a1211 a1230 a1376
              a1510 a1908 a1947 a1990 a1996 a2014
o008_c000 r1: a0619 (m66 index 9735) a0658 (10264)
o008_c001 r0: a0016 a0102 a0174 a0260 a0521 a0619 a0775
o008_c003 r0: a0038 a0123 a0255 a1105 a1129 a1177 a1201 a1593 a1797 a1806 a1903 a1915 a1972
              a1973

An observation, not a claim: the open roots repeat by m66 index across the four classes of pair orbit 8 split so far. Indices 512, 1536, 3584 and 32768 are open in all three classes here, and 512, 1536 and 32768 were open in o008_c002 too (job m71a, a61.md), where they closed at 300 s.

The guesses of m79-predictions.md, written before the jobs ran:

Every instance of rank 1 and 2 UNSAT in all three classes (medium-high confidence): did not hold. Two of rank 1 in o008_c000 stayed open. It held in o008_c001 and o008_c003.
Some rank-0 instances open in each class (about 80%): held. About 5 to 35 per class (low confidence): held (21, 7, 14). Every open instance of rank 0 (medium confidence): did not hold for o008_c000.
A class empty after this one pass (about 15% each): none was.
Median UNSAT wall at most 3 s in each class (high confidence): held (1.12, 1.07, 1.12 s).
No SKIPPED instance (about 75% for m79a, 90% for m79b): held.

The pace rule of m79-predictions.md (median at most 3 s and at most 30 open per class) held in all three classes, so the remaining (B6) classes with an open sweep get the same treatment.

Job m82, and m81b

cube_groups/m82.py is m73.py's pattern: the 42 open instances first, each with 5 minutes of CaDiCaL and then, if still open, 5 of XOR, then the split of one more class per group: o010_c003 (group a, after the 21 of o008_c000) and o010_c005 (group b, after the 7 of o008_c001 and the 14 of o008_c003), each with d = 1, |G| = 384 and 1975 instances (135 of rank 0 with Lemma 93 (b)), the counts of job m66. Unlike m73, two of the re-runs are of rank 1 and carry no Lemma 93 clauses, and the check grades that. Everything else is m69.py, imported unchanged. m81b (the split of o009_c006, written last run) is queued with it. Queueing m81b before m81a is graded departs from m81-predictions.md; the departure and the reason are written in cube_groups/m82-predictions.md before either ran.

Where (B5) and (B6) stand

(B5), 420 classes: all 420 UNSAT (Proposition 35)
(B6), 68 classes: 48 UNSAT, 20 open, every one with an open rank-0 sweep
  d = 1 (14): o008_c000 (21 instances open), o008_c001 (7), o008_c003 (14): m82
              o009_c005 (m81a), o009_c006 (m81b), o010_c003 (m82a), o010_c005 (m82b)
              o009_c007, o010_c000, o010_c001, o010_c004, o010_c006, o010_c007, o010_c008
  d = 2 (6):  o003_c000, o003_c001, o005_c000 to o005_c003
  about 41300 split instances left for the 20; 11670 of them in queued jobs

20 classes of (B6) stand between these notes and A(7) <= 8, which would settle the pair (13, 8).

Limits

The new UNSAT answers are solver answers saved without proof certificates. Proposition 35 rests on every UNSAT answer of the (B5) chain, jobs m42 to m80r, and on the hand results listed above.
No human mathematician has checked Proposition 35 or any of the lemmas it uses.
An UNKNOWN is not evidence either way. o008_c000, o008_c001 and o008_c003 are not counted as empty.
Nothing here settles any pair (a, b) beyond those listed in earlier notes.

Prior work

As for the earlier notes, searches on 2026-10-15 to 2026-10-21 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. 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.