diff --git a/research/dihedral-arbitrary-couplings/README.md b/research/dihedral-arbitrary-couplings/README.md new file mode 100644 index 0000000000..66027d2a88 --- /dev/null +++ b/research/dihedral-arbitrary-couplings/README.md @@ -0,0 +1,220 @@ +# dihedral-arbitrary-couplings +# Arbitrary binary couplings do not reduce the dihedral rank tariff + +**Scoped written theorem; no new kappa.** Adam Gall's [PR1911](https://github.com/CrocSwap/integer-mult-bounds/pull/1911) +already proves the sharp infinite-dihedral tariff for rank-one **idempotent** +couplings. This package extends the gate alphabet to **every binary matrix N**, +including nilpotents and nonprojectors of higher rank, charging each gate +**rank(N)**. The same separate label tariffs remain exact for every finite +number of registers. The new implication is the minor-degree bound without +diagonalizability; the representations, endpoint valuation and attaining words +are credited to PR1911. + +This is a rank bill, not an invocation lower bound. A single gate with N=I +acts on all R roles and is charged R. It is not evidence that an arbitrary +rank-R gate costs R native supplier children. + +## Alphabet and theorem + +Let G be the infinite dihedral group with presentation +G = . Work in M_R(F2[G]), R>=W. Allow arbitrary scalar +GL_R(F2) changes at zero cost, and paid gates + + D_N(g) = I + ([g]+1) N, g in {r,s}, N any binary R by R matrix. + +The price is rank(N), separately for each label. A zero coupling is the identity +and costs zero. Group coefficients commute with scalar entries. Since +([g]+1)^2=0 in characteristic two, **D_N(g)^2=I for every N**; neither +N^2=N nor rank one is required. + +All target and spectator inputs are arbitrary dirty data. The endpoint is exactly + + diag([(rs)^k_1 r^e_1], ..., [(rs)^k_W r^e_W], 1, ..., 1), + +where k_i are integers and e_i in {0,1}. No erasure, COPY, clean state, direct +rotation or other address primitive is free. Every restoration is part of the +word. Then every program satisfies + + sum over r gates rank(N) >= A = sum_i |k_i+e_i|, + sum over s gates rank(N) >= B = sum_i |k_i|. + +The two bounds are attained simultaneously. Positive per-rank prices alpha, +beta therefore have exact minimum alpha*A + beta*B, even with arbitrarily many +restored dirty spectators and free scalar mixing. + +## Proof: replace the projector-similarity step + +Use PR1911's two Laurent representations over L=F2[t,t^-1]: + + C = [[0,1],[1,0]], V = [[0,t],[t^-1,0]], + rho(r)=C, rho(s)=V; sigma(r)=V, sigma(s)=C. + +They are representations because C^2=V^2=I. Formal equality implies represented +equality; the converse is never used. Let delta(M) be the largest degree among +all nonzero square minors, including the empty minor 1. Cauchy--Binet gives +delta(MP)<=delta(M)+delta(P). Every constant invertible matrix, including +represented free scalar changes, has delta zero. + +**Rank-leading-coefficient lemma.** If M=tB+A+t^-1 C0 over a field and +rank(B)=q, every square minor has degree at most q. Expand a minor by +multilinearity in its columns. A term choosing more than q columns from B has +linearly dependent chosen columns, even after restricting to the minor's rows, +so its determinant vanishes. Every other term has degree equal to the number +of B columns minus the number of C0 columns, at most q. This argument includes +all minor sizes, arbitrary A and C0, and possible cancellation. + +In fact delta(M)=q: if q>0 choose a nonzero q by q minor of B. The coefficient +of degree q in the same minor of M is precisely that determinant. For q=0 +the upper bound and empty minor give equality. This equality concerns the +maximum over **all** minors, not the full determinant. + +For a represented V gate, + + rho(D_N(s)) = I + N tensor (I+V) + = t (N tensor E01) + (I+N tensor I) + t^-1 (N tensor E10). + +The positive coefficient has rank rank(N), so +delta(rho(D_N(s)))=rank(N). A represented C gate is constant, +invertible, and has delta zero. Interchanging r and s gives + + delta(rho(D_N(r)))=0, delta(rho(D_N(s)))=rank(N), + delta(sigma(D_N(r)))=rank(N), delta(sigma(D_N(s)))=0. + +No similarity or projector assumption appears here. In particular a nonzero +square-zero N is covered, although it cannot be similar to a nonzero projector. + +As in PR1911, each target block is a monomial permutation matrix. Its exponents +under rho are -k_i,k_i, and under sigma are k_i+e_i,-(k_i+e_i). +Selecting all positive entries gives endpoint deltas B and A; no minor can +exceed their sum. Spectator identity blocks add zero. Subadditivity through +every paid and free gate proves both lower bounds directly, without needing +to normalize away the scalar changes. + +For attainment, use coordinate projectors and the freely reduced literal word +(rs)^k_i r^e_i on each target. It contains |k_i+e_i| r labels and |k_i| s +labels. Different target coordinates commute. The formal group-algebra +identity establishes the endpoint and restores all spectators uniformly. +With left matrix actions execute the displayed word from right to left. +No basis changes or spectator roles are needed for this attaining word. +This matching construction and its tariff are inherited from PR1911. + +## Exact factorization and a dirty-state implementation invoice + +Binary rank factorization gives N=UV=sum_{j=1}^q u_j v_j^T with exactly +q=rank(N) nonzero rank-one terms. For a fixed reflection g and Q=[g]+1, + + product_j (I+Q u_j v_j^T) = I + Q sum_j u_j v_j^T = D_N(g), + +because every cross term contains Q^2=0. The binary matrices need not commute. +This is an identity in the full group algebra, and decomposes the arbitrary +gate at exactly the same formal rank tariff into rank-one gates of the +**enlarged** alphabet. It does not pretend that every term is a projector. + +For a rank-one term uv^T, put theta=v^T u. If theta=1, choose a binary basis +S with first column u and remaining columns a basis of ker(v^T). Then +S^-1 uv^T S=E00 and the canonical operation is one g on role 0. +If theta=0, choose w with v^T w=1 and extend u to a basis of ker(v^T); +the ordered columns [u,w,remaining kernel basis] give E01. Its canonical +operation, in chronological order, is + + a ^= b; b <- g(b); a ^= b; b <- g(b). + +It leaves a+(I+g)b in a and restores arbitrary dirty b. All other roles are +untouched. These identities hold for every involutory linear address action +g, not just the finite fixture in the checker. + +Apply S^-1 before the canonical operation and S after it. Gaussian row +elimination implements these with scalar whole-register XOR additions, +including a three-XOR swap when needed. If c(S) is the emitted number of row +additions for S^-1, its reverse emits S and + + c(S) <= R(R-1)+3(R-1). + +A rank-one projector therefore uses one address call and 2c(S) scalar XORs. +A nilpotent uses **two** address calls and 2c(S)+2 scalar XORs. For a chosen +rank decomposition with z nilpotent factors, the arbitrary gate uses exactly +q+z<=2q address calls and 2 sum_j c(S_j)+2z scalar XORs. All R roles can +start dirty; no extra data array or clean bit is assumed. An explicit schedule +has O(q R^2) operation descriptors. A scalar whole-array XOR costs L bit XORs +for arrays of length L; the address permutation has its own swap/address cost. + +This is a uniform algebraic implementation and word-level invoice. It is not +a native C++ engine admission, an optimized finite-array algorithm, or an +all-size tape/compiler theorem. The lower-bound relaxation optimistically +prices every rank-one coupling at one, including the nilpotent case whose +supplied physical word uses two address calls. Charging more cannot invalidate +the lower bound, but does not identify these tariffs with recursive child rank. + +## Reproduction and evidence + + python3.12 -I -O -B research/dihedral-arbitrary-couplings/verify.py + python3.12 scripts/research_package.py --package research/dihedral-arbitrary-couplings + +Default verification is read-only. Explicit --write regenerates RESULT.json. +The source README is authenticated by SHA-256 and Git blob hash before +mathematical checks; Git-free exports must include that declared input at its +repository-relative path. The generic runner additionally audits historical +task and selected-record provenance. + +The independent finite checks cover all **530 binary matrices** for R=1,2,3: +**473,690 nonempty Laurent minors**, exact rank factorization, full F2[C2] +coefficient convolution, involutions, and compiled dirty-input endpoints. +They also cover all **284 nonzero rank-one matrices** for R=1,2,3,4, +including **129 nilpotents**, with **4,264 symbolic input columns**; every +output row is compared, not just clean inputs or source-only columns. +Thirty-four signed target words have independently reduced literal and +integer normal-form endpoints and matching separate tariffs. + +Five controls expose the invalid projector premise, underpricing rank as +invocations, missing source restoration, missing identity summand, and reversed +basis orientation. Git-free CLI tests check read-only success, source +corruption, Boolean/float receipt substitutions, and actual implementation +mutations. Checks remain active with Python -O. The universal theorem is the +written proof above; finite checks are corroboration, not a Lean proof or +exhaustive search over unbounded words. + +## Sources, overlap, and limits + +Scientific and task base: 6bd33bc0b87a01e9c9d8b1c01576f3ddbcaee850, priority 5. +The prescribed baseline passed before selection. SOURCES.json pins the retained +PR1911 README, selected record and task catalogue. Exact predecessor head: +712593f82739203639d0a169b88c6bcac6f0590c, Adam Gall. Its all-register projector +theorem, representations, target computation, direct witnesses and predecessor +attribution remain credited. An initial projector-only proposal was retired +as duplicate before this package was written. + +Related work was checked before choosing this cut: + +- [PR1941](https://github.com/CrocSwap/integer-mult-bounds/pull/1941) already + includes arbitrary-rank **idempotent** prices in a finite even-dihedral + model. No novelty is claimed for merely replacing a projector by higher rank. +- [PR1589](https://github.com/CrocSwap/integer-mult-bounds/pull/1589), + Arham Tahir, head 010ec8c01c0edbbb08b541be236ab78d096f2ca1, removes the + projector premise for UT3 central targets using a mixed-coefficient rank + argument. It motivates the premise audit; it is not an infinite-dihedral + arbitrary-target theorem. +- [PR2290](https://github.com/CrocSwap/integer-mult-bounds/pull/2290), + Cinna Davis, head 8839972a3cc939ebc17562473082189ea166d7de, adds nilpotents + in a shallow two-role census. That finite search does not supply this + all-length, all-register rank tariff. + +Overlap included open PR bodies, retained closed/merged notes and ledger, and +targeted REST searches. Cached Discussions cover 1,239 records at 15:22Z on +2026-10-15; later claims may be missing. TASK.json records snapshot freshness. +No no-match search proves novelty; arbitrary code diffs were not exhaustively +searched. Coordination is on PR1911, comment 6198753145. + +Finite cyclic actions identify group words and may have cheaper implementations. +The Laurent representation does not factor through those quotients, so this +lower bound is **not** transferred to finite-address permutations. No selected +cold replay, hosted CI, independent human review, supplier hosting/precision, +outer analytic transfer or new multiplication exponent is claimed. +Prepared for ywz65 with substantial OpenAI Codex assistance. Apache-2.0. + +## Open next questions + +1. Find a torsion-aware analogue for finite dihedral targets; first test it on + the quotient relation. The Laurent invariant cannot survive that relation. +2. Bind these primitives to an actual supplier invoice before using rank tariffs + in adoption decisions. Begin with one reflection and every basis XOR; native + hosting, scratch, child rank and recursive transfer remain unproved. diff --git a/research/dihedral-arbitrary-couplings/RESULT.json b/research/dihedral-arbitrary-couplings/RESULT.json new file mode 100644 index 0000000000..b814c8a3e7 --- /dev/null +++ b/research/dihedral-arbitrary-couplings/RESULT.json @@ -0,0 +1,11 @@ +{ + "status": "PASS_DIHEDRAL_ARBITRARY_COUPLINGS", + "binary_matrices": 530, + "minor_determinants": 473690, + "rank_factorizations": 530, + "rank_one_programs": 284, + "nilpotent_programs": 129, + "coefficient_columns": 4264, + "target_words": 34, + "controls": 5 +} diff --git a/research/dihedral-arbitrary-couplings/SOURCES.json b/research/dihedral-arbitrary-couplings/SOURCES.json new file mode 100644 index 0000000000..537aae1843 --- /dev/null +++ b/research/dihedral-arbitrary-couplings/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "6bd33bc0b87a01e9c9d8b1c01576f3ddbcaee850", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + }, + { + "path": "research/infinite-dihedral-register-bound/README.md", + "usage": "input", + "git_blob": "531ddbd1641554cbe5e84a9aec7b695353bb9cbe", + "sha256": "16a97e08710201f33c756c22de54a5073e92fe3053a795151760af456459502c" + } + ] +} diff --git a/research/dihedral-arbitrary-couplings/TASK.json b/research/dihedral-arbitrary-couplings/TASK.json new file mode 100644 index 0000000000..c037f8c2a3 --- /dev/null +++ b/research/dihedral-arbitrary-couplings/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 5, + "base_commit": "6bd33bc0b87a01e9c9d8b1c01576f3ddbcaee850", + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "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": "Infinite-dihedral diagonal targets with arbitrary binary matrix couplings, each charged its binary rank: exact separate reflection tariffs and a dirty-restoring coupling implementation.", + "scope_change_reason": "PR1911 already proves the all-register tariff for rank-one idempotents. Its similarity-to-projector step does not cover nilpotents. Replace that premise by arbitrary binary N at rank(N) tariff and prove the missing minor-degree implication. The initial projector-only proposal was retired as duplicate before implementation.", + "bottleneck_link": "Tests whether enlarging this explicit formal alphabet to nilpotent and higher-rank couplings permits local rank-bill compression; physical adoption remains external.", + "budget_minutes": 60, + "stop_rule": "Prove the rank-leading-coefficient lemma and exact tariff, supply the finite dirty-state implementation invoice, and stop; no larger search or supplier expansion.", + "outcome": "completed", + "evidence": "README.md uniform written proof; verify.py exact binary rank, all minors, formal factorization and full dirty-input columns; RESULT.json and test_cli.py.", + "author": "ywz65", + "ai_assistance": "Substantial OpenAI Codex assistance with proof, code, source and overlap review, and writing.", + "open_questions": [ + { + "question": "Does a torsion-aware invariant give the corresponding sharp rank tariff for finite dihedral targets?", + "why_it_matters": "The Laurent representations here do not factor through finite rotation relations.", + "first_step": "Test the candidate invariant on the quotient relation before searching any words.", + "blocked_by": "Finite address actions identify distinct infinite-dihedral elements." + }, + { + "question": "Can a selected supplier actually realize this rank-priced coupling alphabet at a useful complete cost?", + "why_it_matters": "The formal rank price is optimistic; a nilpotent factor uses two physical address calls in the supplied implementation.", + "first_step": "Bind one reflection and every basis XOR to an actual supplier interface, including all scratch and routing charges.", + "blocked_by": "No hosting, child rank, precision/tape or analytic transfer bridge is supplied." + } + ], + "nonce": "75e0b0e97e175ef7a2c5e1c9c5e9f1a5", + "overlap": { + "open_prs_snapshot": "2026-10-15T18:06:42.717923+00:00", + "discussions_snapshot": "2026-10-15T15:22:22.047084+00:00", + "discussion_records": 1239, + "coverage": "Complete snapshots at stated times, supplemented with targeted REST searches of open and closed PRs and local retained notes/ledger. Discussions stale; no exhaustive code-diff search.", + "closest": [ + "PR1911 projector-only infinite-dihedral tariff (extension, not claimed anew)", + "PR1941 arbitrary-rank idempotents for finite even dihedral groups", + "PR1589 rank-one nilpotents for UT3 central targets", + "PR2290 shallow two-role nilpotent census" + ], + "open_pr_records": 767 + }, + "upstream_checkpoint": { + "commit": "c3c94c2ea2ebcd5d69d1e51b5fe8a36bf79819f5", + "utc": "2026-10-15T18:10Z", + "guidance": "No change; branch fast-forwarded, scientific source pins retained." + } +} diff --git a/research/dihedral-arbitrary-couplings/VERIFY.json b/research/dihedral-arbitrary-couplings/VERIFY.json new file mode 100644 index 0000000000..5bd9857301 --- /dev/null +++ b/research/dihedral-arbitrary-couplings/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/infinite-dihedral-register-bound/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All binary matrices through R=3: all Laurent minors, exact rank factorization, formal C2 gate identities and compiled dirty-input endpoints; all rank-one couplings through R=4 and controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_cli.py" + ], + "timeout_seconds": 120, + "checks": "Git-free read-only replay, authenticated-source rejection, strictly typed receipt rejection and implementation mutation rejection." + } + ] +} diff --git a/research/dihedral-arbitrary-couplings/test_cli.py b/research/dihedral-arbitrary-couplings/test_cli.py new file mode 100644 index 0000000000..c5accfae5f --- /dev/null +++ b/research/dihedral-arbitrary-couplings/test_cli.py @@ -0,0 +1,73 @@ +"""Public CLI checks in a minimal Git-free export.""" +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent + +class CliTests(unittest.TestCase): + def setUp(self): + self.tmp = tempfile.TemporaryDirectory(prefix="dihedral-couplings-") + self.root = Path(self.tmp.name) + self.package = self.root / HERE.relative_to(ROOT) + shutil.copytree(HERE, self.package) + for item in json.loads((HERE/"SOURCES.json").read_bytes())["files"]: + if item["usage"] == "input": + dest = self.root/item["path"] + dest.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT/item["path"], dest) + self.addCleanup(self.tmp.cleanup) + + def call(self): + return subprocess.run([sys.executable,"-I","-O","-B",str(self.package/"verify.py")], + cwd=self.root, capture_output=True, text=True, timeout=60) + + def inventory(self): + return {str(p.relative_to(self.root)): hashlib.sha256(p.read_bytes()).hexdigest() + for p in self.root.rglob("*") if p.is_file()} + + def test_read_only_export(self): + before=self.inventory() + result=self.call() + self.assertEqual(result.returncode,0,result.stderr) + self.assertIn("PASS_DIHEDRAL_ARBITRARY_COUPLINGS",result.stdout) + self.assertEqual(self.inventory(),before) + + def test_source_corruption(self): + source=self.root/"research/infinite-dihedral-register-bound/README.md" + source.write_bytes(source.read_bytes()+b"\nchanged\n") + result=self.call() + self.assertNotEqual(result.returncode,0) + self.assertIn("source SHA mismatch",result.stderr) + + def test_typed_receipt(self): + path=self.package/"RESULT.json" + original=json.loads(path.read_bytes()) + for value in (True,float(original["binary_matrices"])): + altered=dict(original,binary_matrices=value) + path.write_text(json.dumps(altered),encoding="utf-8") + result=self.call() + self.assertNotEqual(result.returncode,0) + self.assertIn("receipt mismatch",result.stderr) + + def test_material_implementation_mutations(self): + path=self.package/"verify.py" + original=path.read_text(encoding="utf-8") + for old,new in [ + ('("xor", 0, 1), ("g", 1, 0), ("xor", 0, 1), ("g", 1, 0)]', + '("xor", 0, 1), ("g", 1, 0), ("xor", 0, 1)]'), + ('best = max(best, value.bit_length()-1-k)', + 'best = max(best, value.bit_length()-1)')]: + self.assertIn(old,original) + path.write_text(original.replace(old,new,1),encoding="utf-8") + result=self.call() + self.assertNotEqual(result.returncode,0) + +if __name__=="__main__": + unittest.main() diff --git a/research/dihedral-arbitrary-couplings/verify.py b/research/dihedral-arbitrary-couplings/verify.py new file mode 100644 index 0000000000..3109f1d029 --- /dev/null +++ b/research/dihedral-arbitrary-couplings/verify.py @@ -0,0 +1,264 @@ +"""Finite corroboration of README's arbitrary-rank dihedral theorem.""" +from __future__ import annotations +import argparse +import hashlib +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent + +def require(ok, message): + if not ok: + raise ValueError(message) + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False) + +def source_check(): + for item in json.loads((HERE / "SOURCES.json").read_bytes())["files"]: + if item["usage"] == "input": + data = (ROOT / item["path"]).read_bytes() + require(hashlib.sha256(data).hexdigest() == item["sha256"], "source SHA mismatch") + blob = hashlib.sha1(b"blob " + str(len(data)).encode() + b"\0" + data).hexdigest() + require(blob == item["git_blob"], "source blob mismatch") + +def rank(rows): + pivots = {} + for x in rows: + while x: + p = x.bit_length() - 1 + if p not in pivots: + pivots[p] = x + break + x ^= pivots[p] + return len(pivots) + +def eye(n): + return tuple(1 << i for i in range(n)) + +def add(a, b): + return tuple(x ^ y for x, y in zip(a, b)) + +def xor(xs): + out = 0 + for x in xs: + out ^= x + return out + +def mul(a, b): + return tuple(xor(b[j] for j in range(len(b)) if row >> j & 1) for row in a) + +def outer(u, v, n): + return tuple(v if u >> i & 1 else 0 for i in range(n)) + +def factor(rows): + """Column-basis factorization, independently recomposed below.""" + n = len(rows) + columns = [sum(((rows[i] >> j) & 1) << i for i in range(n)) for j in range(n)] + basis = [] + for col in columns: + if rank(basis + [col]) > len(basis): + basis.append(col) + lookup = {xor(basis[i] for i in range(len(basis)) if mask >> i & 1): mask + for mask in range(1 << len(basis))} + coordinates = [lookup[col] for col in columns] + return [(u, sum(((c >> i) & 1) << j for j, c in enumerate(coordinates))) + for i, u in enumerate(basis)] + +def pair_mul(a, b): + """Full F2[C2] convolution with binary-matrix coefficients.""" + return (add(mul(a[0], b[0]), mul(a[1], b[1])), + add(mul(a[0], b[1]), mul(a[1], b[0]))) + +def poly_mul(a, b): + result = 0 + while b: + if b & 1: + result ^= a + a <<= 1 + b >>= 1 + return result + +def determinant(matrix): + """Subset expansion in F2[t], independent of the binary rank calculation.""" + n = len(matrix) + values = [0] * (1 << n) + values[0] = 1 + for mask in range(1, 1 << n): + row = mask.bit_count() - 1 + values[mask] = xor(poly_mul(values[mask ^ (1 << j)], matrix[row][j]) + for j in range(n) if mask >> j & 1) + return values[-1] + +def represented(rows): + """Return t*(I+N tensor (I+V)); integer bit j is coefficient of t^j.""" + n = len(rows) + result = [[2 if i == j else 0 for j in range(2*n)] for i in range(2*n)] + for i, row in enumerate(rows): + for j in range(n): + if row >> j & 1: + result[2*i][2*j] ^= 2 + result[2*i][2*j+1] ^= 4 + result[2*i+1][2*j] ^= 1 + result[2*i+1][2*j+1] ^= 2 + return result + +def minor_degree(matrix): + size = len(matrix) + best, tested = 0, 0 + for k in range(1, size+1): + for rr in itertools.combinations(range(size), k): + for cc in itertools.combinations(range(size), k): + value = determinant([[matrix[i][j] for j in cc] for i in rr]) + tested += 1 + if value: + best = max(best, value.bit_length()-1-k) + return best, tested + +def basis_program(u, v, n): + """Row additions taking column basis S to I, hence applying S^-1.""" + theta = (u & v).bit_count() % 2 + columns = [u] + if not theta: + columns.append(next(w for w in range(1, 1 << n) if (v & w).bit_count() % 2)) + for w in range(1, 1 << n): + if not (v & w).bit_count() % 2 and rank(columns + [w]) > len(columns): + columns.append(w) + require(len(columns) == n, "basis completion") + matrix = [sum(((columns[j] >> i) & 1) << j for j in range(n)) for i in range(n)] + ops = [] + def row_add(i, j): + matrix[i] ^= matrix[j] + ops.append(("xor", i, j)) + for j in range(n): + pivot = next(i for i in range(j, n) if matrix[i] >> j & 1) + if pivot != j: + row_add(j, pivot) + row_add(pivot, j) + row_add(j, pivot) + for i in range(n): + if i != j and matrix[i] >> j & 1: + row_add(i, j) + require(tuple(matrix) == eye(n), "basis elimination") + require(len(ops) <= n*(n-1)+3*(n-1), "basis invoice") + return ops, theta + +def compile_rank_one(u, v, n): + before, theta = basis_program(u, v, n) + middle = [("g", 0, 0)] if theta else [ + ("xor", 0, 1), ("g", 1, 0), ("xor", 0, 1), ("g", 1, 0)] + return before + middle + list(reversed(before)), theta + +def identity_data(n, width=2): + return [[1 << (i*width+j) for j in range(width)] for i in range(n)] + +def run(ops, n, width=2): + data = identity_data(n, width) + for kind, i, j in ops: + if kind == "xor": + data[i] = [a ^ b for a, b in zip(data[i], data[j])] + else: + require(kind == "g", "unknown primitive") + data[i] = [data[i][a ^ 1] for a in range(width)] + return data + +def expected(rows, width=2): + n = len(rows) + data = identity_data(n, width) + return [[data[i][a] ^ xor(data[j][a] ^ data[j][a ^ 1] + for j in range(n) if rows[i] >> j & 1) + for a in range(width)] for i in range(n)] + +def normal_word(word): + k, e = 0, 0 + for label in word: + k += (1 if e else -1) if label == "s" else 0 + e ^= 1 + return k, e + +def reduce_word(word): + out = [] + for x in word: + if out and out[-1] == x: + out.pop() + else: + out.append(x) + return out + +def evidence(): + counts = dict(binary_matrices=0, minor_determinants=0, rank_factorizations=0, + rank_one_programs=0, nilpotent_programs=0, coefficient_columns=0, + target_words=0, controls=0) + for n in range(1, 4): + for rows in itertools.product(range(1 << n), repeat=n): + r = rank(rows) + d, tested = minor_degree(represented(rows)) + require(d == r, "Laurent minor degree differs from coupling rank") + counts["minor_determinants"] += tested + factors = factor(rows) + require(len(factors) == r, "factor rank invoice") + combined = (eye(n), (0,)*n) + reconstructed = (0,)*n + ops = [] + for u, v in factors: + one = outer(u, v, n) + reconstructed = add(reconstructed, one) + combined = pair_mul((add(eye(n), one), one), combined) + word, _ = compile_rank_one(u, v, n) + ops.extend(word) + require(reconstructed == rows, "rank factorization changed coupling") + require(combined == (add(eye(n), rows), rows), "rank factors changed formal gate") + gate = (add(eye(n), rows), rows) + require(pair_mul(gate, gate) == (eye(n), (0,)*n), "coupling not involutory") + require(run(ops, n) == expected(rows), "compiled arbitrary coupling endpoint") + counts["binary_matrices"] += 1 + counts["rank_factorizations"] += 1 + for n in range(1, 5): + for u, v in itertools.product(range(1, 1 << n), repeat=2): + word, theta = compile_rank_one(u, v, n) + require(run(word, n, 4) == expected(outer(u, v, n), 4), "rank-one dirty endpoint") + require(sum(x[0] == "g" for x in word) == (1 if theta else 2), "address invoice") + counts["rank_one_programs"] += 1 + counts["nilpotent_programs"] += 1-theta + counts["coefficient_columns"] += 4*n + for k in range(-8, 9): + for e in (0, 1): + word = reduce_word(list(("rs" if k >= 0 else "sr") * abs(k) + "r"*e)) + require(normal_word(word) == (k, e), "attaining formal endpoint") + require(word.count("r") == abs(k+e) and word.count("s") == abs(k), "target tariff") + counts["target_words"] += 1 + nil = (2, 0) + require(mul(nil, nil) == (0, 0) and mul(nil, nil) != nil, "nilpotent control") + counts["controls"] += 1 + require(minor_degree(represented(eye(3)))[0] == 3, "rank underpricing control") + counts["controls"] += 1 + shear = [("xor", 0, 1), ("g", 1, 0), ("xor", 0, 1), ("g", 1, 0)] + require(run(shear[:-1], 2) != expected(nil), "missing dirty restoration accepted") + require(run(shear[1:], 2) != expected(nil), "missing identity summand accepted") + counts["controls"] += 2 + exposed = False + for u, v in itertools.product(range(1, 8), repeat=2): + before, theta = basis_program(u, v, 3) + middle = [("g", 0, 0)] if theta else shear + exposed |= run(list(reversed(before)) + middle + before, 3) != expected(outer(u, v, 3)) + require(exposed, "wrong basis orientation not exposed") + counts["controls"] += 1 + return {"status": "PASS_DIHEDRAL_ARBITRARY_COUPLINGS", **counts} + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--write", action="store_true", help="explicitly replace RESULT.json") + args = parser.parse_args() + source_check() + actual = evidence() + target = HERE / "RESULT.json" + if args.write: + target.write_text(json.dumps(actual, indent=2)+"\n", encoding="utf-8", newline="\n") + else: + require(canonical(json.loads(target.read_bytes())) == canonical(actual), "receipt mismatch") + print(canonical(actual)) + +if __name__ == "__main__": + main()