[unpaidmoon]

Change and mathematical scope

Exhaustive finite census: five nonzero symmetric rational rank-one matrices summing to 4I never have all four targets A+P, A+Q, B+P, and B+Q as subset sums. The shortest once-each equation R+S+T+U+V = 4I therefore admits no word in the PR2085/2112 model. One explicit solution on five pairwise nonparallel primitive directions has full parity image F2^2 and is still not a word.

No κ change. The selected frontier stays 781451/250000000. This census does not lower the eight-call minimum. It does not speak about six or more added frames, or about five added frames together with an old call.

Status: exhaustive finite census, which is a scoped proof of support failure for this one equation, plus one witness. Not a heuristic search and not a multiplication theorem.

Remaining obligations: six once-each frames, and five frames plus one old call.

Task and overlap

Base commit: 17469fff78c22941280f04d39dc5a1faee09c840 on upstream CrocSwap/integer-mult-bounds main.

Task: the five-frame open question of merged PR #6952, discussion comment 19507121. Catalogue card bit-new-register-model, scope_status: changed. The same abelian 2-by-2 restriction was already used by #6942 and #6952.

Overlap checked against open upstream PRs, discussion search, and local packages. No open upstream PR states this five-call census. #6952 is the predecessor and is not redone. #6942 and #7013 are three-frame character work and are not redone. Four added frames plus an old call is a different equation.

Scope is changed from the catalogue card. The card asks for a larger or nonabelian alphabet. This package stays in the abelian symmetric 2-by-2 model because that is the declared remainder of #6952. There is no local call-count saving and no selected-frontier change.

Validation

python3 scripts/research_package.py --package research/five-signed-once-support --check-only
python3.12 scripts/research_package.py --package research/five-signed-once-support

Both passed on Python 3.12.3. The registered verifier also passed under python -O. Each command takes about 20 seconds.

The census splits all 116280 ordered 4-tuples of distinct weight-2 and weight-3 subsets into 71040 invertible solutions off the determinant cone, 44520 inconsistent systems, and 720 rank-4 families whose frozen frame is ±2I, ±(A-B), or ±(P-Q). One invertible determinant is reduced by hand to -2. One singular line is checked by direct addition and freezes 2I. The witness directions are (-1,1), (0,1), (1,0), (1,1), and (1,3).

Not run: predecessor replays, Lean, Docker, and the selected-result cold replay. The inherited determinant identity and subset-sum necessity are not reproved.

Credit

Cinna Davis, PR2085/2112 register model. The determinant and subset-sum necessity are PR2910 as recorded by apoursh in PR6190, package research/bit-two-signed-frame-floor. The three-frame character is research/three-signed-old-once. The four-call support proof and this open question are research/four-signed-once-parity, merged as PR #6952, discussion comment 19507121.

Prepared by unpaidmoon with substantial Cursor Grok assistance. No independent human or formal-kernel review. New work is Apache-2.0.

Open next questions

Can six added signed rank-one frames, each used once and with no old call, meet target support for F1+...+F6 = 4I? This is the smallest useful follow-up. A six-call word would still lower the eight-call minimum, and the complement of a four-element subset is a pair, so sizes 2, 3, and 4 all remain. Blocker: the size lemma uses five frames, so the 116280-tuple domain does not carry over.

Can five added frames plus one old call meet support at length 6? First step: fix one old projector E and test R+S+T+U+V = 4I-E. Blocker: every identity in this package uses the residual 4I.

Workflow feedback

The finite list of pair and triple subsets made an exact census possible without a search over directions. A hand-reduced determinant and one explicitly added singular point kept the rational solver anchored.

#1200