diff --git a/research/four-signed-two-old-support/PROOF.md b/research/four-signed-two-old-support/PROOF.md new file mode 100644 index 0000000000..5d660e68aa --- /dev/null +++ b/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. diff --git a/research/four-signed-two-old-support/README.md b/research/four-signed-two-old-support/README.md new file mode 100644 index 0000000000..6f18d8fff8 --- /dev/null +++ b/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. diff --git a/research/four-signed-two-old-support/SOURCES.json b/research/four-signed-two-old-support/SOURCES.json new file mode 100644 index 0000000000..41a0d8e4ed --- /dev/null +++ b/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" + } + ] +} diff --git a/research/four-signed-two-old-support/TASK.json b/research/four-signed-two-old-support/TASK.json new file mode 100644 index 0000000000..016d1a90cf --- /dev/null +++ b/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 + } +} diff --git a/research/four-signed-two-old-support/VERIFY.json b/research/four-signed-two-old-support/VERIFY.json new file mode 100644 index 0000000000..ed9a4cecb0 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/four-signed-two-old-support/verify.py b/research/four-signed-two-old-support/verify.py new file mode 100644 index 0000000000..e6cf092b82 --- /dev/null +++ b/research/four-signed-two-old-support/verify.py @@ -0,0 +1,176 @@ +#!/usr/bin/env python3 +"""Checks for one length-6 support witness with two old projectors. + +PROOF.md is the argument. This program checks that one declared six-label +solution sums to 4I, that every pair of old projectors leaves four rank-one +added frames, that every target is a two-label subset sum, and that the +odd-c count on this same solution is two calls against four targets. +The witness is one solution, not a census. +""" + +from fractions import Fraction +from itertools import combinations + + +def require(condition, message): + if not condition: + raise SystemExit("FAIL: " + message) + + +def add(frames): + rows = tuple(frames) + return tuple(sum(frame[index] for frame in rows) for index in range(3)) + + +def determinant(frame): + a, b, c = frame + return a * b + c * (a + b) / 2 + + +def rank_one_nonzero(frame): + return frame != (0, 0, 0) and determinant(frame) == 0 + + +def coefficient(direction, scale): + x, y = direction + scale = Fraction(scale) + return (scale * x * (x - y), scale * y * (y - x), scale * 2 * x * y) + + +def parity_c(frame): + require(all(value.denominator == 1 for value in frame), "odd-c test on a non-integral frame") + return int(frame[2]) % 2 + + +A = (1, 0, 0) +B = (0, 1, 0) +P = (0, 0, 1) +Q = (1, 1, -1) +TWO_A = (2, 0, 0) +TWO_B = (0, 2, 0) +FOUR = (4, 4, 0) +PROJECTORS = (A, B, P, Q) +LABELS = (A, B, P, Q, TWO_A, TWO_B) +NAMES = ("A", "B", "P", "Q", "2A", "2B") + + +def targets(): + return { + "AP": add((A, P)), + "AQ": add((A, Q)), + "BP": add((B, P)), + "BQ": add((B, Q)), + } + + +def target_identities(rows): + require(add(rows.values()) == FOUR, "the four targets do not sum to 4I") + for name, row in rows.items(): + require(row[0] + row[1] + row[2] == 2, name + " does not have trace 2") + require(determinant(row) == Fraction(1, 2), name + " does not have determinant 1/2") + complement = add((FOUR, tuple(-value for value in row))) + require(determinant(complement) == Fraction(17, 2), name + " complement determinant changed") + require(parity_c(row) == 1, name + " does not have odd c") + + +def witness_parameterization(): + require(coefficient((1, 0), 1) == A, "A is not the scale-1 axis frame") + require(coefficient((0, 1), 1) == B, "B is not the scale-1 axis frame") + require(coefficient((1, 1), Fraction(1, 2)) == P, "P is not the declared uu^T frame") + require(coefficient((1, -1), Fraction(1, 2)) == Q, "Q is not the declared uu^T frame") + require(coefficient((1, 0), 2) == TWO_A, "2A is not scale 2 on (1,0)") + require(coefficient((0, 1), 2) == TWO_B, "2B is not scale 2 on (0,1)") + require(add((P, Q)) == add((A, B)) == (1, 1, 0), "P+Q and A+B are not both I") + + +def witness_sum(): + for frame, name in zip(LABELS, NAMES): + require(rank_one_nonzero(frame), name + " is not nonzero rank one") + require(add(LABELS) == FOUR, "the six labels do not sum to 4I") + # 3(A+B) + (P+Q) = 3I + I = 4I, using P+Q = A+B = I. + require(add((A, B, P, Q, TWO_A, TWO_B)) == add(( + add((A, A, A)), add((B, B, B)), add((A, B)), + )), "the written sum identity does not match the six labels") + + +def support_scan(rows): + found = {name: [] for name in rows} + for mask in range(1, 1 << 6): + chosen = [LABELS[index] for index in range(6) if mask & (1 << index)] + total = add(chosen) + for name, row in rows.items(): + if total == row: + found[name].append((mask, len(chosen))) + expected = { + "AP": (1 << 0) | (1 << 2), # A+P + "AQ": (1 << 0) | (1 << 3), # A+Q + "BP": (1 << 1) | (1 << 2), # B+P + "BQ": (1 << 1) | (1 << 3), # B+Q + } + for name, mask in expected.items(): + hits = found[name] + require(hits == [(mask, 2)], name + " is not exactly the declared projector pair: " + str(hits)) + + +def every_old_pair(): + rows = targets() + for left, right in combinations(range(4), 2): + old = {left, right} + added = [LABELS[index] for index in range(6) if index not in old] + require(len(added) == 4, "an old pair did not leave four added frames") + for frame in added: + require(rank_one_nonzero(frame), "an added frame is not rank one") + residual = add((FOUR, tuple(-LABELS[left][i] for i in range(3)), + tuple(-LABELS[right][i] for i in range(3)))) + require(add(added) == residual, NAMES[left] + "+" + NAMES[right] + " residual mismatch") + # The six-label scan already hits every target; recheck on this designation. + labels = [LABELS[left], LABELS[right], *added] + seen = set() + for mask in range(1, 1 << 6): + total = add(labels[index] for index in range(6) if mask & (1 << index)) + if total in rows.values(): + seen.add(total) + require(seen == set(rows.values()), NAMES[left] + "+" + NAMES[right] + " misses a target") + + +def character_count(): + detected_calls = sum(parity_c(frame) for frame in LABELS) + detected_targets = sum(parity_c(row) for row in targets().values()) + require(detected_calls == 2, "odd c detects something other than P and Q") + require(parity_c(P) == 1 and parity_c(Q) == 1, "P or Q lost its odd c") + require(parity_c(A) == parity_c(B) == parity_c(TWO_A) == parity_c(TWO_B) == 0, + "an even label became odd") + require(detected_targets == 4, "odd c does not detect every target") + require(detected_calls < detected_targets, "the witness is not a direct character obstruction") + + +def failure_controls(rows): + without_q = [frame for frame in LABELS if frame != Q] + hits = set() + for mask in range(1, 1 << len(without_q)): + total = add(without_q[index] for index in range(len(without_q)) if mask & (1 << index)) + if total in rows.values(): + hits.add(total) + require(rows["AQ"] not in hits and rows["BQ"] not in hits, "dropping Q still realizes an AQ or BQ target") + require(rows["AP"] in hits and rows["BP"] in hits, "dropping Q lost a target that does not use Q") + tampered = (A, B, P, Q, add((TWO_A, (1, 0, 0))), TWO_B) + require(add(tampered) != FOUR, "tampered 2A still sums to 4I") + require(determinant((1, 1, 0)) == 1, "det I changed") + require(not rank_one_nonzero((1, 1, 0)), "I was accepted as rank one") + require(rank_one_nonzero((0, 0, 0)) is False, "the zero matrix was accepted") + + +def main(): + rows = targets() + target_identities(rows) + witness_parameterization() + witness_sum() + support_scan(rows) + every_old_pair() + character_count() + failure_controls(rows) + print("PASS four-signed-two-old-support checks") + + +if __name__ == "__main__": + main()