[petalas]

Result

Scoped proof with an exact finite certificate, plus a conjecture. No new κ. The package is research/q8-mixed-shear-identity-space.

The question comes from unpaidmoon's #4378, which leaves open whether shape (4,1) (four [zi] targets, one [zj]) needs 13 or 15 positive i/j calls in the F2[Q8] dirty-register model. The homogeneous 3t proof (PR3558) uses the identities X K Y = 0 and X K^2 Y = 0. This PR determines what the mixed model offers in place of that pair.

• Theorem A (finite certificate plus written proof). Take active compressions X M_w Y of the 30 label-block monomials E L E … L E with at most three factors L, together with P_i and P_j. The linear identities valid for every exact word, of any shape and any finite dirty workspace, are exactly the 7-dimensional span of the F2[Q8] coefficient equations. Twenty-five explicit exact words give compression rows of rank 25 out of 32.
• Theorem B. Exactly four shears I+h with deg h ≤ 2 satisfy X(I+h)Y = 0: PR3570's K1 and K2, and two cubic shears Q1 and Q2. None of the 12 shear products of degree at most three is an identity.
• Theorem C. Every one of the six pairs of images K1U, K2U, Q1U, Q2U (with U = im Y) meets on an exact one-role three-call word. A two-image cyclic-style argument therefore cannot certify n ≥ 3t for mixed words in this calculus.
• Conjecture D (unproved). dim(K1U+K2U+Q1U+Q2U) ≥ 2t for every exact word. This would imply n ≥ 3t for every mixed shape, hence 15 at (4,1) and 24 at (7,1). It holds on every exact mixed-label word in complete meet-in-the-middle censuses: one role at length 3, and two roles at lengths 5–8. Together these cover 62,444 mixed-label words through length 7 and 407,296 at length 8. All censused shapes have t ≤ 2, where 3t is already known.

The (4,1) minimum is not decided.

Reproduce

~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/q8-mixed-shear-identity-space
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/q8-mixed-shear-identity-space --check-source-history
~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/q8-mixed-shear-identity-space/verify.py          # ~15 s, registered
~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/q8-mixed-shear-identity-space/verify.py --full   # ~3 min, opt-in length-8 census

All four commands passed locally (CPython 3.12, standard library only). The registered check took about 20 s through the package runner. The verifier writes no files.

Limitations and unrun obligations

• Theorem A covers degree ≤ 3 only. It excludes neither higher-degree compression identities, nor rank arguments that are not linear identities, nor arguments using dirty rows and columns.
• Conjecture D has finite evidence only.
• No physical caller, routing, restoration, hosting, precision or supplier is priced.
• Not run: Lean, Docker and the selected cold replay.
• Independent human and formal proof-kernel review are unclaimed.

Open next questions

1. Prove Conjecture D. A proof closes both open lengths of Record the square i-block obstruction for mixed negative Q8 targets. #4378. First test three-role length-9 words with t = 3.
2. Which compression identities exist at degree four and higher? Two-role length-8 samples leave a 16-dimensional annihilator at degree five, possibly small-dimension artefacts.
3. Is there a 13-call (4,1) word? It would refute D. A search restricted to PR3536 six-role cores would be the first step.

Related open work

• Prove the conjugate-pair target needs four calls in every group (no new κ) #6038 (conjugate-pair target, four calls in every group): a different target and model, with no shared quantity.
• Audit Q8 dirty spectator restoration boundary #3906 (Q8 dirty spectator restoration audit): an audit of the restoration boundary. It computes no compression identities.
• Certify that balanced depth-three chain multiplicities break every unit symmetry for m ≤ 24 (no new κ) #6037 (balanced depth-three chain multiplicities): a different object (connector chains), with no shared quantity.

Credit

Builds on PR3517, PR3536, PR3558 and PR3570 (Nick Petalas), cited and not re-audited. The open question is from unpaidmoon's #4378.

CI notes

Both hosted checks passed for head f78a9d4912308264b2c7c04c54d1db76c51d6a6f: plan and replay (research/q8-mixed-shear-identity-space), in run 40609234265. The run's head SHA matches the PR head. The replay ran the registered default command only; the --full census was run locally.