Record a length-6 support witness for two old signed frames (no κ)

research/four-signed-two-old-support/PROOF.md

@@ -0,0 +1,163 @@
+# Two old calls meet length-6 support
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+
+## Claim
+
+In the PR2085/2112 formal register model, fix two distinct old projectors
+`E, F ∈ {A, B, P, Q}`. The length-6 equation with four added frames, each
+used once, is
+
+```
+R + S + T + U = 4I - E - F.
+```
+
+An added frame may equal an old projector. That permission is the one stated
+for the length-5 equation in PR #7083; this note does not widen it.
+
+There is an explicit solution. The six matrices
+
+```
+A, B, P, Q, 2A, 2B
+```
+
+are nonzero symmetric rational rank-one matrices, they sum to `4I`, and every
+target is a subset sum. For every choice of two distinct projectors as
+`E, F`, the other four matrices are the added frames and satisfy the equation.
+Selected κ stays `781451/250000000`.
+
+This is one solution, not a classification. It is not a word. It does not
+say that every solution meets support, and it does not say that no solution
+is a word. Three old calls stay untouched. A bounded search that misses
+other solutions is not a census and is not used here.
+
+The identity "sum of the paid addresses = 4I" and the necessary condition
+"each target is a subset sum of the paid labels" are inherited from
+`research/bit-two-signed-frame-floor/PROOF.md`, Section 1. This file does
+not reprove them. The new fact is the witness and its subset scan.
+
+## 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`. For a primitive integer
+direction `(x,y)` and a nonzero rational scale `s`,
+
+```
+s uu^T = s (x(x-y), y(y-x), 2xy).
+```
+
+The four projectors and the two doubles are that form:
+
+| label | direction | scale | coefficients |
+|---|---|---|---|
+| `A` | `(1,0)` | `1` | `(1,0,0)` |
+| `B` | `(0,1)` | `1` | `(0,1,0)` |
+| `P` | `(1,1)` | `1/2` | `(0,0,1)` |
+| `Q` | `(1,-1)` | `1/2` | `(1,1,-1)` |
+| `2A` | `(1,0)` | `2` | `(2,0,0)` |
+| `2B` | `(0,1)` | `2` | `(0,2,0)` |
+
+Each vector is nonzero and has determinant `ab + c(a+b)/2 = 0`, so each
+matrix is rank one. Also `A+B = P+Q = I = (1,1,0)`.
+
+The four targets 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 `4I = (4,4,0)`. For
+each target `H`, `det(4I-H) = 17/2`, so `4I-H` is not rank one. A singleton
+therefore cannot be a target, and a five-label subset cannot be a target,
+because its complement would be `4I-H`.
+
+## 2. The six labels sum to 4I
+
+```
+A + B + P + Q + 2A + 2B
+  = 3A + 3B + (P+Q)
+  = 3(A+B) + (A+B)
+  = 4(A+B)
+  = 4I.
+```
+
+The same arithmetic is `3I + I`. No cancellation between the six matrices is
+required beyond `P+Q = A+B`.
+
+## 3. Every target is a two-label sum
+
+The four projector pairs are labels in the witness:
+
+```
+A+P,  A+Q,  B+P,  B+Q.
+```
+
+Each target is that pair, so each target is a subset sum of size 2. The
+checker also scans all 63 nonempty subsets and records that, on this
+solution, no target has a carrier of any other size. That scan is a check
+of one solution. It is not a proof that every support solution is a pair of
+projectors.
+
+## 4. Every old pair leaves four added frames
+
+There are six ways to designate `E` and `F`. In each case both are among
+the four projectors, so both are labels, and the other four labels are the
+added frames. Those four are nonzero and rank one by Section 1. Their sum
+is `4I-E-F` because the six labels sum to `4I`.
+
+The three pair-orbits under coordinate exchange and the sign flip are
+represented by `{A,B}`, `{P,Q}`, and `{A,P}`:
+
+| old calls | added frames | residual |
+|---|---|---|
+| `A,B` | `P, Q, 2A, 2B` | `3I` |
+| `P,Q` | `A, B, 2A, 2B` | `3I` |
+| `A,P` | `B, Q, 2A, 2B` | `4I-A-P` |
+
+The other three pairs are the images of `{A,P}`. The subset scan of
+Section 3 uses the same six labels for every row, so support holds for
+each designation.
+
+## 5. This witness fails the odd-c count
+
+Reduce the coefficient of `P` modulo 2. All four targets have odd `c`.
+Among the six labels, `P` has `c=1` and `Q` has `c=-1`; `A`, `B`, `2A`,
+and `2B` have `c` even. Two calls are detected and four targets are
+detected.
+
+The inherited call-versus-target inequality in
+`research/bit-two-signed-frame-floor/PROOF.md`, Section 1, equation (2),
+says that a word needs at least as many detected calls as detected targets.
+This note does not reprove that inequality. Under it, the witness is not a
+word. Support is necessary and, on this solution, not sufficient. Nothing
+here lowers the eight-call minimum or changes the selected record.
+
+## 6. What is not claimed
+
+The length-5 equation `R+S+T+U = 4I-E` is the separate support proof in
+PR #7083. This witness uses six labels and does not reopen that proof.
+Three old calls, the equation `R+S+T+U = 4I-E-F-G`, are a different
+residual. No statement is made about added frames forced to lie outside
+`{A,B,P,Q}`: the permission used here is exactly that they may lie inside
+that set. One solution with that permission does not classify the solutions
+that avoid it.
+
+## Open next questions
+
+Does any other solution of `R+S+T+U = 4I-E-F` meet support and also meet
+the odd-c count, with at least four labels of odd `c`? This witness has
+only two. A word at length 6 would be shorter than the eight-call minimum.
+The first step is one other integral solution with at least four odd-c
+labels, then the same subset scan. This package does not list the solutions.
+
+Can four added frames plus three old calls meet support at length 7? The
+first step is `R+S+T+U = 4I-E-F-G` for three distinct projectors and one
+rational rank-one solution's subset scan. The six-label witness does not
+supply a seventh label.

research/four-signed-two-old-support/README.md

@@ -0,0 +1,87 @@
+# Two old calls meet length-6 support
+
+**Explicit support witness. No new κ and no word.**
+
+Four nonzero symmetric rational rank-one matrices and two distinct old
+projectors can meet target support for
+
+```
+R + S + T + U = 4I - E - F.
+```
+
+The six labels `A`, `B`, `P`, `Q`, `2A`, and `2B` sum to `4I`. Each target
+is one of the pairs `A+P`, `A+Q`, `B+P`, and `B+Q`. Designating any two of
+the four projectors as the old calls leaves the other four labels as added
+frames. Added frames may equal old projectors; that is the permission already
+stated for the length-5 equation. The argument is written in [PROOF.md](PROOF.md).
+
+The same six labels fail the inherited odd-`c` count: `P` and `Q` are the
+only labels with odd `c`, while all four targets have odd `c`. Under that
+inherited inequality the witness is not a word. The inequality is not
+reproved. Selected κ stays `781451/250000000`.
+
+## 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 two-old length-6 question
+left open by the one-old support proof, PR #7083, which itself follows the
+four-call note `research/four-signed-once-parity`. It does not redo either
+proof, and it does not take another three-frame census profile.
+
+Evidence classes, kept apart:
+
+1. **Explicit witness.** The six matrices are the standard `uu^T` frames at
+   the scales in [PROOF.md](PROOF.md). They are nonzero, rank one, and sum
+   to `4I` because `P+Q = A+B = I`. Every old pair is checked, not only one
+   orbit representative.
+2. **Subset scan of that one solution.** All 63 nonempty subsets are summed.
+   Each target occurs, and on this solution it occurs only as the declared
+   projector pair. This is not a census of solutions.
+3. **Odd-c count on that same solution.** Two calls, four targets. The
+   inherited inequality is not reproved. Dropping `Q` removes `A+Q` and
+   `B+Q` and keeps `A+P` and `B+P`. Shifting `2A` by `A` breaks the sum.
+
+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.
+No search over directions or scales is claimed, successful or otherwise.
+
+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-two-old-support --check-only
+python3.12 scripts/research_package.py --package research/four-signed-two-old-support
+```
+
+The direct check is `python3 -I -W error -B research/four-signed-two-old-support/verify.py`.
+
+## Open next questions
+
+Does any other solution of `R+S+T+U = 4I-E-F` meet support and also have at
+least four labels of odd `c`? This witness has two, so the inherited count
+excludes it and does not exclude a different solution. A word at length 6
+would be shorter than the eight-call minimum. The first step is one other
+integral solution with four odd-`c` labels, then the same subset scan.
+
+Can four added frames plus three old calls meet support at length 7? The
+six-label witness has no seventh matrix. The first step is three distinct
+projectors and `R+S+T+U = 4I-E-F-G`, then one rational solution's subset scan.
+
+## 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. The four-call once-each support proof is
+`research/four-signed-once-parity`, PR #6952. The one-old length-5 support
+proof, whose open question asks for this two-old scan, is PR #7083. Neither
+proof is redone here.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. No independent
+human or formal-kernel review. New work is Apache-2.0.

research/four-signed-two-old-support/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840",
+  "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-two-old-support/TASK.json

@@ -0,0 +1,75 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 8,
+  "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840",
+  "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": "Exhibit one rational rank-one solution of R+S+T+U=4I-E-F, for every pair of distinct old projectors, on which all four targets are subset sums, and record that this solution fails the inherited odd-c count.",
+  "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 two-old length-6 support question left open by the one-old equation, for one explicit witness rather than a new alphabet.",
+  "bottleneck_link": "Side result on the signed-frame escape. Support holds for this length-6 witness, but the witness fails the inherited odd-c count, so there is no local call-count saving and no selected-frontier change.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after one explicit six-label support witness and its odd-c count. Do not classify other solutions, and do not start the three-old length-7 equation.",
+  "outcome": "completed",
+  "evidence": "Witness: A,B,P,Q,2A,2B are nonzero rank-one frames summing to 4I because P+Q=A+B=I. Every target is the corresponding projector pair. Every choice of two projectors as old calls leaves four rank-one added frames. Odd c detects P and Q only, against four targets. The inherited inequality is not reproved. This is one solution, not a census.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok assistance with the witness and verifier. No independent human or formal-kernel review.",
+  "open_questions": [
+    {
+      "question": "Does any other solution of R+S+T+U=4I-E-F meet support and also have at least four labels of odd c?",
+      "why_it_matters": "This witness meets support and fails the inherited odd-c count, so it is not a word. A different solution that meets both tests would be shorter than the eight-call minimum.",
+      "first_step": "Find one other integral solution with at least four odd-c labels and repeat the subset scan.",
+      "blocked_by": "This package does not classify the solutions of the length-6 equation."
+    },
+    {
+      "question": "Can four added rank-one frames plus three old calls meet support at length 7?",
+      "why_it_matters": "Length 7 is the remaining once-each profile with four added frames. A word there would be shorter than the eight-call minimum.",
+      "first_step": "Fix three distinct projectors and the equation R+S+T+U=4I-E-F-G, then scan one rational rank-one solution.",
+      "blocked_by": "The six-label witness has no seventh matrix, and the length-6 subset sizes do not transfer."
+    }
+  ],
+  "selection": {
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/pull/7083",
+    "upstream_checked_utc": "2026-11-10T13:30:00Z",
+    "priority_revision": 8
+  }
+}

research/four-signed-two-old-support/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; the six declared uu^T frames sum to 4I; every pair of old projectors leaves four rank-one added frames; each target is the declared size-2 projector pair on this solution; the odd-c count is two calls against four targets; failure controls for dropping Q and for tampering 2A."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Same identities, witness, subset scan, old-pair check, character count, and failure controls under python -O."
+    }
+  ]
+}