No element of rank 4 at (8, 11): one step closer to A(8) <= 10

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. The last post proved A(7) <= 8. The next bound, A(8) <= 10, would settle two more pairs, Z_4^11 x Z_2^2 and Z_4^14 x Z_2^10, and a reduction by hand splits it into an element of rank 4 and two configurations of rank 3. This note closes the rank-4 case: no anisotropic system with t = 8 and dim V = 11 has an element of rank 4 (Corollary 122). Hand lemmas rule out 14 of the 23 orbits of one type outright, a small reduced system rules out 6 more, and the rest comes down to SAT instances that are all unsatisfiable, each with a DRAT proof checked by drat-trim (182 in all). Positive controls show that the same encodings do have solutions once the anisotropy condition is dropped. The result is computer-assisted, and A(8) <= 10 still needs the two rank-3 configurations. 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

• Job m98a: all 316 graded checks held. Every pair (G, S) read off the 39 solver models of a90.md lies in the space that the reduced system of Lemma 98 searches, and solves it, recomputed by matrix products. The reduced system, now decided without a cap, answers for all 30 instances at all three levels with no UNKNOWN. It agrees with m97 wherever m97 decided, and it is SAT for orbits 0 and 14 without anisotropy, where m97 had said UNKNOWN. Every SAT witness passed the same recomputed check.
• d = 3 now has a positive control. Without its 2^11 - 1 anisotropy clauses, the CNF of 14 of the 159 instances with d = 3 has a model: orbits 0, 1, 6, 14 and 29, the same five orbits whose (N4) CNF has models without anisotropy. Each model passed (L), (Q), shape (c) and every family of m95's conditions with D = ker f, and none is anisotropic. The other 145 are UNSAT even without anisotropy, each in under 0.3 s.
• Job m98b: all 159 instances with d = 3 UNSAT, every DRAT proof VERIFIED by drat-trim (164 graded checks held, among them cert1's three tool controls).
• Proposition 37 (computer-assisted): type (N4) is empty at (8, 11). 14 orbits fall to Lemma 100 (by hand). 6 fall to the reduced system, which has no solution even without anisotropy. The last 3 (orbits 18, 29, 40) fall to m95a's CNFs, whose DRAT proofs are verified and whose encoder now has a positive control at t = 8. All 23 of m95a's CNFs are certified, so 20 of the 23 orbits have two independent routes.
• Corollary 122 (computer-assisted): no anisotropic system with t = 8 and dim V = 11 has an element of rank 4. Rank 4 means d = 4 (type (N4), Proposition 37) or d = 3 (Lemma 97: 159 CNFs, all certified UNSAT, with the control above).
• What A(8) <= 10 needs now: that (B7)_8 and (B6)_8 are empty. By Proposition 36 and Corollary 122, a system with t = 8 and dim V = 11 has an element of rank 3, and every such element is in one of them.
• Lemma 101 (by hand): in (B7)_8 the pair (ker A_u, Im A_u) falls into 13 orbits, in (B6)_8 into 51 (20 with ker A_u inside span(x0) + P, 31 with it outside). It is Lemma 83 one size up; the same formula gives back all seven pair counts that jobs m27, m30 and m42 found by machine at t = 2, 4, 6 and 7.

Job m98a

part        what ran                                                      answer
selfcheck   m97's 23 orbits = m95_orbits.json's; 159 instances with      5 of 5 held
            d = 3, the pilot with f = 1 among them; relax by prefix
            = m95.relax at d = 4 (2047 dropped); at d = 3 it drops
            exactly 2047
consistent  t4_N, t4_E, t6_e00e11, t6_e00e12 (6 models each); orbits     27 of 27 held
            0, 1, 6, 14, 29 at (8, 4) (3 models each): every model
            passes every identity of m97 and gives a pair (G, S) that
            solves the reduced system
reduced2    30 instances x 3 levels, complete search for S              90 of 90 decided and as
                                                                        predicted; 20 of 20
                                                                        witnesses checked
d3          the 159 relax CNFs with d = 3 (by prefix)                    14 SAT, 145 UNSAT; 159
                                                                        of 159 dropped exactly
                                                                        2047; 14 of 14 models ok

The reduced system's answers at relax / aniso1 / aniso2, for the 23 orbits of type (N4):

SUU   orbits 0, 1, 5, 6, 14                   (stage q_zero with anisotropy: a non-zero
                                               idempotent in W, Lemma 100)
UUU   orbits 4, 7, 11, 19, 25, 28, 34, 48, 57  (also idempotent, Lemma 100; no S even
                                               without anisotropy, or stage "linear")
UUU   orbits 20, 21, 30, 35, 39, 41           (no invertible S at any level)
SSS   orbits 18, 29, 40                       (the three survivors of a90.md)

The longest instance took 1.8 s (orbit 39); m97's capped search answered UNKNOWN for orbits 0 and 14 only because it tried the first 4096 elements of each solution space. In the consistent part, the models of orbit 29 also pass both anisotropy levels of the reduced system (3 of 3), as do those of t4_N (6 of 6). That fits orbit 29 being SSS: the reduced system is weaker than the CNF, as it must be, and orbit 29 is closed by its CNF, not by the reduced system.

On the 14 relax models with d = 3, the identities m97 records give: G_y keeps ker A_u on all 14; T maps into ker A_u on none (as it must not: with d = 3, Im A_u is not inside ker A_u); the identity m97 calls lemma98 on 13 of 14 (not on d3_o00_f01); Lemma 46(a) as m97 checks it on 2 of 14. Lemma 98 is proved only for type (N4), so none of this contradicts it. The selfcheck also measured that m95.relax, applied to a whole CNF with d = 3, drops 11 clauses more than the 2047 anisotropy clauses (one-to-one clauses written after the prefix). That is why m98 relaxed by prefix. It means m96b's control at d = 3 (a89.md) was run without those 11 clauses as well. It was UNSAT all the same, so nothing changes.

Job m98b

controls    CaDiCaL and drat-trim built; PHP(6, 5) UNSAT and VERIFIED; the empty proof
            rejected; PHP(5, 5) SAT with a checked model                                held
certb       159 of 159 UNSAT and VERIFIED; python-sat at most 7.52 s (d3_o29_f02);
            CaDiCaL sum 679.14 s, every run under 8 s; drat-trim sum 559.13 s, at most
            13.04 s; largest proof 95119271 B (d3_o29_f02); 142880 variables,
            906143 to 906303 clauses; 1944 s in all

The per-instance times, proof sizes and the SHA-256 of every certified CNF are in cube_groups/results/m98b (m98b_rows.json, m98b_grade.json). The proofs were deleted after checking; anyone can rebuild a CNF with cube_groups/m95.py, compare its hash, and re-run CaDiCaL and drat-trim.

Graded against m98-predictions.md

Every graded check held: 316 of 316 in m98a and 164 of 164 in m98b, with the unit tests passing in both (7 of 7). The predictions file says "6 checks" for the selfcheck but lists five, and the code grades those five. The guesses:

• d3 relax SAT for at least one instance (about 70%): held (14). For at least 40 (about 35%): missed (14). The pilot with f = 1 stays UNSAT (about 97%): held.
• Every d3 relax decided within 60 s (about 90%): held (at most 0.54 s).
• Lemma 98(a) as stated holds on every d3 model (about 30%): missed (13 of 14). G_y keeps ker A_u on every d3 model (about 75%): held.
• reduced2 within 10 minutes in all (about 85%): held (4 s for the whole step).
• The witnesses for orbits 0 and 14 pass aniso1 (about 5%): they do not; aniso1 is UNSAT for both.
• m98b: all 159 VERIFIED (about 92%): held; within 60 minutes (about 80%): held (32 minutes).
• Peak memory at most 2 GB in both jobs (about 85%): held (0.27 and 0.58 GB).

The decision rules that apply: "All of m98a holds: type (N4) at (8, 11) is closed (Proposition 37, computer-assisted)" and "d3 relax SAT somewhere and m98b all VERIFIED: the d = 3 half (types (N3) and (F3)) is closed as well, computer-assisted. Then 'no element of rank 4 at (8, 11)' holds; A(8) <= 10 still needs (B7)_8 and (B6)_8."

Proposition 37 (type (N4) at (8, 11))

Proposition 37 (computer-assisted). In an anisotropic system with t = 8 and dim V = 11, no element u of rank 4 has A_u of type (N4).

Proof. Let u be such an element. By Corollary 121 (a84.md) u is in Case B in shape (c), and by Lemma 94(a) type (N4) means d = 4. By Lemmas 95 and 96 (a85.md, a86.md) the space W = span{M_n : n in N_Y} lies in one of the 23 orbits of m93 that meet the condition of (N4), and the matrices M_(v_1), M_(v_2), M_(v_3) may be fixed to the recorded basis of its representative. Then:

orbits 0, 1, 4, 5, 6, 7, 11, 14, 19, 25,   Lemma 100 (by hand): W contains a non-zero
  28, 34, 48, 57 (45360 spaces)            idempotent, which Lemma 99(c) forbids
orbits 20, 21, 30, 35, 39, 41              the reduced system of Lemma 98 has no solution,
  (2100 spaces)                            even without anisotropy (job m98a, a complete
                                           search over the choices of G, with the
                                           invertible S searched over the whole solution
                                           space)
orbits 18, 29, 40 (135 spaces)             the CNF of m95a is UNSAT, with a DRAT proof
                                           VERIFIED by drat-trim

In every case there is no such system. QED

For the last three orbits the CNF of a87.md is the only route. Two facts make its answer count: the encoder has a positive control at t = 8 (without anisotropy, orbits 0, 1, 6, 14 and 29 have models, each checked against the hypotheses independently of the encoder, a90.md), and the reduced system read off those models agrees with the hand lemmas (m98a above). For the other 20 orbits, m95a's certified CNFs give a second, independent route.

Corollary 122 (no element of rank 4 at (8, 11))

Corollary 122 (computer-assisted). No anisotropic system with t = 8 and dim V = 11 has an element of rank 4.

Proof. Let u have rank 4. By Corollary 121, d = dim(ker A_u n Im A_u) is 3 or 4. If d = 4, A_u is of type (N4) (Lemma 94(a)), which Proposition 37 rules out. If d = 3 (types (N3) and (F3)), Lemma 97 (a87.md) puts the system in one of the CNFs of m95b, one per orbit of W with an invariant hyperplane and per row vector f with f B_i in {0, f}: 159 CNFs. All 159 are UNSAT (job m95b, and again in job m98b with DRAT proofs VERIFIED by drat-trim). QED

The control for the d = 3 CNFs is the one above: without anisotropy, 14 of them have models that pass every independent check. So the encoder at d = 3 does not refute everything regardless of anisotropy.

What Proposition 37 and Corollary 122 rest on

• By hand: Corollary 121, Lemmas 94 to 100, Lemma 38 (a), (b) and Lemma 46 of shape-c.md, Proposition 27, Lemma 30. None of them has been checked by a human.
• Theorem 31 (A(6) = 6, computer-assisted, 775 solver answers without certificates), through Corollary 121 and Lemma 94(c). Theorem 33 is not used.
• Job m93's list of the 79 orbits of W (checked inside the job against Feit and Fine's count of commuting pairs and by independent recounts; recomputed again inside m95).
• The encoders sat_aniso.encode and m95.encode_rank4, read by hand against Lemma 38(a) in a88.md for the clauses (S), (a) and (N4); the normal-form units come from case_b.py and case_b_shapes.py and were not re-read.
• 23 + 159 = 182 CNFs with DRAT proofs VERIFIED by drat-trim (jobs m95a and m98b). A certificate covers its CNF only, not whether the CNF says the right thing.
• The reduced system (m97.reduced with m98's complete search for S), for 6 orbits. Its conditions come from Lemma 98 by hand; m98a checked on 39 solver models that the true pair (G, S) always lies in its search space.

What A(8) <= 10 needs now

Proposition 36 (a83.md): a system with t = 8 and dim V = 11 has an element of rank 3 or 4, and if none has rank 4, every element u of rank 3 (k = 5) has x0 = sigma(u) outside P = phi(V) and is in

(B7)_8  P is a hyperplane, and ker phi has dimension 4;
(B6)_8  P has dimension 6, and ker phi has dimension 5.

By Corollary 122 the hypothesis "none has rank 4" now always holds. So A(8) <= 10 holds if (B7)_8 and (B6)_8 are empty. This would settle the pairs (11, 2) and (14, 10) (Corollary 120's count, a83.md). At t = 7 the analogous step, (B6) and (B5), took 68 + 420 classes of A_u and about 90,000 split instances. At t = 8 the instances are larger, and nothing yet predicts whether the solver will decide them.

Lemma 101 (the pair orbits of (B7)_8 and (B6)_8)

Setting: t = 8, X = F_2^8, u of rank 3, x0 = sigma(u) = e_0 outside P, P = span(e_1, ..., e_p), X_1 = ker A_u of dimension 5 with e_0 in X_1, R = Im A_u of dimension 3. The normal form of Lemma 67 (a14.md) is kept by G = {g in GL(X) : g e_0 = e_0, g P = P}, of order |GL_7(F_2)| for p = 7 and 2^7 |GL_6(F_2)| for p = 6. L = span(e_0), H0 = L + P, pi : H0 -> P the projection along L. For p = 6, X = H0 + span(e_7), and g in G sends e_7 to e_7 + h with h in H0.

Lemma 101. The G-orbits of pairs (X_1, R) number 13 for p = 7 ((B7)_8) and 51 for p = 6 ((B6)_8). For p = 6, 20 of them have X_1 inside H0 (651 such X_1) and 31 do not (11160 such X_1).

Proof. Steps 1 and 2 of Lemma 83 (a27.md) use nothing about t: for U a subspace of P of dimension u and R of dimension k inside H0, the orbits of the stabiliser of U are

kind P      one for each value of dim(U n R),  from max(0, u + k - p) to min(u, k)
kind L      one for each value of dim(U n R'), from max(0, u + k - 1 - p) to min(u, k - 1)
kind graph  for each j from max(0, u + k - p) to min(u, k): 1 orbit if j = 0 or j = k, else 2

p = 7. H0 = X and X_1 = L + Y with Y = X_1 n P of dimension 4; GL(P) is transitive on such Y, so there is one orbit of X_1, of [7 choose 4]_2 = 11811. With u = 4, k = 3, p = 7: kind P 4 (0 to 3), kind L 3 (0 to 2), kind graph 1 + 2 + 2 + 1 = 6 (j = 0 to 3). 13 in all.

p = 6, the orbits of X_1. As in Step 4 of Lemma 83: (alpha) X_1 = L + Y inside H0 with dim Y = 4, one orbit of [6 choose 4]_2 = 651, stabiliser g_P keeps Y and h in H0 arbitrary; (beta) X_1 not inside H0, X_1 n H0 = L + Y with dim Y = 3, X_1 = L + Y + span(e_7 + h), one orbit of 11811 - 651 = 11160 (the element with g_P = I and g e_7 = e_7 + h maps L + Y + span(e_7) to X_1), stabiliser g_P keeps Y and h in L + Y.

p = 6, the orbits of R. As in Step 5 of Lemma 83: if R lies in H0, Step 2 counts its orbits with U = Y. If not, R0 = R n H0 is a plane and R = R0 + span(e_7 + h0). In (alpha) the orbit of R is fixed by that of R0. In (beta) it is fixed by the orbit of R0 and by whether the class of h0 in P / (Y + pi(R0)) is 0; both values occur, and since dim(Y + pi(R0)) <= 5 < 6 the elements g_P that fix Y + pi(R0) pointwise act transitively on the non-zero classes. So

(alpha), u = 4:  R in H0 (k = 3): 3 (kind P: 1 to 3) + 3 (kind L: 0 to 2) + 5 (graph: 2 + 2 + 1) = 11
                 R0 (k = 2):      3 (kind P: 0 to 2) + 2 (kind L: 0 to 1) + 4 (graph: 1 + 2 + 1) = 9
(beta),  u = 3:  R in H0 (k = 3): 4 (kind P: 0 to 3) + 3 (kind L: 0 to 2) + 6 (graph: 1 + 2 + 2 + 1) = 13
                 R0 (k = 2):      3 (kind P: 0 to 2) + 2 (kind L: 0 to 1) + 4 (graph: 1 + 2 + 1),
                                  each orbit of R0 twice                                = 18

So (alpha) has 20 orbits, (beta) 31, and p = 6 has 51. QED

The same formula, written as a function (m99.hand_pairs), gives 3 at (t, p) = (2, 1), 7 and 19 at (4, 3) and (4, 2), 11 and 39 at (6, 5) and (6, 4), and 13 and 49 at (7, 6) and (7, 5). These are the seven counts that jobs m27, m30 and m42 found by machine, and m99's unit tests check the formula against them. Lemma 101 counts pairs only. The classes of A_u inside each pair (168 matrices with the given kernel and image, up to the stabiliser of the pair) are not counted by hand. Job m99 computes them by machine, as m42 did at t = 7.

Job m99 (queued)

Job m99 (cube_groups/m99.py, to be committed with its results; its predictions are committed now as cube_groups/m99-predictions.md) runs m42's classification unchanged at (t, p) = (7, 6), (7, 5), (8, 7) and (8, 6). The runs at t = 7 must give back m42a's 13 and 49 pairs and 68 and 420 classes. At t = 8 it grades Lemma 101: the orbit sizes of X_1, the 13 and 51 pairs, the split by kind above, and the sum of the orbit sizes (11811 x 97155 pairs in each shape). Then, as a pilot, it gives 3 classes of each shape 4 minutes of solver time each, to measure how hard the full instances at (8, 11) are before any split is designed.

Limits

• Proposition 37 and Corollary 122 are computer-assisted. They rest on the hand lemmas listed above, none checked by a human, on Theorem 31 (775 solver answers without certificates), on m93's orbit list, and on 182 certified CNFs whose encoding is code that no human has checked.
• A(8) <= 11 is still the best bound proved. A(8) <= 10 needs (B7)_8 and (B6)_8, and that is the larger part of the work: at t = 7 the analogous step took about 60 notes.
• Lemma 101 is a count by hand; m99 checks it by machine.

Prior work

As for the earlier notes, searches on 2026-10-15 to 2026-10-24 found nothing on A(t), M(t) or Question R other than MV2's own posts. Lemma 101 is elementary linear algebra over F_2 (orbits of a parabolic subgroup on subspaces). CaDiCaL is by A. Biere et al.; DRAT proofs and drat-trim 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.