From eeb0cd605415a73b792915aaa9185000f293c84a Mon Sep 17 00:00:00 2001 From: littleBro <3585850+littleBro@users.noreply.github.com> Date: Tue, 13 Oct 2026 04:32:37 +0000 Subject: [PATCH] Prove a determinant obstruction for rank-homogeneous register paths --- .../graded-path-obstruction/.gitattributes | 2 + .../graded-path-obstruction/EXPECTED.json | 27 +++ .../graded-path-obstruction/MANIFEST.json | 16 ++ research/graded-path-obstruction/NOTICE.md | 34 ++++ research/graded-path-obstruction/ORIGINS.json | 15 ++ research/graded-path-obstruction/PROOF.md | 161 +++++++++++++++ research/graded-path-obstruction/README.md | 65 ++++++ .../graded-path-obstruction/VALIDATION.json | 44 ++++ research/graded-path-obstruction/dense.py | 130 ++++++++++++ research/graded-path-obstruction/model.py | 190 ++++++++++++++++++ research/graded-path-obstruction/screen.py | 45 +++++ research/graded-path-obstruction/verify.py | 174 ++++++++++++++++ .../graded-path-obstruction/words.json.gz | Bin 0 -> 3322 bytes 13 files changed, 903 insertions(+) create mode 100644 research/graded-path-obstruction/.gitattributes create mode 100644 research/graded-path-obstruction/EXPECTED.json create mode 100644 research/graded-path-obstruction/MANIFEST.json create mode 100644 research/graded-path-obstruction/NOTICE.md create mode 100644 research/graded-path-obstruction/ORIGINS.json create mode 100644 research/graded-path-obstruction/PROOF.md create mode 100644 research/graded-path-obstruction/README.md create mode 100644 research/graded-path-obstruction/VALIDATION.json create mode 100644 research/graded-path-obstruction/dense.py create mode 100644 research/graded-path-obstruction/model.py create mode 100644 research/graded-path-obstruction/screen.py create mode 100644 research/graded-path-obstruction/verify.py create mode 100644 research/graded-path-obstruction/words.json.gz diff --git a/research/graded-path-obstruction/.gitattributes b/research/graded-path-obstruction/.gitattributes new file mode 100644 index 0000000000..44a23d1fe3 --- /dev/null +++ b/research/graded-path-obstruction/.gitattributes @@ -0,0 +1,2 @@ +* text eol=lf +*.gz binary diff --git a/research/graded-path-obstruction/EXPECTED.json b/research/graded-path-obstruction/EXPECTED.json new file mode 100644 index 0000000000..f01558f7ef --- /dev/null +++ b/research/graded-path-obstruction/EXPECTED.json @@ -0,0 +1,27 @@ +{ + "status": "PASS_GRADED_PATH_OBSTRUCTION", + "counts": { + "excluded": 64, + "dense_middle_paths": 1377, + "determinant_polynomial_controls": 73, + "not_excluded_by_this_criterion": 9, + "positive_nine_call_controls": 3, + "false_homogeneity_rejected": 1, + "inhomogeneous_cancellation_control": 1, + "corrupt_rank_bill_rejected": 1 + }, + "by_origin": { + "four_block_followup": { + "excluded": 8 + }, + "collision_generators": { + "excluded": 23, + "not_excluded_by_this_criterion": 9 + }, + "pr680_regression": { + "excluded": 33 + } + }, + "words_payload_sha256": "a6acbdcbf7e8b28a6b0e0e334b16a3fdc1e06731fef6c6421ff71801f844a511", + "certificates_sha256": "6c6d968b9e1f733f02e1b485356a0fb81c6c38246f3c8e0cc55c36dffc450c5c" +} diff --git a/research/graded-path-obstruction/MANIFEST.json b/research/graded-path-obstruction/MANIFEST.json new file mode 100644 index 0000000000..2e5411046f --- /dev/null +++ b/research/graded-path-obstruction/MANIFEST.json @@ -0,0 +1,16 @@ +{ + "files": { + ".gitattributes": "abeba78466be388a1c5f3cb4ad595b915a0aa9402d1d87e37dfe42762e5b91c5", + "EXPECTED.json": "48825c6d56001d65f5d84eae1225c5b4be567524c140ff309890337487eb3bd3", + "NOTICE.md": "4a5c9fd916f12337f38e1d2ef4f4db32539cc07418b3f59fb81c4193725d18c2", + "ORIGINS.json": "ac91e9b89eee000ce8fd112e97c9f2b5f753426180369a886ff7bcbabc5f8f0a", + "PROOF.md": "696e58423e320033f09bda17f81689273bb8947fe9e48f8379ae1b397e407b4a", + "README.md": "4c3a8ff6a27edde28ae5ccb19398d49c21a9add8036dd41c2233f4148e27e92b", + "VALIDATION.json": "ef454895445f2b85bf1a07db74a09fd29af0ffd8300e70ddc44cf54d5b1cc650", + "dense.py": "760df8621caaa81ab841df39667f910b45b40d9167c02747db346e80649632af", + "model.py": "5d8c14e1aa62185fcb75725f0c337f00423642cebf121545d38a024567fc6dbf", + "screen.py": "1e53ee94f2049491dfdea0078cdb02696544668d22fb84db9185e41405dc6ff4", + "verify.py": "0a45ffdbdaa401e599cfd7d88e1206910ba952b08dda4fcf00dfabdffa237247" + }, + "words_payload_sha256": "a6acbdcbf7e8b28a6b0e0e334b16a3fdc1e06731fef6c6421ff71801f844a511" +} diff --git a/research/graded-path-obstruction/NOTICE.md b/research/graded-path-obstruction/NOTICE.md new file mode 100644 index 0000000000..4e294aed0f --- /dev/null +++ b/research/graded-path-obstruction/NOTICE.md @@ -0,0 +1,34 @@ +# Attribution, pins and overlap + +Prepared by [littleBro](https://github.com/littleBro) with substantial OpenAI +Codex assistance in the research, proof, implementation and validation. +New material is under the repository's Apache-2.0 license. No contributor +endorsement, independent human review, or literature-priority claim is made. + +The open complex m=3, W=3, s=8 register problem and general framework are +credited to eumemic's [PR #288](https://github.com/CrocSwap/integer-mult-bounds/pull/288), +head `475a088b5862f75f0b10596cfd6842d19531a5ec`, and its retained predecessors, +including Swapnil Jain's P1/P2 and the upstream Clifford-frame work. + +The same-author [PR #680](https://github.com/CrocSwap/integer-mult-bounds/pull/680), +head `c3a5b6b7afec35d259c29bc2d8bb8516e975ad31`, supplies the unchanged +`model.py` and `dense.py`, the formal phase-quotient convention, and 33 +regression words. That PR's notices and credited framework are retained by +reference here. This package supplies all runtime dependencies locally and +does not require PR #680 to be merged. + +The eight four-block words and 32 evolved words come from same-author local +research. Their literal contents are supplied in full. Local snapshot hashes +in ORIGINS.json establish extraction provenance only; they are not external +dependencies or claims of public review. + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. The selected result and +`upstream/` are unchanged. The selected supplier was not cold-replayed for +this standalone mathematical addition. + +Overlap review revisited #288 and #680, current PR metadata through #691, +and repository PR searches for homogeneous, determinant and grading. #673 +and #689 concern dirty echo composition, a different object. The reviewed +material did not identify this fixed-path homogeneity criterion or these +eight four-block closures. This is not a review of every PR diff or proof +of novelty. The proof and its scope remain open to maintainer review. diff --git a/research/graded-path-obstruction/ORIGINS.json b/research/graded-path-obstruction/ORIGINS.json new file mode 100644 index 0000000000..21484d91f9 --- /dev/null +++ b/research/graded-path-obstruction/ORIGINS.json @@ -0,0 +1,15 @@ +{ + "base": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "predecessor_pr": 680, + "predecessor_head": "c3a5b6b7afec35d259c29bc2d8bb8516e975ad31", + "vendored_files": { + "model.py": "5d8c14e1aa62185fcb75725f0c337f00423642cebf121545d38a024567fc6dbf", + "dense.py": "760df8621caaa81ab841df39667f910b45b40d9167c02747db346e80649632af" + }, + "same_author_local_input_sha256": { + "watched-search.json.gz": "2e1cb2797e46144fc33481a06576f638399521aeed785f10d644b2e36b807f0c", + "evolution.json.gz": "ff105da6453acf3974243e650e8202fdaf054e7878bc6dddf351e9a656e6e804" + }, + "generator_seed": 6801302, + "note": "Local hashes are provenance only; every literal word required for verification is included." +} diff --git a/research/graded-path-obstruction/PROOF.md b/research/graded-path-obstruction/PROOF.md new file mode 100644 index 0000000000..98522e1e89 --- /dev/null +++ b/research/graded-path-obstruction/PROOF.md @@ -0,0 +1,161 @@ +# A determinant obstruction for rank-homogeneous path collisions + +This is a written proof in a formal group algebra, followed by finite exact +hypothesis checks. It is not a proof-assistant verification or a new integer +multiplication bound. No literature-priority claim is made. + +## 1. General statement + +Let G be a group and let r:G -> Z_{≥0} satisfy + + r(gh) <= r(g) + r(h), r(1) = 0. + +Fix W registers and L >= 1 arbitrary invertible scalar matrices +B_1,...,B_L over a field K. On the two boundaries put + + U = diag([u_1],...,[u_W]), V = diag([v_1],...,[v_W]). + +For each interior layer 1 <= k < L put + + D_k = diag([g_{k,1}],...,[g_{k,W}]). + +All u,v,g are fixed group elements; the B matrices can have any coefficients +and zero pattern compatible with invertibility. Consider + + S = V B_L D_{L-1} B_{L-1} ... B_2 D_1 B_1 U + +over K[G]. An interior path a=(a_1,...,a_{L-1}) has ordered product and degree + + h(a) = g_{L-1,a_{L-1}} ... g_{1,a_1}, + d(a) = sum_k r(g_{k,a_k}). + +For L=1 the only interior path is empty, with product 1 and degree 0. + +**Hypothesis (finite path homogeneity).** Whenever h(a)=h(b), d(a)=d(b). +This concerns this finite collection of paths. It does not assert that rank +is a grading or a homomorphism on G. + +**Endpoint assumption.** In every entry of S, every group element with a +nonzero coefficient has rank at least m. Different entries may use different +group elements; no shared final frame is required by this assumption. + +Then + + W*m <= sum_i r(u_i) + sum_i r(v_i) + sum_{k,i} r(g_{k,i}). (1) + +Thus any word whose right side is less than W*m and satisfies path +homogeneity is impossible for **all** invertible choices of the B matrices. +There is no restriction on L, on the scalar zero patterns, or on the size of +the scalar coefficients. + +## 2. Proof + +Replace each interior D_k by the commuting scalar diagonal matrix + + T_k(t) = diag(t^{r(g_{k,1})},...,t^{r(g_{k,W})}), + +and form the ordinary polynomial matrix + + T(t) = B_L T_{L-1}(t) B_{L-1} ... B_2 T_1(t) B_1. + +Its determinant is exactly + + det T(t) = c * t^D, + c = product_k det B_k != 0, + D = sum_{k,i} r(g_{k,i}). (2) + +For fixed output i and input j, group the paths in the entry T_ij(t) by +their ordered product h. Homogeneity assigns each such product a single +degree d_h, so + + T_ij(t) = sum_h c_{ij,h} * t^{d_h}. + +The same coefficient c_{ij,h} is the coefficient of [v_i h u_j] in S_ij. +Left and right multiplication by fixed group elements are injective, so +distinct h cannot merge in this latter coefficient comparison. + +If c_{ij,h} != 0, the endpoint assumption and subadditivity give + + m <= r(v_i h u_j) + <= r(v_i) + r(h) + r(u_j) + <= r(v_i) + d_h + r(u_j). + +Consequently every nonzero term of T_ij(t) has degree at least +m-r(v_i)-r(u_j). Cancellation between different h at the same degree can +only increase that lower bound; an identically zero entry causes no problem. + +Every term in the ordinary Leibniz determinant expansion therefore has +degree at least + + sum_i (m-r(v_i)-r(u_{sigma(i)})) + = W*m - sum_i r(v_i) - sum_j r(u_j). + +This remains valid if some entry bounds are negative. Since (2) is nonzero, +its degree D is at least this quantity. Rearranging proves (1). + +The argument never maps the whole noncommutative group algebra into K[t]. +Only the coefficients of this fixed path expansion are compared. + +## 3. Why the collision hypothesis matters + +Without homogeneity, a group coefficient can cancel between different +powers of t. The weighted scalar coefficient then need not vanish. + +For example, take an element C of positive rank, and in two interior layers +use diag(1,C) and diag(1,C^{-1}), with identity mixing between them. The two +constant-role paths have product 1 but degrees 0 and 2 when both ranks are 1. +With A=[[1,1],[1,-1]] at entry and A^{-1} at exit, the unweighted group word +is the identity. The weighted matrix is + + A^{-1} diag(1,t) diag(1,t) A + = (1/2) [[1+t^2, 1-t^2], [1-t^2, 1+t^2]]. + +The off-diagonal group coefficients vanish, but the displayed polynomials +do not. The verifier includes this control and rejects a forged homogeneous +classification of an exact Clifford inverse-pair word. + +Failure of homogeneity is only a necessary escape from this obstruction. +It is not a construction or evidence that invertible coefficients exist. + +## 4. Clifford specialization and scope + +The finite checker uses the same three-qubit projective Clifford group +algebra as PR #680. For a Clifford symplectic matrix [[A,B],[C,D]], define +r(g)=rank_F2(B). Composition gives B_{gh}=A_g B_h+B_g D_h, hence the required +subadditivity. Every listed free monomial operation has rank zero; each +paid C_v=((1+i)/2)I+((1-i)/2)X_v has rank one. The rank of a complete unary +layer is therefore no larger than its literal paid-call count. + +The usual endpoint condition, one full-rank left monomial coset for each +input stream, implies the weaker endpoint assumption above with m=3. +For W=3 and eight paid calls the right side of (1) is at most eight, which +contradicts nine whenever path homogeneity holds. + +Projective equality here retains Pauli conjugation signs and quotients only +scalar phase. The supplied rational-Gaussian generators have central phases +in {1,-1,i,-i}; the intended tensor realization removes them when the tensor +multiplicity is divisible by four, as in the predecessor model. The result +is stated in that formal group algebra. It does not infer formal linear +independence from the concrete 8-by-8 representation. That representation +is used only to independently check group equalities and ranks. + +## 5. What the supplied words establish + +All 73 literal words have eight paid calls. The criterion excludes 64: + +- Eight four-block descendants previously left unresolved by bounded + support/polynomial searches. +- Twenty-three of 32 words from two generations of a collision generator. +- All 33 three-block words already excluded by PR #680, as regressions. + +Nine evolved words fail the homogeneity hypothesis and remain unclassified +by this theorem. The cases are not an exhaustive enumeration of any +four-block family or of the full register model. The fixed unary words and +mixing locations matter. Inserting or changing unary operations can change +the hypothesis. + +The proof supplies a search filter: a successful word with paid cost below +W*m must admit coincident interior products of different accumulated ranks. +Merely counting repeated products, including repetitions of the same unary +choice on different registers, is insufficient. The new criterion is +independent of the support, torus and polynomial solvers used in PR #680. diff --git a/research/graded-path-obstruction/README.md b/research/graded-path-obstruction/README.md new file mode 100644 index 0000000000..e78e55412b --- /dev/null +++ b/research/graded-path-obstruction/README.md @@ -0,0 +1,65 @@ +# Rank-homogeneous paths: a determinant obstruction + +**Scoped theorem and exact finite verification. No new kappa or primitive.** + +A scalar determinant tracks accumulated unary rank whenever all paths with +the same interior group product have the same rank sum. The resulting +inequality rules out a saving, for any number of scalar mixing blocks and +arbitrary invertible complex coefficients, subject to that explicit path +hypothesis. See [the complete proof](PROOF.md). + +This closes eight previously unresolved four-block Clifford words and 23 +additional evolved words at m=3, W=3, s=8. It also recovers the 33 exclusions +in [PR #680](https://github.com/CrocSwap/integer-mult-bounds/pull/680) by a +different argument. Nine supplied words fail the new hypothesis and are +kept as unknown, not reported as solutions or impossibility results. + +## Replay + +Python 3.10+ and the standard library are sufficient. From the repository: + +```sh +python3 -I -B research/graded-path-obstruction/verify.py +``` + +Expected: `PASS_GRADED_PATH_OBSTRUCTION`, with 64 exclusions and nine words +not excluded by this criterion. The checker uses no network, Git checkout +dependencies, external solvers, or sibling research directories. It writes +no files. Assertions are required; optimized execution is explicitly rejected. + +The replay checks the finite hypotheses using both signed Clifford tableaus +and exact 8-by-8 Gaussian matrices, including 1,377 interior paths. It also +checks 73 polynomial determinant identities, three exact nine-call positive +controls, a heterogeneous inverse-pair control, and deliberate certificate +corruptions. It compares the complete result with [EXPECTED.json](EXPECTED.json). +Input and source integrity checks are described in [VALIDATION.json](VALIDATION.json). + +The general conclusion rests on the written determinant argument, not on +extrapolation from these finite controls. The obstruction is to formal group +algebra words with the stated fixed unary layers. The full W=3, s=8 problem +from [PR #288](https://github.com/CrocSwap/integer-mult-bounds/pull/288) remains +open. There is no bit-side construction, supplier invoice, all-size compiler +proof, or change to the selected frontier here. + +## Search consequence + +The eight follow-up words originally survived very short polynomial searches. +Diagonal gauge normalization then provided exact refutations of the seven +stored arithmetic supports, but bounded searches over other supports still +stalled. Inspection of their collision classes exposed the determinant +criterion, which closes the whole fixed words without coefficient search. + +For future synthesis, require a collision between **different accumulated +ranks** before spending time on scalar coefficients. This is a necessary +filter, not a score predicting existence. The 32 evolved words here are a +finite literal corpus, not a claim that their generator families are exhausted. + +`words.json.gz` contains all 73 literal words; matrix entries at `mix3` gates +are identity placeholders marking locations where the theorem permits any +GL(3,C) matrix. `screen.py` checks the hypotheses. `verify.py` reconstructs +them using independent Gaussian matrices. `model.py` and `dense.py` are +unchanged, attributed copies from the public PR #680 head. + +See [NOTICE.md](NOTICE.md) and [ORIGINS.json](ORIGINS.json) for source pins and +attribution. No independent human review, Lean verification, repository-wide +replay, or remote CI is represented as completed. diff --git a/research/graded-path-obstruction/VALIDATION.json b/research/graded-path-obstruction/VALIDATION.json new file mode 100644 index 0000000000..393379b173 --- /dev/null +++ b/research/graded-path-obstruction/VALIDATION.json @@ -0,0 +1,44 @@ +{ + "status": "Exact local replay passed before publication", + "platform": "Windows, Python 3.14.4, standard library", + "command": "python3 -I -B research/graded-path-obstruction/verify.py", + "expected_status": "PASS_GRADED_PATH_OBSTRUCTION", + "evidence": "Signed tableau and exact Gaussian-matrix classifications agree on 73 words and 1377 internal paths; 64 exclusions, nine criterion-unknown words. Polynomial determinant checks and positive/rejection controls are listed in EXPECTED.json.", + "scope": "Written general proof plus independent finite hypothesis checks; not a proof assistant or independent human review.", + "not_claimed": [ + "new kappa", + "new positive register primitive", + "all-size multiplication theorem", + "full supplier or repository-wide replay", + "remote CI" + ], + "isolation_and_corruption_checks": { + "relocated_isolated": { + "exit_code": 0, + "seconds": 0.5829, + "expected_result": true + }, + "recompressed_input": { + "exit_code": 0, + "seconds": 0.6254, + "expected_result": true + }, + "corrupt_payload": { + "exit_code": 1, + "seconds": 0.2365, + "expected_result": false + }, + "corrupt_expected": { + "exit_code": 1, + "seconds": 0.2479, + "expected_result": false + }, + "optimized_rejected": { + "exit_code": 1, + "seconds": 0.0807, + "expected_result": false + } + }, + "full_replay_seconds": 0.63, + "selected_record_check": "PASS selected record, exact kappa, original source inventory and proof supplement: 51110230636731/31250000000000000" +} diff --git a/research/graded-path-obstruction/dense.py b/research/graded-path-obstruction/dense.py new file mode 100644 index 0000000000..6bef093135 --- /dev/null +++ b/research/graded-path-obstruction/dense.py @@ -0,0 +1,130 @@ +"""Independent exact Gaussian-matrix operator and endpoint controls. + +The matrix arithmetic does not use tableau update formulas. +Apache-2.0; substantial OpenAI Codex assistance. +""" +from fractions import Fraction as Q +from functools import lru_cache +from model import IDENTITY, FREE + +N = 8 + + +def rot(a, b, p): + return ((a, b), (-b, a), (-a, -b), (b, -a))[p % 4] + + +def normalize(e, re, im, projective=False): + while e and all(value % 2 == 0 for value in re+im): + e -= 1 + re, im = [v//2 for v in re], [v//2 for v in im] + variants = [] + for p in range(4 if projective else 1): + entries = [rot(a, b, p) for a, b in zip(re, im)] + variants.append((e, tuple(a for a, _ in entries), tuple(b for _, b in entries))) + return min(variants) + + +def identity(): + return normalize(0, [int(i == j) for i in range(N) for j in range(N)], [0]*64) + + +@lru_cache(maxsize=40_000) +def multiply(a, b, projective=False): + ea, ar, ai = a + eb, br, bi = b + re, im = [0]*64, [0]*64 + for i in range(N): + for k in range(N): + x, y = ar[8*i+k], ai[8*i+k] + if x == y == 0: + continue + for j in range(N): + u, v = br[8*k+j], bi[8*k+j] + re[8*i+j] += x*u-y*v + im[8*i+j] += x*v+y*u + return normalize(ea+eb, re, im, projective) + + +def pauli(value): + x, z, p = value & 7, (value >> 3) & 7, value >> 6 + re, im = [0]*64, [0]*64 + for col in range(8): + re[8*(col ^ x)+col], im[8*(col ^ x)+col] = rot(1, 0, p+2*((z & col).bit_count() % 2)) + return normalize(0, re, im) + + +@lru_cache(None) +def operator(op): + name, a, b = op + re, im = [0]*64, [0]*64 + if name == "C": + for col in range(8): + re[8*col+col], im[8*col+col] = 1, 1 + re[8*(col ^ a)+col], im[8*(col ^ a)+col] = 1, -1 + return normalize(1, re, im) + for col in range(8): + row, p = col, 0 + if name == "S": + p = (col >> a) & 1 + elif name == "X": + row ^= 1 << a + elif name == "Z": + p = 2*((col >> a) & 1) + elif name == "CX": + row ^= ((col >> a) & 1) << b + elif name == "CZ": + p = 2*((col >> a) & 1)*((col >> b) & 1) + else: + raise ValueError(op) + re[8*row+col], im[8*row+col] = rot(1, 0, p) + return normalize(0, re, im) + + +@lru_cache(maxsize=10_000) +def signature(matrix): + # Recover all six conjugated generators by GP = P'G, independently of + # the optimized tableau update formulas used by the search. + images = [] + for generator in IDENTITY: + wanted = multiply(matrix, pauli(generator)) + matches = [value for value in range(256) if multiply(pauli(value), matrix) == wanted] + assert len(matches) == 1 + images.append(matches[0]) + return tuple(images) + + +def independent_frame(g): + basis = [value & 63 for value in g] + result = 0 + for value in range(64): + image = 0 + for i in range(6): + if value & (1 << i): + image ^= basis[i] + if image & 7 == 0: + result |= 1 << value + return result + + +def execute(program): + unit = normalize(*identity(), projective=True) + rows = [{(r, unit): Q(1)} for r in range(3)] + for gate in program: + if gate[0] == 'mix3': + changed = [] + for r in range(3): + row = {} + for c in range(3): + for key, value in rows[c].items(): + row[key] = row.get(key, 0)+gate[1+3*r+c]*value + changed.append({key: value for key, value in row.items() if value}) + rows = changed + else: + op = ('C', gate[2], 0) if gate[0] == 'paid' else FREE[gate[2]] + changed = {} + for (column, matrix), value in rows[gate[1]].items(): + key = column, multiply(operator(op), matrix, True) + changed[key] = changed.get(key, 0)+value + rows[gate[1]] = {key: value for key, value in changed.items() if value} + return [{(col, signature(matrix)): value for (col, matrix), value in row.items()} for row in rows] diff --git a/research/graded-path-obstruction/model.py b/research/graded-path-obstruction/model.py new file mode 100644 index 0000000000..1ebf1ebd7c --- /dev/null +++ b/research/graded-path-obstruction/model.py @@ -0,0 +1,190 @@ +"""Exact three-stream projective Clifford group-algebra model. + +Apache-2.0. Substantial OpenAI Codex assistance; see NOTICE.md. +""" +from fractions import Fraction as Q +from functools import lru_cache +from itertools import combinations + +M = 3 +IDENTITY = tuple([1 << i for i in range(M)] + [1 << (M+i) for i in range(M)]) +Op = tuple[str, int, int] +PAIRS = ((0, 1), (0, 2), (1, 2)) +FREE = tuple([('S', i, 0) for i in range(M)] + + [('X', i, 0) for i in range(M)] + + [('Z', i, 0) for i in range(M)] + + [('CX', i, j) for i in range(M) for j in range(M) if i != j] + + [('CZ', i, j) for i, j in combinations(range(M), 2)]) + + +def pauli_image(op: Op, value: int) -> int: + x, z, p = value & 7, (value >> 3) & 7, value >> 6 + name, a, b = op + if name == "C": + if (z & a).bit_count() & 1: + x ^= a + p -= 1 + elif name == "S": + u = (x >> a) & 1 + p += u + z ^= u << a + elif name == "X": + p += 2*((z >> a) & 1) + elif name == "Z": + p += 2*((x >> a) & 1) + elif name == "CX": + x ^= ((x >> a) & 1) << b + z ^= ((z >> b) & 1) << a + elif name == "CZ": + u, v = (x >> a) & 1, (x >> b) & 1 + p += 2*u*v + z ^= (u << b) | (v << a) + else: + raise ValueError(op) + return x | (z << 3) | ((p % 4) << 6) + + +def rank_binary(values: list[int]) -> int: + pivots: dict[int, int] = {} + for value in values: + while value: + pivot = value.bit_length()-1 + if pivot in pivots: + value ^= pivots[pivot] + else: + pivots[pivot] = value + break + return len(pivots) + + +def fourier_rank(group: tuple[int, ...]) -> int: + return rank_binary([value & 7 for value in group[M:]]) + + +class Engine: + def __init__(self): + self.groups = [IDENTITY] + self.ids = {IDENTITY: 0} + self.transitions = lru_cache(maxsize=150_000)(self._transition) + self.frames = lru_cache(maxsize=40_000)(self._frame) + + def _frame(self, group_id): + g = self.groups[group_id] + basis = [sum((((g[M+i] >> j) & 1) << i) + | (((g[i] >> j) & 1) << (M+i)) for i in range(M)) + for j in range(M)] + span = [0] + for v in basis: + span += [w ^ v for w in span] + assert len(set(span)) == 8 + return sum(1 << v for v in span) + + def _transition(self, op, group_id): + new = tuple(pauli_image(op, value) for value in self.groups[group_id]) + if new not in self.ids: + self.ids[new] = len(self.groups) + self.groups.append(new) + return self.ids[new] + + def frame_info(self, group): + return self.frames(group), fourier_rank(self.groups[group]) + + +def add_poly(target, source, scalar=1, bit=0): + for mask, coefficient in source.items(): + assert not mask & bit + key = mask | bit + value = target.get(key, 0)+scalar*coefficient + if value: + target[key] = value + else: + target.pop(key, None) + + +def generic_paths(ring, program, kind): + """One independent variable per matrix entry, one selected entry per path.""" + rows = [{i: {0: 1}} for i in range(3)] + blocks = 0 + for gate in program: + if gate[0] not in ('mix', 'mix3'): + _, role, index = gate + op = ('C', index, 0) if gate[0] == 'paid' else FREE[index] + rows[role] = {(ring.transitions(op, key >> 2) << 2) | (key & 3): p + for key, p in rows[role].items()} + continue + assert gate[0] == ('mix' if kind == 2 else 'mix3') + roles = PAIRS[gate[1]] if kind == 2 else range(3) + changed = [] + for i in range(kind): + row = {} + for j, role in enumerate(roles): + bit = 1 << (kind*kind*blocks+kind*i+j) + for key, polynomial in rows[role].items(): + add_poly(row.setdefault(key, {}), polynomial, bit=bit) + changed.append(row) + for role, row in zip(roles, changed): + rows[role] = row + blocks += 1 + return tuple(rows), blocks + + +def coefficient_records(ring, rows): + records, targets = [], [set() for _ in range(3)] + for output, row in enumerate(rows): + # Interned integer IDs depend on what an Engine saw earlier. Proof + # row IDs must instead follow stable Clifford tableaus and columns. + for key, polynomial in sorted(row.items(), key=lambda item: (item[0] & 3, ring.groups[item[0] >> 2])): + frame, rank = ring.frame_info(key >> 2) + column = key & 3 + records.append({'output': output, 'column': column, 'frame': frame, + 'rank': rank, 'poly': polynomial}) + if rank == 3: + targets[column].add(frame) + return records, targets + + +def decode(program): + result = [] + for raw in program: + kind = raw[0] + if kind == 'mix3': + assert len(raw) == 10 + gate = (kind, *(Q(x) for x in raw[1:])) + else: + assert kind in ('paid', 'free') and len(raw) == 3 + assert type(raw[1]) is int and 0 <= raw[1] < 3 + assert type(raw[2]) is int + assert (1 <= raw[2] <= 7) if kind == 'paid' else (0 <= raw[2] < 18) + gate = tuple(raw) + result.append(gate) + return tuple(result) + + +def execute(ring, program): + rows = [{i: Q(1)} for i in range(3)] + for gate in program: + if gate[0] == 'mix3': + changed = [] + for r in range(3): + row = {} + for c in range(3): + for key, value in rows[c].items(): + row[key] = row.get(key, 0)+gate[1+3*r+c]*value + changed.append({key: value for key, value in row.items() if value}) + rows = changed + else: + op = ('C', gate[2], 0) if gate[0] == 'paid' else FREE[gate[2]] + rows[gate[1]] = {(ring.transitions(op, key >> 2) << 2) | (key & 3): value + for key, value in rows[gate[1]].items()} + return tuple(rows) + + +def endpoint_frames(ring, rows): + answer = [] + for column in range(3): + values = {ring.frame_info(key >> 2) for row in rows for key, v in row.items() + if v and key & 3 == column} + if len(values) != 1 or next(iter(values))[1] != 3: + return None + answer.append(next(iter(values))[0]) + return answer diff --git a/research/graded-path-obstruction/screen.py b/research/graded-path-obstruction/screen.py new file mode 100644 index 0000000000..eaaf54632a --- /dev/null +++ b/research/graded-path-obstruction/screen.py @@ -0,0 +1,45 @@ +"""Exact hypotheses for the rank-homogeneous path obstruction. + +The theorem is in PROOF.md. A failed hypothesis means unknown, never feasible. +Apache-2.0; substantial OpenAI Codex assistance; see NOTICE.md. +""" +from collections import defaultdict +from itertools import product +from model import Engine, FREE, fourier_rank + + +def layers(program): + stages=[[[] for _ in range(3)]] + for gate in program: + if gate[0]=='mix3': + stages.append([[] for _ in range(3)]) + else: + stages[-1][gate[1]].append(('C',gate[2],0) if gate[0]=='paid' else FREE[gate[2]]) + if len(stages)<2: + raise ValueError('at least one scalar block is required') + return stages + + +def group(ring,operations): + g=0 + for op in operations:g=ring.transitions(op,g) + return g + + +def certificate(program): + stages=layers(program);ring=Engine() + ranks=[[fourier_rank(ring.groups[group(ring,u)]) for u in stage] for stage in stages] + classes=defaultdict(list) + for path in product(range(3),repeat=len(stages)-2): + operations=[op for k,r in enumerate(path,1) for op in stages[k][r]] + tableau=ring.groups[group(ring,operations)] + cost=sum(ranks[k][r] for k,r in enumerate(path,1)) + classes[tableau].append((path,cost)) + classes=sorted((sorted((list(p),c) for p,c in values) for values in classes.values()),key=lambda x:x[0][0]) + mixed=sum(len({c for p,c in values})>1 for values in classes) + rank_bill=sum(map(sum,ranks));paid=sum(g[0]=='paid' for g in program) + if rank_bill>paid: + raise ValueError('rank subadditivity control failed') + return {'scalar_blocks':len(stages)-1,'paid_calls':paid,'unary_ranks':ranks, + 'rank_bill':rank_bill,'middle_classes':classes,'heterogeneous_classes':mixed, + 'status':'excluded' if mixed==0 and rank_bill<9 else 'not_excluded_by_this_criterion'} diff --git a/research/graded-path-obstruction/verify.py b/research/graded-path-obstruction/verify.py new file mode 100644 index 0000000000..0609120d46 --- /dev/null +++ b/research/graded-path-obstruction/verify.py @@ -0,0 +1,174 @@ +"""Standalone exact replay, with independent Gaussian-matrix path grouping.""" +if not __debug__: + raise SystemExit('Run without -O: inherited Clifford checks require assertions.') +from collections import Counter,defaultdict +from copy import deepcopy +from fractions import Fraction as Q +from hashlib import sha256 +from itertools import permutations,product +from pathlib import Path +import gzip,json,sys + +# Permit an isolated interpreter and an unrelated current working directory. +ROOT=Path(__file__).resolve().parent +sys.path.insert(0,str(ROOT)) +from model import decode,Engine,execute,fourier_rank,endpoint_frames +from screen import layers,certificate +import dense + + +def dense_certificate(program): + stages=layers(program) + matrices=[];ranks=[] + for stage in stages: + matrices.append([]);ranks.append([]) + for operations in stage: + a=dense.identity() + for op in operations:a=dense.multiply(dense.operator(op),a,True) + counts=[sum(a[1][8*r+c]!=0 or a[2][8*r+c]!=0 for r in range(8)) for c in range(8)] + assert len(set(counts))==1 and counts[0] in (1,2,4,8) + matrices[-1].append(a);ranks[-1].append(counts[0].bit_length()-1) + classes=defaultdict(list) + for path in product(range(3),repeat=len(stages)-2): + a=dense.identity() + for k,r in enumerate(path,1):a=dense.multiply(matrices[k][r],a,True) + a=dense.normalize(*a,projective=True) + classes[a].append((list(path),sum(ranks[k][r] for k,r in enumerate(path,1)))) + classes=sorted((sorted(v) for v in classes.values()),key=lambda x:x[0][0]) + return ranks,classes + + +def check_certificate(program,saved): + wanted=certificate(program) + assert saved==wanted + ranks,classes=dense_certificate(program) + assert saved['unary_ranks']==ranks and saved['middle_classes']==classes + return wanted + + +def add(a,b): + out=dict(a) + for e,c in b.items():out[e]=out.get(e,0)+c + return {e:c for e,c in out.items() if c} + + +def mul(a,b): + out={} + for e,c in a.items(): + for f,d in b.items():out[e+f]=out.get(e+f,0)+c*d + return {e:c for e,c in out.items() if c} + + +def determinant(matrix): + out={} + for p in permutations(range(3)): + term={0:(-1)**sum(p[i]>p[j] for i in range(3) for j in range(i+1,3))} + for r,c in enumerate(p):term=mul(term,matrix[r][c]) + out=add(out,term) + return out + + +def determinant_control(program,cert): + blocks=cert['scalar_blocks'];matrices=[];det=1 + for k in range(blocks): + b=[[1,k+1,0],[0,1,1],[1,0,1]];matrices.append(b) + actual=determinant([[{0:x} if x else {} for x in row] for row in b]) + assert actual=={0:k+2};det*=k+2 + current=[[{0:x} if x else {} for x in row] for row in matrices[0]] + for k in range(1,blocks): + current=[ [{e+cert['unary_ranks'][k][r]:c for e,c in p.items()} for p in row] + for r,row in enumerate(current)] + b=matrices[k];out=[[{} for _ in range(3)] for _ in range(3)] + for r,c,j in product(range(3),repeat=3):out[r][c]=add(out[r][c],mul({0:b[r][j]},current[j][c])) + current=out + degree=sum(map(sum,cert['unary_ranks'][1:-1])) + assert determinant(current)=={degree:det} + concrete=[];at=0 + for gate in program: + if gate[0]=='mix3':concrete.append(('mix3',*(x for row in matrices[at] for x in row)));at+=1 + else:concrete.append(gate) + if cert['status']=='excluded': + ring=Engine();rows=execute(ring,concrete) + assert any(fourier_rank(ring.groups[key>>2])<3 for row in rows for key,c in row.items() if c) + + +def controls(counts): + identity=('mix3',1,0,0,0,1,0,0,0,1) + boundary=tuple(('paid',role,axis) for role in range(3) for axis in (1,2,4))+(identity,) + cert=certificate(boundary);check_certificate(boundary,cert) + assert cert['scalar_blocks']==1 and cert['rank_bill']==9 and cert['heterogeneous_classes']==0 + assert cert['status']=='not_excluded_by_this_criterion' + ring=Engine();assert endpoint_frames(ring,execute(ring,boundary)) is not None + counts['positive_nine_call_controls']+=1 + # Three commuting independent butterflies on every stream: exact boundary. + for extra in (0,2): + word=[identity] + for axis in (1,2,4): + word.extend(('paid',role,axis) for role in range(3));word.append(identity) + word.extend([identity]*extra);word=tuple(word) + cert=certificate(word);check_certificate(word,cert) + assert cert['rank_bill']==9 and cert['heterogeneous_classes']==0 + assert cert['status']=='not_excluded_by_this_criterion' + ring=Engine();assert endpoint_frames(ring,execute(ring,word)) is not None + counts['positive_nine_call_controls']+=1 + # The same group element arises with degrees 0 and 2: C^-1 C = I. + word=(identity,('paid',1,1),identity,('paid',1,1),('free',1,3),identity) + cert=certificate(word);check_certificate(word,cert) + assert cert['heterogeneous_classes'] and cert['status']=='not_excluded_by_this_criterion' + forged=deepcopy(cert);forged['heterogeneous_classes']=0;forged['status']='excluded' + try:check_certificate(word,forged) + except AssertionError:counts['false_homogeneity_rejected']+=1 + else:raise AssertionError('false homogeneity accepted') + # Omitting homogeneity would preserve a cancellation incorrectly: + # A^-1 diag(1,t) diag(1,t) A has off-diagonal (1-t^2)/2, + # whereas the unweighted group word A^-1 diag(I,C^-1 C) A is I. + off={0:Q(1,2),2:Q(-1,2)} + assert sum(off.values())==0 and off + counts['inhomogeneous_cancellation_control']+=1 + + +def replay(): + payload=gzip.decompress((ROOT/'words.json.gz').read_bytes()) + data=json.loads(payload);counts=Counter();origins=defaultdict(Counter);certificates=[] + assert len({c['id'] for c in data['cases']})==len(data['cases']) + for case in data['cases']: + word=decode(case['program']);cert=certificate(word) + assert cert['paid_calls']==8 + check_certificate(word,cert);determinant_control(word,cert) + certificates.append({'id':case['id'],'certificate':cert}) + counts[cert['status']]+=1;origins[case['origin']][cert['status']]+=1 + counts['dense_middle_paths']+=3**(cert['scalar_blocks']-1) + counts['determinant_polynomial_controls']+=1 + controls(counts) + sample=decode(data['cases'][0]['program']);forged=deepcopy(certificates[0]['certificate']) + forged['rank_bill']+=1 + try:check_certificate(sample,forged) + except AssertionError:counts['corrupt_rank_bill_rejected']+=1 + else:raise AssertionError('corrupt rank bill accepted') + packed=json.dumps(certificates,sort_keys=True,separators=(',',':')).encode() + return {'status':'PASS_GRADED_PATH_OBSTRUCTION','counts':dict(counts), + 'by_origin':{k:dict(v) for k,v in origins.items()}, + 'words_payload_sha256':sha256(payload).hexdigest(), + 'certificates_sha256':sha256(packed).hexdigest()} + + +def check_manifest(): + manifest=json.loads((ROOT/'MANIFEST.json').read_text(encoding='utf-8')) + expected={'.gitattributes','model.py','dense.py','screen.py','verify.py', + 'EXPECTED.json','ORIGINS.json','README.md','PROOF.md','NOTICE.md','VALIDATION.json'} + assert set(manifest['files'])==expected + for name,wanted in manifest['files'].items(): + assert sha256((ROOT/name).read_bytes()).hexdigest()==wanted, 'Source integrity mismatch: '+name + payload=gzip.decompress((ROOT/'words.json.gz').read_bytes()) + assert sha256(payload).hexdigest()==manifest['words_payload_sha256'], 'Word payload integrity mismatch' + origins=json.loads((ROOT/'ORIGINS.json').read_text(encoding='utf-8')) + for name,wanted in origins['vendored_files'].items(): + assert sha256((ROOT/name).read_bytes()).hexdigest()==wanted + + +if __name__=='__main__': + check_manifest() + report=replay() + expected=json.loads((ROOT/'EXPECTED.json').read_text(encoding='utf-8')) + if report!=expected:raise SystemExit('Expected certificate mismatch') + print(json.dumps(report,sort_keys=True)) diff --git a/research/graded-path-obstruction/words.json.gz b/research/graded-path-obstruction/words.json.gz new file mode 100644 index 0000000000000000000000000000000000000000..9c3bdb6dcb852e2bf4df4dd967d51dfad5ae1914 GIT binary patch literal 3322 zcmVUB~{I@3>rZ;(+L`zNjIwJvcMq! zzCAPBnX)BP6iL}Gmml(=RCU?1#oOT_`N!SI4=)cdcR&32$KB&kcR$>{Jb!uo<(*CM z?A_t+>HPTl@$2jVetP=#{Qloxo<9EP{imldU!H#d_4)PV=kwF&^M{{b|MO&p>pkp2xbGY~&b9q5?2>18j4pUKfyC^q{ z@-CfMD4h&px+YO}o@bTK=yuKJ8#I@1-CVx)$=Ck=1>TVhuy_UVm|^ld7QLioh#ghB z6CweKbVu-Pg+8KQxX-t}4v4x+H4%K*u1hFcrge)F%#4hu@7m_?nsuH|h)7&65-3y_`30Y!L6&JvG%p&HXb&IxMDyT+ z@Kh7@-}qRckQ2{|rUK$?C-DPG`LFY2FzU)+EXkm|X&KzbYF4pg*}jd-pttN;lxU*^ zW|p~!%!yGYqL?|dM91#PaRly?4$%<3WT&MHnzbeh91)=>&)y`UJR%2XirIx3k8pZ% zJNc*}&2E=wHEG@j^oj(uD`-5kG(Y_I^yRmQpWYdBDa{{WMfmaM@#*XP&ktW8&L4hx zI==wo>@FqqcqzaMbQLD3^p+MagpQc9pvbaVt{sutm=8o{rX@(rxhx56~h zXk{)JG22=3(0lL))W9R+JF6W2B9io7N-a}LZOZSv@$SZ(Wyd+h>tT^uo@M5}y~{=7 zXb+l!W5wJH?~3Rp@a{0dfhR0O11u?V^6Le;aZI^k2f_lVzXq zFZA+6525ic%RtEpwW^^jtc?=m8V~N%l#a2#V)frc?c$UxUScbDh;cj^SBg4E=8`!M9mEF1QMg zOcflIv@X@-2sHR1fLH|46){Wto1j=&AzhO2>@mKW?&Uk;mN;~ixQd(aCv;^*)$%iC z=MM%3;jalcliz;v*?F1wg6V_-)Cnz4M_)Ii9d)D96O>%du?)b_iwz(N;kz6jB{m1v zqe^e6D9!L$W%+S17=t*A)PI_6$O`%rnpi6uNtB)^o%iN$~7WWmYa)j5fN7E&MxqLrWsv@bI39%p=SZg zqD2{=K?)=26(Pzr){g4vbn?#aNSpG&*(K|mJEB@v zKiQmgtg)s~gN5=Ctw)QxqYMT3hP?jB9cOW{hbslJtlt3ls1n4F;M%#fdgX*`PD>so z{OV*8N2S%lghwiKR$vSGCAQ1?g9RBG)~fm~CntcNmRe4vsLD+T-bD`(LwDDH6OW*k zRkJAcQV`9c5^vNX3;}mqPy-@R-pi2fv2vS=DPuk1+*d7Lz%$5AX7#yY71CuvqN0vN z$RPj+IvaRTTkN@+JvRe6tZDl}9W}0Eg;F;XG2V1gcif4>J5hKMqA=_YO&p-YsXgrl zy?a4#$AaEs%(Pec3J`W@c7%Nfe`zDQH+3_OHIGhJdeogUXRm}tJrDEvM(EX4*gaH` z_MJwpMWc3Zw^gf%?Yky`7qK0i0S=tsOAT~k*c}ts+2mH?Y&UG7K}L^+*p1-S#GL9) zTO}D0qAtLZV;gqz#7>^LCGv!eds1oJNhNwqOrp**T1}Mr-Dh0dqyC%D==T85x8`5% z4F>S0c*PSsfS$z6?Nh0-Xxd3^tBLwgJGEOaI)PI<0aOy47E{{{Vdf=ibc;^B*_&0Z zA)C6lq`HM%s<#`&0(Rc04sWzGrqYfDJfGvyOy^?&cr51-EuFMl50qIJM`WNQqk z(Yx1}qzgA~srP9qw-3q|9a|2eb0hP`+dd;{h-5=^4!wRHhE118nKwU7P_-aW$oXcSe%gVFpDfg-+_$90j9Dc2TsZ2Av)aCD63_`FIsQ|bYnqh z*u(DE|Mi1wHe}_Q2*qe1Ulf`0rZz31Jhi#Q`pc-3H%yN&CeHb&xnN#WCdZI zeKCH=14DHt@M~Tv&qZvhZ@Ci*G6D7+0Zvkz?jRR2gKF^wp_!gQmMt+K3F|3Na&oT4 zcth0EuYA$54h)?#3m>&ankDN-FBpwRVP(q+P3KySH>5Q;$l;4de%)M)QYNRY)eAw; zz=_rqLxhN#-?GG7B~l5&4n^ zN$fzN)t)AX*3_D#jakYFYBsEI{+_g;O%x!atO!MNX<#+8C|-?0DGhw|ri3(tld(bu zICA`aWR^%$^K=!0__TrZosg8$YLHT*1&^R!J|U8Nok}`sbySehIYjy`!cC3|~iL3VqP_}eSh%FwLit`MJ9y7HxYLP{( z6#Ph1?$UOpH3$zU2@vIgTFJD?BFgAuP0Ep+ZA{}&G8N|7cE0gO0x1KDPFse7fexdW znGrYgH@y52x&LZXDh^FG+NT=T&w8b(h2b03K(kCxJiE}ODA*WvmlM*iEjJdlh`&uG z?S&99p%hlrvQ5E}_$*0W?~+=3hm29-Pqp_j)Q7kPcLAI=gyh zS|s}!i$i?s!8bEms`d`%sg(`j3n|HNYVH#tPV7*QDaN(ZjU3Dkl#*%0F_D<~j#QO` zkh(BVsyN~?N{Xmz7LSXh>uew1bU)IuMVr7Pb=63^EL;nhJ8l41iU@C1TOs9;UUR^CZ+gJ`JX^>T20OkK?;Z?~#RxlGS5?~N50Ml`=&qr8S| zx2HPF8Ch>JNi#bmPu5wQG;kt;q~vF!v@q~+u~K@L#%zoWmaF-7C!RC$u;Q{1v~TgO z9j-jFc<4Hf&ruxvug$=8hwkH=(fUEk@w4LKWo6{>qtd)CL?h+oCFeLAFfw}UtDW~* zs~=#cygi5BNhy4OGmT8-Gcl@FauQ|bsCB${*k%chIKbj%E(-ycXXwwFdkwgmdU6v} zH(2{dLoLjUT3pR2CObqb3qh$EviOla>6?0t7`P^HJQMAK?HcJdht>+_H7W)N)~JGk z-0CZ?whBVtpQW4-kySkoeX?U3L!ZPg(tX1Z^jVbPqQLHMR<@*S2vOAKtVC+B5i!%i zHfigkyqM+Md0_6fobDZ|okJqAS%X6yAhQ%k7On~v^uXX@g}Ru@R7SgV`6q!FB@a(TxGnq^B9VilE|2x@cKt3BoQ z*r1`-;Za^PDYm&9aK{P)y@Ee*(hc-#QlO4Xkh>)tRj%-HB?iP?6DjQW6 z?P=EXzC4uk9R65kKCgmv@5GtdHG8h7b&WhA16gIsapDZ*nqAXVZ}2JL1W#|-Sc|f+ z(nCvKb4Bvxu1B{cFf{AnGi-z$QoQTY?Ifj{^{$dy@Qyu*sL}fll}WU6Wwv=5F>z!G zL(VLQsB*d(3~NMkdOEZYq?|h4YB#_7$4nU%LoK(98u44LmC60L`)~jHAKw*JvA+cY E0I2zF(EtDd literal 0 HcmV?d00001