diff --git a/research/clifford-lattice-rigidity/PROOF.md b/research/clifford-lattice-rigidity/PROOF.md new file mode 100644 index 0000000000..0eee6782e3 --- /dev/null +++ b/research/clifford-lattice-rigidity/PROOF.md @@ -0,0 +1,156 @@ +# Rigidity of Gaussian lattices under local Clifford generators + +This proof was produced by Nick Petalas. Apache-2.0. + +Write O=Z[i], pi=1+i, r>=1 and N=2^r. Let B_r be the Gaussian Newton lattice +from Clear1nsight's PR3382, `research/p104-clifford-exactness`: + + B_r = { f(x)=sum_S a_S x_S : pi^|S| divides a_S }, + E_r = [[1,0],[1,pi]] tensor ... tensor [[1,0],[1,pi]], + B_r = E_r O^N. + +We cite its all-rank maximality and intertwiners. In particular, every integral +Gaussian module invariant under every local ideal butterfly C_j lies inside +B_r. The local physical operators are + + C(a,b)=((a+b+i(a-b))/2, (a+b-i(a-b))/2), + S(a,b)=(a,ib). + +In E_1 coefficient coordinates their matrices are + + A = [[1,1],[0,i]], B = [[1,0],[i,i]]. + +The predecessor proves that B_r is stable under these and the broader affine +address/Clifford monomial alphabet, and that the literal signed-floor word is +exact on B_r. Those exactness/closure theorems are not new claims here. + +## 1. The generated integral order is the whole matrix ring + +Let E_ab denote an ordinary two-by-two matrix unit, with zero-based indices. +Exact multiplication gives + + (A-iI)(B-iI) = -i E_00. + +Indeed the only possibly nonzero entry is (0,0), whose value is +`(1-i)^2+i=-i`, a Gaussian unit. Therefore the unital O-algebra generated by +A and B contains + + E_00 = i (A-iI)(B-iI), + E_01 = E_00 A - E_00, + E_10 = -i (B E_00 - E_00), + E_11 = I-E_00. + +These are all matrix units. Conversely A and B have entries in O. Hence + + O[A,B] = M_2(O). (1) + +At r bits, the generators at bit j act as A or B at that tensor factor and +identity at all others. Each local algebra thus contains its four local matrix +units. Their products over the r distinct factors are every global matrix unit +E_uv, with u,v in {0,1}^r. It follows that + + O[A_1,B_1,...,A_r,B_r] = M_N(O). (2) + +Here the subscripted B_j denotes a coefficient phase matrix, not the Newton +lattice. The argument uses both local generators on every bit; omitting a +phase can invalidate the conclusion. + +## 2. Classification of all invariant integral Gaussian modules + +**Theorem.** Every nonzero O-submodule L of O^N invariant under all the +physical C_j and S_j is of the form + + L = alpha B_r, 0 != alpha in Z[i]. (3) + +The scalar is unique up to a Gaussian unit. Conversely every such scalar +multiple is invariant. In particular there is no further nonhomothetic +integral lattice in this fixed alphabet. + +**Proof.** By the credited maximality theorem, L is contained in B_r. Thus +Lambda=E_r^-1 L is an O-submodule of O^N. It is stable under all coefficient +generators, and hence under their full matrix algebra (2). + +Put J={a in O : a e_0 belongs to Lambda}. This is an ideal. If v belongs +to Lambda, then E_0j v=v_j e_0 belongs to Lambda, so each v_j belongs to J. +Therefore Lambda is contained in J^N. Conversely a e_0 in Lambda implies +a e_j=E_j0(a e_0) in Lambda for every j. Addition gives J^N contained in +Lambda. Thus Lambda=J^N. + +The Gaussian integers form a principal ideal domain, so J=alpha O. Since +Lambda is nonzero, alpha is nonzero. Then L=E_r(alpha O^N)=alpha B_r. +Equality of principal ideals gives uniqueness up to units. The converse +follows from the predecessor's invariant O-module B_r. This also shows that +any nonzero module in scope has full rank and finite index; these need not +be additional hypotheses. The zero module is the sole zero case. + +If desired, the index follows from the known Newton determinant: + + [O^N : alpha B_r] = (alpha*conjugate(alpha))^N + * 2^(r 2^(r-1)). (4) + +The index of B_r itself is predecessor/classical tensor-lattice arithmetic. +The new statement is the absence of any other invariant module shape. + +The hypothesis of Gaussian-module closure matters: it includes arbitrary +Gaussian integer linear combinations, or equivalently additive closure plus +the global i phase. It does not cover correlated, nonlinear or nonadditive +entrance domains. Requiring each local C_j and S_j is stronger than requiring +one particular whole transform and its inverse. + +## 3. Uniform integral quarter closure is impossible in this class + +**Corollary.** No nonzero L in the theorem satisfies + + f in L and f/4 in O^N => f/4 in L. (5) + +This is a closure requirement on all admitted independent sources, not a +claim that every actual quarter operation fails. + +**Proof.** Write L=alpha B_r and m=max(r,4). On the binary cube set + + f(x)=alpha pi^m x_1...x_r. + +Its sole nonzero Newton coefficient is divisible by alpha pi^r, so f belongs +to L. Every coordinate is divisible by four because pi^4=-4 and m>=4. +The quotient f/4 is consequently a Gaussian-integer field. + +After cancelling the nonzero alpha, its top Newton coefficient has pi +valuation m-4. This is strictly below r for every r>=1. Thus f/4 is outside +alpha B_r, contradicting (5). This is a constructive witness for every alpha +and r, not a finite failed search. + +Consequently a uniform replacement lattice with the same independent-input +and local-generator contract cannot repair the quarter-ADD boundary merely +by choosing another invariant lattice. A source in 4L can still be divided +into L. A caller can therefore change the boundary to a divisibility +filtration, restrict the source updates, change the gate alphabet, or prove +a correlated/nonlinear entrance. These alternatives require their own proof +and complete cost; the corollary excludes none of them. + +## 4. Finite corroboration and scope + +The verifier constructs the four matrix units from the displayed A,B words +and checks all sixteen products. For ranks one through seven it tensors the +units and checks the action of every resulting E_uv on a dense coefficient +vector with distinct nonzero Gaussian entries. The two-by-two matrix equality +and written tensor argument establish the operator identity; a dense test +alone would not prove it. + +A separate complete finite module census enumerates all 67 additive subgroups +of (Z[i]/2)^2, imposes scalar i and A,B invariance, and finds exactly the +three scalar-ideal modules: zero, (pi)/(2) in each coordinate, and the whole +module. This checks the first nontrivial ideal sandwich. It does not prove +classification at arbitrary modulus or dimension by enumeration. + +An explicit C-only skew lattice in coefficient coordinates, O e_0 + pi O e_1, +is A-invariant but not B-invariant. Signed fixtures check scalar-ideal +preservation; the universal quarter witness is tested for seven scalars at +each rank through seven. No predecessor scientific replay is performed. + +This is a scoped written classification and quarter-closure obstruction, with +finite exact corroboration. No complete caller, physical/native admission, +precision/tape or recursive cost improvement, new kappa, complete multiplication +theorem, independent human review or formal proof-kernel acceptance follows. +Matrix-unit arguments and the ideal classification for full matrix rings are +classical; the new application is the full integral order and resulting rigidity +of this fixed P104 entrance alphabet. diff --git a/research/clifford-lattice-rigidity/README.md b/research/clifford-lattice-rigidity/README.md new file mode 100644 index 0000000000..48c22dfcb3 --- /dev/null +++ b/research/clifford-lattice-rigidity/README.md @@ -0,0 +1,118 @@ +# All local-Clifford invariant P104 lattices are scalar multiples + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Scoped mathematical proof with finite corroboration. No new kappa.** +Every nonzero Gaussian-integer module of fields on an r-bit cube, invariant +under each local P104 butterfly and each single-bit i phase, is a Gaussian +scalar multiple of the known Newton lattice: + + L = alpha B_r, alpha in Z[i] nonzero, + B_r = { sum_S a_S x_S : (1+i)^|S| divides a_S }. + +Thus no different lattice shape in this fixed alphabet repairs the uniform +quarter-division boundary. For every alpha and r>=1, the explicit field + + f(x) = alpha (1+i)^max(r,4) x_1...x_r + +belongs to L and has integral f/4, while f/4 is outside L. Source-dependent +divisibility filtrations, changed alphabets and nonlinear entrance domains +remain possible; this is not a universal supplier obstruction. + +Clear1nsight's [PR3382](https://github.com/CrocSwap/integer-mult-bounds/pull/3382) +already proves the Newton lattice's exact lifting, phase closure and maximal +integral entrance. Those are cited premises. The new step is the identity + + i(A-iI)(B-iI) = E_00, + A=[[1,1],[0,i]], B=[[1,0],[i,i]], + +which yields every matrix unit. Tensoring gives the full integral matrix +algebra on all coefficient coordinates. Its invariant modules are precisely +J^N for Gaussian ideals J; principality gives the classification above. +[PROOF.md](PROOF.md) gives the all-rank argument and the universal quarter +witness. Classical matrix-unit and principal-ideal methods retain their credit. + +## Reproduction and evidence + +From the repository root, with standard-library CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/clifford-lattice-rigidity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/clifford-lattice-rigidity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/clifford-lattice-rigidity +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/clifford-lattice-rigidity --check-source-history +``` + +Any CPython 3.12 interpreter can replace the local path. Expected marker: +`PASS_CLIFFORD_LATTICE_RIGIDITY ranks=1..7 scalar_classes_only quarter_closure=excluded no_new_kappa`. + +The verifier constructs all four local matrix units and checks all sixteen +products; tensors them through rank seven; exhausts all 67 additive subgroups +of `(Z[i]/2)^2`, retaining exactly the three scalar-ideal modules; and checks +the necessity of the phase premise. Signed scalar-ideal fixtures and 49 integral +quarter counterexamples corroborate the universal proof. No predecessor code +is imported or run. The all-rank result is a written proof, not an extrapolation +from these checks. + +Every run prints a generated SHA256 receipt for the six package files and +writes nothing. Explicit exceptions keep all checks active under optimization. +Generic metadata, committed-byte/source-history checks and hosted CI remain +separate from mathematical acceptance. + +## Limits and decision + +The theorem fixes all local bit butterflies and single-bit i phases, and +requires Gaussian-module closure. It does not classify a smaller caller-specific +alphabet, nonadditive/correlated states or domains exact only after a whole word. +The quarter result excludes a uniform lattice closed under every integral +quarter; it permits a stronger source contract such as `4L -> L`. + +No codecs, physical owners, native realization, movement, full precision/storage +policy, complete signed invoice, fast recursive implementation or actual caller +are supplied. No frontier, supplier or multiplication theorem is changed. +No selected cold replay, Lean/Docker execution, independent human review or +formal proof-kernel acceptance is claimed. Stop at this classification; a +construction needs a changed boundary and its own complete budget. + +The verifier fixes rank<=7 and at most 128 coordinates. Tensor tests have +21,844 row/column pairs in total; the module census has at most 67 subgroups +of a 16-element space and four expansion rounds. Each function is under +60 lines, and receipts read six files capped at 200 KB each. Python-managed +allocation is the explicit Power of Ten deviation; live collections are bounded +by these domains. No recursion, network, subprocess, external mutable state or +dynamic code loading is used. Both registered modes use warnings as errors. + +## Open next questions + +1. Can a pinned caller maintain a divisibility filtration through quarter ADDs? + First trace its actual scalar coefficients and phase/butterfly generators. + A paid codec, independent target contract, native/recursive costs and physical + storage remain blockers. The uniform-lattice obstruction does not settle this. +2. Can a smaller actual local-generator alphabet retain a nonhomothetic + lattice that helps a complete bill? First fix that exact alphabet and every + required prefix; omitting the phase already allows skew lattices. No + smaller-alphabet classification or favourable cost is supplied here. + +Structured questions and scope are in [TASK.json](TASK.json). + +## Sources and credit + +Credit Clear1nsight's PR3382 for the Gaussian Newton lattice, all-rank maximal +integral entrance, coefficient intertwiners, exact lifting and actual collector +binding. Credit Ross Richardson's PR3068 for the earlier phase/quarter closure +boundary; Tekalign's PR3025/3033 for the floor word; Nick Petalas's PR3035/3037 +for the distinct period lattice; Arham Tahir's PR3046 for inverse-domain work; +and ywz65's PR2586 with the retained P104/native, Clifford, geometry and numerical +lineage. The classical Clifford/Barnes-Wall context remains credited by PR3382. +These predecessors are cited, not recertified as this contribution. + +[SOURCES.json](SOURCES.json) pins the statements, task catalogue and selected +record at canonical main `19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority +revision 8. The original helper-inventory card is explicitly changed to this +numerical-interface obstruction; no complete productive/paid invoice is asserted. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19221619) +predicted an exactness theorem already covered by merged PR3382. The +[scope correction](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19221942) +credits that overlap. This package claims only the subsequent rigidity theorem +and its uniform quarter-closure consequence. diff --git a/research/clifford-lattice-rigidity/SOURCES.json b/research/clifford-lattice-rigidity/SOURCES.json new file mode 100644 index 0000000000..098d06c55a --- /dev/null +++ b/research/clifford-lattice-rigidity/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-invariant-lifting-lattice/README.md", + "usage": "provenance", + "git_blob": "92a71faba58a00c1b145dc722fde38a0bf75ffb8", + "sha256": "426721af0f8b391aa56ce2c6968b78bf4e9b386e794eb5b4854d88243762c19d" + }, + { + "path": "research/p104-invariant-lifting-lattice/PROOF.md", + "usage": "provenance", + "git_blob": "5dfde304a04513f302de41861e9131f1446595b9", + "sha256": "7a34534dd75a2ae4b77d9779fee9ce43372d8a6d2038c6a763deff1f99ce7830" + }, + { + "path": "research/p104-reversible-lifting/README.md", + "usage": "provenance", + "git_blob": "05eddb238528e00e0985a2cdb2e04e7595cbbb51", + "sha256": "051a886e9777b6ace444920df1fd46c285dc0251d7ef6fac570dc12cca7c4bc8" + }, + { + "path": "research/p104-clifford-exactness/README.md", + "usage": "provenance", + "git_blob": "581edcfcbcc31cf78c02f9873c14094f9b37e1bf", + "sha256": "7374b6b360fa6755f68ee513467de1c0436a48a22a9584a3c27687e73a16a7db" + }, + { + "path": "research/p104-clifford-exactness/PROOF.md", + "usage": "provenance", + "git_blob": "10b3202c788b5b03188eed91181441dfd793ff7f", + "sha256": "1ca8c0e7e78f0f39de6cff7accc68ccd3901bfb50759bf7a2e2896bcf63bf081" + } + ] +} diff --git a/research/clifford-lattice-rigidity/TASK.json b/research/clifford-lattice-rigidity/TASK.json new file mode 100644 index 0000000000..d2d083da1b --- /dev/null +++ b/research/clifford-lattice-rigidity/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a changed helper inventory earn productive credit that survives completion, compilation and the actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Specify all arbitrary inputs, owned fields, restored outputs and a physically legal consumer. Compare complete P and T, including target debits and precision/stock costs. #5599 is a positive control for target refinement, not permission to split every helper for free. #5614 is a hypothetical compiler budget, not an emitted 145-split word. Stop at the first unpaid boundary or a failing optimistic full bill.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "productive helper", + "target refinement", + "5599", + "5614" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Classify all Gaussian-integer modules invariant under every local P104 butterfly and single-bit i phase as scalar multiples of the credited Newton lattice; exclude uniform integral quarter closure for every nonzero such module.", + "scope_change_reason": "Original attack on the quarter-ADD blocker. Main overlap identified PR3382 as the owner of the initially predicted exactness/maximality/phase result. Only the subsequent full-matrix-order rigidity theorem and universal quarter witness are new here.", + "bottleneck_link": "The quarter boundary cannot be repaired by a different uniform Clifford-invariant Gaussian lattice: the full local coefficient order forces a scalar multiple. A changed source filtration/alphabet and complete invoice remain necessary.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified rigidity/closure obstruction and package it. No predecessor audit, changed supplier or dependent construction search.", + "outcome": "completed", + "evidence": "PROOF.md and verify.py: generated matrix units and their sixteen products, all tensor units at ranks 1..7, complete 67-subgroup modulo-two census, scalar ideal fixtures and 49 quarter witnesses.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a pinned caller maintain a divisibility filtration through quarter ADDs?", + "why_it_matters": "Integral quarter division can leave the new phase-stable exactness domain.", + "first_step": "Trace every scalar coefficient and address/phase generator of one literal collector.", + "blocked_by": "Full codec, native/recursive bill, target independence and storage/ownership contract." + }, + { + "question": "Can a smaller actual generator alphabet preserve a useful nonhomothetic entrance?", + "why_it_matters": "The classification requires every local butterfly and single-bit phase; removing a phase permits a skew lattice.", + "first_step": "Pin one caller alphabet and every required prefix before classifying its invariant modules.", + "blocked_by": "A complete caller and favourable paid codec/native/storage tariff; no smaller-alphabet search is performed here." + } + ], + "coordination": { + "source_pr": "original", + "source_author": "original", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19221619", + "upstream_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "priority_revision": 8, + "conceptual_predecessor_pr": 3382, + "progress_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19221942" + }, + "environment": { + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "version": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "Python standard library only" + } +} diff --git a/research/clifford-lattice-rigidity/VERIFY.json b/research/clifford-lattice-rigidity/VERIFY.json new file mode 100644 index 0000000000..3b56585ca2 --- /dev/null +++ b/research/clifford-lattice-rigidity/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "New integral-order rigidity: generated matrix units/products, tensor units through rank seven, all 67 additive subgroups modulo two, scalar ideals and universal quarter witnesses." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same rigidity and boundary corroboration under optimization, with explicit exceptions active." + } + ] +} diff --git a/research/clifford-lattice-rigidity/verify.py b/research/clifford-lattice-rigidity/verify.py new file mode 100644 index 0000000000..e7c35f5b96 --- /dev/null +++ b/research/clifford-lattice-rigidity/verify.py @@ -0,0 +1,247 @@ +"""Exact matrix-unit and invariant-lattice rigidity corroboration. + +Produced by Nick Petalas. Apache-2.0. +""" +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +Z = (0, 0) +O = (1, 0) +I = (0, 1) +PI = (1, 1) +FILES = ("README.md", "PROOF.md", "verify.py", "TASK.json", "SOURCES.json", "VERIFY.json") + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def add(a, b): + return (a[0] + b[0], a[1] + b[1]) + + +def neg(a): + return (-a[0], -a[1]) + + +def mul(a, b): + return (a[0]*b[0] - a[1]*b[1], a[0]*b[1] + a[1]*b[0]) + + +def scale(matrix, value): + return tuple(mul(value, x) for x in matrix) + + +def matrix_add(a, b): + return tuple(add(x, y) for x, y in zip(a, b)) + + +def matrix_mul(a, b): + need(len(a) == len(b) == 4, "fixed two-by-two matrices") + return tuple(add(mul(a[2*r], b[c]), mul(a[2*r+1], b[2+c])) + for r in range(2) for c in range(2)) + + +def units(): + identity = (O, Z, Z, O) + butterfly = (O, O, Z, I) + phase = (O, Z, I, I) + minus_i = scale(identity, neg(I)) + e00 = scale(matrix_mul(matrix_add(butterfly, minus_i), + matrix_add(phase, minus_i)), I) + e01 = matrix_add(matrix_mul(e00, butterfly), scale(e00, (-1, 0))) + e10 = scale(matrix_add(matrix_mul(phase, e00), scale(e00, (-1, 0))), neg(I)) + e11 = matrix_add(identity, scale(e00, (-1, 0))) + result = (e00, e01, e10, e11) + for index, matrix in enumerate(result): + need(matrix == tuple(O if j == index else Z for j in range(4)), "generated matrix unit") + for a, b in product(range(4), repeat=2): + expected = result[2*(a//2)+b%2] if a%2 == b//2 else (Z,)*4 + need(matrix_mul(result[a], result[b]) == expected, "matrix-unit multiplication law") + return result, butterfly, phase + + +def rank_of(values): + size = len(values) + need(2 <= size <= 128 and size & (size-1) == 0, "rank 1..7 only") + return size.bit_length()-1 + + +def apply_local(values, bit, matrix): + rank = rank_of(values) + need(0 <= bit < rank and len(matrix) == 4, "local matrix domain") + out = list(values) + for address in range(len(values)): + if not address & (1 << bit): + other = address | (1 << bit) + a, b = values[address], values[other] + out[address] = add(mul(matrix[0], a), mul(matrix[1], b)) + out[other] = add(mul(matrix[2], a), mul(matrix[3], b)) + return out + + +def tensor_unit_checks(local_units): + records = [] + for rank in range(1, 8): + size = 1 << rank + values = [(j+1, 2*j+3) for j in range(size)] + for row, column in product(range(size), repeat=2): + actual = list(values) + for bit in range(rank): + unit = local_units[2*((row >> bit)&1)+((column >> bit)&1)] + actual = apply_local(actual, bit, unit) + expected = [values[column] if j == row else Z for j in range(size)] + need(actual == expected, "tensor product gives the requested global matrix unit") + records.append({"rank": rank, "global_units": size*size}) + return records + + +def divide_pi(value): + a, b = value + need((a-b) % 2 == 0, "nonintegral Gaussian division") + return ((a+b)//2, (b-a)//2) + + +def power_pi(exponent): + need(0 <= exponent <= 7, "fixed Gaussian power bound") + value = O + for _ in range(exponent): + value = mul(value, PI) + return value + + +def encode(values): + rank = rank_of(values) + out = [mul(value, power_pi(mask.bit_count())) for mask, value in enumerate(values)] + for bit in range(rank): + for mask in range(len(out)): + if mask & (1 << bit): + out[mask] = add(out[mask], out[mask ^ (1 << bit)]) + return out + + +def member(values): + rank = rank_of(values) + out = list(values) + for bit in range(rank): + for mask in range(len(out)): + if mask & (1 << bit): + out[mask] = add(out[mask], neg(out[mask ^ (1 << bit)])) + for mask, value in enumerate(out): + for _ in range(mask.bit_count()): + if (value[0]-value[1]) % 2: + return False + value = divide_pi(value) + return True + + +def gaussian_divides(divisor, value): + norm = divisor[0]**2 + divisor[1]**2 + need(norm > 0, "nonzero ideal generator") + numerator = mul(value, (divisor[0], -divisor[1])) + return numerator[0] % norm == numerator[1] % norm == 0 + + +def quotient(value, divisor): + need(gaussian_divides(divisor, value), "exact Gaussian quotient") + norm = divisor[0]**2 + divisor[1]**2 + a, b = mul(value, (divisor[0], -divisor[1])) + return (a//norm, b//norm) + + +def scalar_lattice_member(values, scalar): + if not all(gaussian_divides(scalar, value) for value in values): + return False + return member([quotient(value, scalar) for value in values]) + + +def quarter_controls(): + scalars = (O, I, PI, (2, 0), (2, 1), (3, -1), (-7, 4)) + cases = 0 + for rank in range(1, 8): + size = 1 << rank + basis = [Z]*(size-1) + [power_pi(max(rank, 4))] + for scalar in scalars: + values = [mul(scalar, value) for value in basis] + need(scalar_lattice_member(values, scalar), "scaled lattice quarter entrance") + need(all(x % 4 == 0 for z in values for x in z), "quarter has integral coordinates") + divided = [tuple(x//4 for x in z) for z in values] + need(not scalar_lattice_member(divided, scalar), "every scalar lattice fails quarter closure") + cases += 1 + return cases + + +def residue_action(value, matrix): + vector = [((value >> (2*j))&1, (value >> (2*j+1))&1) for j in range(2)] + image = apply_local(vector, 0, matrix) + return sum(((a % 2)+2*(b % 2)) << (2*j) for j, (a, b) in enumerate(image)) + + +def finite_module_census(butterfly, phase): + """All 67 additive subgroups of (Z[i]/2)^2, then impose i,C,S.""" + spaces = {frozenset({0})} + for _ in range(4): + next_spaces = set(spaces) + for space in spaces: + for value in range(16): + next_spaces.add(frozenset(space | {x ^ value for x in space})) + need(len(next_spaces) <= 67, "bounded complete subgroup census") + spaces = next_spaces + need(len(spaces) == 67, "all binary dimension-four subspaces") + scalar_i = (I, Z, Z, I) + stable = [] + for _, ordered in sorted((len(s), tuple(sorted(s))) for s in spaces): + space = frozenset(ordered) + if all(residue_action(v, m) in space for v in space for m in (scalar_i, butterfly, phase)): + stable.append(sorted(space)) + need(stable == [[0], [0, 3, 12, 15], list(range(16))], "only the three scalar ideals survive") + for vector in ([O, Z], [Z, PI]): + need(gaussian_divides(PI, apply_local(vector, 0, butterfly)[1]), "C-only skew lattice is invariant") + need(not gaussian_divides(PI, apply_local([O, Z], 0, phase)[1]), "phase premise is necessary") + return {"additive_subgroups": 67, "invariant": stable, "C_only_skew_counterexample": True} + + +def ideal_preservation(butterfly, phase): + count = 0 + for rank in range(1, 8): + size = 1 << rank + for scalar in (O, PI, (2, 1)): + coefficients = [mul(scalar, (j-17, 3*j+2)) for j in range(size)] + physical = encode(coefficients) + need(scalar_lattice_member(physical, scalar), "independent coefficient fixture") + for bit in range(rank): + for matrix in (butterfly, phase): + image = apply_local(coefficients, bit, matrix) + need(scalar_lattice_member(encode(image), scalar), "scalar ideal invariant") + count += 1 + return count + + +def hashes(): + root = Path(__file__).resolve().parent + result = {} + for name in FILES: + content = (root/name).read_bytes() + need(len(content) <= 200_000, "bounded receipt source") + result[name] = sha256(content).hexdigest() + return result + + +def main(): + local_units, butterfly, phase = units() + result = {"local_units": 4, "local_unit_products": 16, + "tensor_units": tensor_unit_checks(local_units), + "finite_module": finite_module_census(butterfly, phase), + "ideal_generator_checks": ideal_preservation(butterfly, phase), + "integral_quarter_counterexamples": quarter_controls(), + "sha256": hashes()} + print(json.dumps(result, sort_keys=True)) + print("PASS_CLIFFORD_LATTICE_RIGIDITY ranks=1..7 scalar_classes_only quarter_closure=excluded no_new_kappa") + + +if __name__ == "__main__": + main()