Prove four once-each rank-one frames miss the four-call endpoint.

research/four-signed-once-parity/PROOF.md

@@ -0,0 +1,146 @@
+# Four once-each rank-one frames do not meet the four-call endpoint
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+
+## Claim
+
+In the PR2085/2112 formal register model, the shortest determinant equation that uses four new labels once each is
+
+```
+R + S + T + U = 4I.
+```
+
+It is the zero-old-call case: four paid calls and no call on `A`, `B`, `P`, or `Q`. Two statements are proved about it.
+
+1. **Support proof.** No choice of four nonzero symmetric rational rank-one matrices satisfies target support for this equation. The equation therefore admits no word. This does not lower the eight-call minimum, and it does not speak about five, six, or seven calls.
+2. **Parity-image witness, not a census.** The same equation has an explicit rational solution whose integral span has full parity image `F2^2`. The three-frame route, "the image misses `(1,1)`, so an AB or PQ form kills every added frame," does not apply to every four-frame solution. That witness is still character-excluded by a direct count, and it is not a word.
+
+Selected κ stays `781451/250000000`. Nothing here is a multiplication theorem, a search failure presented as nonexistence, or a statement about five or more added frames.
+
+The determinant identity `sum of paid addresses = 4I` and the necessary condition "each target exponent is a subset sum of the paid labels" are inherited from the normalization recorded in `research/bit-two-signed-frame-floor/PROOF.md`, Section 1 (itself from PR2910 and PR6190). This file does not reprove them.
+
+## 1. Setup
+
+Addresses are rational symmetric 2-by-2 matrices. Write
+
+```
+A = diag(1,0),  B = diag(0,1),
+P = [[1,1],[1,1]]/2,  Q = [[1,-1],[-1,1]]/2.
+```
+
+A coefficient vector `(a,b,c)` means `aA + bB + cP`, with matrix
+
+```
+[[a + c/2, c/2], [c/2, b + c/2]],
+```
+
+trace `a+b+c`, and determinant `ab + c(a+b)/2`. The matrix is nonzero and rank one exactly when the vector is nonzero and the determinant is zero.
+
+The four targets and their coefficient vectors are
+
+```
+A+P = (1,0,1),   A+Q = (2,1,-1),
+B+P = (0,1,1),   B+Q = (1,2,-1).
+```
+
+Each has trace 2 and determinant `1/2`. Their sum is `2A+2B+2P+2Q = 4I`, with coefficient vector `(4,4,0)`.
+
+For a primitive integer direction `u = (u1,u2)` and a nonzero rational scale `s`,
+
+```
+s uu^T = s (u1(u1-u2), u2(u2-u1), 2 u1 u2).
+```
+
+Every nonzero symmetric rational rank-one matrix has this form. The parity image of an integral coefficient vector is
+
+```
+φ(a,b,c) = ((a+b) mod 2, c mod 2) in F2^2.
+```
+
+## 2. Only pairs can carry a target
+
+**Lemma 1.** Let `F1,F2,F3,F4` be nonzero symmetric rational rank-one matrices with sum `4I`. A subset sum equal to a target has size exactly 2.
+
+**Proof.** The empty sum is 0. A singleton has determinant 0, while each target has determinant `1/2`. The full sum is `4I`, with trace 8, while each target has trace 2. A three-element subset sums to a target `H` only if the omitted frame equals `4I-H`. For every target,
+
+```
+det(4I-H) = 16 - 4·tr(H) + det(H) = 16 - 8 + 1/2 = 17/2 ≠ 0,
+```
+
+so `4I-H` is not rank one. The only remaining subsets are the pairs.
+
+## 3. The fifteen pair patterns
+
+There are six unordered pairs among four calls and `C(6,4) = 15` ways to choose four of them. Each target would have to be a different pair, because the four targets are distinct. `verify.py` enumerates all 15 graphs. Their sorted degree sequences are only
+
+```
+(2,2,2,2)  three times,  and  (3,2,2,1)  twelve times.
+```
+
+That enumeration is exhaustive for the pair patterns. It is not a search over directions or scales.
+
+**Theorem 2.** No four nonzero symmetric rational rank-one matrices summing to `4I` have all four targets as subset sums.
+
+**Proof.** By Lemma 1 every target is a pair sum, so some four-edge graph as above has its four edge sums equal to the four targets. The sum of those edge sums is therefore `4I`.
+
+If every degree is 2, the edge sum is twice the sum of the four frames, hence `2·4I = 8I`. Then `8I = 4I`, which is false.
+
+If the degrees are 3, 2, 2, and 1, label the degree-3 call `F` and the unique edge disjoint from `F` by `X+Y`. The fourth call is `Z`. The edge sum is
+
+```
+3F + 2X + 2Y + Z.
+```
+
+Subtracting the total sum `F+X+Y+Z = 4I` gives the matrix identity
+
+```
+2F + X + Y = 0.
+```
+
+The edge `X+Y` equals some target `H`, so `F = -H/2`. Then
+
+```
+det(F) = det(-H/2) = (1/4)·det(H) = 1/8 ≠ 0,
+```
+
+so `F` is not rank one.
+
+Both patterns contradict the rank-one hypothesis. Therefore target support fails for every solution of the equation, and the equation admits no word.
+
+The direct eight-call word, two old labels on each target, is untouched. Theorem 2 removes only the four-call equation.
+
+## 4. A full parity image
+
+**Witness.** The directions and scales
+
+```
+(0,1) at -3,   (1,-1) at 5/2,   (1,1) at 1/2,   (1,2) at 1
+```
+
+give the integral frames
+
+```
+R = (0,-3,0),  S = (5,5,-5),  T = (0,0,1),  U = (-1,2,4).
+```
+
+Their sum is `(4,4,0)`. Each determinant is 0 and each vector is nonzero, so each frame is rank one. The integer combinations
+
+```
+R = (0,-3,0),   S = (5,5,-5),   S+U = (4,7,-1)
+```
+
+have parity images `(1,0)`, `(0,1)`, and `(1,1)`. The zero combination has image `(0,0)`. The parity image of the integral span is all of `F2^2`.
+
+In particular neither coordinate functional vanishes on that span. No integer form of shape `(odd,odd,even)` or `(even,even,odd)` is even on all four frames: the first shape reduces to `a+b` modulo 2, and `R` has `a+b` odd; the second reduces to `c` modulo 2, and `S` has `c` odd. The three-frame extension, which needs one of those shapes to kill every added frame, does not apply to this solution.
+
+This is one explicit solution. It is not an enumeration of all four-direction solutions, and a full parity image is not a word.
+
+## 5. The witness still fails a direct character count
+
+The same witness is excluded by the inherited call-versus-target inequality, without killing every frame. Reduce the coefficient of `P` modulo 2. All four targets have odd `P`-coefficient, so all four are detected. Among the frames, only `S` and `T` have odd `P`-coefficient, so two calls are detected. Two calls against four targets is forbidden.
+
+Theorem 2 already excludes the witness as a word. Section 5 records that evading the vanishing test is not the same as surviving every first-order character. The witness also fails support, as Theorem 2 requires: none of its fifteen nonempty subset sums equals a target. That fifteen-line check is a check of one solution, not the proof.
+
+## Open next questions
+
+Lengths 5, 6, and 7 with four added labels, and every decomposition with five or more added frames, are untouched. One extra old call changes both the residual and the allowed subset sizes, so Theorem 2 does not apply. A solution whose parity image is full can still fail a character that detects only some of the new frames.

research/four-signed-once-parity/README.md

@@ -0,0 +1,48 @@
+# Four once-each signed frames and the four-call equation
+
+**Support proof, plus one parity-image witness. No new κ and no word.**
+
+The shortest determinant equation that uses four new labels once each is `R+S+T+U = 4I`: four paid calls and no old call. In the PR2085/2112 model that equation admits no word. Every target would have to be a sum of two of the four rank-one frames, and all 15 ways of choosing four pairs contradict the rank-one hypothesis. The argument is written in [PROOF.md](PROOF.md).
+
+The same equation has one explicit rational solution whose parity image is all of `F2^2`. The three-frame test, which needs that image to miss `(1,1)`, does not apply to every four-frame solution. The witness is still excluded by a direct character count (two calls against four targets) and by the support proof. It is one solution, not a census, and it is not a word.
+
+The selected record stays κ = `781451/250000000`. Lengths 5, 6, and 7, and five or more added frames, stay open.
+
+## Scope and evidence
+
+Original card: `bit-new-register-model`, with `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 takes the four-frame question left open by the all-old-once three-frame note, discussion comment 19493126, which itself follows comment 19377832. It does not redo that three-frame proof and it does not take another three-frame census profile.
+
+Evidence classes, kept apart:
+
+1. **Proof.** Lemma 1 and Theorem 2 exclude target support for every rational solution of `R+S+T+U = 4I` by four nonzero symmetric rank-one matrices. The 15 pair graphs are the entire case split. The determinant identities `det H = 1/2`, `det(4I-H) = 17/2`, and `det(-H/2) = 1/8` are checked exactly.
+2. **Explicit witness, not a census.** Directions `(0,1)`, `(1,-1)`, `(1,1)`, `(1,2)` at scales `-3`, `5/2`, `1/2`, `1` sum to `4I`, and `R`, `S`, and `S+U` realize parity images `(1,0)`, `(0,1)`, and `(1,1)`. No AB or PQ form kills all four frames.
+3. **Direct count on that one witness.** The `P`-coefficient modulo 2 detects two calls and four targets. The inherited inequality is not reproved. The witness's fifteen nonempty subset sums miss every target; that list checks the witness and is not Theorem 2.
+
+The determinant identity and the subset-sum necessity are inherited from `research/bit-two-signed-frame-floor` and are not reproved. Predecessor replays, Lean, Docker, and the selected-result cold replay were not run.
+
+Source commits, Git blobs, and SHA256 pins are in [SOURCES.json](SOURCES.json). The selected record and catalogue are historical provenance. Full Git history is needed to resolve those pins.
+
+## Reproduce
+
+From the repository root, with Python 3.12:
+
+```sh
+python3 scripts/research_package.py --package research/four-signed-once-parity --check-only
+python3.12 scripts/research_package.py --package research/four-signed-once-parity
+```
+
+The direct check is `python3 -I -W error -B research/four-signed-once-parity/verify.py`.
+
+## Open next questions
+
+Can four added signed rank-one frames plus one, two, or three old calls meet support at length 5, 6, or 7? Theorem 2 uses exactly four calls. A useful first step is one old projector `E` and the equation `R+S+T+U = 4I-E`, then the same pair test on one rational solution. No such solution is supplied here.
+
+Can five or more added signed rank-one frames lower the eight-call minimum? The four-call support proof and the three-frame character both stop at the number of frames they assume. A useful first step is five primitive directions and the shortest determinant equation that uses each new label once.
+
+A full parity image does not by itself survive every character: the witness above is still excluded by a character that detects only two of the four frames.
+
+## Credit
+
+The register model is Cinna Davis's PR2085/2112 formal model. The determinant and the subset-sum necessity are the PR2910 package as recorded in apoursh's two-signed-frame floor, PR6190. That floor stopped at two added frames. The three-frame all-old-once character is the fork package `research/three-signed-old-once`, discussion comment 19493126, and is not redone here. The concrete handoff is discussion comment 19377832.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. No independent human or formal-kernel review. New work is Apache-2.0.

research/four-signed-once-parity/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ]
+}

research/four-signed-once-parity/TASK.json

@@ -0,0 +1,75 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "bit-new-register-model",
+    "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/bit-three-register-lower-bound/README.md",
+      "certificates/selected-result.json",
+      "research/bit-gl3-mixed-targets-length10/README.md",
+      "docs/research/community-efficient1000-review.md"
+    ],
+    "methods": [
+      "Construct the smallest exact identity in a newly specified legal operation alphabet.",
+      "Derive a target-specific relaxation bound for that same explicit alphabet."
+    ],
+    "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.",
+    "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.",
+    "allowed_variations": [
+      "Choose a fixed larger register count or a specified nonabelian operation family."
+    ],
+    "scope_change_triggers": [
+      "Remaining inside the already-excluded three-register abelian model.",
+      "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result."
+    ],
+    "overlap_terms": [
+      "three-register",
+      "nonabelian",
+      "group algebra"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "For the shortest four-label equation R+S+T+U=4I, prove that target support fails for every nonzero symmetric rational rank-one solution, and exhibit one solution whose parity image is all of F2^2.",
+  "scope_change_reason": "The card asks for a larger or nonabelian native alphabet. This package stays in the abelian symmetric 2-by-2 model and answers the four-frame question left open by the all-old-once three-frame character, for the single shortest once-each equation.",
+  "bottleneck_link": "Side result on the signed-frame escape. The four-call equation admits no word, so there is no local call-count saving and no selected-frontier change.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the four-call support proof and one explicit parity-image witness. Do not search lengths 5, 6, or 7, and do not start five or more frames.",
+  "outcome": "completed",
+  "evidence": "Support proof: every target has trace 2 and determinant 1/2, so only pair sums can match, and all 15 four-edge graphs give either 8I=4I or a frame equal to -H/2. Parity witness, not a census: directions (0,1),(1,-1),(1,1),(1,2) at scales -3,5/2,1/2,1 have full parity image and are still excluded by a two-call character count. The inherited determinant and subset-sum necessity are not reproved.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok assistance with the proof and verifier. No independent human or formal-kernel review.",
+  "open_questions": [
+    {
+      "question": "Can four added signed rank-one frames plus one, two, or three old calls meet support at length 5, 6, or 7?",
+      "why_it_matters": "Theorem 2 excludes only the four-call equation. A word at length 7 would lower the eight-call minimum.",
+      "first_step": "Fix one old projector E and the equation R+S+T+U=4I-E, then repeat the pair test on one rational rank-one solution.",
+      "blocked_by": "The pair classification uses exactly four calls. One extra old call changes the residual and the allowed subset sizes."
+    },
+    {
+      "question": "Can five or more added signed rank-one frames lower the eight-call minimum?",
+      "why_it_matters": "The four-call support proof and the three-frame character both stop at the number of frames they assume.",
+      "first_step": "Fix five primitive directions and the shortest determinant equation that uses each new label once, then repeat the parity-image test.",
+      "blocked_by": "No five-frame support or character reduction is supplied."
+    }
+  ],
+  "selection": {
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19377832",
+    "upstream_checked_utc": "2026-11-10T02:30:00Z",
+    "priority_revision": 8
+  }
+}

research/four-signed-once-parity/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Target determinant identities; exhaustive classification of all 15 four-edge pair graphs; one declared four-frame witness with full parity image, a two-call character count, and no target subset sum; failure controls for a tampered sum and for I as a rank-one summand."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Same identities, graph census, witness, and failure controls under python -O."
+    }
+  ]
+}