From e6aac77f79560add2c47c761d9defff96934d88d Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 10 Nov 2026 10:36:55 +0000 Subject: [PATCH] Classify length-6 support for five frames plus one old projector. Five rational rank-one frames plus one fixed projector meet target support exactly when three frames are the complementary projectors and the other two split 2I. Every integral splitting fails the inherited character count, so none of those solutions is a word and the selected frontier is unchanged. Co-authored-by: unpaidmoon --- research/five-signed-one-old/PROOF.md | 210 +++++++ research/five-signed-one-old/README.md | 44 ++ research/five-signed-one-old/SOURCES.json | 18 + research/five-signed-one-old/TASK.json | 69 +++ research/five-signed-one-old/VERIFY.json | 34 ++ research/five-signed-one-old/verify.py | 709 ++++++++++++++++++++++ 6 files changed, 1084 insertions(+) create mode 100644 research/five-signed-one-old/PROOF.md create mode 100644 research/five-signed-one-old/README.md create mode 100644 research/five-signed-one-old/SOURCES.json create mode 100644 research/five-signed-one-old/TASK.json create mode 100644 research/five-signed-one-old/VERIFY.json create mode 100644 research/five-signed-one-old/verify.py diff --git a/research/five-signed-one-old/PROOF.md b/research/five-signed-one-old/PROOF.md new file mode 100644 index 0000000000..87f10cd845 --- /dev/null +++ b/research/five-signed-one-old/PROOF.md @@ -0,0 +1,210 @@ +# Five frames plus one old projector meet support only by splitting 2I + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. + +## Claim + +In the PR2085/2112 formal register model, fix one old projector `E` in `{A,B,P,Q}` and five nonzero symmetric rational rank-one matrices. For the once-each equation + +``` +R + S + T + U + V = 4I - E +``` + +target support holds if and only if, up to order, three of the five matrices are the three old projectors other than `E` and the other two are a rational rank-one splitting of `2I`. + +Every integral solution of that form fails the inherited `P`-coefficient character: exactly two of the six labels have odd `P`-coefficient, and all four targets do. Those solutions are not words. A non-integral splitting is a support solution and is not, by itself, a word. + +Selected κ stays `781451/250000000`. Nothing here is a multiplication theorem, a κ change, or a lowering of the eight-call minimum. Six added frames with no old call, four added frames plus an old call, and two or more old calls stay outside this equation. + +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 `research/bit-two-signed-frame-floor/PROOF.md`, Section 1. The character inequality in that same section is inherited and is not reproved. 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`. The matrix is nonzero and rank one exactly when the vector is nonzero and `2ab + c(a+b) = 0`. The old projectors are + +``` +A = (1,0,0), B = (0,1,0), P = (0,0,1), Q = (1,1,-1). +``` + +Each has trace 1. Opposite pairs sum to `I = (1,1,0)`: + +``` +A + B = P + Q = I, A + B + P + Q = 2I = (2,2,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 `E` as above, `4I-E` has trace 7. Write `E⊥` for the opposite of `E` and `{G,G⊥}` for the other opposite pair. The three projectors other than `E` are exactly `{E⊥,G,G⊥}`, and they sum to `2I-E`. + +## 2. Which subset sizes can be targets + +The six paid labels are the five frames and `E`. They sum to `4I`. + +**Lemma 1.** A subset sum equal to a target has size 2, 3, or 4. + +The empty sum is 0. A singleton has determinant 0, while each target has determinant `1/2`. The full sum has trace 8, while each target has trace 2. A five-element subset sums to a target `H` only if the omitted label equals `4I-H`. The same expansion used for five frames with no old call gives + +``` +det(4I-H) = 16 - 4·tr(H) + det(H) = 17/2 ≠ 0, +``` + +so `4I-H` is not rank one. The only remaining sizes are 2, 3, and 4. + +There are `C(6,2)+C(6,3)+C(6,4) = 50` such subsets. The four targets are distinct, so the four subsets are distinct. The support domain is the `C(50,4) = 230300` unordered 4-tuples, each with `4! = 24` assignments of the targets and with each of the four choices of `E`. That list is the whole domain left by Lemma 1. It is not a sample of directions or scales. + +## 3. The construction + +**Theorem 2.** Let `X` and `2I-X` both be nonzero and rank one. For each projector `E`, the five matrices `{E⊥, G, G⊥, X, 2I-X}` sum to `4I-E`, and the four subsets + +``` +{E⊥,G}, {E⊥,G⊥}, {E,G}, {E,G⊥} +``` + +are the four targets in some order. + +The three complementary projectors sum to `2I-E`, so the five matrices sum to `4I-E`. The four displayed pairs are subset sums of the six labels, and direct addition shows they are the four targets: + +| `E` | Frozen frames | The four pair sums | +|---|---|---| +| `A` | `B,P,Q` | `B+P, B+Q, A+P, A+Q` | +| `B` | `A,P,Q` | `A+P, A+Q, B+P, B+Q` | +| `P` | `A,B,Q` | `A+Q, B+Q, A+P, B+P` | +| `Q` | `A,B,P` | `A+P, B+P, A+Q, B+Q` | + +The pairs `A+B` and `P+Q` equal `I`, which is not a target, and they are not used. The two summands of `2I` do not appear in these subsets, so every splitting works. In particular `2I-E` itself is not rank one for any projector `E`, so neither free frame is `E`. + +One integral solution for `E=B` is + +``` +A, P, Q, 2A, 2B. +``` + +One pairwise nonparallel solution, still for `E=B`, uses the splitting in Section 4 at `t=2`: + +``` +A, P, Q, (-2/5, 4/5, 8/5), (12/5, 6/5, -8/5). +``` + +The directions are `(1,0)`, `(1,1)`, `(1,-1)`, `(1,2)`, and `(2,-1)`, at scales `1`, `1/2`, `1/2`, `2/5`, and `2/5`. No two are parallel. Both solutions meet support. Neither is claimed to be a word. + +## 4. Every splitting of 2I + +**Lemma 3.** For a symmetric matrix `X=(a,b,c)`, + +``` +Q(2I-X) - Q(X) = 4(2 - a - b - c), +``` + +where `Q=2ab+c(a+b)`. Thus `X` and `2I-X` are both rank one if and only if `X` is nonzero and rank one and has trace 2. The partner is then automatically nonzero, because `2I` is not rank one. + +The identity is the polynomial expansion checked by `verify.py`. If both quadrics vanish, the trace equals 2. Conversely, trace 2 and `Q(X)=0` force `Q(2I-X)=0`. + +On the trace-2 slice, `b=2-c-a` and `Q(X)=0` become a quadratic in `a` whose discriminant is `4-c^2`. For an integer vector, `c` is an integer. If `|c|≥3`, then `c^2≥9>4`, so the discriminant is negative. Inside `-2≤c≤2` the discriminant is a square only for `c=0,±2`, and the only nonzero rank-one solutions are + +``` +2A=(2,0,0), 2B=(0,2,0), 2P=(0,0,2), 2Q=(2,2,-2). +``` + +They form the two pairs `{2A,2B}` and `{2P,2Q}`. Every coordinate `c` in these four vectors is even. + +For every rational `t`, + +``` +X(t) = ( 2(1-t)/(1+t^2), 2t(t-1)/(1+t^2), 4t/(1+t^2) ) +``` + +has trace 2 and lies on the cone, and `X(0)=2A`, `X(1)=2P`. The partner of `2B` is `2A`, which is the missing point of this chart. The verifier checks the formula at `t=0,1,2,3,1/2,5`. These are infinitely many distinct splittings; the trace-2 cone is the full set. + +## 5. Integral solutions are not words + +**Theorem 4.** Every integral support solution of the equation fails the inherited `P`-coefficient test, so it is not a word. + +By Theorem 5 below, an integral support solution has the multiset in Theorem 2 with an integral splitting. Section 4 lists those splittings, and both frames have even `c`. The six labels are the four projectors together with that pair. Among `A,B,P,Q`, only `P` and `Q` have odd `c`. Exactly two calls are detected. All four targets have odd `c`. The inherited inequality forbids a word. The addresses lie in the old lattice `ZA+ZB+ZP`, so the character is the ordinary `P`-coefficient modulo 2. The inequality itself is not reproved. + +The same count does not apply to a non-integral splitting. Section 4's `t=2` witness has denominator 5. It meets support and is not claimed to survive, or to fail, every character. + +## 6. No other support solution exists + +**Theorem 5.** Every rational rank-one solution with target support is one of the solutions in Theorem 2. + +The proof is the case division of the domain in Section 2. `verify.py` decides every tuple. The hand arguments are the twin obstruction and the trace obstruction. The other branches are finite and are exhausted by the program. + +### Duplicate frame rows + +Two distinct subsets can impose the same row on the five unknown frames only when one is `S` and the other is `S∪{E}`. Their equations say `E=H2-H1` for two distinct targets. The twelve differences are + +``` +A+Q-(A+P) = (1,1,-2), A+P-(A+Q) = (-1,-1,2), +B+P-(A+P) = (-1,1,0), A+P-(B+P) = (1,-1,0), +B+Q-(A+P) = (0,2,-2), A+P-(B+Q) = (0,-2,2), +B+Q-(A+Q) = (-1,1,0), A+Q-(B+Q) = (1,-1,0), +B+P-(A+Q) = (-2,0,2), A+Q-(B+P) = (2,0,-2), +B+Q-(B+P) = (1,1,-2), B+P-(B+Q) = (-1,-1,2). +``` + +None equals `A=(1,0,0)`, `B=(0,1,0)`, `P=(0,0,1)`, or `Q=(1,1,-1)`. There are 22370 such 4-tuples. Each is inconsistent for every projector and every target assignment. + +### Rank 3 + +A matrix with all 4-by-4 minors zero has rank at most 3. Every one of the 2450 such matrices has rank exactly 3. Its left kernel is two-dimensional, and both kernel vectors annihilate the rows. For every projector and every target assignment, one of those vectors misses the right-hand side. No rank-3 system is consistent. No rank below 3 occurs. + +### Rank 4 with no frozen frame + +The remaining singular matrices have rank 4, so the adjugate has rank 1 and supplies the left and right kernels. On 3840 matrices the right kernel has no zero coordinate. Every primitive left kernel has the shape with two `+1` entries among the four subset rows, zeroes elsewhere there, and `-1` on the total row. The six shapes and their counts are + +| Left kernel | Count | +|---|---:| +| `(1,0,0,1,-1)` | 800 | +| `(0,1,0,1,-1)` | 640 | +| `(0,1,1,0,-1)` | 640 | +| `(1,0,1,0,-1)` | 640 | +| `(0,0,1,1,-1)` | 560 | +| `(1,1,0,0,-1)` | 560 | + +Thus two subset rows sum to the total row. The corresponding right-hand sides would satisfy + +``` +(H_p - ε_p E) + (H_q - ε_q E) = 4I - E, +``` + +where each `ε` is 0 or 1. The left trace is `4-(ε_p+ε_q)`, hence 2, 3, or 4. The right trace is 7. The system is inconsistent for every projector and every target assignment. + +### One frozen frame + +On 27840 matrices the right kernel has exactly one zero. That frame is constant on the solution line. Of the systems that are consistent, 16320 freeze a frame that is zero or off the cone, so the whole line fails. The other 960 freeze a rank-one frame. For those, if one moving frame `X` lies on the cone, each of the other three moving frames lies on the cone only if a fixed linear form in `X` vanishes. The verifier solves those three linear forms. None of the 960 systems has a rank-one solution. + +### Three frozen frames + +On 53400 matrices the right kernel has exactly three zeroes. The two nonzero kernel coefficients sum to zero, so the sum of the two moving frames is constant on each solution space. Of the consistent systems, 28560 freeze a frame off the cone. The other 240, sixty for each projector `E`, freeze exactly the three complementary projectors, and the moving sum is `2I`. Substituting `2A` and `2B` satisfies every equation of each of these 240 systems. Because the moving sum is invariant, every rank-one point of each system is a splitting of `2I`. The 240 systems are in bijection with the ways to place those three projectors into five positions, `4·P(5,3)=240`. + +### Invertible systems + +The other 120400 matrices are invertible. Cramer's rule, with the cofactor matrix checked against `M·adj(M)=det(M)I` on every one of them, produces a unique rational solution for each of the `120400·24·4 = 11558400` right-hand sides. Every solution has a zero frame or a frame off the cone. + +One of those matrices is the incidence matrix of subsets `{0,1}`, `{0,2}`, `{1,2}`, `{0,3}`, with no `E` bit. Its determinant is `-2`, by the same integer row reduction already recorded for this matrix in the five-call note, and again by the cofactor routine here. For `E=A` and the targets in the order `A+P,A+Q,B+P,B+Q`, the unique frames are + +``` +(3/2, 0, -1/2), (-1/2, 0, 3/2), (1/2, 1, -1/2), +(-1/2, 2, -1/2), (2, 1, 0). +``` + +Their quadrics are `-3/4`, `-3/4`, `1/4`, `-11/4`, and `4`. This is one invertible case, not a substitute for the census. The same solver recovers the `t=2` witness from the subset sums of these four masks, and it stops recovering that witness if the total row is shifted by `A`. + +## 7. What was not proved + +The census is exhaustive for this one equation. It is not a search over a bounded box of directions. A support solution is not a legal word: the factors still have to multiply to the target in the group algebra. Theorem 4 excludes only the integral solutions. Discussion #2091 and the fixed fifth address `R=(1,1/2)` are a different alphabet; this note does not revisit that word search and does not contradict its eight-call conclusion, because no word is exhibited here. + +## Open next questions + +Can one rational splitting of `2I` make the length-6 support solution into a word? A word would lower the eight-call minimum. The integral pairs `{2A,2B}` and `{2P,2Q}` already fail the `P`-coefficient test. The first unchecked point on the same chart is `t=2`, whose frames are displayed in Section 3. Passing that character would still not be a word: support and the first-order count are necessary, not sufficient. diff --git a/research/five-signed-one-old/README.md b/research/five-signed-one-old/README.md new file mode 100644 index 0000000000..9ad189df9b --- /dev/null +++ b/research/five-signed-one-old/README.md @@ -0,0 +1,44 @@ +# Five rank-one frames plus one old call, at length 6 + +**Support classification, plus an integral character obstruction. No new κ and no word.** + +Fix one old projector `E` in `{A,B,P,Q}`. Five nonzero symmetric rational rank-one matrices sum to `4I-E` and meet all four targets as subset sums if and only if three of them are the other three old projectors and the other two split `2I`. The argument is [PROOF.md](PROOF.md). + +The integral splittings are exactly `{2A,2B}` and `{2P,2Q}`. Each integral solution then detects two calls and four targets under the `P`-coefficient modulo 2, so it is not a word. One pairwise nonparallel splitting, at chart parameter `t=2`, is a support witness only. The selected record stays κ = `781451/250000000`. This classification does not lower the eight-call minimum. + +## 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 answers the length-6 question left open by the five-call census, discussion comment 19514165 on PR #7024. The equation is `R+S+T+U+V=4I-E`. It does not redo the five-call residual `4I`, the four-call theorem, a four-frame equation with an old call, or six added frames with no old call. + +Evidence classes, kept apart: + +1. **Proof of the construction and of the splitting identity.** For each projector `E`, the three complementary projectors plus any rank-one splitting of `2I` meet support. The identity `Q(2I-X)-Q(X)=4(2-tr X)` classifies those splittings. The integral points are the two pairs above, read off the discriminant `4-c^2`. +2. **Exhaustive finite census, and therefore the converse.** Lemma 1 leaves subset sizes 2, 3, and 4: 230300 unordered 4-tuples. Of them, 22370 duplicate an `E`-bit row and contradict the twelve target differences; 2450 have rank 3 and an inconsistent left kernel; 3840 have a full-support kernel and fail the trace test `2,3,4 ≠ 7`; 27840 freeze one frame and do not meet the cone; 53400 freeze three frames, of which only 240 are consistent and on the cone, and those 240 are the construction. The other 120400 tuples are invertible and off the cone. One invertible determinant is the known value `-2`. +3. **Explicit witnesses, not a word.** `A,P,Q,2A,2B` with old call `B`, and the `t=2` frames `(-2/5,4/5,8/5)` and `(12/5,6/5,-8/5)` on directions `(1,2)` and `(2,-1)`. The integral witness fails the inherited character count. The non-integral witness is support only. + +The determinant identity, the subset-sum necessity, and the character inequality 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/five-signed-one-old --check-only +python3.12 scripts/research_package.py --package research/five-signed-one-old +``` + +The direct check is `python3 -I -W error -B research/five-signed-one-old/verify.py`. It takes about 90 seconds. + +## Open next questions + +Can one rational splitting of `2I` make this length-6 support solution into a word? A word would lower the eight-call minimum. The integral pairs already fail the `P`-coefficient test. A useful first step is the same count on the displayed `t=2` frames. Passing it would still not be a word: support is necessary, not sufficient. + +Six added frames with no old call, and four added frames plus an old call, are different equations and are not answered here. + +## Credit + +The register model is Cinna Davis's PR2085/2112 formal model. The determinant, the subset-sum necessity, and the character inequality are the PR2910 package as recorded in apoursh's two-signed-frame floor, PR6190. The three-frame all-old-once character is `research/three-signed-old-once`. The four-call support proof is `research/four-signed-once-parity`, merged as PR #6952. The five-call census and this open question are PR #7024, discussion comment 19514165. None of those theorems is redone. Discussion #2091 studies one fixed fifth address and is not this residual equation. + +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/five-signed-one-old/SOURCES.json b/research/five-signed-one-old/SOURCES.json new file mode 100644 index 0000000000..41a0d8e4ed --- /dev/null +++ b/research/five-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/five-signed-one-old/TASK.json b/research/five-signed-one-old/TASK.json new file mode 100644 index 0000000000..710ae9a7bf --- /dev/null +++ b/research/five-signed-one-old/TASK.json @@ -0,0 +1,69 @@ +{ + "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 the equation R+S+T+U+V=4I-E, classify the rational rank-one solutions that meet target support, and show that every integral solution fails the inherited P-coefficient character.", + "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 length-6 question left open by the five-call census: five added frames plus one old projector.", + "bottleneck_link": "Side result on the signed-frame escape. Length-6 support exists, but every integral solution fails the inherited character test, so there is no local call-count saving and no selected-frontier change.", + "budget_minutes": 60, + "stop_rule": "Stop after the length-6 support classification for exactly one old projector and the integral character obstruction. Do not census six frames with no old call, and do not add a second old call.", + "outcome": "completed", + "evidence": "Exhaustive finite census of the 230300 subset 4-tuples: support holds exactly when three frames are the complementary old projectors and the other two split 2I. Integral splits are {2A,2B} and {2P,2Q}; each detects two calls and four targets. One non-integral pairwise nonparallel witness at t=2 is support only. The inherited determinant, subset-sum necessity, and character inequality are not reproved.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance with the census, the splitting identity, and the verifier. No independent human or formal-kernel review.", + "open_questions": [ + { + "question": "Can one rational splitting of 2I make the length-6 support solution into a word?", + "why_it_matters": "A legal word would lower the eight-call minimum. The integral splittings already fail the P-coefficient test, so only a non-integral splitting could remain.", + "first_step": "Apply the inherited P-coefficient character to the displayed t=2 frames (-2/5,4/5,8/5) and (12/5,6/5,-8/5), with old call B and frozen frames A, P, and Q.", + "blocked_by": "Support and the first-order character count are necessary, not sufficient. A passing character on t=2 would still not be a word." + } + ], + "selection": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19514165", + "upstream_checked_utc": "2026-11-10T10:07:00Z", + "priority_revision": 8 + } +} diff --git a/research/five-signed-one-old/VERIFY.json b/research/five-signed-one-old/VERIFY.json new file mode 100644 index 0000000000..0af2a357d1 --- /dev/null +++ b/research/five-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": 300, + "checks": "Splitting identity and integral 2I points; direct support for every projector and both integral splittings; nonparallel t=2 witness; exhaustive classification of all 230300 subset 4-tuples, with the 240 surviving systems in bijection with projector placements; positive control that the invertible solver recovers the t=2 witness; failure controls for I, zero, A+P, and a tampered total." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Same identities, census, witness, positive control, and failure controls under python -O." + } + ] +} diff --git a/research/five-signed-one-old/verify.py b/research/five-signed-one-old/verify.py new file mode 100644 index 0000000000..d973c7d3dd --- /dev/null +++ b/research/five-signed-one-old/verify.py @@ -0,0 +1,709 @@ +#!/usr/bin/env python3 +"""Length-6 support for five rank-one frames plus one old projector. + +PROOF.md holds the argument. This program checks the construction, the +splitting identity, the integral character obstruction, and the exhaustive +incidence census that makes the construction necessary. +""" + +from fractions import Fraction +from itertools import combinations, permutations +from math import gcd + + +TARGETS = ((1, 0, 1), (2, 1, -1), (0, 1, 1), (1, 2, -1)) +TARGET_NAME = { + (1, 0, 1): "A+P", + (2, 1, -1): "A+Q", + (0, 1, 1): "B+P", + (1, 2, -1): "B+Q", +} +PROJECTORS = ( + ("A", (1, 0, 0)), + ("B", (0, 1, 0)), + ("P", (0, 0, 1)), + ("Q", (1, 1, -1)), +) +BY_NAME = dict(PROJECTORS) +OPPOSITE = {"A": "B", "B": "A", "P": "Q", "Q": "P"} +OTHER_PAIR = {"A": ("P", "Q"), "B": ("P", "Q"), "P": ("A", "B"), "Q": ("A", "B")} +TOTAL = (4, 4, 0) +TWO_I = (2, 2, 0) +MASKS = tuple(m for m in range(64) if bin(m).count("1") in (2, 3, 4)) +PERMS = tuple(permutations(range(4))) +HAND_MASKS = (3, 5, 6, 9) +HAND_E = (1, 0, 0) +HAND_FRAMES = ( + (Fraction(3, 2), Fraction(0), Fraction(-1, 2)), + (Fraction(-1, 2), Fraction(0), Fraction(3, 2)), + (Fraction(1, 2), Fraction(1), Fraction(-1, 2)), + (Fraction(-1, 2), Fraction(2), Fraction(-1, 2)), + (Fraction(2), Fraction(1), Fraction(0)), +) +FULL_SHAPES = { + (1, 0, 0, 1, -1): 800, + (0, 1, 0, 1, -1): 640, + (0, 1, 1, 0, -1): 640, + (1, 0, 1, 0, -1): 640, + (0, 0, 1, 1, -1): 560, + (1, 1, 0, 0, -1): 560, +} + + +def require(condition, message): + if not condition: + raise SystemExit("FAIL: " + message) + + +def quad(frame): + a, b, c = frame + return 2 * a * b + c * (a + b) + + +def add(frames): + return tuple(sum(frame[i] for frame in frames) for i in range(3)) + + +def sub(left, right): + return tuple(left[i] - right[i] for i in range(3)) + + +def rank_one_nonzero(frame): + return frame != (0, 0, 0) and quad(frame) == 0 + + +def det4(a, b, c, d): + return ( + a[0] * (b[1] * (c[2] * d[3] - c[3] * d[2]) - b[2] * (c[1] * d[3] - c[3] * d[1]) + b[3] * (c[1] * d[2] - c[2] * d[1])) + - a[1] * (b[0] * (c[2] * d[3] - c[3] * d[2]) - b[2] * (c[0] * d[3] - c[3] * d[0]) + b[3] * (c[0] * d[2] - c[2] * d[0])) + + a[2] * (b[0] * (c[1] * d[3] - c[3] * d[1]) - b[1] * (c[0] * d[3] - c[3] * d[0]) + b[3] * (c[0] * d[1] - c[1] * d[0])) + - a[3] * (b[0] * (c[1] * d[2] - c[2] * d[1]) - b[1] * (c[0] * d[2] - c[2] * d[0]) + b[2] * (c[0] * d[1] - c[1] * d[0])) + ) + + +def minors(rows): + cofactors = [[0] * 5 for _ in range(5)] + for i in range(5): + for j in range(5): + minor = [] + for ii in range(5): + if ii == i: + continue + minor.append(tuple(rows[ii][jj] for jj in range(5) if jj != j)) + sign = 1 if ((i + j) & 1) == 0 else -1 + cofactors[i][j] = sign * det4(*minor) + determinant = sum(rows[0][j] * cofactors[0][j] for j in range(5)) + return determinant, cofactors + + +def adj_identity(rows, cofactors, determinant): + for p in range(5): + for q in range(5): + got = sum(rows[p][k] * cofactors[q][k] for k in range(5)) + require(got == (determinant if p == q else 0), "cofactor expansion is not the adjugate") + + +def solve4(mat, rhs): + determinant = det4(*(tuple(row) for row in mat)) + if determinant == 0: + return None + solution = [] + for col in range(4): + replaced = [] + for r in range(4): + row = list(mat[r]) + row[col] = rhs[r] + replaced.append(tuple(row)) + solution.append(Fraction(det4(*replaced), determinant)) + return solution + + +def primitive(vec): + scale = 0 + for value in vec: + scale = gcd(scale, abs(value)) + require(scale != 0, "primitive of the zero vector") + vec = tuple(value // scale for value in vec) + for value in vec: + if value > 0: + return vec + if value < 0: + return tuple(-item for item in vec) + return vec + + +def monom(a=0, b=0, c=0, coeff=1): + return {} if coeff == 0 else {(a, b, c): coeff} + + +def poly_add(left, right): + out = dict(left) + for key, value in right.items(): + out[key] = out.get(key, 0) + value + if out[key] == 0: + del out[key] + return out + + +def poly_scale(poly, factor): + return {key: factor * value for key, value in poly.items() if factor * value} + + +def poly_mul(left, right): + out = {} + for (a, b, c), u in left.items(): + for (d, e, f), v in right.items(): + key = (a + d, b + e, c + f) + out[key] = out.get(key, 0) + u * v + if out[key] == 0: + del out[key] + return out + + +def splitting_identity(): + a, b, c = monom(1, 0, 0), monom(0, 1, 0), monom(0, 0, 1) + qx = poly_add(poly_scale(poly_mul(a, b), 2), poly_mul(c, poly_add(a, b))) + ya = poly_add(monom(coeff=2), poly_scale(a, -1)) + yb = poly_add(monom(coeff=2), poly_scale(b, -1)) + yc = poly_scale(c, -1) + qy = poly_add(poly_scale(poly_mul(ya, yb), 2), poly_mul(yc, poly_add(ya, yb))) + difference = poly_add(qy, poly_scale(qx, -1)) + expect = poly_add(monom(coeff=8), poly_add(poly_scale(a, -4), poly_add(poly_scale(b, -4), poly_scale(c, -4)))) + require(difference == expect, "Q(2I-X)-Q(X) is not 4(2-trace X)") + # (2-c)^2 - 2 c (c-2) = 4-c^2, the discriminant of the trace-2 slice. + cc = monom(0, 0, 1) + two = monom(coeff=2) + two_minus = poly_add(two, poly_scale(cc, -1)) + disc = poly_add(poly_mul(two_minus, two_minus), poly_scale(poly_mul(cc, poly_add(cc, poly_scale(two, -1))), -2)) + expect_disc = poly_add(monom(coeff=4), poly_scale(poly_mul(cc, cc), -1)) + require(disc == expect_disc, "the trace-2 discriminant is not 4-c^2") + + +def integral_splits(): + # For an integer c with |c| >= 3, c^2 >= 3^2 = 9 > 4, so 4-c^2 < 0. + require(3 * 3 == 9 and 9 > 4, "the integer bound 3^2 > 4 failed") + found = [] + nonsquares = [] + for c_value in range(-2, 3): + disc = 4 - c_value * c_value + root = int(disc ** 0.5) + if root * root != disc: + nonsquares.append(c_value) + continue + for sign in { -root, root }: + if (2 - c_value + sign) % 2: + continue + a_value = (2 - c_value + sign) // 2 + b_value = 2 - c_value - a_value + frame = (a_value, b_value, c_value) + partner = (2 - a_value, 2 - b_value, -c_value) + if rank_one_nonzero(frame) and rank_one_nonzero(partner): + found.append(frame) + require(nonsquares == [-1, 1], "the only non-square discriminants in -2..2 are not c=±1") + require(sorted(set(found)) == [(0, 0, 2), (0, 2, 0), (2, 0, 0), (2, 2, -2)], "integral 2I splits changed") + for frame in found: + require(quad(sub(TWO_I, frame)) == 0, "integral partner left the cone") + require(frame[2] % 2 == 0, "an integral splitting has odd c") + + +def chart(parameter): + parameter = Fraction(parameter) + den = 1 + parameter * parameter + return ( + Fraction(2 * (1 - parameter), den), + Fraction(2 * parameter * (parameter - 1), den), + Fraction(4 * parameter, den), + ) + + +def direction_of(frame): + scale_frame = coefficient_direction(frame) + require(scale_frame is not None, "frame is not a primitive rank-one expansion") + return scale_frame + + +def coefficient_direction(frame): + # Recover a primitive integer direction when the frame is s uu^T. + a, b, c = (Fraction(value) for value in frame) + if c == 0: + if a == 0 and b != 0: + return ((0, 1), b) + if b == 0 and a != 0: + return ((1, 0), a) + return None + if a == 0 and b == 0: + # u = v, and c = 2 s u^2, so the direction is (1,1) and s = c/2. + return ((1, 1), c / 2) + if a == 0: + return None + # b/a = -v/u when a != 0. Use c = 2 s u v. + ratio = -b / a + # ratio = v/u. Choose a small integer representation. + num, den = ratio.numerator, ratio.denominator + direction = (den, num) + g = gcd(abs(direction[0]), abs(direction[1])) + direction = (direction[0] // g, direction[1] // g) + u, v = direction + base = (u * (u - v), v * (v - u), 2 * u * v) + require(base[0] != 0, "direction formula lost the a coordinate") + scale = a / base[0] + require(tuple(scale * value for value in base) == (a, b, c), "scale does not reproduce the frame") + return direction, scale + + +def support_pairs(name): + opposite = OPPOSITE[name] + first, second = OTHER_PAIR[name] + return ( + add((BY_NAME[opposite], BY_NAME[first])), + add((BY_NAME[opposite], BY_NAME[second])), + add((BY_NAME[name], BY_NAME[first])), + add((BY_NAME[name], BY_NAME[second])), + ) + + +def construction(): + require(add((BY_NAME["A"], BY_NAME["B"], BY_NAME["P"], BY_NAME["Q"])) == TWO_I, "the four projectors do not sum to 2I") + for name, projector in PROJECTORS: + require(rank_one_nonzero(projector), name + " is not rank one") + require(sum(projector) == 1, name + " does not have trace 1") + require(not rank_one_nonzero(sub(TWO_I, projector)), "2I-E is rank one for " + name) + others = [BY_NAME[item] for item in (OPPOSITE[name],) + OTHER_PAIR[name]] + require(add(others) == sub(TWO_I, projector), "the complementary projectors do not sum to 2I-E") + pairs = support_pairs(name) + require(sorted(pairs) == sorted(TARGETS), "the four cross pairs are not the four targets for " + name) + for left, right in (((2, 0, 0), (0, 2, 0)), ((0, 0, 2), (2, 2, -2))): + frames = others + [left, right] + require(add(frames) == sub(TOTAL, projector), "integral witness misses 4I-E for " + name) + for frame in frames: + require(rank_one_nonzero(frame), "integral witness frame is not rank one") + detected = sum(frame[2] % 2 for frame in frames) + (projector[2] % 2) + require(detected == 2, "integral witness does not detect exactly two odd-c calls") + for parameter in (0, 1, 2, 3, Fraction(1, 2), 5): + left = chart(parameter) + right = sub(TWO_I, left) + require(rank_one_nonzero(left) and rank_one_nonzero(right), "chart point is not a splitting at " + str(parameter)) + require(sum(left) == 2, "chart point does not have trace 2") + # The point at infinity of this chart is 2B. + require(rank_one_nonzero((0, 2, 0)) and sub(TWO_I, (0, 2, 0)) == (2, 0, 0), "2B is not a splitting") + nonparallel = chart(2) + partner = sub(TWO_I, nonparallel) + directions = [] + for frame, expected in ( + (BY_NAME["A"], (1, 0)), + (BY_NAME["P"], (1, 1)), + (BY_NAME["Q"], (1, -1)), + (nonparallel, (1, 2)), + (partner, (2, -1)), + ): + direction, _scale = direction_of(frame) + # Normalise sign so the first nonzero coordinate is positive. + if direction[0] < 0 or (direction[0] == 0 and direction[1] < 0): + direction = (-direction[0], -direction[1]) + require(direction == expected, "direction moved: " + str(direction)) + directions.append(direction) + for i, left in enumerate(directions): + for right in directions[i + 1 :]: + require(left[0] * right[1] - left[1] * right[0] != 0, "two witness directions are parallel") + frames = [BY_NAME["A"], BY_NAME["P"], BY_NAME["Q"], nonparallel, partner] + require(add(frames) == sub(TOTAL, BY_NAME["B"]), "nonparallel witness misses 4I-B") + require(set(support_pairs("B")) == set(TARGETS), "nonparallel pattern misses a target") + + +def character_targets(): + detected = 0 + for target in TARGETS: + require((target[0] + target[1]) % 2 == 1 and target[2] % 2 == 1, "a target is not odd in both parities") + detected += target[2] % 2 + require(detected == 4, "not every target has odd P-coefficient") + + +def hand_invertible(): + rows = [[(mask >> column) & 1 for column in range(5)] for mask in HAND_MASKS] + rows.append([1, 1, 1, 1, 1]) + determinant, cofactors = minors(rows) + require(determinant == -2, "the worked incidence determinant is not -2") + adj_identity(rows, cofactors, determinant) + rhs = [] + for index, target in enumerate(TARGETS): + rhs.append(target) + rhs.append(sub(TOTAL, HAND_E)) + frames = [] + for column in range(5): + coords = [] + for coord in range(3): + numer = sum(cofactors[row][column] * rhs[row][coord] for row in range(5)) + coords.append(Fraction(numer, determinant)) + frames.append(tuple(coords)) + require(tuple(frames) == HAND_FRAMES, "worked frames moved") + for frame in frames: + require(quad(frame) != 0, "worked invertible frame met the cone") + # Positive control: the same matrix recovers the nonparallel witness from its own subset sums. + witness = [BY_NAME["A"], BY_NAME["P"], BY_NAME["Q"], chart(2), sub(TWO_I, chart(2))] + true_rhs = [] + for row in rows: + true_rhs.append(tuple(sum(row[column] * witness[column][coord] for column in range(5)) for coord in range(3))) + recovered = [] + for column in range(5): + coords = [] + for coord in range(3): + numer = sum(cofactors[row][column] * true_rhs[row][coord] for row in range(5)) + coords.append(Fraction(numer, determinant)) + recovered.append(tuple(coords)) + require(recovered == witness, "solver did not recover the nonparallel witness") + tampered = [tuple(true_rhs[row]) for row in range(5)] + tampered[4] = (tampered[4][0] + 1, tampered[4][1], tampered[4][2]) + moved = [] + for column in range(5): + coords = [] + for coord in range(3): + numer = sum(cofactors[row][column] * tampered[row][coord] for row in range(5)) + coords.append(Fraction(numer, determinant)) + moved.append(tuple(coords)) + require(moved != witness, "tampered total still recovered the witness") + + +def target_differences(): + bad = {projector for _name, projector in PROJECTORS} + for left in TARGETS: + for right in TARGETS: + if left == right: + continue + require(sub(left, right) not in bad, "a target difference equals a projector") + + +def matrix_rows(masks): + rows = [[(mask >> column) & 1 for column in range(5)] for mask in masks] + rows.append([1, 1, 1, 1, 1]) + return rows + + +def rhs_for(masks, perm, projector): + rhs = [] + for index in range(4): + target = TARGETS[perm[index]] + bit = (masks[index] >> 5) & 1 + rhs.append(tuple(target[coord] - bit * projector[coord] for coord in range(3))) + rhs.append(sub(TOTAL, projector)) + return rhs + + +def particular_solution(rows, cofactors, rhs): + pivot = None + for i in range(5): + for j in range(5): + if cofactors[i][j] != 0: + pivot = (i, j) + break + if pivot: + break + require(pivot is not None, "particular solution requested on a zero adjugate") + i, j = pivot + kernel = cofactors[i][:] + require(kernel[j] != 0, "pivot cofactor vanished") + for row in range(5): + require(sum(rows[row][col] * kernel[col] for col in range(5)) == 0, "cofactor row is not a kernel vector") + keep_rows = [row for row in range(5) if row != i] + keep_cols = [col for col in range(5) if col != j] + mat = [[rows[row][col] for col in keep_cols] for row in keep_rows] + columns = [] + for coord in range(3): + solved = solve4(mat, [rhs[row][coord] for row in keep_rows]) + require(solved is not None, "the pivot minor was singular") + full = [None] * 5 + for col, value in zip(keep_cols, solved): + full[col] = value + full[j] = Fraction(0) + columns.append(full) + frames = [(columns[0][f], columns[1][f], columns[2][f]) for f in range(5)] + for row in range(5): + for coord in range(3): + got = sum(rows[row][col] * frames[col][coord] for col in range(5)) + require(got == rhs[row][coord], "particular solution misses an equation") + return frames, kernel + + +def left_kernel(rows): + matrix = [[Fraction(rows[r][c]) for r in range(5)] for c in range(5)] + pivots = {} + rank = 0 + for col in range(5): + pivot = None + for row in range(rank, 5): + if matrix[row][col] != 0: + pivot = row + break + if pivot is None: + continue + matrix[rank], matrix[pivot] = matrix[pivot], matrix[rank] + pivot_value = matrix[rank][col] + for entry in range(5): + matrix[rank][entry] /= pivot_value + for row in range(5): + if row != rank and matrix[row][col] != 0: + factor = matrix[row][col] + for entry in range(5): + matrix[row][entry] -= factor * matrix[rank][entry] + pivots[col] = rank + rank += 1 + free = [col for col in range(5) if col not in pivots] + basis = [] + for column in free: + vector = [Fraction(0)] * 5 + vector[column] = Fraction(1) + for col, row in pivots.items(): + vector[col] = -matrix[row][column] + basis.append(vector) + return rank, basis + + +def polar_blocks(frames, kernel, moving): + """Linear conditions for every moving frame but the first to be rank one when the first is.""" + first = moving[0] + scale = Fraction(kernel[first]) + equations = [] + for other in moving[1:]: + ratio = Fraction(kernel[other]) / scale + shift = tuple(frames[other][coord] - ratio * frames[first][coord] for coord in range(3)) + # B(shift, X) = -Q(shift)/ratio, with X the first moving frame. + equations.append( + ( + 2 * shift[1] + shift[2], + 2 * shift[0] + shift[2], + shift[0] + shift[1], + -quad(shift) / ratio, + ) + ) + return equations + + +def linear_rank(equations): + if not equations: + return 0, [], {} + matrix = [[Fraction(value) for value in row] for row in equations] + pivots = {} + rank = 0 + for col in range(3): + pivot = None + for row in range(rank, len(matrix)): + if matrix[row][col] != 0: + pivot = row + break + if pivot is None: + continue + matrix[rank], matrix[pivot] = matrix[pivot], matrix[rank] + pivot_value = matrix[rank][col] + for entry in range(4): + matrix[rank][entry] /= pivot_value + for row in range(len(matrix)): + if row != rank and matrix[row][col] != 0: + factor = matrix[row][col] + for entry in range(4): + matrix[row][entry] -= factor * matrix[rank][entry] + pivots[col] = rank + rank += 1 + for row in range(rank, len(matrix)): + if matrix[row][3] != 0: + return -1, None, None + return rank, matrix, pivots + + +def completes(frames, kernel, moving): + equations = polar_blocks(frames, kernel, moving) + for equation in equations: + if equation[0] == 0 and equation[1] == 0 and equation[2] == 0 and equation[3] != 0: + return False + usable = [equation for equation in equations if equation[:3] != (0, 0, 0)] + rank, matrix, pivots = linear_rank(usable) + if rank < 0: + return False + point = [Fraction(0), Fraction(0), Fraction(0)] + for col, row in pivots.items(): + point[col] = matrix[row][3] + free = [col for col in range(3) if col not in pivots] + if free: + # The only open families in this census are the trace-2 planes, handled + # structurally before this call. A free polar system would be a new case. + return None + candidate = tuple(point) + return quad(candidate) == 0 and candidate != (0, 0, 0) + + +def census(): + require(len(MASKS) == 50, "subset count is not 50") + require(len(list(combinations(range(50), 4))) == 230300, "unordered domain is not 230300") + twin = 0 + rank3 = 0 + invertible = 0 + hits = 0 + full_shapes = {} + zero_masks = {1: 0, 3: 0} + frozen_killed = {1: 0, 3: 0} + consistent = {1: 0, 3: 0} + survivors = 0 + by_projector = {name: 0 for name, _ in PROJECTORS} + placements = set() + for comb in combinations(range(50), 4): + masks = [MASKS[index] for index in comb] + groups = {} + for mask in masks: + groups.setdefault(mask & 31, []).append(mask) + if any(len(group) > 1 for group in groups.values()): + twin += 1 + for group in groups.values(): + require(len(group) <= 2, "a frame projection has more than two masks") + if len(group) == 2: + require(group[0] ^ group[1] == 32, "duplicate rows are not an E-bit pair") + continue + rows = matrix_rows(masks) + determinant, cofactors = minors(rows) + adj_identity(rows, cofactors, determinant) + if determinant != 0: + invertible += 1 + columns = list(zip(*cofactors)) + for perm in PERMS: + for _name, projector in PROJECTORS: + rhs = rhs_for(masks, perm, projector) + good = True + for column in columns: + numer = [ + sum(column[row] * rhs[row][coord] for row in range(5)) + for coord in range(3) + ] + if numer == [0, 0, 0] or 2 * numer[0] * numer[1] + numer[2] * (numer[0] + numer[1]) != 0: + good = False + break + if good: + hits += 1 + continue + if all(cofactors[i][j] == 0 for i in range(5) for j in range(5)): + rank3 += 1 + rank, basis = left_kernel(rows) + require(rank == 3 and len(basis) == 2, "a zero adjugate was not rank 3") + for vector in basis: + for col in range(5): + require(sum(vector[row] * rows[row][col] for row in range(5)) == 0, "rank-3 vector is not a left kernel") + require(basis[0] != basis[1], "rank-3 kernel vectors repeat") + for perm in PERMS: + for _name, projector in PROJECTORS: + rhs = rhs_for(masks, perm, projector) + inconsistent = False + for vector in basis: + for coord in range(3): + if sum(vector[row] * rhs[row][coord] for row in range(5)) != 0: + inconsistent = True + break + if inconsistent: + break + require(inconsistent, "a rank-3 system was consistent") + continue + row_index = next(i for i in range(5) if any(cofactors[i][j] for j in range(5))) + kernel = cofactors[row_index] + zeros = [index for index in range(5) if kernel[index] == 0] + if not zeros: + column = next(j for j in range(5) if kernel[j]) + shape = primitive([cofactors[row][column] for row in range(5)]) + require(shape[4] == -1 and sum(shape[:4]) == 2 and set(shape[:4]) <= {0, 1}, "full kernel shape is not a pair of subset rows") + full_shapes[shape] = full_shapes.get(shape, 0) + 1 + for row in range(5): + require(sum(shape[i] * rows[i][row] for i in range(5)) == 0, "full-kernel lambda misses the row dependence") + continue + require(len(zeros) in (1, 3), "unexpected frozen-frame count " + str(len(zeros))) + zero_masks[len(zeros)] += 1 + moving = [index for index in range(5) if kernel[index] != 0] + if len(zeros) == 3: + require(len(moving) == 2, "three frozen frames did not leave two moving frames") + require(kernel[moving[0]] + kernel[moving[1]] == 0, "a three-frozen kernel does not cancel") + column = next(j for j in range(5) if kernel[j]) + lam = [cofactors[row][column] for row in range(5)] + for row in range(5): + require(sum(lam[i] * rows[i][row] for i in range(5)) == 0, "singular lambda is not a left kernel") + for perm in PERMS: + for name, projector in PROJECTORS: + rhs = rhs_for(masks, perm, projector) + if any(sum(lam[row] * rhs[row][coord] for row in range(5)) != 0 for coord in range(3)): + continue + consistent[len(zeros)] += 1 + frames, solved_kernel = particular_solution(rows, cofactors, rhs) + require(all((solved_kernel[i] == 0) == (kernel[i] == 0) for i in range(5)), "kernel zeros moved") + killed = False + for index in zeros: + if not rank_one_nonzero(frames[index]): + killed = True + if killed: + frozen_killed[len(zeros)] += 1 + continue + if len(zeros) == 1: + completed = completes(frames, solved_kernel, moving) + require(completed is False, "a one-frozen family met the cone") + continue + survivors += 1 + by_projector[name] += 1 + require(solved_kernel[moving[0]] + solved_kernel[moving[1]] == 0, "moving kernel coefficients do not cancel") + moving_sum = add((frames[moving[0]], frames[moving[1]])) + require(moving_sum == TWO_I, "survivor moving frames do not sum to 2I") + frozen = [] + for index in zeros: + require(all(value.denominator == 1 for value in frames[index]), "frozen frame is not integral") + frozen.append(tuple(int(value) for value in frames[index])) + expected = {BY_NAME[item] for item in (OPPOSITE[name],) + OTHER_PAIR[name]} + require(set(frozen) == expected, "survivor frozen frames are not the complementary projectors") + explicit = [None] * 5 + for index, frame in zip(zeros, frozen): + explicit[index] = frame + explicit[moving[0]] = (2, 0, 0) + explicit[moving[1]] = (0, 2, 0) + placements.add((name, tuple(zip(zeros, frozen)))) + for row in range(5): + for coord in range(3): + got = sum(rows[row][col] * explicit[col][coord] for col in range(5)) + require(got == rhs[row][coord], "2A+2B misses a survivor equation") + for frame in explicit: + require(rank_one_nonzero(frame), "explicit survivor frame is not rank one") + require(twin == 22370, "twin count changed: " + str(twin)) + require(rank3 == 2450, "rank-3 count changed: " + str(rank3)) + require(invertible == 120400, "invertible count changed: " + str(invertible)) + require(hits == 0, "an invertible system met the cone") + require(full_shapes == FULL_SHAPES, "full-kernel shapes changed: " + str(full_shapes)) + require(consistent == {1: 17280, 3: 28800}, "consistent singular counts changed: " + str(consistent)) + require(frozen_killed == {1: 16320, 3: 28560}, "frozen-kill counts changed: " + str(frozen_killed)) + require(survivors == 240, "survivor count changed: " + str(survivors)) + require(by_projector == {"A": 60, "B": 60, "P": 60, "Q": 60}, "survivors are not uniform in E") + require(len(placements) == 240, "projector placements are not in bijection with the survivors") + require(zero_masks == {1: 27840, 3: 53400}, "frozen-pattern counts changed: " + str(zero_masks)) + require( + twin + rank3 + invertible + sum(full_shapes.values()) + zero_masks[1] + zero_masks[3] == 230300, + "the mask domain was not partitioned", + ) + + +def failure_controls(): + require(not rank_one_nonzero((0, 0, 0)), "zero was accepted") + require(not rank_one_nonzero((1, 1, 0)), "I was accepted") + require(quad((1, 1, 0)) == 2, "Q(I) changed") + broken = (1, 0, 1) + require(quad(broken) == 1, "Q(A+P) changed") + require(not rank_one_nonzero(broken), "A+P was accepted as rank one") + + +def main(): + require(len(PERMS) == 24, "there are not 24 target assignments") + require(det4((1, 0, 0, 0), (0, 1, 0, 0), (0, 0, 1, 0), (0, 0, 0, 1)) == 1, "det I_4 is not 1") + for target in TARGETS: + require(sum(target) == 2, "a target trace is not 2") + require(quad(target) == 1, "twice a target determinant is not 1") + complement = (4 - target[0], 4 - target[1], -target[2]) + require(quad(complement) == 17, "twice det(4I-H) is not 17") + splitting_identity() + integral_splits() + construction() + character_targets() + target_differences() + hand_invertible() + failure_controls() + census() + print("PASS five-signed-one-old checks") + + +if __name__ == "__main__": + main()