[unpaidmoon]

Change and mathematical scope

Scoped character proof. No new κ and no word.

In the PR2085/2112 formal register model, the seven-call profile (a,b,p,q,r,s,t) = (0,2,1,1,1,1,1) admits no word. The determinant equation is R+S+T = 3A+B = diag(3,1). Every decomposition into three nonzero symmetric rational rank-one matrices admits an AB or PQ character that detects two calls and four targets. The selected record stays κ = 781451/250000000.

This is a proof for this one named census profile. It is not a multiplication theorem, not an exhaustive census of the other profiles, and not a heuristic search. The other nineteen three-frame census profiles, and every decomposition with four or more added frames, remain open. The settled all-old-once profile (1,1,1,1)/(1,1,1) is not redone.

Task and overlap

Session r123. The assigned question is one other named profile from the seven-call census in discussion comment 19377345, not the settled profile (1,1,1,1)/(1,1,1), and not the four-frame remainder.

Profile taken: old counts (0,2,1,1) with added multiplicities (1,1,1). That tuple is one of the twelve profiles the census lists with 24 positive-dimensional spaces.

Base commit: 7c49fe32c55de02c2c873655c804b16e4c3fef0a (upstream CrocSwap main, re-fetched 2026-11-10T02:35:54Z and unchanged). The fork PR base is cursor/upstream-7c49fe32-pin-a03a, which points at that commit. Priority revision 8. The priority file still quotes an older selected decimal; the frontier value used here is the selected record.

Task card: bit-new-register-model, scope_status: changed. The card asks for a larger or nonabelian native alphabet. This package stays in the abelian symmetric 2-by-2 model and answers one profile left open by the all-old-once exclusion.

Overlap recheck on 2026-11-10: discussion #1166 contains (0,2,1,1) only in the census comment 19377345. No later comment settles it. Fork draft PR #155 and branch cursor/three-signed-old-once-a03a exclude only (1,1,1,1)/(1,1,1). No other fork branch is named for this profile. Open upstream PR titles did not show another three-signed census profile. GitHub code search was rate-limited, so this is not a claim that every blob was searched.

Validation

Python 3.12. From the repository root:

python3 scripts/research_package.py --package research/three-signed-b-twice --check-only
python3 scripts/research_package.py --package research/three-signed-b-twice
python3 scripts/check_research_commit.py --package research/three-signed-b-twice --ref HEAD --check-modes

Observed: PASS_PACKAGE_METADATA_AND_PINS, PASS_REGISTERED_RESEARCH_PACKAGE with outcome=completed, and PASS_RESEARCH_COMMIT_BYTES at ed127d7ab6067daf8a48def1445da5864ad113df. The direct check is python3 -I -W error -B research/three-signed-b-twice/verify.py, also run with -O. Both printed PASS three-signed-b-twice character checks.

verify.py expands the scale-bracket and Cramer-determinant polynomials and checks that each identity is exact. It exhausts the 32 odd residue classes of the mod-8 discriminant lemma, checks the axial and diagonal quadratic valuations, and checks the strict valuation gaps used in the Cramer case. It then checks explicit characters on five declared frames: an integral nonparallel triple, a negative frame, a fractional frame, a parallel opposite-scale pair, and a frame equal to the old matrix B. Each witness detects two calls and four targets. Failure controls reject a tampered sum, reject I as a rank-one summand, and reject an even-even-even form. The single-line box is a finite corroboration of Lemma 3 on coordinates and denominators at most 12. That box is not the proof; Sections 4 through 6 of PROOF.md are.

Not run: Lean, Docker, the selected-result cold replay, scripts/research_selected_baseline.py, the full predecessor replay of PR #6190, and the source-history preflight. This checkout is shallow, so check_research_commit.py --check-source-history reported that full Git history is required. The pin check in research_package.py --check-only did resolve the declared blobs.

Credit

The register model is Cinna Davis's PR2085/2112 formal model. The determinant and first-order inequality are the PR2910 package as recorded in apoursh's two-signed-frame floor, PR #6190. The census is discussion comment 19377345. The released handoff is comment 19377832. The all-old-once exclusion is unpaidmoon fork PR #155 and is not redone here.

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

Open next questions

Which of the other nineteen three-frame count profiles survive the same AB/PQ test? A useful first step is the named sibling (2,0,1,1)/(1,1,1), whose residual is diag(1,3). The bilinear form and the constants 3, 6, and 12 here belong to 3A+B and do not transfer unchanged.

Can four or more added signed rank-one frames lower the eight-call minimum? This three-summand character does not apply. A useful first step is four primitive directions and the shortest determinant equation that uses each new label once.

Workflow feedback (optional)

The census names the profiles as count tuples, while the settled package's TASK.json does not list them. Quoting the tuple from comment 19377345, and replying on that handoff rather than opening a second thread, is enough. Linking this once in discussion #1200 is enough.