[petalas]

Result

Claim type: scoped written proof with exact finite corroboration. No κ change.

This answers part of Open next question 2 of apoursh's #6089 (research/bit-positive-frame-use): is the third necessary multiplicity profile (0,1,3,3,m) realizable for any m >= 2?

Theorem. If m = 2^k for some k >= 0, no exact word in #6089's formal PR2085/2112 four-target model has the profile (0,1,3,3,m), at any finite width w >= 4. The model has rank-one binary idempotent calls over F2[Λ], free GL_w(F2) mixing and exactly restored dirty workspace.

m = 1 is #6089's exclusion; m = 2, 4, 8, ... are new. For these m, the attained count profiles are exactly #6089's two subdivision profiles.

Proof idea. After #6089's normal form, send [R] -> 1+s and [B],[P] -> 1. Then [A],[Q] -> (1+s)^m = 1+s^m over F2. The s^m coefficient of the word is the single ordered product E_1...E_m of the R projectors plus the three Q projectors, and it must equal diag(1,0,0,1). #6089's first-order B character gives N_B + ΣN_Q = diag(0,1,1,0). Adding the two equations gives N_B + E_1...E_m = D_w, which has rank at most 2 on the left and rank 4 on the right.

The full argument is in research/bit-positive-frame-third-profile/PROOF.md. It also explains why the argument stops when m has an odd factor.

Evidence

verify.py uses exact arithmetic and needs only the standard library. It checks:

• the pinned Classify usable positive rank-one frames and their exact call counts #6089 proof bytes;
• the lattice and character tables for m = 2^k, k <= 10;
• the coefficient lemma on 1,600 random profile words at w = 4, 5 and m = 1, 2, 4, 8;
• 72 group-algebra homomorphism checks;
• that Classify usable positive rank-one frames and their exact call counts #6089's attained subdivision words are exact and satisfy the same equations, and that a mutated word is rejected;
• the rank step, exhaustively at w = 4, 5.

The random words corroborate the lemma; the proof does not depend on them.

~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/bit-positive-frame-third-profile/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/bit-positive-frame-third-profile/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/bit-positive-frame-third-profile
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/bit-positive-frame-third-profile --check-source-history

Locally (CPython 3.12), all four pass: PASS_POSITIVE_FRAME_THIRD_PROFILE_POWERS_OF_TWO twice, PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=partial in about 1 s, and PASS_RESEARCH_COMMIT_BYTES.

Limitations

• Only powers of two are settled. For m = 3, 5, 6, 7, ... the profile is neither constructed nor excluded.
• Classify usable positive rank-one frames and their exact call counts #6089's minimum m+7, its length spectrum, the selected frontier and κ are unchanged.
• No native implementation, independent human review or formal-kernel check is supplied.

Open next questions

1. Is (0,1,3,3,m) realizable when m has an odd factor o >= 3? At m = 3 the two characters only give E_1+E_2+E_3+N_B = D_w, which coordinate projectors satisfy, so a second-order character or an exact 10-call search at w = 4 is the next step.
2. Is there a uniform obstruction for every m >= 2? The blocker is the rank of the elementary sum e_{2^k}(E) once o >= 3.

Related open work

No open PR, including this account's later PRs #6664 to #6675, studies this profile or the positive added-frame classification.

CI notes

All checks passed at head 7b6bf6ff83e905f27c063edb07300daaa4ccc899: plan and replay (research/bit-positive-frame-third-profile), run https://github.com/CrocSwap/integer-mult-bounds/actions/runs/41670611518.

Credit

Produced by Nick Petalas. apoursh's #6089 supplies the model reduction, symmetries, necessary profile list, B character and subdivision words, and poses the question. Cinna Davis's PR2085/2112 supply the model and endpoint, and PR2910/PR6032 the determinant and first-order methods.