[jwr404]

Summary

Exact computer-assisted partial result in a formal model. No new κ.

This follows up the open question of #5005, which proved two coordinate 3-cycles cost exactly 12 at R = 2. Here the target is diag([c],[c],[e]) in M_3(F2[GL_3(F2)]): 168 paid factors, free scalar maps, and an arbitrary dirty third register restored exactly.

• Result. No realizing word has length ≤ 10, and one of length 12 exists. So the cost is 11 or 12, and a dirty register saves at most one call. Length 11 is open.
• Engine. search.c extends Two coordinate 3-cycles cost twelve formal calls: exact search excludes length ≤ 11 (no new κ) #5005's meet-in-the-middle to three registers.
  • Word reductions: cancellation, and an exact commutation normal form (9,912 commuting ordered pairs).
  • Symmetry: lexicographically least pair representatives under 36 target-fixing algebra automorphisms (827 of 28,056 pairs).
  • Fingerprint key matches are checked exactly with a stored radius-two ball.
• Forward ball. The counts are 169 / 22,051 / 2,705,791 / 325,910,698. The radius-two count matches the merged gl3-order7-dirty-register-seed39ae.
• Parity cannot finish the case. Calls 0, 28, 84, 0, 84 multiply to I, from the relation C01·C02·C12 = C12·C01 on one register.

Evidence

Check	Where
Length ≤ 8 (depth 3 + 5), plus all controls	registered replay, 31 s locally
Length ≤ 9 (depth 4 + 5)	local receipt in RESULT.json
Length ≤ 10 (depth 4 + 6), 3.5·10¹¹ backward nodes, 53 min on 16 cores, 9 GB	local receipt in RESULT.json

The default verifier checks:

• compilation with -Wall -Wextra -Werror;
• an exact binding of the C products to the merged Python formal model at R = 3 (36 random words);
• an engine self-test and the state counts;
• positive controls with and without symmetry: diag(c,e,e), diag(C7,C7,e) and two swaps, each with nothing at length ≤ 5 and length 6 found;
• the 12-call word and the odd relation;
• the main search: nothing at length ≤ 6 without symmetry, and nothing at length ≤ 8 with it.

verify.py --full reruns the local runs. The recorded runs are bound to search.c by hash. The binary that ran is byte-identical to a fresh compile.

In tamper tests, a changed search.c fails the hash binding, and a broken generator product fails the semantic binding.

Scope

Card bit-new-register-model, scope changed (TASK.json). Only n = 3, R = 3 is covered. Length 11, R ≥ 4, spectators, native operations, tariffs and κ are not settled. Selected frontier and frozen evidence are unchanged.

Claim: #1166 (comment)
Base: ff3cc58e370d0f678e529246f8c73e8094e18fcf, priority revision 7.

Credit: #4939 (formal model), #4974 and JoyboyBrian's three-cycle-address-floor (single-cycle cost 6), Cinna Davis's order-7 package (ball cross-check), and the predecessors of #4950/#4968/#5005.

🤖 Generated with Claude Code