From 977b3451cea127c598cb07315180fc6c6bc4f4b6 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 10 Nov 2026 09:05:21 +0000 Subject: [PATCH] Prove four rank-one frames plus one old call miss length-5 support. The equation R+S+T+U=4I-E has no target support for one old projector, so that length-5 profile admits no word. Selected kappa is unchanged. Co-authored-by: unpaidmoon --- research/four-signed-one-old/PROOF.md | 273 +++++++++++++ research/four-signed-one-old/README.md | 50 +++ research/four-signed-one-old/SOURCES.json | 18 + research/four-signed-one-old/TASK.json | 75 ++++ research/four-signed-one-old/VERIFY.json | 34 ++ research/four-signed-one-old/verify.py | 471 ++++++++++++++++++++++ 6 files changed, 921 insertions(+) create mode 100644 research/four-signed-one-old/PROOF.md create mode 100644 research/four-signed-one-old/README.md create mode 100644 research/four-signed-one-old/SOURCES.json create mode 100644 research/four-signed-one-old/TASK.json create mode 100644 research/four-signed-one-old/VERIFY.json create mode 100644 research/four-signed-one-old/verify.py diff --git a/research/four-signed-one-old/PROOF.md b/research/four-signed-one-old/PROOF.md new file mode 100644 index 0000000000..4c0077e784 --- /dev/null +++ b/research/four-signed-one-old/PROOF.md @@ -0,0 +1,273 @@ +# Four rank-one frames plus one old call miss length 5 + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. + +## Claim + +In the PR2085/2112 formal register model, consider five paid labels: four nonzero symmetric rational rank-one matrices `R,S,T,U`, each used once, and one old projector + +``` +E ∈ {A, B, P, Q}, +``` + +also used once. The determinant identity for this count is + +``` +R + S + T + U = 4I - E. +``` + +No such matrices have all four targets as subset sums. The count therefore admits no word. Selected κ stays `781451/250000000`. + +This is one equation, the length-5 profile with exactly one old call. It does not speak about two or three old calls, about five or more added frames, or about any larger alphabet. A solution of the sum equation is not by itself a word; the support obstruction is what excludes the word. The two declared solutions in Section 8 satisfy the sum and are not a classification of all such sums. + +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 argument is the support obstruction for this one residual. + +## 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 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. Every nonzero symmetric rational rank-one matrix has this form for some primitive integer direction and nonzero rational scale. Either sign is allowed, and a new frame may repeat an old projector. + +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) = 16 - 4·tr(H) + det(H) = 17/2 ≠ 0, +``` + +so `4I-H` is not rank one. Write + +``` +φ(a,b,c) = ((a+b) mod 2, c mod 2). +``` + +Each target has `φ = (1,1)`. The vector `4I` is even in every coordinate, so each complement `4I-H` has `φ = (1,1)` as well. Thus all eight possible pair-sums below have parity `(1,1)` and trace 2 or 6. + +Two linear automorphisms are used to move projectors. The coordinate exchange is `(a,b,c) ↦ (b,a,c)`. It swaps `A` with `B`, fixes `P` and `Q`, and swaps `A+P` with `B+P` and `A+Q` with `B+Q`. The sign flip is `(a,b,c) ↦ (a+c, b+c, -c)`. It swaps `P` with `Q`, fixes `A` and `B`, and swaps `A+P` with `A+Q` and `B+P` with `B+Q`. Both are conjugations by an invertible rational matrix, namely the exchange matrix and `diag(1,-1)`, so both preserve rank, determinant, and subset sums, and both fix `4I`. A support solution for `E=B` would exchange to a support solution for `E=A`. A support solution for `E=Q` would flip to a support solution for `E=P`. The case split is written for `A` and `P`. The verifier repeats the same arithmetic for `B` and `Q`. + +## 2. Only pairs and triples can carry a target + +**Lemma 1.** Let five nonzero symmetric rational rank-one matrices sum to `4I`. A subset summing to a target has size 2 or 3. + +**Proof.** The empty sum is 0. A singleton has determinant 0, while each target has determinant `1/2`. The full sum is `4I`. A four-element subset sums to a target `H` only if the omitted matrix equals `4I-H`, which has determinant `17/2` and is not rank one. + +Each target therefore determines a unique unordered pair: the size-2 block of the partition into 2+3. That pair sums to `H` or to `4I-H`. Different targets give different pairs, because `H` and `4I-H` are not targets (traces 2 and 6) and the four targets are distinct. The carrying graph has four edges on the five labels. + +## 3. The carrying graph is bipartite + +**Lemma 2.** Every carrying edge joins coefficient vectors whose parities differ by `(1,1)`. The carrying graph has no odd cycle. + +**Proof.** Section 1 records that every admissible edge sum, whether `H` or `4I-H`, has `φ = (1,1)`. Endpoint parities therefore differ by `(1,1)`. An odd cycle has no such 2-coloring. + +## 4. The remaining graphs + +**Lemma 3.** A simple graph with five vertices and four edges, and with no odd cycle, is a tree or a 4-cycle plus an isolated vertex. The trees are the star, the path, and the fork of degrees `3,2,1,1,1`. + +**Proof.** With no odd cycle the graph is bipartite. If it is acyclic, then `e = v-1`, so it is a tree. Five positive degrees summing to 8 are one of + +``` +(4,1,1,1,1), (3,2,1,1,1), (2,2,2,1,1), +``` + +and each sequence determines one tree: the star, the fork, and the path. + +If the graph contains a cycle, the excess is `e-v+c = c-1 ≥ 1`, so there are at least two components. The cyclic component then has `n` vertices and `n` edges, and the complementary forest has `5-n` vertices and `4-n` edges. A forest on `m` vertices has at most `m-1` edges, and `4-n ≤ (5-n)-1`, so equality holds: the complement is a tree and there are exactly two components. Thus `n ≥ 4` for a simple even cycle, and `n ≤ 4` because the complement is nonempty. The cyclic component is a 4-cycle, and the other component is a single vertex. + +## 5. Every tree misses the projector trace + +**Lemma 4.** No carrying tree is consistent with `E` having trace 1. + +**Proof.** Every carrying edge has trace 2 or 6. + +On the star, label the center `C` and the edge sums `M1,M2,M3,M4`. The leaves are `Mi-C`, so + +``` +M1+M2+M3+M4 - 3C = 4I. +``` + +Traces give `4k = 3 tr(C)` for some integer `k` with `0 ≤ k ≤ 4`, hence `3 tr(C) ≡ 0 (mod 4)`. If the center is `E`, then `tr(C)=1` and `3 ≢ 0 (mod 4)`. If `E` is a leaf of edge `M`, then `C = M-E` and `tr(C) ∈ {1,5}`. In both subcases `3 tr(C) ≡ 3 (mod 4)`. + +On the path `F0-F1-F2-F3-F4` with edge sums `M0,M1,M2,M3`, propagation gives + +``` +F0 = 4I - M1 - M3 +``` + +and then `Fi+1 = Mi - Fi`. Substituting produces + +``` +F0+F1+F2+F3+F4 = F0 + M1 + M3, +``` + +so the displayed formula is forced by the total sum. The five traces are + +``` +8-tr(M1)-tr(M3), +tr(M0)+tr(M1)+tr(M3)-8, +8-tr(M0)-tr(M3), +tr(M0)+tr(M2)+tr(M3)-8, +8-tr(M0)-tr(M2). +``` + +Each input trace is even and 8 is even, so every vertex trace is even. The projector trace is 1. + +On the fork, let `C` meet leaves `L1,L2` and a degree-2 vertex `D`, and let `D` meet the third leaf `L3`. With edge sums `M1,M2` at the leaves of `C`, bridge `Mcd`, and outer edge `M3`, + +``` +L1=M1-C, L2=M2-C, D=Mcd-C, L3=M3-D. +``` + +The bridge cancels in the total sum and leaves + +``` +C = M1+M2+M3-4I. +``` + +Every vertex is an integer combination of even-trace matrices and `4I`, so every vertex trace is even. + +`verify.py` checks the path and fork closed forms on an affine basis and checks that all 16 trace patterns stay even. + +## 6. A 4-cycle opposite the old call has odd trace + +**Lemma 5.** The carrying graph cannot be a 4-cycle on the four new frames with `E` isolated. + +**Proof.** Order the cycle `F0,F1,F2,F3` with edge sums `M01,M12,M23,M30`. Solving the edges leaves one free matrix, and the cycle consistency condition is independent of that matrix. The sum of the four frames collapses to `M12+M30`. The total sum would require + +``` +M12+M30 = 4I-E. +``` + +The left side has even trace. The right side has trace `8-1 = 7`. + +## 7. The 4-cycle through the old call + +The only graph left is a 4-cycle through `E` and three new frames, with the fourth new frame isolated. Order the cycle `E,X,Z,Y`. + +**Lemma 6.** If `X` and `Y` are rank one, the two edges at `E` are direct target sums, and they are the unique pair in the following table. + +| `E` | edges at `E` | resulting neighbors | +|---|---|---| +| `A` | `A+P`, `A+Q` | `P`, `Q` | +| `B` | `B+P`, `B+Q` | `P`, `Q` | +| `P` | `A+P`, `B+P` | `A`, `B` | +| `Q` | `A+Q`, `B+Q` | `A`, `B` | + +**Proof.** There are eight candidate edge matrices. For `E=A`, + +``` +(A+P)-A = P, (A+Q)-A = Q, +(B+P)-A = (-1,1,1), det = -1, +(B+Q)-A = (0,2,-1), det = -1, +``` + +and the four complements `4I-H-A` have determinants `5,5,6,6`. Only `A+P` and `A+Q` work. They use different targets, so both edges at `E` are accounted for. The same eight evaluations with `E=P` leave only `(A+P)-P = A` and `(B+P)-P = B`; the other six determinants are `-1,-1,5,6,5,6`. The rows `B` and `Q` follow by the automorphisms of Section 1, and the verifier recomputes them directly. + +The opposite edges must carry the other two targets, each either direct or complemented. Write `MX,MY` for the edge sums at `E` and `RX,RY` for the opposite sums. Consistency is `MX+RY = MY+RX`, or + +``` +RY - RX = MY - MX. +``` + +For `E=A` and `(MX,MY) = (A+P, A+Q)`, the required difference is `Q-P = (1,1,-2)`. The eight ways to assign `{B+P, B+Q}` and their complements are: + +| `X-Z` | `Y-Z` | difference | +|---|---|---| +| `B+P` | `B+Q` | `(1,1,-2)` | +| `B+P` | `4I-(B+Q)` | `(3,1,0)` | +| `4I-(B+P)` | `B+Q` | `(-3,-1,0)` | +| `4I-(B+P)` | `4I-(B+Q)` | `(-1,-1,2)` | +| `B+Q` | `B+P` | `(-1,-1,2)` | +| `B+Q` | `4I-(B+P)` | `(3,1,0)` | +| `4I-(B+Q)` | `B+P` | `(-3,-1,0)` | +| `4I-(B+Q)` | `4I-(B+P)` | `(1,1,-2)` | + +Only the first and last rows match `(1,1,-2)`. The opposite neighbor order asks for `(1,1,-2)` negated, which selects the fourth and fifth rows. Those four labelings produce two framesets. + +Direct opposite edges `B+P` and `B+Q`: + +``` +X = P, Y = Q, Z = B, W = 2I. +``` + +Here `W` is the isolated frame. `det(2I) = 4 ≠ 0`. + +Both opposite edges complemented: + +``` +X = P, Y = Q, Z = (3,2,0), W = (-1,1,0), +``` + +with determinants `6` and `-1`. + +For `E=P` and `(MX,MY) = (A+P, B+P)`, the required difference is `(B+P)-(A+P) = (-1,1,0)`. Among the eight assignments of `{A+Q, B+Q}`, the matches are the direct pair + +``` +(B+Q) - (A+Q) = (-1,1,0) +``` + +and the fully complemented pair + +``` +(4I-(A+Q)) - (4I-(B+Q)) = (B+Q)-(A+Q) = (-1,1,0). +``` + +The other six differences are not `(-1,1,0)`. These two rows give + +``` +X = A, Y = B, Z = Q, W = 2I +``` + +and + +``` +X = A, Y = B, Z = (2,2,1), W = (1,1,-2), +``` + +with a determinant `4`, or determinants `6` and `-1`. Swapping the two edges at `E` repeats these frames. In every consistent labeling, some new frame has nonzero determinant. + +## 8. Two declared solutions of the sum + +The sum equation alone has rational rank-one solutions. Two are recorded here. They are examples, not a census. + +For `E=A`, the directions and scales + +``` +(1,0) at 4, (0,1) at 2, (1,1) at -2, (1,2) at 1 +``` + +give `(4,0,0)`, `(0,2,0)`, `(0,0,-4)`, and `(-1,2,4)`. Their sum is `(3,4,0) = 4I-A`. Each is nonzero and rank one. None of the 31 nonempty subsets of these four frames together with `A` equals a target. In particular the pair test, restricted to size-2 sums, finds no target. + +For `E=P`, the directions and scales + +``` +(1,0) at 1, (0,1) at 1, (1,1) at 1, (1,-1) at 3/2 +``` + +give `A`, `B`, `(0,0,2)`, and `(3,3,-3)`. Their sum is `(4,4,-1) = 4I-P`. The pairs `A+P` and `B+P` are targets, so a pair test on this one solution does not miss every target. The other two targets are not subset sums of any size. Support still fails. One solution's pair test is not the theorem. + +## 9. Census, as a separate check + +Lemma 1 reduces support to a finite set of carrying assignments: four distinct pairs on five labeled vertices, a bijection from the four targets to those pairs, and a direct-or-complement bit for each target. There are `P(10,4)·16 = 80640` assignments for each of the four projectors. + +`verify.py` solves each assignment by exact integer elimination, independently of the tree and cycle case split. For each projector it finds 80064 inconsistent systems and 576 consistent systems. Every consistent system has degree sequence `(2,2,2,2,0)` with `E` of degree 2, so the census independently sees only the 4-cycle through `E`. None of the 576 solutions is four nonzero rank-one frames. A planted near-miss, the frames `P,B,Q,2I` with `E=A`, solves back to those frames, and changing one edge sum makes the system inconsistent. + +This census is exhaustive for the finite domain in Lemma 1. It is not a search over directions, scales, or denominators, and it is not a heuristic. It is a second proof of the same support statement. It does not replace the case split, and the case split does not assume the census. + +## 10. Consequence + +By the inherited subset-sum necessity, a word with these five labels would have all four targets as subset sums. No such labels exist, so the length-5 profile admits no word. The direct eight-call word is untouched. Nothing here lowers the eight-call minimum or changes the selected record. + +## Open next questions + +Two old calls, and three old calls, are open. Lemmas 3 through 7 use five labels. A sixth label changes the allowed subset sizes and the degree sum, so the 4-cycle analysis does not apply. diff --git a/research/four-signed-one-old/README.md b/research/four-signed-one-old/README.md new file mode 100644 index 0000000000..d30205fa55 --- /dev/null +++ b/research/four-signed-one-old/README.md @@ -0,0 +1,50 @@ +# Four rank-one frames plus one old call + +**Support proof for one length-5 profile. No new κ and no word.** + +Four nonzero symmetric rational rank-one matrices and one old projector `E ∈ {A,B,P,Q}` do not meet target support for + +``` +R + S + T + U = 4I - E. +``` + +In the PR2085/2112 model that is the length-5 profile with four added frames, each used once, and exactly one old call. The profile admits no word. The argument is written in [PROOF.md](PROOF.md). + +The selected record stays κ = `781451/250000000`. Lengths 6 and 7, with two or three old calls, stay open. Five or more added frames stay the separate question in [research/four-signed-once-parity](../four-signed-once-parity). + +## 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 one-old-call question left open by the four-call note, discussion comment 19507121. It does not redo that four-call proof, the three-frame character, or another three-frame census profile. + +Evidence classes, kept apart: + +1. **Proof.** Lemmas 1–7 exclude target support for every rational solution of `R+S+T+U = 4I-E` by four nonzero symmetric rank-one matrices and one old projector. Subset size, parity, the tree list, and the two 4-cycle framesets are the whole case split. The determinant identities `det H = 1/2` and `det(4I-H) = 17/2` are checked exactly. +2. **Exhaustive finite census of the same carrying assignments.** For each of the four projectors, all `80640` choices of four distinct pairs, target bijections, and direct-or-complement bits are solved by exact integer elimination. Each projector has 576 consistent systems, all of them 4-cycles through `E`, and none of those solutions is rank one. This is not a search over directions or scales. +3. **Two declared solutions of the sum, not a census.** For `E=A`, directions `(1,0),(0,1),(1,1),(1,2)` at scales `4,2,-2,1` sum to `4I-A`, and no nonempty subset of the five labels is a target. For `E=P`, directions `(1,0),(0,1),(1,1),(1,-1)` at scales `1,1,1,3/2` sum to `4I-P`. Exactly two targets, `A+P` and `B+P`, occur as pairs, and the other two targets do not occur at all. A pair test on one solution is not the theorem. + +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-one-old --check-only +python3.12 scripts/research_package.py --package research/four-signed-one-old +``` + +The direct check is `python3 -I -W error -B research/four-signed-one-old/verify.py`. + +## Open next questions + +Can four added signed rank-one frames plus two old calls meet support at length 6? A word at length 6 would still be shorter than the eight-call minimum. The first step is two old projectors `E,F`, the equation `R+S+T+U = 4I-E-F`, and one rational rank-one solution's subset scan. The five-label case split does not apply: a sixth label changes the allowed subset sizes. + +Can the same four frames plus three old calls meet support at length 7? That is the shortest remaining profile in the question left by the four-call note. The first step is three old projectors and `R+S+T+U = 4I-E-F-G`. Seven labels are a different graph, so neither the length-5 cycle list nor a failed length-6 search would settle it. + +## 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, discussion comment 19507121, and is not redone here. The three-frame all-old-once character and the `(0,2,1,1)` profile are neighboring results and are not reused as lemmas. + +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-one-old/SOURCES.json b/research/four-signed-one-old/SOURCES.json new file mode 100644 index 0000000000..41a0d8e4ed --- /dev/null +++ b/research/four-signed-one-old/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-one-old/TASK.json b/research/four-signed-one-old/TASK.json new file mode 100644 index 0000000000..4f1f5547ea --- /dev/null +++ b/research/four-signed-one-old/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": "For one old projector E and four nonzero symmetric rational rank-one matrices, prove that R+S+T+U=4I-E has no target support, and record two rational solutions of the sum whose subset scans miss support.", + "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 one-old-call question left open by the four once-each frames, for the single length-5 equation.", + "bottleneck_link": "Side result on the signed-frame escape. The length-5 one-old-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 length-5 one-old-call support proof, its carrying-assignment census, and two declared sum-solutions. Do not start two or three old calls, and do not start five or more frames.", + "outcome": "completed", + "evidence": "Proof: subset sizes are only 2 or 3, the carrying graph is bipartite, trees miss trace 1, an isolated old call has odd trace, and the 4-cycle through E leaves a frame of determinant 4, 6, or -1. Census, separately: 80640 assignments per projector, 576 consistent 4-cycles, zero rank-one solutions. Declared solutions, not a census: one sum for E=A with no target subset, and one sum for E=P with exactly the pair hits A+P and B+P. 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 two old calls meet support at length 6?", + "why_it_matters": "The length-5 equation is excluded. A word at length 6 would still be shorter than the eight-call minimum.", + "first_step": "Fix two old projectors E and F and the equation R+S+T+U=4I-E-F, then scan the subsets of one rational rank-one solution.", + "blocked_by": "The five-label size list and the 4-cycle degree sum do not apply to six labels." + }, + { + "question": "Can four added signed rank-one frames plus three old calls meet support at length 7?", + "why_it_matters": "Length 7 is the shortest remaining profile in the question left by the four-call support proof. A word there would lower the eight-call minimum.", + "first_step": "Fix three old projectors E, F, and G and the equation R+S+T+U=4I-E-F-G, then test one rational rank-one solution for target subsets.", + "blocked_by": "Seven labels are a different graph. A negative length-6 search would not settle this profile." + } + ], + "selection": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19507121", + "upstream_checked_utc": "2026-11-10T08:58:51Z", + "priority_revision": 8 + } +} diff --git a/research/four-signed-one-old/VERIFY.json b/research/four-signed-one-old/VERIFY.json new file mode 100644 index 0000000000..d49749a438 --- /dev/null +++ b/research/four-signed-one-old/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": 120, + "checks": "Target determinant and parity identities; tree closed forms and even-trace patterns; incident-edge determinants; the sixteen opposite-edge assignments for each old projector; two declared sum-solutions and a positive subset-scan control; exact census of all 80640 carrying assignments for each of the four projectors, with a near-miss round trip." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same identities, closed forms, survivor list, declared solutions, and carrying-assignment census under python -O." + } + ] +} diff --git a/research/four-signed-one-old/verify.py b/research/four-signed-one-old/verify.py new file mode 100644 index 0000000000..c2327851c9 --- /dev/null +++ b/research/four-signed-one-old/verify.py @@ -0,0 +1,471 @@ +#!/usr/bin/env python3 +"""Checks for four rank-one frames plus one old projector. + +PROOF.md is the argument. The checks below are exact arithmetic for that +case split, two declared sum-solutions, and an independent census of every +carrying-pair assignment. The census solves linear systems; it does not +search directions or scales. +""" + +from fractions import Fraction +from itertools import permutations, product +from math import gcd + + +FOUR = (4, 4, 0) +A = (1, 0, 0) +B = (0, 1, 0) +P = (0, 0, 1) +Q = (1, 1, -1) +PROJECTORS = {"A": A, "B": B, "P": P, "Q": Q} +TARGET_NAMES = ("AP", "AQ", "BP", "BQ") +TARGETS = { + "AP": (1, 0, 1), + "AQ": (2, 1, -1), + "BP": (0, 1, 1), + "BQ": (1, 2, -1), +} +EDGES = ( + (0, 1), (0, 2), (0, 3), (0, 4), + (1, 2), (1, 3), (1, 4), + (2, 3), (2, 4), + (3, 4), +) +EXPECTED_INCIDENT = { + "A": (("AP", 0, P), ("AQ", 0, Q)), + "B": (("BP", 0, P), ("BQ", 0, Q)), + "P": (("AP", 0, A), ("BP", 0, B)), + "Q": (("AQ", 0, A), ("BQ", 0, B)), +} + + +def require(condition, message): + if not condition: + raise SystemExit("FAIL: " + message) + + +def add(frames): + total = [0, 0, 0] + for frame in frames: + for index in range(3): + total[index] += frame[index] + return tuple(total) + + +def sub(left, right): + return tuple(left[index] - right[index] for index in range(3)) + + +def trace(frame): + return frame[0] + frame[1] + frame[2] + + +def determinant(frame): + a, b, c = (Fraction(value) for value in frame) + return a * b + c * (a + b) / 2 + + +def rank_one_nonzero(frame): + return frame != (0, 0, 0) and determinant(frame) == 0 + + +def parity(frame): + return ((frame[0] + frame[1]) % 2, frame[2] % 2) + + +def carrying(name, bit): + target = TARGETS[name] + if bit == 0: + return target + return sub(FOUR, target) + + +def matrix(frame): + a, b, c = frame + half = Fraction(c, 2) + return ((a + half, half), (half, b + half)) + + +def determinant_matrix(rows): + return rows[0][0] * rows[1][1] - rows[0][1] * rows[1][0] + + +def coefficient(direction, scale): + x, y = direction + factor = Fraction(scale) + return (factor * x * (x - y), factor * y * (y - x), factor * 2 * x * y) + + +def target_hits(labels): + wanted = set(TARGETS.values()) + found = [] + width = len(labels) + for mask in range(1, 1 << width): + chosen = [labels[index] for index in range(width) if mask & (1 << index)] + total = add(chosen) + if total in wanted: + found.append((mask, total, len(chosen))) + return found + + +def target_identities(): + require(add(TARGETS.values()) == FOUR, "the four targets do not sum to 4I") + for name in TARGET_NAMES: + target = TARGETS[name] + require(trace(target) == 2, name + " does not have trace 2") + require(determinant(target) == Fraction(1, 2), name + " does not have determinant 1/2") + require(parity(target) == (1, 1), name + " does not have parity (1,1)") + complement = sub(FOUR, target) + require(trace(complement) == 6, name + " complement does not have trace 6") + require(determinant(complement) == Fraction(17, 2), name + " complement determinant changed") + require(parity(complement) == (1, 1), name + " complement is not parity (1,1)") + require(not rank_one_nonzero(complement), name + " complement was accepted as rank one") + + +def automorphism_checks(): + basis = ((1, 0, 0), (0, 1, 0), (0, 0, 1)) + samples = list(basis) + list(PROJECTORS.values()) + list(TARGETS.values()) + samples.append((2, 2, 0)) + for frame in samples: + swapped = (frame[1], frame[0], frame[2]) + reflected = (frame[0] + frame[2], frame[1] + frame[2], -frame[2]) + require(determinant(swapped) == determinant(frame), "coordinate swap changed a determinant") + require(determinant(reflected) == determinant(frame), "sign flip changed a determinant") + require(matrix(swapped) == ( + (matrix(frame)[1][1], matrix(frame)[1][0]), + (matrix(frame)[0][1], matrix(frame)[0][0]), + ), "coordinate swap is not conjugation by the exchange matrix") + raw = matrix(frame) + reflected_matrix = ((raw[0][0], -raw[0][1]), (-raw[1][0], raw[1][1])) + require(matrix(reflected) == reflected_matrix, "sign flip is not conjugation by diag(1,-1)") + require(determinant_matrix(reflected_matrix) == determinant_matrix(raw), + "sign flip failed to preserve the matrix determinant") + require((B[1], B[0], B[2]) == A, "swap does not exchange A and B") + require((P[0] + P[2], P[1] + P[2], -P[2]) == Q, "sign flip does not exchange P and Q") + require((Q[0] + Q[2], Q[1] + Q[2], -Q[2]) == P, "sign flip does not exchange Q and P") + for name, image in (("AP", "BP"), ("AQ", "BQ"), ("BP", "AP"), ("BQ", "AQ")): + frame = TARGETS[name] + require((frame[1], frame[0], frame[2]) == TARGETS[image], "swap moved " + name + " incorrectly") + + +def star_obstruction(): + # 3 tr(C) = 4k. The center trace is 1, or one more or less than an edge trace. + require(3 * 1 % 4 != 0, "three times the projector trace became divisible by 4") + for edge_trace in (2, 6): + center_trace = edge_trace - 1 + require(3 * center_trace % 4 != 0, "a leaf placement made the star trace equation possible") + + +def path_and_fork_identities(): + def matrices(): + yield ((0, 0, 0), (0, 0, 0), (0, 0, 0), (0, 0, 0)) + for slot in range(4): + for axis in range(3): + rows = [(0, 0, 0)] * 4 + value = [0, 0, 0] + value[axis] = 1 + rows[slot] = tuple(value) + yield tuple(rows) + + for row in matrices(): + m0, m1, m2, m3 = row + f0 = sub(sub(FOUR, m1), m3) + f1 = sub(m0, f0) + f2 = sub(m1, f1) + f3 = sub(m2, f2) + f4 = sub(m3, f3) + require(add((f0, f1, f2, f3, f4)) == FOUR, "path propagation missed 4I") + require(add((f0, f1)) == m0 and add((f1, f2)) == m1, "path edge equation failed") + require(add((f2, f3)) == m2 and add((f3, f4)) == m3, "path edge equation failed") + center = sub(add((m0, m1, m2)), FOUR) + branch = sub(m3, center) + leaves = (sub(m0, center), sub(m1, center), sub(m2, branch)) + require(add((center, branch, leaves[0], leaves[1], leaves[2])) == FOUR, "fork sum failed") + for bits in range(16): + edge_traces = [2 if (bits >> index) & 1 else 6 for index in range(4)] + path_traces = ( + 8 - edge_traces[1] - edge_traces[3], + edge_traces[0] + edge_traces[1] + edge_traces[3] - 8, + 8 - edge_traces[0] - edge_traces[3], + edge_traces[0] + edge_traces[2] + edge_traces[3] - 8, + 8 - edge_traces[0] - edge_traces[2], + ) + fork_center = edge_traces[0] + edge_traces[1] + edge_traces[2] - 8 + fork_branch = edge_traces[3] - fork_center + fork_traces = ( + fork_center, + fork_branch, + edge_traces[0] - fork_center, + edge_traces[1] - fork_center, + edge_traces[2] - fork_branch, + ) + for value in path_traces + fork_traces: + require(value % 2 == 0, "a tree vertex trace became odd") + require(value != 1, "a tree vertex had the projector trace") + + +def isolated_projector_trace(): + for old in PROJECTORS.values(): + require(trace(sub(FOUR, old)) == 7, "4I-E does not have trace 7") + for left in (2, 6): + for right in (2, 6): + require(left + right != 7, "two edge traces summed to the odd residual") + + +def incident_edges(name): + old = PROJECTORS[name] + found = [] + for target_name in TARGET_NAMES: + for bit in (0, 1): + value = carrying(target_name, bit) + frame = sub(value, old) + if rank_one_nonzero(frame): + found.append((target_name, bit, frame)) + found.sort() + expected = tuple(sorted(EXPECTED_INCIDENT[name])) + require(tuple(found) == expected, name + " incident edges changed: " + str(found)) + return found + + +def c4_survivors(name): + found = incident_edges(name) + old = PROJECTORS[name] + names = [item[0] for item in found] + rest = [target_name for target_name in TARGET_NAMES if target_name not in names] + require(len(rest) == 2, name + " did not leave two opposite targets") + survivors = [] + for orient in (0, 1): + edge_x, edge_y = (names[0], names[1]) if orient == 0 else (names[1], names[0]) + for bit_x in (0, 1): + for bit_y in (0, 1): + for swap in (0, 1): + opposite_x, opposite_y = (rest[0], rest[1]) if swap == 0 else (rest[1], rest[0]) + mx = carrying(edge_x, 0) + my = carrying(edge_y, 0) + rx = carrying(opposite_x, bit_x) + ry = carrying(opposite_y, bit_y) + if add((mx, ry)) != add((my, rx)): + continue + frames = ( + sub(mx, old), + sub(my, old), + add((sub(rx, mx), old)), + sub(sub(FOUR, my), rx), + ) + require(not all(rank_one_nonzero(frame) for frame in frames), + name + " C4 survivor was rank one") + survivors.append(tuple(sorted(frames))) + require(len(survivors) == 4, name + " had " + str(len(survivors)) + " C4 survivors") + kinds = set(survivors) + require(len(kinds) == 2, name + " survivor patterns changed") + flat = [determinant(frame) for frames in kinds for frame in frames] + require(Fraction(4) in flat and Fraction(6) in flat and Fraction(-1) in flat, + name + " survivor determinants changed: " + str(flat)) + two_i = (2, 2, 0) + require(any(two_i in frames for frames in kinds), name + " lost the 2I near-miss") + return survivors + + +def declared_solutions(): + axial = [ + coefficient(direction, scale) + for direction, scale in (((1, 0), 4), ((0, 1), 2), ((1, 1), -2), ((1, 2), 1)) + ] + diagonal = [ + coefficient(direction, scale) + for direction, scale in ( + ((1, 0), 1), + ((0, 1), 1), + ((1, 1), 1), + ((1, -1), Fraction(3, 2)), + ) + ] + require(add(axial) == sub(FOUR, A), "axial solution does not sum to 4I-A") + require(add(diagonal) == sub(FOUR, P), "diagonal solution does not sum to 4I-P") + for frame in axial + diagonal: + require(rank_one_nonzero(frame), "declared frame is not rank one") + axial_hits = target_hits(axial + [A]) + diagonal_hits = target_hits(diagonal + [P]) + require(axial_hits == [], "axial solution gained a target subset: " + str(axial_hits)) + pair_hits = [hit for hit in diagonal_hits if hit[2] == 2] + require(len(pair_hits) == 2, "diagonal solution did not keep exactly two pair hits") + require(len({hit[1] for hit in diagonal_hits}) == 2, "diagonal solution meets more than two targets") + covered = {hit[1] for hit in diagonal_hits} + require(covered == {TARGETS["AP"], TARGETS["BP"]}, "diagonal pair hits are not A+P and B+P") + positive = target_hits([A, B, P, Q, (2, 2, 0)]) + require(len({hit[1] for hit in positive}) == 4, "positive control missed a target") + require(not rank_one_nonzero((2, 2, 0)), "2I was accepted as rank one") + broken = (add((axial[0], (1, 0, 0))),) + tuple(axial[1:]) + require(add(broken) != sub(FOUR, A), "tampered solution still sums to 4I-A") + 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, "zero was accepted as rank one") + + +def pair_rows(left, right, rhs, old): + rows = [] + for axis in range(3): + row = [0] * 13 + for vertex, sign in ((left, 1), (right, 1)): + if vertex < 4: + row[3 * vertex + axis] += sign + else: + row[12] -= old[axis] + row[12] += rhs[axis] + rows.append(row) + return rows + + +def total_rows(old): + residual = sub(FOUR, old) + rows = [] + for axis in range(3): + row = [0] * 13 + for vertex in range(4): + row[3 * vertex + axis] = 1 + row[12] = residual[axis] + rows.append(row) + return rows + + +def solve(rows): + working = [row[:] for row in rows] + width = 12 + height = len(working) + cursor = 0 + pivots = [] + for column in range(width): + selected = None + best = None + for index in range(cursor, height): + value = working[index][column] + if value and (best is None or abs(value) < best): + best = abs(value) + selected = index + if selected is None: + continue + working[cursor], working[selected] = working[selected], working[cursor] + divisor = 0 + for index in range(column, width + 1): + divisor = gcd(divisor, working[cursor][index]) + if working[cursor][column] < 0: + divisor = -divisor + if divisor not in (0, 1): + for index in range(column, width + 1): + working[cursor][index] //= divisor + pivot = working[cursor][column] + for index in range(height): + if index == cursor or working[index][column] == 0: + continue + factor = working[index][column] + reduced = gcd(pivot, factor) + pivot_scale = pivot // reduced + factor_scale = factor // reduced + for entry in range(column, width + 1): + working[index][entry] = ( + pivot_scale * working[index][entry] - factor_scale * working[cursor][entry] + ) + pivots.append(column) + cursor += 1 + if cursor == height: + break + for index in range(cursor, height): + if working[index][width]: + return None + free = [column for column in range(width) if column not in pivots] + if free: + return ("free", len(free)) + solution = [0] * width + for index, column in enumerate(pivots): + for other in range(width): + if other != column and working[index][other]: + return ("dirty", column) + pivot = working[index][column] + rhs = working[index][width] + if rhs % pivot: + return ("nonint", column) + solution[column] = rhs // pivot + return solution + + +def frames_of(solution): + return tuple(tuple(solution[3 * index:3 * index + 3]) for index in range(4)) + + +def integer_determinant(frame): + a, b, c = frame + return 2 * a * b + c * (a + b) + + +def census(): + options = [(TARGETS[name], sub(FOUR, TARGETS[name])) for name in TARGET_NAMES] + for name, old in PROJECTORS.items(): + base_rows = total_rows(old) + inconsistent = solved = free = nonint = dirty = hits = 0 + checked = 0 + for chosen in permutations(range(10), 4): + edges = [EDGES[index] for index in chosen] + for bits in product((0, 1), repeat=4): + checked += 1 + rows = [row[:] for row in base_rows] + for edge, bit, choices in zip(edges, bits, options): + rows.extend(pair_rows(edge[0], edge[1], choices[bit], old)) + answer = solve(rows) + if answer is None: + inconsistent += 1 + continue + if isinstance(answer, tuple) and answer[0] == "free": + free += 1 + continue + if isinstance(answer, tuple) and answer[0] == "nonint": + nonint += 1 + continue + if isinstance(answer, tuple): + dirty += 1 + continue + solved += 1 + degrees = [0, 0, 0, 0, 0] + for edge in edges: + degrees[edge[0]] += 1 + degrees[edge[1]] += 1 + require(degrees[4] == 2, name + " consistent graph did not put E on the cycle") + require(sorted(degrees) == [0, 2, 2, 2, 2], name + " consistent degree sequence changed") + frames = frames_of(answer) + if all(frame != (0, 0, 0) and integer_determinant(frame) == 0 for frame in frames): + hits += 1 + require(checked == 80640, name + " census missed an assignment") + require(inconsistent == 80064 and solved == 576, name + " census counts changed") + require(free == nonint == dirty == hits == 0, name + " census accepted a non-rigid or rank-one solution") + near = solve( + total_rows(A) + + pair_rows(0, 4, TARGETS["AP"], A) + + pair_rows(2, 4, TARGETS["AQ"], A) + + pair_rows(0, 1, TARGETS["BP"], A) + + pair_rows(1, 2, TARGETS["BQ"], A) + ) + require(frames_of(near) == (P, B, Q, (2, 2, 0)), "near-miss round trip changed") + tampered = solve( + total_rows(A) + + pair_rows(0, 4, add((TARGETS["AP"], (1, 0, 0))), A) + + pair_rows(2, 4, TARGETS["AQ"], A) + + pair_rows(0, 1, TARGETS["BP"], A) + + pair_rows(1, 2, TARGETS["BQ"], A) + ) + require(tampered is None, "tampered near-miss stayed consistent") + + +def main(): + target_identities() + automorphism_checks() + star_obstruction() + path_and_fork_identities() + isolated_projector_trace() + for name in PROJECTORS: + c4_survivors(name) + declared_solutions() + census() + print("PASS four-signed-one-old checks") + + +if __name__ == "__main__": + main()