[jwr404]

Result

In the formal model M_2(F2[GL_3(F2)]) of #4939/#4950/#4968, a pair of coordinate 3-cycles diag([c],[c]) has no realizing word of length ≤ 11. Two shortest 3-cycle words attain 12, so the cost is exactly 12, and additive: the two registers share no paid work.

This answers the smallest case of #4968's open question. #4974's support lemma settles single targets but only bounds the largest one. Permutation cuts cannot even certify a single 3-cycle; they reach about 3.5 of 6.

No new κ. The selected exponent stays 60403/20000000. This is a negative formal-model screen.

Method

search.c is an exact meet-in-the-middle search. Paid calls are involutions, and free scalars are normalized away (#4939 step 1).

• Forward. A depth-first search from I to depth ≤ 5 records 61-bit fingerprints: 16,292,362 distinct states.
• Backward. A depth-first search from T to depth ≤ 6 looks up every state. Fingerprints are deterministic, and the run records zero key matches, which excludes every word of length ≤ 11. Any match would have been re-verified by an exact forward re-search.
• Symmetry. The target and generator set are fixed by 36 algebra automorphisms (automorphisms of GL_3 fixing c, times GL_2(F2) register conjugation). They form a single orbit on the 36 generators.
• Symmetry-free confirmation. The search is repeated without the reduction, over all 36 first letters in parallel shards, again with zero key matches.

Evidence

verify.py uses the standard library and C11. It takes about 75 s locally with 9 shards. It:

• compiles with -Wall -Wextra -Werror;
• binds the C engine to the merged Python formal.py on 84 random words by exact state comparison;
• reproduces the distinct-state counts 37 / 1,033 / 26,551 / 663,496;
• runs positive controls on diag([c],[e]), diag([s01],[s12]) and diag([s01],[s01]): nothing at length ≤ 5, and 6 is found;
• checks the 12-call attaining word in Python;
• runs both main searches.

Breaking the generator product or perturbing the forward count makes it fail.

CI runners have fewer cores than my machine, so the symmetry-free shards take longer there. They are expected to fit the 600 s cap.

Task and overlap

Card bit-new-register-model, scope changed (see TASK.json). Base: canonical main f259dabc7d70e0db8d6d36bfda888f008bbfecc1, priority revision 7. CLAIM.

Only n = 3, R = 2 is covered. A third dirty register, spectator coordinates and other multi-target cases remain open.

Test plan

python3.12 -B scripts/research_package.py --package research/two-three-cycle-additivity --check-only
python3.12 -B scripts/research_package.py --package research/two-three-cycle-additivity
python3.12 -B scripts/check_research_commit.py --package research/two-three-cycle-additivity

All pass locally on Linux with CPython 3.12.14 and GCC 16.2.1.

Credit

• Mihir Srivastava (Prove six-call two-SWAP cost with arbitrary address spectators #4939).
• JoyboyBrian (Prove a single three-cycle costs six with arbitrary address spectators #4974).
• PR1989, the GL2 corollary, commdata2338 (PR1414/PR1495), PR1541 and Gareth Davidson (PR1333).

Prepared by James Reed with substantial Anthropic Claude (Claude Code) assistance. Apache-2.0. No independent human review.

🤖 Generated with Claude Code