From 7f2d4b3e4eca3a79a3ee1a18963732678b505ed4 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 10 Nov 2026 02:08:52 +0000 Subject: [PATCH] Prove four once-each rank-one frames miss the four-call endpoint. The shortest equation using each new label once is R+S+T+U=4I. Target support fails for every rational rank-one solution, and one explicit solution has a full parity image. No kappa change. Co-authored-by: unpaidmoon --- research/four-signed-once-parity/PROOF.md | 146 ++++++++++++++ research/four-signed-once-parity/README.md | 48 +++++ research/four-signed-once-parity/SOURCES.json | 18 ++ research/four-signed-once-parity/TASK.json | 75 +++++++ research/four-signed-once-parity/VERIFY.json | 34 ++++ research/four-signed-once-parity/verify.py | 190 ++++++++++++++++++ 6 files changed, 511 insertions(+) create mode 100644 research/four-signed-once-parity/PROOF.md create mode 100644 research/four-signed-once-parity/README.md create mode 100644 research/four-signed-once-parity/SOURCES.json create mode 100644 research/four-signed-once-parity/TASK.json create mode 100644 research/four-signed-once-parity/VERIFY.json create mode 100644 research/four-signed-once-parity/verify.py diff --git a/research/four-signed-once-parity/PROOF.md b/research/four-signed-once-parity/PROOF.md new file mode 100644 index 0000000000..d5df86375c --- /dev/null +++ b/research/four-signed-once-parity/PROOF.md @@ -0,0 +1,146 @@ +# Four once-each rank-one frames do not meet the four-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 four new labels once each is + +``` +R + S + T + U = 4I. +``` + +It is the zero-old-call case: four paid calls and no call on `A`, `B`, `P`, or `Q`. Two statements are proved about it. + +1. **Support proof.** No choice of four nonzero symmetric rational rank-one matrices satisfies target support for this equation. The equation therefore admits no word. This does not lower the eight-call minimum, and it does not speak about five, six, or seven calls. +2. **Parity-image witness, not a census.** The same equation has an explicit rational solution whose integral span has full parity image `F2^2`. The three-frame route, "the image misses `(1,1)`, so an AB or PQ form kills every added frame," does not apply to every four-frame solution. That witness is still character-excluded by a direct count, and it is not a word. + +Selected κ stays `781451/250000000`. Nothing here is a multiplication theorem, a search failure presented as nonexistence, or a statement about five or more added frames. + +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. + +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)`. + +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 can carry a target + +**Lemma 1.** Let `F1,F2,F3,F4` be nonzero symmetric rational rank-one matrices with sum `4I`. A subset sum equal to a target has size exactly 2. + +**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 three-element subset sums to a target `H` only if the omitted frame equals `4I-H`. For every target, + +``` +det(4I-H) = 16 - 4·tr(H) + det(H) = 16 - 8 + 1/2 = 17/2 ≠ 0, +``` + +so `4I-H` is not rank one. The only remaining subsets are the pairs. + +## 3. The fifteen pair patterns + +There are six unordered pairs among four calls and `C(6,4) = 15` ways to choose four of them. Each target would have to be a different pair, because the four targets are distinct. `verify.py` enumerates all 15 graphs. Their sorted degree sequences are only + +``` +(2,2,2,2) three times, and (3,2,2,1) twelve times. +``` + +That enumeration is exhaustive for the pair patterns. It is not a search over directions or scales. + +**Theorem 2.** No four nonzero symmetric rational rank-one matrices summing to `4I` have all four targets as subset sums. + +**Proof.** By Lemma 1 every target is a pair sum, so some four-edge graph as above has its four edge sums equal to the four targets. The sum of those edge sums is therefore `4I`. + +If every degree is 2, the edge sum is twice the sum of the four frames, hence `2·4I = 8I`. Then `8I = 4I`, which is false. + +If the degrees are 3, 2, 2, and 1, label the degree-3 call `F` and the unique edge disjoint from `F` by `X+Y`. The fourth call is `Z`. The edge sum is + +``` +3F + 2X + 2Y + Z. +``` + +Subtracting the total sum `F+X+Y+Z = 4I` gives the matrix identity + +``` +2F + X + Y = 0. +``` + +The edge `X+Y` equals some target `H`, so `F = -H/2`. Then + +``` +det(F) = det(-H/2) = (1/4)·det(H) = 1/8 ≠ 0, +``` + +so `F` is not rank one. + +Both patterns contradict the rank-one hypothesis. Therefore target support fails for every solution of the equation, and the equation admits no word. + +The direct eight-call word, two old labels on each target, is untouched. Theorem 2 removes only the four-call equation. + +## 4. A full parity image + +**Witness.** The directions and scales + +``` +(0,1) at -3, (1,-1) at 5/2, (1,1) at 1/2, (1,2) at 1 +``` + +give the integral frames + +``` +R = (0,-3,0), S = (5,5,-5), T = (0,0,1), U = (-1,2,4). +``` + +Their sum is `(4,4,0)`. Each determinant is 0 and each vector is nonzero, so each frame is rank one. The integer combinations + +``` +R = (0,-3,0), S = (5,5,-5), S+U = (4,7,-1) +``` + +have parity images `(1,0)`, `(0,1)`, and `(1,1)`. The zero combination has image `(0,0)`. The parity image of the integral span is all of `F2^2`. + +In particular neither coordinate functional vanishes on that span. No integer form of shape `(odd,odd,even)` or `(even,even,odd)` is even on all four frames: the first shape reduces to `a+b` modulo 2, and `R` has `a+b` odd; the second reduces to `c` modulo 2, and `S` has `c` odd. 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. It is not an enumeration of all four-direction solutions, and a full parity image is not a word. + +## 5. The witness still fails a direct character count + +The same witness is excluded by the inherited call-versus-target inequality, without killing every frame. Reduce the coefficient of `P` modulo 2. All four targets have odd `P`-coefficient, so all four are detected. Among the frames, only `S` and `T` have odd `P`-coefficient, so two calls are detected. Two calls against four targets is forbidden. + +Theorem 2 already excludes the witness as a word. Section 5 records that evading the vanishing test is not the same as surviving every first-order character. The witness also fails support, as Theorem 2 requires: none of its fifteen nonempty subset sums equals a target. That fifteen-line check is a check of one solution, not the proof. + +## Open next questions + +Lengths 5, 6, and 7 with four added labels, and every decomposition with five or more added frames, are untouched. One extra old call changes both the residual and the allowed subset sizes, so Theorem 2 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/four-signed-once-parity/README.md b/research/four-signed-once-parity/README.md new file mode 100644 index 0000000000..31c6ba7c75 --- /dev/null +++ b/research/four-signed-once-parity/README.md @@ -0,0 +1,48 @@ +# Four once-each signed frames and the four-call equation + +**Support proof, plus one parity-image witness. No new κ and no word.** + +The shortest determinant equation that uses four new labels once each is `R+S+T+U = 4I`: four paid calls and no old call. In the PR2085/2112 model that equation admits no word. Every target would have to be a sum of two of the four rank-one frames, and all 15 ways of choosing four pairs contradict the rank-one hypothesis. The argument is written in [PROOF.md](PROOF.md). + +The same equation has one explicit rational solution 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 four-frame solution. The witness is still excluded by a direct character count (two calls against four targets) and by the support proof. It is one solution, not a census, and it is not a word. + +The selected record stays κ = `781451/250000000`. Lengths 5, 6, and 7, and five or more added frames, stay open. + +## 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 four-frame question left open by the all-old-once three-frame note, discussion comment 19493126, which itself follows comment 19377832. It does not redo that three-frame proof and it does not take another three-frame census profile. + +Evidence classes, kept apart: + +1. **Proof.** Lemma 1 and Theorem 2 exclude target support for every rational solution of `R+S+T+U = 4I` by four nonzero symmetric rank-one matrices. The 15 pair graphs are the entire case split. The determinant identities `det H = 1/2`, `det(4I-H) = 17/2`, and `det(-H/2) = 1/8` are checked exactly. +2. **Explicit witness, not a census.** Directions `(0,1)`, `(1,-1)`, `(1,1)`, `(1,2)` at scales `-3`, `5/2`, `1/2`, `1` sum to `4I`, and `R`, `S`, and `S+U` realize parity images `(1,0)`, `(0,1)`, and `(1,1)`. No AB or PQ form kills all four 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 fifteen nonempty subset sums miss every target; that list checks the witness and is not Theorem 2. + +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-once-parity --check-only +python3.12 scripts/research_package.py --package research/four-signed-once-parity +``` + +The direct check is `python3 -I -W error -B research/four-signed-once-parity/verify.py`. + +## Open next questions + +Can four added signed rank-one frames plus one, two, or three old calls meet support at length 5, 6, or 7? Theorem 2 uses exactly four calls. A useful first step is one old projector `E` and the equation `R+S+T+U = 4I-E`, then the same pair test on one rational solution. No such solution is supplied here. + +Can five or more added signed rank-one frames lower the eight-call minimum? The four-call support proof and the three-frame character both stop at the number of frames they assume. A useful first step is five primitive directions and the shortest determinant equation that uses each new label once. + +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 four 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 fork package `research/three-signed-old-once`, discussion comment 19493126, and is not redone here. The concrete handoff is discussion comment 19377832. + +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-once-parity/SOURCES.json b/research/four-signed-once-parity/SOURCES.json new file mode 100644 index 0000000000..594089b9c7 --- /dev/null +++ b/research/four-signed-once-parity/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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-once-parity/TASK.json b/research/four-signed-once-parity/TASK.json new file mode 100644 index 0000000000..a280085f07 --- /dev/null +++ b/research/four-signed-once-parity/TASK.json @@ -0,0 +1,75 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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 four-label equation R+S+T+U=4I, prove that target support fails for every nonzero symmetric rational rank-one solution, and exhibit one 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 four-frame question left open by the all-old-once three-frame character, for the single shortest once-each equation.", + "bottleneck_link": "Side result on the signed-frame escape. The four-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 four-call support proof and one explicit parity-image witness. Do not search lengths 5, 6, or 7, and do not start five or more frames.", + "outcome": "completed", + "evidence": "Support proof: every target has trace 2 and determinant 1/2, so only pair sums can match, and all 15 four-edge graphs give either 8I=4I or a frame equal to -H/2. Parity witness, not a census: directions (0,1),(1,-1),(1,1),(1,2) at scales -3,5/2,1/2,1 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 proof and verifier. No independent human or formal-kernel review.", + "open_questions": [ + { + "question": "Can four added signed rank-one frames plus one, two, or three old calls meet support at length 5, 6, or 7?", + "why_it_matters": "Theorem 2 excludes only the four-call equation. A word at length 7 would lower the eight-call minimum.", + "first_step": "Fix one old projector E and the equation R+S+T+U=4I-E, then repeat the pair test on one rational rank-one solution.", + "blocked_by": "The pair classification uses exactly four calls. One extra old call changes the residual and the allowed subset sizes." + }, + { + "question": "Can five or more added signed rank-one frames lower the eight-call minimum?", + "why_it_matters": "The four-call support proof and the three-frame character both stop at the number of frames they assume.", + "first_step": "Fix five primitive directions and the shortest determinant equation that uses each new label once, then repeat the parity-image test.", + "blocked_by": "No five-frame support or character reduction is supplied." + } + ], + "selection": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19377832", + "upstream_checked_utc": "2026-11-10T02:30:00Z", + "priority_revision": 8 + } +} diff --git a/research/four-signed-once-parity/VERIFY.json b/research/four-signed-once-parity/VERIFY.json new file mode 100644 index 0000000000..21ff0abd3c --- /dev/null +++ b/research/four-signed-once-parity/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Target determinant identities; exhaustive classification of all 15 four-edge pair graphs; one declared four-frame witness with full parity image, a two-call character count, and no target subset sum; failure controls for a tampered sum and for I as a rank-one summand." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same identities, graph census, witness, and failure controls under python -O." + } + ] +} diff --git a/research/four-signed-once-parity/verify.py b/research/four-signed-once-parity/verify.py new file mode 100644 index 0000000000..27c8abecf8 --- /dev/null +++ b/research/four-signed-once-parity/verify.py @@ -0,0 +1,190 @@ +#!/usr/bin/env python3 +"""Checks for the four-call signed-frame equation R+S+T+U = 4I. + +PROOF.md holds the argument. This program checks the determinant +identities, exhausts the 15 pair graphs, and checks one declared +parity-image witness. The graph list is the whole set of 4-edge +patterns on four calls. The witness is one solution, not a census. +""" + +from fractions import Fraction +from itertools import combinations + + +EDGES = ((0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)) + +WITNESS_DIRECTIONS = ((0, 1), (1, -1), (1, 1), (1, 2)) +WITNESS_SCALES = (Fraction(-3), Fraction(5, 2), Fraction(1, 2), Fraction(1)) + + +def require(condition, message): + if not condition: + raise SystemExit("FAIL: " + message) + + +def coefficient(direction, scale): + x, y = direction + return tuple(scale * value for value in (x * (x - y), y * (y - x), 2 * x * y)) + + +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 scale(frame, factor): + return tuple(factor * value for value in frame) + + +def rank_one_nonzero(frame): + return frame != (0, 0, 0) and determinant(frame) == 0 + + +def targets(): + a = (1, 0, 0) + b = (0, 1, 0) + p = (0, 0, 1) + q = (1, 1, -1) + return ( + add((a, p)), + add((a, q)), + add((b, p)), + add((b, q)), + ) + + +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 degrees(graph): + counts = [0, 0, 0, 0] + for i, j in graph: + counts[i] += 1 + counts[j] += 1 + return tuple(sorted(counts, reverse=True)) + + +def formal_edge_sum(graph): + total = [0, 0, 0, 0] + for i, j in graph: + total[i] += 1 + total[j] += 1 + return tuple(total) + + +def target_identities(): + rows = targets() + require(add(rows) == (4, 4, 0), "the four targets do not sum to 4I") + for row in rows: + require(trace(row) == 2, "a target trace is not 2") + require(determinant(row) == Fraction(1, 2), "a target determinant is not 1/2") + complement = add(((4, 4, 0), scale(row, -1))) + require(determinant(complement) == Fraction(17, 2), "det(4I-H) is not 17/2") + require(determinant(scale(row, Fraction(-1, 2))) == Fraction(1, 8), "det(-H/2) is not 1/8") + + +def pair_patterns(): + graphs = list(combinations(EDGES, 4)) + require(len(graphs) == 15, "pair patterns are not the 15 four-edge graphs") + seen = {} + for graph in graphs: + kind = degrees(graph) + seen[kind] = seen.get(kind, 0) + 1 + edge_sum = formal_edge_sum(graph) + if kind == (2, 2, 2, 2): + require(edge_sum == (2, 2, 2, 2), "a 2-regular edge sum is not twice the total") + elif kind == (3, 2, 2, 1): + counts = [0, 0, 0, 0] + for i, j in graph: + counts[i] += 1 + counts[j] += 1 + hub = counts.index(3) + leaf_edge = next(edge for edge in graph if hub not in edge) + difference = [edge_sum[i] - 1 for i in range(4)] + expected = [0, 0, 0, 0] + expected[hub] = 2 + expected[leaf_edge[0]] += 1 + expected[leaf_edge[1]] += 1 + require(tuple(difference) == tuple(expected), "leaf reduction failed for " + str(graph)) + else: + raise SystemExit("FAIL: unexpected degree sequence " + str(kind)) + require(seen == {(2, 2, 2, 2): 3, (3, 2, 2, 1): 12}, "degree census changed: " + str(seen)) + + +def witness_frames(): + frames = [ + coefficient(direction, scale) + for direction, scale in zip(WITNESS_DIRECTIONS, WITNESS_SCALES) + ] + require(add(frames) == (4, 4, 0), "witness does not sum to 4I") + for frame in frames: + require(rank_one_nonzero(frame), "witness frame is not rank one") + return tuple(frames) + + +def witness_parity(frames): + images = { + (0, 0): parity((0, 0, 0)), + (1, 0): parity(frames[0]), + (0, 1): parity(frames[1]), + (1, 1): parity(add((frames[1], frames[3]))), + } + require(images[(1, 0)] == (1, 0), "R does not have parity (1,0)") + require(images[(0, 1)] == (0, 1), "S does not have parity (0,1)") + require(images[(1, 1)] == (1, 1), "S+U does not have parity (1,1)") + require(set(images.values()) == {(0, 0), (1, 0), (0, 1), (1, 1)}, "parity image is not full") + # An AB form reduces to a+b mod 2, and a PQ form reduces to c mod 2. + require(images[(1, 0)][0] == 1, "AB shape would kill every frame") + require(images[(0, 1)][1] == 1, "PQ shape would kill every frame") + + +def witness_character(frames): + detected_calls = sum(parity(frame)[1] for frame in frames) + detected_targets = sum(parity(row)[1] for row 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 = set(targets()) + hits = [] + for mask in range(1, 16): + chosen = [frames[i] for i in range(4) if mask & (1 << i)] + if add(chosen) in rows: + hits.append(mask) + require(hits == [], "witness subset sums hit a target: " + str(hits)) + + +def failure_controls(frames): + broken = (frames[0], frames[1], frames[2], add((frames[3], (1, 0, 0)))) + require(add(broken) != (4, 4, 0), "tampered witness still sums to 4I") + # I has coefficient (1,1,0) and determinant 1, so it is not rank one. + require(determinant((1, 1, 0)) == 1, "det I changed") + require(not rank_one_nonzero((1, 1, 0)), "I was accepted as rank one") + require(rank_one_nonzero((0, 0, 0)) is False, "the zero matrix was accepted") + + +def main(): + target_identities() + pair_patterns() + frames = witness_frames() + witness_parity(frames) + witness_character(frames) + witness_support(frames) + failure_controls(frames) + print("PASS four-signed-once-parity checks") + + +if __name__ == "__main__": + main()