From 961b749fa40a1117d0746064528d2dfa290c57e0 Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 28 Oct 2026 04:28:00 -0400 Subject: [PATCH] Exclude seven-call words using two added positive rank-one BIT frames Answers open question 1 of handoff #6104 (and PR6089's two-frame question): determinant residual, exact target-support systems and exact-lattice / 2-local character rank eliminate every count profile with at most seven calls that uses both added frames. Stdlib verifier with an independent concrete-split route, eight-call positive controls and negative controls. Co-Authored-By: Claude Opus 5.5 --- .../README.md | 243 ++++++++++ .../SOURCES.json | 24 + .../TASK.json | 76 +++ .../VERIFY.json | 36 ++ .../verify.py | 434 ++++++++++++++++++ 5 files changed, 813 insertions(+) create mode 100644 research/bit-two-positive-frames-seven-call/README.md create mode 100644 research/bit-two-positive-frames-seven-call/SOURCES.json create mode 100644 research/bit-two-positive-frames-seven-call/TASK.json create mode 100644 research/bit-two-positive-frames-seven-call/VERIFY.json create mode 100644 research/bit-two-positive-frames-seven-call/verify.py diff --git a/research/bit-two-positive-frames-seven-call/README.md b/research/bit-two-positive-frames-seven-call/README.md new file mode 100644 index 0000000000..98eb6718d0 --- /dev/null +++ b/research/bit-two-positive-frames-seven-call/README.md @@ -0,0 +1,243 @@ +# Two added positive frames cannot give a seven-call word + +This package answers open question 1 of JoyboyBrian's +[handoff #6104](https://github.com/CrocSwap/integer-mult-bounds/discussions/6104), +which is also apoursh's two-frame question in +[PR #6089](https://github.com/CrocSwap/integer-mult-bounds/pull/6089). Add two +nonzero positive rational rank-one addresses `R` and `S` to the PR2085/2112 +four-target alphabet. Then **no exact word of at most seven calls uses both +of them**. This holds for every direction and scale of `R` and `S`, every +finite restored dirty width and any free binary mixing. + +The proof uses only necessary conditions: the determinant identity, the four +target-support systems, and first-order character rank on the exact address +lattice. It needs no word census. A stdlib verifier enumerates every count +profile, settles the pinned splits exactly, and checks the uniform lemma for +the seven continuous families on a direction grid. No new κ, supplier or +native saving is claimed. + +## Model + +As in PR6089 and the handoff, put + +```text +A = [[1,0],[0,0]] B = [[0,0],[0,1]] +P = (1/2)[[1,1],[1,1]] Q = (1/2)[[1,-1],[-1,1]] (A+B = P+Q = I) +``` + +Let `R`, `S` be nonzero positive semidefinite rational symmetric rank-one +matrices. They may coincide with each other or with an old address. Let +`Lambda = ZA + ZB + ZP + ZR + ZS`, which has rank three. Work in +`F2[Lambda]`. A paid call is `I_w + ([F]-1)N` with `F in {A,B,P,Q,R,S}` and +`N` a binary rank-one idempotent on any finite width `w >= 4`. Free +address-independent `GL_w(F2)` maps cost nothing. The endpoint is + +```text +T_w = diag([A+P], [A+Q], [B+P], [B+Q], 1, ..., 1) +``` + +with every extra role restored. Write `a,b,p,q,r,s` for the label counts. The +question requires `r, s >= 1` and `a+b+p+q+r+s <= 7`, so `n = a+b+p+q <= 5`. + +## Theorem + +For every finite `w >= 4` and every such `R, S`, no exact word with at most +seven paid calls has `r >= 1` and `s >= 1`. + +Combined with PR6089's single-frame theorem (an `R`-using word has at least +`m+7 >= 8` calls) and the known eight-call floor for `{A,B,P,Q}`, this means +no word with at most two added positive frames beats eight calls. That +combined statement inherits PR6089's review status. PR6089 is pending and is +not re-verified here. + +## Proof + +**Step 1 (determinant; Nick Petalas, PR2910).** `det(I+([F]-1)xy^T) = [F]`, +free maps have determinant 1, and `det T_w = [4I]`. So + +```text +rR + sS = M := 4I - aA - bB - pP - qQ. +``` + +Since `R` and `S` are positive and nonzero, `M` is positive semidefinite and +nonzero. Write `X = rR`, so that `S = (M-X)/s`. Both `X` and `M-X` must be +positive rank one. Of the profiles with `r,s >= 1` and `n+r+s <= 7`, 442 have +positive semidefinite nonzero `M`. + +**Step 2 (support).** Conjugate the free maps to the end. By augmentation the +last free map is the identity (PR6089 §1). Expand each factor as +`(I+N) + [F]N`. The coefficient of `[H]` in a diagonal entry is a sum over +subsets of calls whose labels sum to `H`. So for each target exponent +`H_j`, there are integers `0 <= u_F <= count(F)` with +`sum_F u_F F = H_j`. With `alpha = u_R/r - u_S/s` and `beta = u_S/s`, this +reads + +```text +alpha X = H_j - (u_A A + u_B B + u_P P + u_Q Q) - beta M =: K. +``` + +There are two cases: + +- If `alpha = 0`, the solution holds for every split exactly when `K = 0`. + Call that solution *free*. +- If `alpha != 0`, it forces `X = K/alpha`. This counts only when `X` and + `M-X` are positive rank one. + +A target with no free solution confines `X` to a finite set. Exactly seven +profiles have a free solution for all four targets: +`(1,1,1,1,1,1)`, `(1,1,1,1,1,2)`, `(1,1,1,1,2,1)`, `(2,1,1,1,1,1)`, +`(1,2,1,1,1,1)`, `(1,1,2,1,1,1)` and `(1,1,1,2,1,1)`. All seven use the +old-only support, which is unique: for `A+P` it is `u_A = u_P = 1` and the +rest zero, and similarly for the other targets. The enumeration finds no +balanced free support (`alpha = 0`, `beta > 0`) at seven calls. In every other +profile, the four finite sets intersect in 32 splits in total. Every one of +them has `R` and `S` proportional to old addresses, for example +`(0,1,1,1,1,3)` with `R = 2B` and `S = A`. + +**Step 3 (characters; method from PR6089 and the handoff).** An additive +`chi: Lambda -> F2` induces the ring map `[F] -> 1 + chi(F) eps` into +`F2[eps]/(eps^2)`. Exactness gives +`sum_{i: chi(F_i)=1} N_i = diag(chi(H_1),...,chi(H_4),0,...)`. Hence the +number of detected calls is at least the number of targets with +`chi(H_j) = 1`. For each of the 32 pinned splits, the verifier computes an +integer basis of the actual `Lambda` and tests all eight characters. Each +split fails for some character, with 2 detected calls against 4 targets. + +**Step 4 (the seven continuous families).** Let +`L = Z_(2)A + Z_(2)B + Z_(2)P`, the old lattice with odd denominators +allowed. Its coordinates are `(alpha, beta, gamma) = (m11-m12, m22-m12, 2m12)`. +If `R, S` lie in `L`, then two functionals restrict to characters of +`Lambda`: + +```text +chi_PQ = gamma mod 2 (A,B -> 0; P,Q -> 1; all four targets -> 1) +chi_AB = alpha+beta mod 2 (A,B -> 1; P,Q -> 0; all four targets -> 1) +``` + +If such a character also kills `R` and `S`, it detects exactly two calls in +every family (`p+q = 2` or `a+b = 2` respectively) against four targets. That +is a contradiction. Write the split direction as a primitive integer vector +`(x,y)` and `pi = (x^2, y^2, xy)/h` with `h = x^2+y^2`. + +- *`M = 2I`: profiles `(1,1,1,1,r,s)`, `(r,s)` in `{(1,1),(1,2),(2,1)}`.* + Here `det(2I - t vv^T) = 0` forces `X = 2 pi_u` and `M - X = 2 pi_{u⊥}`. + So `{R,S}` is `{2pi_u, 2pi_{u⊥}}`, `{2pi_u, pi_{u⊥}}` or `{pi_u, 2pi_{u⊥}}`. + - If `x` and `y` have opposite parity, `h` is odd. Then `pi_u` and `pi_{u⊥}` + have 2-integral entries and lie in `L`. Their `gamma = ±2xy/h` is even, so + `chi_PQ` kills all four matrices. + - If `x` and `y` are both odd, then `h = 2k` with `k` odd. Now + `2pi_u = (x^2,y^2,xy)/k` lies in `L` with `alpha+beta = (x-y)^2/k`, which + is divisible by 4. Also `pi_{u⊥} = (y^2,x^2,-xy)/(2k)` has + `alpha = y(y+x)/(2k)`, `beta = x(x+y)/(2k)` and `gamma = -xy/k`, so it + lies in `L` with `alpha+beta = (x+y)^2/(2k)`, which is even. The + `u <-> u⊥` swap covers the remaining two matrices. So `chi_AB` kills them. + + This extends the handoff's `M = 2I` argument to `r` or `s` equal to 2, where + `R` or `S` is no longer in `2L`. +- *`M = diag(1,2)`: profile `(2,1,1,1,1,1)`.* The matrix determinant lemma + forces `X = 2uu^T/(2x^2+y^2)`, with `R = X` and `S = M - X`. + - If `y` is odd, the denominator is odd, `X` lies in `L`, and + `gamma = 4xy/(2x^2+y^2)` is even. + - If `y = 2y1`, then `x` is odd and `X = (x^2, 4y1^2, 2xy1)/k` with `k` + odd. So `X` lies in `L` and `gamma = 4xy1/k` is even. + + Since `M = A + 2B` has `chi_PQ(M) = 0`, `chi_PQ` kills `R` and `S`. +- *The other three doubled profiles.* They are images of `(2,1,1,1,1,1)` under + PR6089 §3's symmetries. Conjugation by `J` fixes `chi_PQ`. Conjugation by + `H` permutes `A,B,P,Q`, preserves `L`, and exchanges `chi_PQ` with + `chi_AB`. So `(1,2,1,1,1,1)` uses `chi_PQ`, and `(1,1,2,1,1,1)` and + `(1,1,1,2,1,1)` use `chi_AB`. The verifier checks all four doubled + profiles directly, without using the symmetry. + +Every profile is now excluded. QED + +## Evidence + +`verify.py` uses only the stdlib and exact `Fraction` arithmetic. It imports +no repository module or predecessor executable. It checks the following: + +- the live source hash; +- all 442 positive semidefinite residual profiles of length at most seven; +- the support classification: exactly the seven free families and 32 pinned + splits; +- an exact-lattice integer basis and all eight characters for every pinned + split; +- for each free family and every primitive direction with + `|x|, y <= 30`, 7,784 cases in all: + - the parameterization; + - membership in `L`; + - the lemma's character kills `R` and `S`, with 2 detected calls against 4 + targets; + - an independent exact-lattice check that agrees. + +These grid cases are regression checks; the uniform claim rests on Step 4. + +As an independent route that bypasses the `alpha`/`K` classification, the +verifier also picks 46,916 concrete splits over all 442 profiles. It uses +primitive directions up to height 8 for definite `M` and rational scales +`k/m`, `m <= 40`, for rank-one `M`. It tests literal subset sums for all four +targets: 648 pass, and the exact-lattice characters kill every one of them. +The verifier also runs these controls: + +- *Positive control.* At eight calls, real words survive every filter: 77 + survivors, including `R = S = A` at `(0,2,2,2,1,1)` and the free + `(1,1,2,2,1,1)`. One literal eight-call word, with `R = A` and `S = B` + relabelled, is multiplied out in `F2[Lambda]` and equals the endpoint. +- *Negative controls.* Without the support step, 28 seven-call profiles + survive the characters at the split `u = (1,0)`. Naive mod-2 reduction of + `1/2` is rejected. A mutated target changes the free-family list. + +Runtime is about 30 s per command. + +## Reproduce + +```sh +python3.12 -I -W error -B research/bit-two-positive-frames-seven-call/verify.py +python3.12 -I -O -W error -B research/bit-two-positive-frames-seven-call/verify.py +``` + +## Limits + +- This is a formal-model lower bound. It provides no native operation, + tariff, supplier or κ change, and makes no all-field claim. +- Only at most two added positive rank-one frames are covered. Three or more + frames, negative or indefinite frames, and higher-rank added addresses are + not covered. +- The combined "nothing beats eight" corollary depends on the pending PR6089 + and is not independently re-verified here. +- The grid checks are regression evidence, not the proof of Step 4. + +## Open next questions + +1. **Three or more added positive frames.** With `k` frames, the residual + becomes a `k`-term positive rank-one decomposition of `M`. That gives + `k-1` continuous parameters. Relevance: this would close the "more + positive frames" route for this endpoint at seven calls. First step: + repeat Step 2 with `alpha` replaced by a linear form in the `k` split + matrices. Check whether the free families still need + `a, b, p, q >= 1`, which leaves at most `7-4 = 3` added calls. Blocker: + the 2-local membership of a general decomposition is not automatic. +2. **Eight-call words using two frames.** The eight-call survivors include + new non-duplicate candidates, for example `(1,3,0,1,1,2)` with `R = 2A` + and `S = P/2`. Decide which are realizable, as in PR6089's `{m+7, 2m+6}` + spectrum. Relevance: this is the complete length spectrum, not a cheaper + word. First step: try subdivision words. +3. **Non-positive added frames.** The positivity of `M` is what makes the + finite residual list. Indefinite rank-one frames remove it. A different + bound on the residual is needed first. + +## Credit + +- JoyboyBrian (#6104): the two-frame question, the residual + parameterization, and the `M = 2I`, `r = s = 1` character argument + extended here. +- apoursh (PR6089): the one-frame classification, the reduction to paid-only + words, and the symmetries. +- Nick Petalas (PR2910): the determinant method. +- Cinna Davis (PR2085/2112): the model and endpoint. +- Philippe Van Velzen: the eight-call floor. +- The retained BIT lineage credited in those sources. + +New material prepared for JosieElliston by Claude Opus 5.5 via Claude Code, +Apache-2.0. Substantial AI assistance. There is no human or proof-kernel +acceptance. diff --git a/research/bit-two-positive-frames-seven-call/SOURCES.json b/research/bit-two-positive-frames-seven-call/SOURCES.json new file mode 100644 index 0000000000..71e4b3eede --- /dev/null +++ b/research/bit-two-positive-frames-seven-call/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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" + }, + { + "path": "research/bit-fifth-frame-determinant-obstruction/README.md", + "usage": "input", + "git_blob": "608a24af8bc3d27ee1554c94872601bb3a409f67", + "sha256": "fa3f0f951146caa5b1eb7b7417175eb7a380cae8674e4a470407517dac40f227" + } + ] +} diff --git a/research/bit-two-positive-frames-seven-call/TASK.json b/research/bit-two-positive-frames-seven-call/TASK.json new file mode 100644 index 0000000000..d23c0fd914 --- /dev/null +++ b/research/bit-two-positive-frames-seven-call/TASK.json @@ -0,0 +1,76 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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": "In the PR2085/2112 four-target formal register model extended by two nonzero positive rational rank-one added addresses R,S (any direction and scale, possibly coinciding), prove that no exact word of at most seven paid calls uses both R and S, for every finite restored dirty width and free binary mixing.", + "scope_change_reason": "Took the open handoff #6104 question 1 (JoyboyBrian), which is also PR6089's two-frame open question, instead of the card's native larger/nonabelian construction. This is a formal alphabet lower bound on the same endpoint.", + "bottleneck_link": "Scoped side result: adding up to two positive rank-one frames cannot produce a cheaper (fewer than eight call) primitive for this endpoint; such extensions are not a route to a BIT saving here.", + "budget_minutes": 60, + "stop_rule": "Stop at a complete necessary-condition elimination of every count profile with an exact verifier, or at the first surviving profile (reported as the remaining obligation). No word census.", + "outcome": "completed", + "evidence": "README.md proof: determinant residual (442 psd profiles), exact support systems (7 free families with old-only supports, 32 pinned splits, all on old directions), exact-lattice character rank kills all pinned splits, uniform 2-local chi_PQ/chi_AB lemma kills the seven free families. verify.py (stdlib, ~5 s) checks all finite steps, 7784 grid regression cases for the free families against both the lemma and the exact lattice a direct-subset-sum regression over 46916 concrete splits of all 442 profiles (648 support survivors, all killed by exact-lattice characters), an eight-call positive control (77 survivors incl. literal word multiplied out) and negative controls.", + "author": "Josie Elliston (Claude Opus 5.5 via Claude Code)", + "ai_assistance": "Proof, verifier and package prepared by Claude Opus 5.5 via Claude Code for JosieElliston; an independent read-only OpenAI Codex adversarial review was requested. No human or proof-kernel acceptance.", + "open_questions": [ + { + "question": "Do three or more added positive rank-one frames allow a word of at most seven calls?", + "why_it_matters": "Closes the positive-frame extension route for this endpoint at seven calls.", + "first_step": "Repeat the support classification with the split replaced by a k-term positive rank-one decomposition of M; check whether free families still force a,b,p,q>=1.", + "blocked_by": "2-local membership of a general multi-term decomposition is not automatic." + }, + { + "question": "Which eight-call two-frame survivors (for example (1,3,0,1,1,2) with R=2A, S=P/2) are realizable?", + "why_it_matters": "Gives the complete two-frame length spectrum, as PR6089 did for one frame; not a cheaper word.", + "first_step": "Try subdivision words for each of the 77 eight-call survivors.", + "blocked_by": "None known." + }, + { + "question": "Do indefinite added rank-one frames escape the eight-call floor?", + "why_it_matters": "Positivity of the residual is what makes the profile list finite here.", + "first_step": "Find a substitute bound on the residual counts without positivity.", + "blocked_by": "No finite residual list without positivity." + } + ] +} diff --git a/research/bit-two-positive-frames-seven-call/VERIFY.json b/research/bit-two-positive-frames-seven-call/VERIFY.json new file mode 100644 index 0000000000..f9be4bdcac --- /dev/null +++ b/research/bit-two-positive-frames-seven-call/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-fifth-frame-determinant-obstruction/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source hash; all 442 psd determinant profiles of length <=7; exact support classification (7 free, 32 pinned); exact-lattice characters on pinned splits; 2-local lemma and exact lattice on 7784 free-family grid cases (regression); eight-call positive controls incl. a literal word; negative controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source hash; all 442 psd determinant profiles of length <=7; exact support classification (7 free, 32 pinned); exact-lattice characters on pinned splits; 2-local lemma and exact lattice on 7784 free-family grid cases (regression); eight-call positive controls incl. a literal word; negative controls." + } + ] +} diff --git a/research/bit-two-positive-frames-seven-call/verify.py b/research/bit-two-positive-frames-seven-call/verify.py new file mode 100644 index 0000000000..9603a845bd --- /dev/null +++ b/research/bit-two-positive-frames-seven-call/verify.py @@ -0,0 +1,434 @@ +#!/usr/bin/env python3 +"""Two added positive rank-one BIT frames cannot shorten the PR2085 endpoint. + +Stdlib only, exact rationals, no repository imports. Checks, for every count +profile with at most seven calls that uses both added labels R and S: + +1. the determinant residual M = rR + sS (PR2910 method); +2. the four exact target-support systems, which either pin the split X = rR + or hold for every split ("free" family); +3. for every pinned split, the character rank inequality on the exact integer + lattice generated by A, B, P, R, S (all eight F2 characters); +4. for the seven free families, the written uniform 2-local character lemma, + evaluated on every primitive direction in a bounded grid, plus the exact + lattice check on the same grid (regression only; the proof is README.md); + +and positive/negative controls: at eight calls genuine words survive every +filter (one is multiplied out in the formal group algebra), and dropping the +support filter leaves seven-call survivors. + +Josie Elliston, with Claude Opus 5.5 (Claude Code). Apache-2.0. +""" +from fractions import Fraction as Fr +from itertools import product +from math import gcd, lcm +import hashlib +import json +import pathlib +import sys + +PKG = pathlib.Path(__file__).resolve().parent +ROOT = PKG.parent.parent + +H = Fr(1, 2) +# symmetric 2x2 rational matrices as (m11, m22, m12) +A = (Fr(1), Fr(0), Fr(0)) +B = (Fr(0), Fr(1), Fr(0)) +P = (H, H, H) +Q = (H, H, -H) +I2 = (Fr(1), Fr(1), Fr(0)) +OLD = (A, B, P, Q) +NAMES = ("A", "B", "P", "Q", "R", "S") +TARGETS = tuple(tuple(x + y for x, y in zip(F, G)) + for F, G in ((A, P), (A, Q), (B, P), (B, Q))) + + +def add(*vs): + return tuple(sum(c, Fr(0)) for c in zip(*vs)) + + +def sc(k, v): + return tuple(k * x for x in v) + + +def det(v): + return v[0] * v[1] - v[2] * v[2] + + +def tr(v): + return v[0] + v[1] + + +def psd_rank1(v): + """Nonzero positive semidefinite rank-one symmetric matrix.""" + return det(v) == 0 and tr(v) > 0 + + +def residual(cnt): + a, b, p, q = cnt[:4] + return add(sc(4, I2), sc(-a, A), sc(-b, B), sc(-p, P), sc(-q, Q)) + + +def profiles(max_len): + out = [] + for a, b, p, q in product(range(max_len + 1), repeat=4): + n = a + b + p + q + for r in range(1, max_len - n): + for s in range(1, max_len - n - r + 1): + M = residual((a, b, p, q)) + # rR + sS = M with R, S nonzero psd forces M psd, nonzero + if tr(M) > 0 and det(M) >= 0: + out.append(((a, b, p, q, r, s), M)) + return out + + +def support(cnt, M): + """For each target: 'ALL' (a support solution valid for every split) or + the finite set of splits X = rR that some support solution forces.""" + r, s = cnt[4], cnt[5] + res = [] + for Ht in TARGETS: + free, pinned = False, set() + for u in product(*(range(c + 1) for c in cnt)): + old = add(*(sc(u[i], OLD[i]) for i in range(4))) + # u_R R + u_S S = alpha X + beta M with X = rR, S = (M - X)/s + alpha = Fr(u[4], r) - Fr(u[5], s) + beta = Fr(u[5], s) + K = add(Ht, sc(-1, old), sc(-beta, M)) + if alpha == 0: + if all(x == 0 for x in K): + free = True + else: + X = sc(1 / alpha, K) + if psd_rank1(X) and psd_rank1(add(M, sc(-1, X))): + pinned.add(X) + res.append("ALL" if free else pinned) + return res + + +# ---- exact lattice and its eight F2 characters ------------------------- + +def zbasis(vecs): + D = 1 + for v in vecs: + for x in v: + D = lcm(D, x.denominator) + rows = [[int(x * D) for x in v] for v in vecs if any(v)] + basis = [] + for col in range(3): + piv = [r for r in rows if r[col] != 0] + rest = [r for r in rows if r[col] == 0] + while len(piv) > 1: + piv.sort(key=lambda r: abs(r[col])) + p0, new = piv[0], [piv[0]] + for r in piv[1:]: + k = r[col] // p0[col] + rr = [x - k * y for x, y in zip(r, p0)] + (new if rr[col] != 0 else rest).append(rr) + piv = new + if piv: + basis.append(piv[0]) + rows = [r for r in rest if any(r)] + if rows: + raise SystemExit("FAIL: lattice reduction left a residue") + return [tuple(Fr(x, D) for x in b) for b in basis] + + +def coords(v, basis): + v = list(v) + out = [] + for b in basis: + col = next(i for i in range(3) if b[i] != 0) + k = v[col] / b[col] + if k.denominator != 1: + raise SystemExit("FAIL: element outside lattice") + out.append(int(k)) + v = [x - k * y for x, y in zip(v, b)] + if any(v): + raise SystemExit("FAIL: element outside lattice span") + return out + + +def lattice_killers(cnt, R, S): + """Characters chi of Lambda=Z with #detected calls < rank of + the target's first-order image; returned as values on (A,B,P,Q,R,S).""" + labels = OLD + (R, S) + basis = zbasis(labels) + if len(basis) != 3: + raise SystemExit("FAIL: lattice rank is not three") + lc = [coords(F, basis) for F in labels] + tc = [coords(Ht, basis) for Ht in TARGETS] + out = [] + for chi in product(range(2), repeat=3): + ev = lambda c: sum(x * y for x, y in zip(c, chi)) % 2 # noqa: E731 + detected = sum(cnt[i] * ev(lc[i]) for i in range(6)) + rank = sum(ev(c) for c in tc) + if detected < rank: + out.append(tuple(ev(c) for c in lc)) + return out + + +# ---- 2-local characters of the old lattice ------------------------------ + +def odd_den(x): + return x.denominator % 2 == 1 + + +def l2_coords(v): + """Coordinates in the basis (A, B, P): v = alpha A + beta B + gamma P.""" + gamma = 2 * v[2] + return (v[0] - v[2], v[1] - v[2], gamma) + + +def in_L2(v): + return all(odd_den(c) for c in l2_coords(v)) + + +def mod2(x): + if not odd_den(x): + raise SystemExit("FAIL: reduction of a non-2-integral value") + return (x.numerator * x.denominator) % 2 + + +def chi_PQ(v): # A,B -> 0, P,Q -> 1 : twice the off-diagonal entry + return mod2(l2_coords(v)[2]) + + +def chi_AB(v): # A,B -> 1, P,Q -> 0 + al, be, _ = l2_coords(v) + return mod2(al + be) + + +def first_order_rank(chi, cnt, labels): + detected = sum(cnt[i] * chi(labels[i]) for i in range(6)) + rank = sum(chi(Ht) for Ht in TARGETS) + return detected, rank + + +def split_from_direction(M, x, y): + """The unique positive rank-one X on direction (x,y) with M-X rank one.""" + x, y = Fr(x), Fr(y) + d = det(M) + Minv = (M[1] / d, M[0] / d, -M[2] / d) + den = Minv[0] * x * x + Minv[1] * y * y + 2 * Minv[2] * x * y + return (x * x / den, y * y / den, x * y / den) + + +def sha256(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def main(): + global TARGETS + checks = [] + + # --- source pins (live inputs only) --- + src = json.loads((PKG / "SOURCES.json").read_text()) + for row in src["files"]: + if row["usage"] == "input": + if sha256(ROOT / row["path"]) != row["sha256"]: + raise SystemExit("FAIL: source hash " + row["path"]) + checks.append("source hashes") + + # --- 1-2. determinant residuals and support systems, length <= 7 --- + profs = profiles(7) + free, pinned = [], [] + for cnt, M in profs: + sup = support(cnt, M) + fin = [x for x in sup if x != "ALL"] + if not fin: + free.append((cnt, M)) + continue + for X in sorted(set.intersection(*fin)): + pinned.append((cnt, M, X)) + expected_free = sorted([(1, 1, 1, 1, 1, 1), (1, 1, 1, 1, 1, 2), + (1, 1, 1, 1, 2, 1), (2, 1, 1, 1, 1, 1), + (1, 2, 1, 1, 1, 1), (1, 1, 2, 1, 1, 1), + (1, 1, 1, 2, 1, 1)]) + if sorted(c for c, _ in free) != expected_free: + raise SystemExit("FAIL: free families %r" % (free,)) + if len(profs) != 442 or len(pinned) != 32: + raise SystemExit("FAIL: counts %d profiles, %d pinned" % (len(profs), len(pinned))) + balanced = 0 + for cnt, M in profs: + for Ht in TARGETS: + for u in product(*(range(c + 1) for c in cnt)): + if u[5] and Fr(u[4], cnt[4]) == Fr(u[5], cnt[5]): + old = add(*(sc(u[i], OLD[i]) for i in range(4))) + if add(Ht, sc(-1, old), sc(-Fr(u[5], cnt[5]), M)) == (0, 0, 0): + balanced += 1 + if balanced: + raise SystemExit("FAIL: balanced free support exists") + checks.append("442 psd residual profiles; 7 free families (old-only supports; " + "no balanced R,S support); 32 pinned splits") + + # --- 3. exact-lattice character rank on every pinned split --- + for cnt, M, X in pinned: + R = sc(Fr(1, cnt[4]), X) + S = sc(Fr(1, cnt[5]), add(M, sc(-1, X))) + if not (psd_rank1(R) and psd_rank1(S)): + raise SystemExit("FAIL: pinned split not positive rank one") + if not lattice_killers(cnt, R, S): + raise SystemExit("FAIL: pinned split survives %r" % (cnt,)) + for Z in (R, S): + if not any(Fr(Z[0]) * F[1] == Fr(Z[1]) * F[0] and Z[0] * F[2] == Z[2] * F[0] + and Z[1] * F[2] == Z[2] * F[1] for F in OLD): + raise SystemExit("FAIL: pinned frame off the old directions") + checks.append("all 32 pinned splits lie on old directions and fail an " + "exact-lattice character rank") + + # --- 4. free families: uniform 2-local lemma on a direction grid --- + grid = 30 + ndirs = 0 + for cnt, M in free: + r, s = cnt[4], cnt[5] + for x in range(-grid, grid + 1): + for y in range(0, grid + 1): + if gcd(x, y) != 1 or (y == 0 and x != 1): + continue + X = split_from_direction(M, x, y) + R, S = sc(Fr(1, r), X), sc(Fr(1, s), add(M, sc(-1, X))) + if not (psd_rank1(R) and psd_rank1(S) and det(add(M, sc(-1, X))) == 0): + raise SystemExit("FAIL: parameterization") + labels = OLD + (R, S) + if not (in_L2(R) and in_L2(S)): + raise SystemExit("FAIL: split outside L_(2)") + # written lemma: chi_PQ unless M = 2I and x, y both odd + use_AB = (M == add(I2, I2)) and x % 2 == 1 and y % 2 == 1 + chi = chi_AB if use_AB else chi_PQ + if cnt[:4] != (1, 1, 1, 1) and cnt[:4] != (2, 1, 1, 1) \ + and cnt[:4] not in ((1, 2, 1, 1), (1, 1, 2, 1), (1, 1, 1, 2)): + raise SystemExit("FAIL: unexpected family") + if cnt[:4] in ((1, 1, 2, 1), (1, 1, 1, 2)): + # H-conjugate images of the A-doubled family: chi_AB + chi = chi_AB + if chi(R) or chi(S): + raise SystemExit("FAIL: lemma character detects R or S %r %r" % (cnt, (x, y))) + det_, rk = first_order_rank(chi, cnt, labels) + if not (det_ == 2 and rk == 4): + raise SystemExit("FAIL: lemma rank %r" % ((cnt, x, y, det_, rk),)) + if not lattice_killers(cnt, R, S): + raise SystemExit("FAIL: exact lattice disagrees %r" % ((cnt, x, y),)) + ndirs += 1 + checks.append("free families: %d (family, direction) cases match the 2-local lemma " + "and the exact lattice (regression; proof in README)" % ndirs) + + # --- 4b. independent route: concrete splits, direct subset sums --- + tested, sup_pass = direct_support_regression(profs) + checks.append("direct route: %d concrete splits over all 442 profiles, %d pass " + "literal subset-sum support, none passes the exact lattice " + "(regression)" % (tested, sup_pass)) + + # --- 5a. positive control: eight calls, genuine words survive --- + surv8 = [] + for cnt, M in profiles(8): + if sum(cnt) != 8: + continue + sup = support(cnt, M) + fin = [x for x in sup if x != "ALL"] + if not fin: + surv8.append((cnt, "free")) + continue + for X in set.intersection(*fin): + R = sc(Fr(1, cnt[4]), X) + S = sc(Fr(1, cnt[5]), add(M, sc(-1, X))) + if not lattice_killers(cnt, R, S): + surv8.append((cnt, R, S)) + if ((0, 2, 2, 2, 1, 1), A, A) not in surv8 or ((1, 1, 2, 2, 1, 1), "free") not in surv8: + raise SystemExit("FAIL: positive control filtered out") + if not word_control(): + raise SystemExit("FAIL: literal eight-call word") + checks.append("eight-call controls survive (%d survivors); literal word with R=A,S=B " + "equals the endpoint" % len(surv8)) + + # --- 5b. negative controls --- + # without support, characters alone leave a seven-call survivor + loose = 0 + for cnt, M in profs: + if det(M) == 0: + continue + X = split_from_direction(M, 1, 0) + R, S = sc(Fr(1, cnt[4]), X), sc(Fr(1, cnt[5]), add(M, sc(-1, X))) + if not lattice_killers(cnt, R, S): + loose += 1 + if loose == 0: + raise SystemExit("FAIL: support filter was not needed") + # naive mod-2 reduction of P's off-diagonal 1/2 is not a character value + try: + mod2(H) + raise SystemExit("FAIL: naive reduction accepted") + except SystemExit as e: + if "naive" in str(e): + raise + # a mutated target (A+P -> 2A) changes the free-family list + saved = TARGETS + TARGETS = (add(A, A),) + saved[1:] + mut = [c for c, M in profs if all(x == "ALL" for x in support(c, M))] + TARGETS = saved + if sorted(mut) == expected_free: + raise SystemExit("FAIL: target mutation undetected") + checks.append("negative controls: %d seven-call profiles survive characters " + "without support; naive reduction rejected; target mutant detected" % loose) + + for c in checks: + print("ok:", c) + print("PASS: no exact word of at most seven calls uses two positive rank-one frames") + + +# ---- independent concrete-split regression -------------------------------- + +def direct_support_regression(profs, grid=8): + """Does not use the alpha/K classification: picks concrete splits + (primitive directions for definite M, rational scales for rank-one M), + tests literal subset sums of the labels for all four targets, then the + exact-lattice characters.""" + tested = sup_pass = 0 + for cnt, M in profs: + r, s = cnt[4], cnt[5] + if det(M) > 0: + Xs = [split_from_direction(M, x, y) + for x in range(-grid, grid + 1) for y in range(0, grid + 1) + if gcd(x, y) == 1 and not (y == 0 and x != 1)] + else: + Xs = sorted({sc(Fr(k, m), M) for m in range(2, 41) for k in range(1, m)}) + for X in Xs: + R = sc(Fr(1, r), X) + S = sc(Fr(1, s), add(M, sc(-1, X))) + if not (psd_rank1(R) and psd_rank1(S)): + raise SystemExit("FAIL: concrete split") + tested += 1 + labels = OLD + (R, S) + sums = {add(*(sc(u[i], labels[i]) for i in range(6))) + for u in product(*(range(c + 1) for c in cnt))} + if all(Ht in sums for Ht in TARGETS): + sup_pass += 1 + if not lattice_killers(cnt, R, S): + raise SystemExit("FAIL: concrete survivor %r" % ((cnt, R, S),)) + return tested, sup_pass + + +# ---- literal formal group-algebra word (positive control) --------------- + +def word_control(): + """Eight diagonal calls with R=A and S=B relabelled; multiply out.""" + def call(F, j): + # I + ([F]-1) e_j e_j^T : diagonal, entry j is [F] + return j, F + word = [("R", 0), ("P", 0), ("A", 1), ("Q", 1), ("S", 2), ("P", 2), ("B", 3), ("Q", 3)] + lab = {"A": A, "B": B, "P": P, "Q": Q, "R": A, "S": B} + diag = [{(Fr(0), Fr(0), Fr(0)): 1} for _ in range(4)] + for name, j in word: + F = lab[name] + e = diag[j] + new = {} + for k, c in e.items(): # multiply by [F] + kk = add(k, F) + new[kk] = (new.get(kk, 0) + c) % 2 + diag[j] = {k: c for k, c in new.items() if c} + want = [{t: 1} for t in TARGETS] + dets = add(*(lab[n] for n, _ in word)) + return diag == want and dets == sc(4, I2) + + +if __name__ == "__main__": + sys.exit(main())