[petalas]

Result

Finite exact minimum (exhaustive finite certificate). No new κ. In M4(F2[S3]) with paid labels x = (1 2), y = (2 3) and calls D_N(g) = I + ([g]+[e]) N over all 120 rank-one idempotents N of M4(F2), the target diag([xyx],[xyx],[e],[e]) needs exactly six paid calls. Roles 2 and 3 are arbitrary dirty roles returned unchanged.

This answers open question 1 of Wentao Li's #4084 (research/s3-three-role-xyx), which proves six with three roles: a fourth restored dirty role does not save a call. The claim covers four roles only.

Evidence

• Phi : F2[S3] -> M2(F2) x F2[C2], [g] -> (rho(g), c^sign(g)), is checked to be an algebra isomorphism. In the C2 block each paid factor is I + delta N with delta^2 = 0. In the M2 block it is a transvection of F2^8.
• Paid factors are involutions, so a word of length at most five exists exactly when ball(I,3) meets T * ball(I,2). ball(I,2) has layers 1, 240, 32650. Every element of ball(I,2) and every one-call extension was tested: zero hits. The M8(F2) image alone also has zero hits.
• Calibration: the same engine with three roles gives layers [1, 56, 1750, 45396], matching the pinned Research: one dirty role does not lower S3 longest Coxeter double minimum (no new kappa) #4084 certificate.
• An independent engine multiplying in M4(F2[S3]) produces the same 32,891-state ball(I,2) under Phi.
• Positive controls: the search finds words of length at most five for diag([xyx],[xy],[e],[e]) and diag([x],[y],[xy],[e]).
• The direct word x y x on role 0, then on role 1, equals the target. Each of its six one-call omissions does not.

Reproduce

From the repository root, with CPython 3.12 (here ~/git/integer-mult-bounds/.venv/bin/python3.12):

python3.12 -I -B research/s3-xyx-four-role-minimum/verify.py
python3.12 -I -O -B research/s3-xyx-four-role-minimum/verify.py
python3.12 -B scripts/research_package.py --package research/s3-xyx-four-role-minimum
python3.12 -B scripts/check_research_commit.py --package research/s3-xyx-four-role-minimum --check-source-history

Local results: both direct runs print PASS_S3_XYX_FOUR_ROLE ... ball_i2_layers=[1, 240, 32650] ... short_hits=0 rho_quotient_hits=0 direct=6 target_minimum=6 in about 11 s each. The registered replay prints PASS_REGISTERED_RESEARCH_PACKAGE (about 22 s for both commands), and the commit check prints PASS_RESEARCH_COMMIT_BYTES.

Limitations

One target, four roles, and the optimistic unit-cost formal alphabet. Five or more roles, other S3 targets, free address maps, native source generation, hosting and supplier pricing are not covered. No selected-frontier, κ or multiplication-theorem change. No unrun proof obligation is claimed as discharged.

Open next questions

1. Does a fifth or any larger number of restored dirty roles lower the six-call minimum? Five roles have 992 factors. Their ball(I,2) is estimated, not computed, at up to about 5 x 10^5 states, which is slow for this pure-Python search. A uniform argument in the M_{2m}(F2) block is the likely route.
2. Is the rho quotient enough for every role count? At four roles the M8(F2) image alone excludes length five. Characterizing short products of these restricted transvections that act as the partial swap would give a cleaner certificate.

Related open work

• Add S3 three-register rank lower bound #3893 (open): the two-dimensional representation-rank bound in the same S3 alphabet, for the different target diag([s],[t],[st]). This package uses the same representation as one block of its faithful encoding and does not compute that target.

Credit

Target, alphabet, three-role minimum and the open question: Wentao Li / VictorLiwentao, #4084. Alphabet lineage: Cinna Davis's two-register S3 census and the representation bound of #3893. The four-role search, controls and note were produced by Nick Petalas.

CI notes

All checks passed for head b96ecfbda694cf4917d54b0c567d0ff5cbee8155 in run https://github.com/CrocSwap/integer-mult-bounds/actions/runs/40530572035: plan (5m55s) and replay (research/s3-xyx-four-role-minimum) (2m6s).