From 5b19247cd04c49472d6ae9f4d42a87c1d484b3e1 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 10 Nov 2026 09:00:00 +0000 Subject: [PATCH] Prove five once-each rank-one frames miss the five-call endpoint. The shortest equation R+S+T+U+V=4I has no target-supporting rational rank-one solution: an exhaustive census of the 116280 pair-and-triple tuples, plus one full-parity witness that is not a word. No kappa change. Co-authored-by: unpaidmoon --- research/five-signed-once-support/PROOF.md | 188 +++++++++ research/five-signed-once-support/README.md | 48 +++ .../five-signed-once-support/SOURCES.json | 18 + research/five-signed-once-support/TASK.json | 75 ++++ research/five-signed-once-support/VERIFY.json | 34 ++ research/five-signed-once-support/verify.py | 364 ++++++++++++++++++ 6 files changed, 727 insertions(+) create mode 100644 research/five-signed-once-support/PROOF.md create mode 100644 research/five-signed-once-support/README.md create mode 100644 research/five-signed-once-support/SOURCES.json create mode 100644 research/five-signed-once-support/TASK.json create mode 100644 research/five-signed-once-support/VERIFY.json create mode 100644 research/five-signed-once-support/verify.py diff --git a/research/five-signed-once-support/PROOF.md b/research/five-signed-once-support/PROOF.md new file mode 100644 index 0000000000..a8bf7e443b --- /dev/null +++ b/research/five-signed-once-support/PROOF.md @@ -0,0 +1,188 @@ +# Five once-each rank-one frames do not meet the five-call endpoint + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. + +## Claim + +In the PR2085/2112 formal register model, the shortest determinant equation that uses five new labels once each is + +``` +R + S + T + U + V = 4I. +``` + +It is the zero-old-call case: five paid calls and no call on `A`, `B`, `P`, or `Q`. Two statements are made about it. + +1. **Exhaustive finite census of target support.** No five nonzero symmetric rational rank-one matrices summing to `4I` have all four targets as subset sums. The equation therefore admits no word. The domain is finite because a target-carrying subset has size 2 or 3, and every ordered 4-tuple of such subsets is solved exactly. This is a proof of that scoped support statement by complete case analysis. It is not a heuristic search, and it is not a hand classification into two degree patterns of the kind used for four calls. +2. **Parity-image witness, not a census.** The same sum, without the support requirement, has an explicit solution in five pairwise nonparallel primitive directions whose integral span has full parity image `F2^2`. The three-frame route does not apply to every five-frame solution. That witness is still not a word: the census already excludes it, and a direct character count on this one solution detects two calls and four targets. + +Selected κ stays `781451/250000000`. Nothing here is a multiplication theorem, a statement about six or more added frames, or a statement about five added frames together with an old call. The census does not lower the eight-call minimum. It removes only this five-call 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 the normalization recorded in `research/bit-two-signed-frame-floor/PROOF.md`, Section 1 (itself from PR2910 and PR6190). This file does not reprove them. + +## 1. Setup + +Addresses are rational symmetric 2-by-2 matrices. Write + +``` +A = diag(1,0), B = diag(0,1), +P = [[1,1],[1,1]]/2, Q = [[1,-1],[-1,1]]/2. +``` + +A coefficient vector `(a,b,c)` means `aA + bB + cP`, with matrix + +``` +[[a + c/2, c/2], [c/2, b + c/2]], +``` + +trace `a+b+c`, and determinant `ab + c(a+b)/2`. The matrix is nonzero and rank one exactly when the vector is nonzero and the determinant is zero. Equivalently, the integer polynomial `2ab + c(a+b)` is zero. + +The four targets and their coefficient vectors are + +``` +A+P = (1,0,1), A+Q = (2,1,-1), +B+P = (0,1,1), B+Q = (1,2,-1). +``` + +Each has trace 2 and determinant `1/2`. Their sum is `2A+2B+2P+2Q = 4I`, with coefficient vector `(4,4,0)` and determinant 16. + +For a primitive integer direction `u = (u1,u2)` and a nonzero rational scale `s`, + +``` +s uu^T = s (u1(u1-u2), u2(u2-u1), 2 u1 u2). +``` + +Every nonzero symmetric rational rank-one matrix has this form. The parity image of an integral coefficient vector is + +``` +φ(a,b,c) = ((a+b) mod 2, c mod 2) in F2^2. +``` + +## 2. Only pairs and triples can carry a target + +**Lemma 1.** Let `F1,...,F5` be nonzero symmetric rational rank-one matrices with sum `4I`. A subset sum equal 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`, with trace 8, while each target has trace 2. A four-element subset sums to a target `H` only if the omitted frame equals `4I-H`. For every target the matrix expansion gives + +``` +det(4I-H) = 16 - 4·tr(H) + det(H) = 16 - 8 + 1/2 = 17/2 ≠ 0, +``` + +and the coefficient formula for `(4-a,4-b,-c)` gives the same value. So `4I-H` is not rank one. The only remaining subset sizes are 2 and 3. + +The four targets are distinct, so the four subsets are distinct. There are `C(5,2)+C(5,3) = 20` candidate subsets and `C(20,4)·4! = 116280` ordered 4-tuples. That list is the whole domain. It is not a sample of directions or scales. + +## 3. The incidence system + +Label the five frames by columns. For an ordered 4-tuple of subsets, let `M` be the 5-by-5 integer matrix whose first four rows are the subset indicators and whose last row is `(1,1,1,1,1)`. Target support and the sum `4I` are the three integer systems + +``` +M f_a = r_a, M f_b = r_b, M f_c = r_c, +``` + +where the right-hand sides are the corresponding coordinates of the four targets followed by `4`, `4`, or `0`. Any rational solution of the matrix equation is a candidate. It is a rank-one solution only if every column frame is nonzero and lies on the determinant cone. + +`verify.py` decides every tuple by the Leibniz determinant of `M`, which is an integer. The sign convention is anchored by `det I_5 = 1` and by one 5-by-5 determinant computed by hand in Section 4. + +- If `det M ≠ 0`, Cramer's rule supplies the unique rational solution. The program checks the matrix residual `M n = (det M) r` on every coordinate and rejects the tuple unless some frame is zero or off the cone. +- If `det M = 0`, exact rational row reduction is run twice, once with columns left to right and once right to left. An inconsistent augmented matrix removes the tuple. A consistent system of rank other than 4, or a rank-4 kernel with no zero coordinate, would be left unresolved and the program would fail. Neither occurs. Every remaining system has rank 4 and a kernel coordinate equal to zero, so the corresponding frame is constant on the whole affine line. That constant frame is off the cone, and the two elimination orders agree on its value. + +The cone test uses the integer numerator `2ab+c(a+b)`. A zero numerator with a nonzero vector would have been reported as a hit. There is no hit. + +## 4. A worked invertible tuple + +Take the subsets of column indices + +``` +{0,1}, {0,2}, {1,2}, {0,3}, +``` + +with indicators `(1,1,0,0,0)`, `(1,0,1,0,0)`, `(0,1,1,0,0)`, and `(1,0,0,1,0)`. Row reduction of the incidence matrix, subtracting the first row from the later rows that begin with 1 and then expanding, gives determinant `-2`. The same value is what the Leibniz routine returns. Cramer's rule produces the unique frames + +``` +(3/2, 0, -1/2), (-1/2, 0, 3/2), (1/2, 1, -1/2), +(-1/2, 2, -1/2), (3, 1, 0). +``` + +Their integer numerators `2ab+c(a+b)`, cleared of the common denominator, are nonzero. This tuple is one invertible case. It is not a substitute for the census. + +## 5. A worked rank-4 tuple + +Take the subsets + +``` +{0,1}, {0,2}, {1,3}, {2,3}. +``` + +Adding the first subset equation to the fourth, and the second to the third, gives the same relation + +``` +F0+F1+F2+F3 = (A+P)+(B+Q) = 2I = (2,2,0), +``` + +because both pairings of targets sum to `2I`. The total-sum equation then freezes the omitted frame: + +``` +F4 = 4I - 2I = 2I = (2,2,0). +``` + +The determinant of `2I` is 4, so `F4` is not rank one. The kernel may still move `F0,F1,F2,F3`. It cannot move `F4`, and one non-rank-one frame excludes the whole line. One point on the line is + +``` +(2,1,-1), (-1,-1,2), (0,0,0), (1,2,-1), (2,2,0). +``` + +Direct addition checks the four subset equations and the total sum. The zero third frame is an artifact of this parameter value, not a second frozen frame. The program records the frozen value `2I` for the tuple. + +## 6. Census + +The program classifies all 116280 tuples. + +| Class | Count | Rank-one support | +|---|---:|---| +| Invertible, unique rational solution off the cone | 71040 | none | +| Inconsistent augmented matrix | 44520 | none | +| Consistent rank 4, one frame frozen off the cone | 720 | none | + +The 720 frozen frames take only the six values + +``` +±2I = ±(2,2,0), ±(A-B) = ±(1,-1,0), ±(P-Q) = ±(1,1,-2), +``` + +each for 120 tuples. Their determinants are `4` or `-1`. No consistent system of rank below 4 occurs, and no rank-4 kernel lacks a zero coordinate. Those are checked assertions, not omitted branches. + +Therefore no rational rank-one solution has target support. By the inherited subset-sum necessity, the equation admits no word. The direct eight-call word, two old labels on each target, is untouched. + +## 7. A full parity image + +**Witness.** The directions and scales + +``` +(-1,1) at 1, (0,1) at -1, (1,0) at 3, (1,1) at -1/2, (1,3) at 1/2 +``` + +give the integral frames + +``` +(2,2,-2), (0,-1,0), (3,0,0), (0,0,-1), (-1,3,3). +``` + +Their sum is `(4,4,0)`. Each determinant is 0 and each vector is nonzero. The five directions are pairwise nonparallel. The integer combinations + +``` +(0,-1,0), (0,0,-1), (0,-1,-1) +``` + +have parity images `(1,0)`, `(0,1)`, and `(1,1)`. The parity image of the integral span is all of `F2^2`. + +No integer form of shape `(odd,odd,even)` or `(even,even,odd)` is even on all five frames. The three-frame extension, which needs one of those shapes to kill every added frame, does not apply to this solution. + +This is one explicit solution of the sum. It is not an enumeration of all five-direction solutions. A full parity image is not a word, and Section 6 already excludes this witness as a support solution: none of its 31 nonempty subset sums equals a target. + +## 8. The witness still fails a direct character count + +Reduce the coefficient of `P` modulo 2. All four targets have odd `P`-coefficient. Among the five frames, only `(0,0,-1)` and `(-1,3,3)` have odd `P`-coefficient, so two calls are detected. Two calls against four targets is forbidden by the inherited inequality. The inequality is not reproved here. Section 8 records that evading the vanishing test is not the same as surviving every first-order character, for this one solution. It is not a character theorem for every five-frame solution of the sum. + +## Open next questions + +Six once-each added frames, and every five-frame equation whose residual is not `4I`, are untouched. One extra old call changes both the residual and the allowed subset sizes, so Lemma 1 does not apply. A solution whose parity image is full can still fail a character that detects only some of the new frames. diff --git a/research/five-signed-once-support/README.md b/research/five-signed-once-support/README.md new file mode 100644 index 0000000000..2128afa28c --- /dev/null +++ b/research/five-signed-once-support/README.md @@ -0,0 +1,48 @@ +# Five once-each signed frames and the five-call equation + +**Exhaustive finite support census, plus one parity-image witness. No new κ and no word.** + +The shortest determinant equation that uses five new labels once each is `R+S+T+U+V = 4I`: five paid calls and no old call. In the PR2085/2112 model that equation admits no word. Lemma 1 of [PROOF.md](PROOF.md) limits a target-carrying subset to size 2 or 3, and every one of the 116280 ordered 4-tuples of such subsets fails the rank-one cone. The argument and the census counts are in [PROOF.md](PROOF.md). + +The same sum has one explicit rational solution on five pairwise nonparallel primitive directions whose parity image is all of `F2^2`. The three-frame test, which needs that image to miss `(1,1)`, does not apply to every five-frame solution. The witness is still excluded by the support census and by a direct character count on that one solution. It is one solution, not a census, and it is not a word. + +The selected record stays κ = `781451/250000000`. Six or more added frames, and five added frames together with an old call, stay open. This census 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 takes the five-frame question left open by the four-call note, discussion comment 19507121, which itself follows the three-frame note. It does not redo the four-call theorem, the three-frame character, or a four-frame equation with an old call. + +Evidence classes, kept apart: + +1. **Exhaustive finite census, and therefore a scoped proof of support failure.** The domain is the 116280 ordered 4-tuples of distinct weight-2 and weight-3 subsets. Of them, 71040 have invertible incidence matrices and a unique rational solution off the determinant cone, 44520 are inconsistent, and 720 are consistent of rank 4 with one frame frozen at `±2I`, `±(A-B)`, or `±(P-Q)`. No tuple meets the rank-one hypothesis. The determinant identities `det H = 1/2` and `det(4I-H) = 17/2` are checked exactly, and one invertible determinant is reduced by hand to `-2`. This is not a heuristic search and not a sample of directions. +2. **Explicit witness, not a census.** Directions `(-1,1)`, `(0,1)`, `(1,0)`, `(1,1)`, `(1,3)` at scales `1`, `-1`, `3`, `-1/2`, `1/2` sum to `4I`, and three declared integer combinations realize parity images `(1,0)`, `(0,1)`, and `(1,1)`. No AB or PQ form kills all five frames. +3. **Direct count on that one witness.** The `P`-coefficient modulo 2 detects two calls and four targets. The inherited inequality is not reproved. The witness's nonempty subset sums miss every target; that list checks the witness and is not the census. + +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/five-signed-once-support --check-only +python3.12 scripts/research_package.py --package research/five-signed-once-support +``` + +The direct check is `python3 -I -W error -B research/five-signed-once-support/verify.py`. + +## Open next questions + +Can six added signed rank-one frames, each used once and with no old call, meet target support for `F1+...+F6 = 4I`? A six-call word would still lower the eight-call minimum, and this census uses exactly five columns. A useful first step is to rewrite the size lemma: the complement of a four-element subset is now a pair, so sizes 2, 3, and 4 all remain possible, and then to test one six-direction solution. No such census is supplied here. + +Can five added frames plus one old call meet support at length 6? Lemma 1 uses the residual `4I`. A useful first step is one old projector `E` and the equation `R+S+T+U+V = 4I-E`, then the subset-size test on that residual. No such solution is supplied here. + +A full parity image does not by itself survive every character: the witness above is still excluded by a character that detects only two of the five frames. + +## Credit + +The register model is Cinna Davis's PR2085/2112 formal model. The determinant and the subset-sum necessity are the PR2910 package as recorded in apoursh's two-signed-frame floor, PR6190. That floor stopped at two added frames. The three-frame all-old-once character is the package `research/three-signed-old-once`. The four-call support proof and the open five-frame question are the package `research/four-signed-once-parity`, merged as PR6952, discussion comment 19507121. Neither is redone here. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. No independent human or formal-kernel review. New work is Apache-2.0. diff --git a/research/five-signed-once-support/SOURCES.json b/research/five-signed-once-support/SOURCES.json new file mode 100644 index 0000000000..41a0d8e4ed --- /dev/null +++ b/research/five-signed-once-support/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/five-signed-once-support/TASK.json b/research/five-signed-once-support/TASK.json new file mode 100644 index 0000000000..eb19b16043 --- /dev/null +++ b/research/five-signed-once-support/TASK.json @@ -0,0 +1,75 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "For the shortest five-label equation R+S+T+U+V=4I, prove by an exhaustive support census that no nonzero symmetric rational rank-one solution has all four targets as subset sums, and exhibit one five-direction solution whose parity image is all of F2^2.", + "scope_change_reason": "The card asks for a larger or nonabelian native alphabet. This package stays in the abelian symmetric 2-by-2 model and answers the five-frame question left open by the four-call support census, for the single shortest once-each equation.", + "bottleneck_link": "Side result on the signed-frame escape. The five-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 five-call support census and one explicit parity-image witness. Do not census six frames, and do not add an old call.", + "outcome": "completed", + "evidence": "Exhaustive finite census: every target has trace 2 and determinant 1/2, so only subset sizes 2 and 3 can match, and all 116280 ordered 4-tuples fail. 71040 are invertible and off the cone, 44520 are inconsistent, and 720 freeze one frame at \u00b12I, \u00b1(A-B), or \u00b1(P-Q). Parity witness, not a census: directions (-1,1),(0,1),(1,0),(1,1),(1,3) at scales 1,-1,3,-1/2,1/2 have full parity image and are still excluded by a two-call character count. The inherited determinant and subset-sum necessity are not reproved.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance with the census and verifier. No independent human or formal-kernel review.", + "open_questions": [ + { + "question": "Can six added signed rank-one frames, each used once and with no old call, meet target support for F1+...+F6=4I?", + "why_it_matters": "A six-call word would still lower the eight-call minimum. The five-column census does not apply, and the complement of a four-element subset is now a pair.", + "first_step": "Rewrite the size lemma for six frames, keeping subset sizes 2, 3, and 4, then test one six-direction rational solution.", + "blocked_by": "Lemma 1 uses five frames. Size 4 is no longer the complement of a single frame, so the 116280-tuple domain does not carry over." + }, + { + "question": "Can five added signed rank-one frames plus one old call meet support at length 6?", + "why_it_matters": "A length-6 word would lower the eight-call minimum. Theorem-level support failure in this package uses the residual 4I.", + "first_step": "Fix one old projector E and the equation R+S+T+U+V=4I-E, then repeat the subset-size test on that residual.", + "blocked_by": "Every identity here uses the residual 4I. One old call changes the allowed subset sizes." + } + ], + "selection": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19507121", + "upstream_checked_utc": "2026-11-10T08:40:00Z", + "priority_revision": 8 + } +} diff --git a/research/five-signed-once-support/VERIFY.json b/research/five-signed-once-support/VERIFY.json new file mode 100644 index 0000000000..0937107bdb --- /dev/null +++ b/research/five-signed-once-support/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Target and complement determinant identities; Leibniz anchor det I_5=1 and one hand-reduced det -2; exhaustive classification of all 116280 support tuples into 71040 invertible, 44520 inconsistent and 720 rank-4 families with the six frozen frames; one declared five-direction witness with full parity image, a two-call character count and no target subset sum; positive control that the same solver recovers that witness from its own subset sums; failure controls for a tampered target, for I, and for the zero matrix." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Same identities, census, witness, positive control and failure controls under python -O." + } + ] +} diff --git a/research/five-signed-once-support/verify.py b/research/five-signed-once-support/verify.py new file mode 100644 index 0000000000..18514ddba5 --- /dev/null +++ b/research/five-signed-once-support/verify.py @@ -0,0 +1,364 @@ +#!/usr/bin/env python3 +"""Checks for the five-call equation R+S+T+U+V = 4I. + +PROOF.md holds the argument. This program checks the subset-size +identities, exhausts every ordered 4-tuple of distinct weight-2 and +weight-3 subsets, and checks one declared five-direction witness. +The tuple list is the whole support domain left by the size lemma. +The witness is one solution of the sum, not a census of solutions. +""" + +from fractions import Fraction +from itertools import combinations, permutations + + +TARGETS = ((1, 0, 1), (2, 1, -1), (0, 1, 1), (1, 2, -1)) +TOTAL = (4, 4, 0) +MASKS = tuple(mask for mask in range(32) if bin(mask).count("1") in (2, 3)) +BAD_FROZEN = { + (2, 2, 0), + (-2, -2, 0), + (1, -1, 0), + (-1, 1, 0), + (1, 1, -2), + (-1, -1, 2), +} +HAND_MASKS = (3, 5, 6, 9) +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(3), Fraction(1), Fraction(0)), +) +SINGULAR_MASKS = (3, 5, 10, 12) +WITNESS_DIRECTIONS = ((-1, 1), (0, 1), (1, 0), (1, 1), (1, 3)) +WITNESS_SCALES = (Fraction(1), Fraction(-1), Fraction(3), Fraction(-1, 2), Fraction(1, 2)) +WITNESS_FRAMES = ( + (2, 2, -2), + (0, -1, 0), + (3, 0, 0), + (0, 0, -1), + (-1, 3, 3), +) + +PERMS = [] +for _perm in permutations(range(5)): + inversions = sum(1 for i in range(5) for j in range(i + 1, 5) if _perm[i] > _perm[j]) + PERMS.append((_perm, 1 if inversions % 2 == 0 else -1)) + + +def require(condition, message): + if not condition: + raise SystemExit("FAIL: " + message) + + +def coefficient(direction, scale): + x, y = direction + scale = Fraction(scale) + return (scale * x * (x - y), scale * y * (y - x), 2 * scale * x * y) + + +def quad(frame): + a, b, c = frame + return 2 * a * b + c * (a + b) + + +def determinant(frame): + a, b, c = frame + return a * b + c * (a + b) / 2 + + +def trace(frame): + return frame[0] + frame[1] + frame[2] + + +def add(frames): + return tuple(sum(frame[i] for frame in frames) for i in range(3)) + + +def rank_one_nonzero(frame): + return frame != (0, 0, 0) and quad(frame) == 0 + + +def parity(frame): + require(all(value.denominator == 1 for value in frame), "parity on a non-integral frame") + return ((int(frame[0]) + int(frame[1])) % 2, int(frame[2]) % 2) + + +def det5(rows): + total = 0 + for perm, sign in PERMS: + total += ( + sign + * rows[0][perm[0]] + * rows[1][perm[1]] + * rows[2][perm[2]] + * rows[3][perm[3]] + * rows[4][perm[4]] + ) + return total + + +def incidence(masks, targets, total): + rows = [] + rhs = [[], [], []] + for index, mask in enumerate(masks): + rows.append([(mask >> column) & 1 for column in range(5)]) + for coord in range(3): + rhs[coord].append(targets[index][coord]) + rows.append([1, 1, 1, 1, 1]) + for coord in range(3): + rhs[coord].append(total[coord]) + return rows, rhs + + +def cramer(rows, rhs): + denominator = det5(rows) + numerators = [] + for column in range(5): + coords = [] + for coord in range(3): + replaced = [row[:] for row in rows] + for row_index in range(5): + replaced[row_index][column] = rhs[coord][row_index] + coords.append(det5(replaced)) + numerators.append(tuple(coords)) + return denominator, numerators + + +def residual_ok(rows, rhs, numerators, denominator): + for row_index in range(5): + for coord in range(3): + got = sum(rows[row_index][column] * numerators[column][coord] for column in range(5)) + if got != denominator * rhs[coord][row_index]: + return False + return True + + +def rref_family(rows, rhs, reverse): + columns = list(range(4, -1, -1)) if reverse else list(range(5)) + matrix = [ + [Fraction(rows[row][column]) for column in range(5)] + [Fraction(rhs[coord][row]) for coord in range(3)] + for row in range(5) + ] + pivot_of = {} + rank = 0 + for column in columns: + pivot = None + for row in range(rank, 5): + if matrix[row][column] != 0: + pivot = row + break + if pivot is None: + continue + matrix[rank], matrix[pivot] = matrix[pivot], matrix[rank] + pivot_value = matrix[rank][column] + for entry in range(8): + matrix[rank][entry] /= pivot_value + for row in range(5): + if row == rank or matrix[row][column] == 0: + continue + factor = matrix[row][column] + for entry in range(0, 8): + matrix[row][entry] -= factor * matrix[rank][entry] + pivot_of[column] = rank + rank += 1 + for row in range(rank, 5): + if any(matrix[row][5 + coord] != 0 for coord in range(3)): + return ("inconsistent",) + if rank != 4: + return ("unhandled", rank) + free = [column for column in range(5) if column not in pivot_of] + if len(free) != 1: + return ("unhandled", rank) + free = free[0] + kernel = [Fraction(0)] * 5 + kernel[free] = Fraction(1) + for column, row in pivot_of.items(): + kernel[column] = -matrix[row][free] + zeros = [column for column in range(5) if kernel[column] == 0] + if zeros == []: + return ("unhandled", "no frozen frame") + frozen = [] + for column in zeros: + row = pivot_of[column] + frozen.append(tuple(matrix[row][5 + coord] for coord in range(3))) + return ("family", tuple(frozen), tuple(kernel)) + + +def target_identities(): + require(len(PERMS) == 120, "the symmetric group on five letters has 120 elements") + require(sum(sign for _, sign in PERMS) == 0, "permutation signs are not balanced") + identity = [[1 if i == j else 0 for j in range(5)] for i in range(5)] + require(det5(identity) == 1, "Leibniz determinant of the identity is not 1") + require(len(MASKS) == 20, "weight-2 and weight-3 subsets are not the 20 masks") + require(len(set(TARGETS)) == 4, "the four targets are not distinct") + require(add(TARGETS) == TOTAL, "the four targets do not sum to 4I") + for target in TARGETS: + require(trace(target) == 2, "a target trace is not 2") + require(determinant(target) == Fraction(1, 2), "a target determinant is not 1/2") + require(quad(target) == 1, "twice a target determinant is not 1") + complement = (4 - target[0], 4 - target[1], -target[2]) + require(determinant(complement) == Fraction(17, 2), "det(4I-H) is not 17/2") + matrix_expansion = 16 - 4 * trace(target) + determinant(target) + require(matrix_expansion == Fraction(17, 2), "the complement expansion is not 17/2") + require(determinant(TOTAL) == 16, "det(4I) is not 16") + require(trace(TOTAL) == 8, "the trace of 4I is not 8") + + +def support_census(): + invertible = 0 + inconsistent = 0 + families = 0 + frozen_seen = {} + for chosen in combinations(MASKS, 4): + for masks in permutations(chosen): + rows, rhs = incidence(masks, TARGETS, TOTAL) + denominator = det5(rows) + if denominator != 0: + invertible += 1 + _, numerators = cramer(rows, rhs) + require( + residual_ok(rows, rhs, numerators, denominator), + "Cramer residual failed for " + str(masks), + ) + off_cone = False + for coords in numerators: + if quad(coords) != 0 or coords == (0, 0, 0): + off_cone = True + break + require(off_cone, "invertible system met the rank-one cone at " + str(masks)) + continue + forward = rref_family(rows, rhs, False) + backward = rref_family(rows, rhs, True) + require(forward[0] == backward[0], "elimination order disagreed on " + str(masks)) + if forward[0] == "inconsistent": + inconsistent += 1 + continue + require(forward[0] == "family", "singular system was not discharged: " + str(forward)) + require(forward[1] == backward[1], "frozen frames depended on elimination order") + families += 1 + killed = False + for frame in forward[1]: + require(all(value.denominator == 1 for value in frame), "a frozen frame is not integral") + key = tuple(int(value) for value in frame) + frozen_seen[key] = frozen_seen.get(key, 0) + 1 + if not rank_one_nonzero(frame): + killed = True + require(killed, "a rank-4 family kept every frozen frame on the cone") + require(invertible == 71040, "invertible count changed: " + str(invertible)) + require(inconsistent == 44520, "inconsistent count changed: " + str(inconsistent)) + require(families == 720, "rank-4 family count changed: " + str(families)) + require(invertible + inconsistent + families == 116280, "the support domain was not fully counted") + require(set(frozen_seen) == BAD_FROZEN, "frozen frames changed: " + str(sorted(frozen_seen))) + for frame in BAD_FROZEN: + require(determinant(frame) in (Fraction(4), Fraction(-1)), "a named frozen frame is rank one") + require(frozen_seen[frame] == 120, "frozen frame " + str(frame) + " is not seen 120 times") + + +def hand_examples(): + rows, rhs = incidence(HAND_MASKS, TARGETS, TOTAL) + denominator, numerators = cramer(rows, rhs) + require(denominator == -2, "the worked incidence determinant is not -2") + frames = tuple(tuple(Fraction(numerators[column][coord], denominator) for coord in range(3)) for column in range(5)) + require(frames == HAND_FRAMES, "the worked five frames moved") + for frame in frames: + require(quad(frame) != 0, "the worked example met the rank-one cone") + singular_rows, singular_rhs = incidence(SINGULAR_MASKS, TARGETS, TOTAL) + require(det5(singular_rows) == 0, "the singular fixture is invertible") + # One explicit point on this affine line. The third frame vanishes only at + # this parameter value; the fifth frame is the frozen one. + point = ((2, 1, -1), (-1, -1, 2), (0, 0, 0), (1, 2, -1), (2, 2, 0)) + for row in range(5): + for coord in range(3): + got = sum(singular_rows[row][column] * point[column][coord] for column in range(5)) + require(got == singular_rhs[coord][row], "singular point misses an equation") + require(quad(point[4]) == 8, "twice det(2I) is not 8") + family = rref_family(singular_rows, singular_rhs, False) + require(family[0] == "family", "the singular fixture is not a rank-4 family") + require(family[1] == ((Fraction(2), Fraction(2), Fraction(0)),), "the singular fixture does not freeze 2I") + + +def positive_control(): + witness = tuple(coefficient(direction, scale) for direction, scale in zip(WITNESS_DIRECTIONS, WITNESS_SCALES)) + require(witness == tuple(tuple(Fraction(value) for value in frame) for frame in WITNESS_FRAMES), "witness frames moved") + require(add(witness) == tuple(Fraction(value) for value in TOTAL), "witness does not sum to 4I") + for frame in witness: + require(rank_one_nonzero(frame), "witness frame is not rank one") + fake_targets = [] + for mask in HAND_MASKS: + chosen = [witness[index] for index in range(5) if mask & (1 << index)] + fake_targets.append(add(chosen)) + rows, rhs = incidence(HAND_MASKS, fake_targets, add(witness)) + denominator, numerators = cramer(rows, rhs) + require(denominator != 0, "the positive-control incidence is singular") + recovered = tuple( + tuple(Fraction(numerators[column][coord], denominator) for coord in range(3)) for column in range(5) + ) + require(recovered == witness, "the solver did not recover the declared rank-one frames") + tampered = (fake_targets[0], fake_targets[1], fake_targets[2], add((fake_targets[3], (1, 0, 0)))) + tampered_rows, tampered_rhs = incidence(HAND_MASKS, tampered, add(witness)) + _, tampered_nums = cramer(tampered_rows, tampered_rhs) + tampered_frames = tuple( + tuple(Fraction(tampered_nums[column][coord], denominator) for coord in range(3)) for column in range(5) + ) + require(tampered_frames != witness, "tampered targets still recovered the witness") + + +def witness_parity(frames): + images = { + (0, 0): parity((0, 0, 0)), + (1, 0): parity(frames[1]), + (0, 1): parity(frames[3]), + (1, 1): parity(add((frames[1], frames[3]))), + } + require(images[(1, 0)] == (1, 0), "(0,1) at scale -1 does not have parity (1,0)") + require(images[(0, 1)] == (0, 1), "(1,1) at scale -1/2 does not have parity (0,1)") + require(images[(1, 1)] == (1, 1), "the sum of those two frames does not have parity (1,1)") + require(set(images.values()) == {(0, 0), (1, 0), (0, 1), (1, 1)}, "parity image is not full") + require(images[(1, 0)][0] == 1, "an AB shape would kill every frame") + require(images[(0, 1)][1] == 1, "a PQ shape would kill every frame") + + +def witness_character(frames): + detected_calls = sum(parity(frame)[1] for frame in frames) + detected_targets = sum(parity(tuple(Fraction(value) for value in target))[1] for target in TARGETS) + require(detected_calls == 2, "P-coefficient detects something other than two calls") + require(detected_targets == 4, "P-coefficient does not detect every target") + require(detected_calls < detected_targets, "witness is not a direct character obstruction") + + +def witness_support(frames): + rows = {tuple(Fraction(value) for value in target) for target in TARGETS} + hits = [] + for mask in range(1, 32): + chosen = [frames[index] for index in range(5) if mask & (1 << index)] + if add(chosen) in rows: + hits.append(mask) + require(hits == [], "witness subset sums hit a target: " + str(hits)) + + +def failure_controls(): + require(determinant((1, 1, 0)) == 1, "det I changed") + require(not rank_one_nonzero((1, 1, 0)), "I was accepted as rank one") + require(rank_one_nonzero((0, 0, 0)) is False, "the zero matrix was accepted") + broken = add((WITNESS_FRAMES[0], (1, 0, 0))) + require(quad(broken) != 0, "tampering the witness by A kept it rank one") + + +def main(): + target_identities() + hand_examples() + positive_control() + witness = tuple(coefficient(direction, scale) for direction, scale in zip(WITNESS_DIRECTIONS, WITNESS_SCALES)) + witness_parity(witness) + witness_character(witness) + witness_support(witness) + failure_controls() + support_census() + print("PASS five-signed-once-support checks") + + +if __name__ == "__main__": + main()