diff --git a/research/a1-dihedral-multiplicity-matrix/PROOF.md b/research/a1-dihedral-multiplicity-matrix/PROOF.md new file mode 100644 index 0000000000..174f183807 --- /dev/null +++ b/research/a1-dihedral-multiplicity-matrix/PROOF.md @@ -0,0 +1,119 @@ +# A concrete multiplicity operator for the dihedral component + +This contribution was produced by Nick Petalas. New material is Apache-2.0. +Claim type: scoped written proof with an exact finite matrix certificate. + +## Input and predecessor boundary + +Use the signed-orbit basis of the historical c=1, joint (+1,+1) space E and +its integer matrix B=4A_1 from unpaidmoon #6964. They are the two live JSON +inputs under `research/a1-joint-216-charpoly/evidence/`. E has dimension 216. +This package takes that representation and B as inputs. It does not rebuild +its characteristic polynomial or certify its origin as a physical operator. + +The question and dihedral generators are unpaidmoon +[#7065](https://github.com/CrocSwap/integer-mult-bounds/pull/7065), head +`ee0202a8eafa4c0b84bef97ecfb5691f6affc9c6`. Its PROOF.md, sections "Operator +and group" and "The isotypic component", fixes the following convention. +The coordinate signed permutation has output i equal to eps[i] times input +inv[i]. Its label map sends each query port to the port of the corresponding +canonical root. Extend that map linearly to F2^9. On the 4096 coordinates +(i,a), it acts by the coordinate permutation, its sign, and that label map. + +For R use inv=(0,1,6,7,3,2,5,4) and minus signs at 0,7. For U use +inv=(0,1,2,3,7,6,5,4), with all signs positive. In the pinned E basis they +are signed permutation matrices. The new checker derives those matrices +from the pinned query and the supplied orbit vectors, without importing any +predecessor executable. + +Put + + P6 = 2I + R - R^2 - 2R^3 - R^4 + R^5, + W = image_Q(P6). + +The checker verifies P6^2=6P6 and trace(P6)=768. Since an idempotent over Q +has eigenvalues zero and one, rank(P6)=128. This identifies exactly the +component named W in #7065; no census of the full signed stabilizer is needed. + +## Explicit construction + +All indices below are zero based. For each j=0,...,215 form the integer column + + v_j = (I+U) P6 e_j. + +Scan j in increasing order. Retain a column precisely when it is independent +over Q of the previously retained columns. The rule is unambiguous and the +checker finds 64 retained columns. Let V be their 216-by-64 matrix. Every +column has two or three nonzero entries. Thus this is a concrete basis +specified by fixed input bytes and rational arithmetic, without a search seed +or an arbitrary choice of a complement. + +Express each Bv_j in this basis. Define the 64-by-64 matrix K by + + 2 B V = V K. (1) + +The checker performs exact rational elimination for this construction. Every +entry of K is an integer. Define T=K/8, so A_1 V=V T. +The `--matrix` command emits every entry of K and every retained column of V, +together with the selected source-column indices and a canonical SHA256. +No predecessor polynomial is used to select or compute an entry of K. + +Let C=[V,RV]. The exact identities checked on every column are + + U V = V, + R^2 V = RV - V, + U RV = V - RV, + P6 V = 6V, + 2 B RV = RV K. (2) + +They imply P6 RV=6RV because P6 is a polynomial in R. Consequently image(C) +is contained in W. A separate dense modular elimination finds rank(C)=128; +a nonzero minor modulo 1000003 is also nonzero over Q. Thus C is an +isomorphism Q^128 -> W. In its coordinates, + + C^-1 (A_1|W) C = [[T,0],[0,T]], + C^-1 (R|W) C = [[0,-I],[I,I]], + C^-1 (U|W) C = [[I,I],[0,-I]]. (3) + +Here C^-1 means the inverse onto W, not an inverse of a rectangular map on +all of E. Equations (1)-(3) construct the multiplicity-space operator and +its actual intertwiner, rather than infer its existence from a squared +characteristic polynomial. The dihedral action is the usual rational +2-dimensional representation on the displayed two blocks. The commutant +therefore has the displayed two equal copies of T. + +## Exact claim and remaining arithmetic question + +The output T is dyadic. Its least positive common denominator in this basis +is exactly eight, certified by 8T=K integral and an odd entry of K. This is +an explicit rational answer to the matrix part of #7065's question. It does +not provide the integer matrix of T requested there. In particular, the +integral matrix K represents 8A_1, not A_1. No normalization factor is free. + +As a consequence of (3), chi_(A_1|W)=chi_T^2. If the characteristic-polynomial +result of #7065 is used as a cited premise, uniqueness of the monic square +root in Q[x] gives chi_T=q, with q exactly as published there. This package +neither recomputes q nor independently verifies that predecessor result. +Likewise it computes no new zero-eigenspace or shifted rank of B. + +## Certificate and verification scope + +The replay constructs the matrix, verifies all exact identities, and checks +rank with an independently encoded dense modular elimination. A further dense +integer product checks both operator blocks directly. The output receipt binds +all six package files and all three live inputs by SHA256. `--matrix` includes +the complete executable certificate. The receipt is computed, never handwritten. + +Controls change an entry of K, omit or duplicate a basis column, rescale K +incorrectly, or change its domain basis without changing K. They distinguish +one 64-dimensional block from the required 128-dimensional component, and +verify that the component is proper in E. These are finite certificate controls, +not an exhaustive perturbation census. + +The result is exact linear algebra on the stated pinned inputs. It supplies no +native decoder, physical realization, changed recursive invoice, new kappa, +selected-frontier change or complete multiplication theorem. Numerical rounding, +source access, dirty restoration, ownership, frames, storage/tapes, compiler +closure and outer recovery remain separate obligations. Independent human and +formal proof-kernel review are unclaimed. No Lean, Docker, selected cold replay, +degree-881 replay or predecessor characteristic-polynomial suite is run. diff --git a/research/a1-dihedral-multiplicity-matrix/README.md b/research/a1-dihedral-multiplicity-matrix/README.md new file mode 100644 index 0000000000..8ddca678d0 --- /dev/null +++ b/research/a1-dihedral-multiplicity-matrix/README.md @@ -0,0 +1,106 @@ +# An explicit dyadic 64-dimensional multiplicity operator + +This contribution was produced by Nick Petalas. Apache-2.0. + +A new exact basis exposes the 128-dimensional dihedral component W of the +historical A_1 centre block as two equal 64-dimensional operator blocks: + + C^-1 (A_1|W) C = diag(T,T), T=K/8, K integral. + +The basis C=[V,RV] is explicit; each column of V has only two or three nonzero +entries in the pinned 216-dimensional orbit basis. The least common denominator +of T in this basis is eight. The complete matrix and intertwiner are emitted +by the command below, with a generated source-bound receipt. + +Claim type: scoped written proof with an exact finite matrix certificate. +This is a partial answer to unpaidmoon +[#7065](https://github.com/CrocSwap/integer-mult-bounds/pull/7065), Open next +question 2, which requests an integer multiplicity operator. The rational +operator is now concrete; a change of lattice giving an integer T remains open. +The predecessor's characteristic polynomial is cited, rather than replayed. +No new kappa is claimed. [PROOF.md](PROOF.md) gives the exact construction, +intertwining identities and distinction between T and its integer dilation K. + +## Reproduce + +From the repository root, CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/a1-dihedral-multiplicity-matrix/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/a1-dihedral-multiplicity-matrix/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/a1-dihedral-multiplicity-matrix +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/a1-dihedral-multiplicity-matrix --check-source-history +``` + +Replace the executable with another CPython 3.12 path if needed. The standalone +checker authenticates its three live JSON inputs before constructing the result. +It imports no predecessor program. Normal replay writes nothing. To retain the +complete new matrix and basis, add `--matrix --emit /absolute/new/scratch/result.json` +to a direct command. Receipt paths inside the checkout and existing files reject. +The matrix convention is `T=K/8`, `C=[V,RV]`, `2BC=C diag(K,K)` for B=4A_1. + +The marker is `PASS_A1_DIHEDRAL_MULTIPLICITY_MATRIX`. Every entry of both +operator blocks is checked exactly, all new group-action identities are checked, +and dense modular elimination proves the doubled basis is independent. Controls +reject corrupted matrices, missing or repeated columns, a wrong scale and an +unmatched domain-basis change. The integer K has 668 nonzero entries in [-64,96]. The doubled basis has +rank 128; a separate dense calculation checks all 27,648 operator identity +entries, and nine semantic controls pass. The canonical certificate SHA256 is +`98ceb6e760b187a30e185e3b5dcd4041018801bca9ea0d60c94631001e86e7f7`. +Warning-strict normal and optimized runs on CPython 3.12.15 take about 0.22 +seconds each locally, below their separate 120-second limits. These are timeout +checks, not performance comparisons. Counts and hashes are generated by the verifier. +Finite certificate verification and the written argument have no proof-kernel or +independent human acceptance claim. Hosted CI status belongs in the PR body. + +## Scope, sources and credit + +[SOURCES.json](SOURCES.json) pins the main-tree input bytes and historical card +and selected-record provenance at `e54523517d0f03e58352e647c403a5af3e525a57`. +The formal-interface-lemma card changes to a constructive algebraic side result, +with no formalization or discharge of a selected framework assumption. The first +source-binding orientation command passed for selected kappa `0.00363005817`. +The output is tied to one historical centre query, not the selected physical word. + +Credit unpaidmoon #7065 at `ee0202a8eafa4c0b84bef97ecfb5691f6affc9c6` for W, +its dihedral generators, polynomial and explicit-matrix question; unpaidmoon +#6964 for the orbit basis and B; #6944/#7008/#7023 for the sign and normalizer +splittings; JoyboyBrian for the initial handoff; Ali Romman #4958/#4720 for the +query/Bell action; Krzysztof Wojt for the degree-881 certificate; and the retained +#1719 representation lineage. Nick Petalas #5120/#6302/#7172 are related +annihilator and width bounds, not inputs or steps of this construction. +The elementary representation and elimination methods are classical. + +Entry checks read live open/account PRs, recent handoffs and active Discussions, +main-tree and merged object/formula searches, and the relevant open PR bodies. +The cached helper covered 760 open PRs and 7347 Discussion records with reported +complete pagination; its sparse local notes covered only 208 of 10178 paths. +Separate Git searches covered omitted main READMEs. Unpublished work and arbitrary +historical diffs remain outside that bounded overlap picture. +[Advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19571932). + +## Open next questions + +- Can an explicit invariant lattice turn this particular T into an integer + matrix with a similarly sparse intertwiner? Begin with the emitted dyadic + matrix and retain its factor of eight. No such lattice basis is supplied. +- Can a physical consumer use this multiplicity decomposition at a favorable + complete cost? First specify its source/target access, actual basis conversion, + dirty restoration and complete recursive bill. Those costs are unknown here. + +No native or rounded execution, selected cold replay, degree-881 replay, Lean, +Docker, new kappa, supplier admission or selected-frontier change is supplied. +Independent human and formal proof-kernel review are unclaimed. + +## Implementation bounds + +The terminating checker has no recursion, subprocesses, network or generated +code. Dimensions are fixed at 4096 ambient coordinates, 216 input coordinates, +128 output-basis columns and a 64-by-64 multiplicity matrix. JSON reads are capped +at two million bytes. Every algebraic loop ranges over those bounded finite +collections. Python's managed arithmetic allocates dynamically; this is the +Power of Ten fixed-allocation deviation, with fixed domains bounding live data. +The optional receipt stream is closed on every exit. All functions are below +60 lines. Explicit exceptions preserve checks under optimized Python. +Warning-strict normal/optimized execution and source compilation are the available +diagnostics. No external static analyzer or allocator instrumentation is claimed. diff --git a/research/a1-dihedral-multiplicity-matrix/SOURCES.json b/research/a1-dihedral-multiplicity-matrix/SOURCES.json new file mode 100644 index 0000000000..542a3b36e0 --- /dev/null +++ b/research/a1-dihedral-multiplicity-matrix/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/a1-joint-216-charpoly/evidence/basis.json", + "usage": "input", + "git_blob": "5e524a41ed1c65017b7d902b5445aedd2eb606ff", + "sha256": "e198cd71f4100d2629ecc25fb40b135a8c18c7756be8bc80bf24d7b349af418a" + }, + { + "path": "research/a1-joint-216-charpoly/evidence/matrix.json", + "usage": "input", + "git_blob": "23bccaef6f24e6e644bdba81f58e9217787ab16c", + "sha256": "44f40ad5a12daf7c8493b42e1e9ddc4ef338b317ee5fdfc6de1b413642ca97aa" + }, + { + "path": "research/centre-polynomial-cache-limits/frozen/work/centre-encoding-campaign-20261014/lanes/circuit-interface/INTERFACE.json", + "usage": "input", + "git_blob": "4201e9a04c12273b919e2cae60a6b6482c8150f3", + "sha256": "5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3" + } + ] +} diff --git a/research/a1-dihedral-multiplicity-matrix/TASK.json b/research/a1-dihedral-multiplicity-matrix/TASK.json new file mode 100644 index 0000000000..bb198c2e48 --- /dev/null +++ b/research/a1-dihedral-multiplicity-matrix/TASK.json @@ -0,0 +1,108 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Construct an explicit dyadic 64-dimensional multiplicity operator and rational intertwiner for the historical A1 dihedral component W of dimension 128.", + "scope_change_reason": "The named source asks for an explicit multiplicity matrix; this is a constructive algebraic side result, not a formal caller binding or a replay of the predecessor polynomial.", + "bottleneck_link": "An explicit smaller operator and intertwiner make one historical centre decoder interface concrete. No physical conversion tariff or selected-supplier improvement is supplied.", + "budget_minutes": 60, + "stop_rule": "Stop at the first exact multiplicity-space compression; retain the integer-lattice and physical-consumer questions.", + "outcome": "completed", + "evidence": "PROOF.md and the deterministic source-bound matrix certificate emitted by verify.py; exact intertwining, group action, scaled projector identities and independent dense modular rank.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an explicit invariant lattice make this T integral with a sparse intertwiner?", + "why_it_matters": "The source asks for an integer matrix of T, while the new matrix is dyadic with denominator eight.", + "first_step": "Use the emitted K/8 and construct an invariant lattice; retain every basis-conversion denominator.", + "blocked_by": "No such lattice basis is supplied." + }, + { + "question": "Can a fully priced physical consumer use this decomposition?", + "why_it_matters": "Algebraic compression alone does not change the paid recursive moment.", + "first_step": "Pin source/target access and price basis conversions, dirty restoration and all caller costs.", + "blocked_by": "No physical consumer or complete tariff is supplied." + } + ], + "predecessor": { + "pr": 7065, + "author": "unpaidmoon", + "head": "ee0202a8eafa4c0b84bef97ecfb5691f6affc9c6", + "role": "W, dihedral generators and explicit-matrix question; polynomial cited, not replayed" + }, + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19571932" +} diff --git a/research/a1-dihedral-multiplicity-matrix/VERIFY.json b/research/a1-dihedral-multiplicity-matrix/VERIFY.json new file mode 100644 index 0000000000..39e396dc37 --- /dev/null +++ b/research/a1-dihedral-multiplicity-matrix/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/a1-joint-216-charpoly/evidence/basis.json", + "research/a1-joint-216-charpoly/evidence/matrix.json", + "research/centre-polynomial-cache-limits/frozen/work/centre-encoding-campaign-20261014/lanes/circuit-interface/INTERFACE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Construct the new matrix and intertwiner; exact projector and dihedral identities, two operator blocks, dense rank and semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the complete finite certificate with optimization; explicit acceptance guards remain active." + } + ] +} diff --git a/research/a1-dihedral-multiplicity-matrix/verify.py b/research/a1-dihedral-multiplicity-matrix/verify.py new file mode 100644 index 0000000000..87f290724e --- /dev/null +++ b/research/a1-dihedral-multiplicity-matrix/verify.py @@ -0,0 +1,337 @@ +#!/usr/bin/env python3 +"""Construct and certify the dyadic multiplicity operator for the pinned A1 W. + +New construction produced by Nick Petalas. Apache-2.0. +No predecessor executable or characteristic-polynomial computation is run. +""" +import argparse +import hashlib +import json +import math +from fractions import Fraction +from pathlib import Path +import sys + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +EVIDENCE = "research/a1-joint-216-charpoly/evidence/" +QUERY = ("research/centre-polynomial-cache-limits/frozen/work/" + "centre-encoding-campaign-20261014/lanes/circuit-interface/INTERFACE.json") +FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") +R_INV = (0, 1, 6, 7, 3, 2, 5, 4) +R_EPS = (-1, 1, 1, 1, 1, 1, 1, -1) +U_INV = (0, 1, 2, 3, 7, 6, 5, 4) +CHARACTER = (2, 1, -1, -2, -1, 1) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def bounded_json(path): + raw = path.read_bytes() + need(len(raw) <= 2_000_000, "JSON capacity") + return json.loads(raw), raw + + +def inputs(): + sources, _ = bounded_json(PACKAGE / "SOURCES.json") + loaded = {} + hashes = {} + for row in sources["files"]: + if row["usage"] == "input": + obj, raw = bounded_json(ROOT / row["path"]) + digest = hashlib.sha256(raw).hexdigest() + need(digest == row["sha256"], "input hash: " + row["path"]) + loaded[row["path"]] = obj + hashes[row["path"]] = digest + vectors = [dict(v) for v in loaded[EVIDENCE + "basis.json"]["vectors"]] + matrix = loaded[EVIDENCE + "matrix.json"]["rows"] + query = loaded[QUERY] + ports = list(map(int, query["ports"])) + columns = [tuple(int(query["R"][i].get(str(j), 0)) for i in range(8)) + for j in range(112)] + need(len(vectors) == len(matrix) == 216, "216-space input dimension") + need(all(len(row) == 216 for row in matrix), "square input matrix") + need(all(type(x) is int and -28 <= x <= 28 for row in matrix for x in row), + "input matrix entry range") + need(len(ports) == len(set(ports)) == 112, "query ports") + need(all(0 < p < 512 for p in ports), "nine-bit port") + need(all(v and all(0 <= i < 4096 and c in (-1, 1) for i, c in v.items()) + for v in vectors), "signed orbit basis entries") + need(sum(len(v) for v in vectors) == len({i for v in vectors for i in v}), + "disjoint orbit supports") + return vectors, matrix, ports, columns, hashes + + +def normalize(vector): + need(len(vector) == 8 and any(vector), "nonzero root") + first = next(x for x in vector if x) + need(first in (-1, 1), "root sign") + return tuple(first * x for x in vector) + + +def label_action(inv, eps, ports, columns): + need(sorted(inv) == list(range(8)) and len(eps) == 8, "coordinate permutation") + need(all(s in (-1, 1) for s in eps), "coordinate signs") + lookup = {normalize(c): p for c, p in zip(columns, ports, strict=True)} + mapping = {} + for c, p in zip(columns, ports, strict=True): + image = normalize(tuple(eps[i] * c[inv[i]] for i in range(8))) + need(image in lookup, "root leaves query") + mapping[p] = lookup[image] + linear = {0: 0} + for p in ports: + if p not in linear: + linear.update({a ^ p: b ^ mapping[p] for a, b in list(linear.items())}) + need(len(linear) <= 512, "label-map capacity") + need(len(linear) == len(set(linear.values())) == 512, "label automorphism") + need(all(linear[a] == b for a, b in mapping.items()), "linear label agreement") + return linear + + +def orbit_action(inv, eps, ports, columns, vectors): + linear = label_action(inv, eps, ports, columns) + sigma = [inv.index(i) for i in range(8)] + owners = {i: (j, c) for j, v in enumerate(vectors) for i, c in v.items()} + result = [] + for v in vectors: + image = {sigma[i // 512] * 512 + linear[i % 512]: c * eps[sigma[i // 512]] + for i, c in v.items()} + pivot = min(image) + need(pivot in owners, "actor leaves pinned space") + j, s = owners[pivot] + s *= image[pivot] + need(image == {i: s * c for i, c in vectors[j].items()}, "orbit action") + result.append((j, s)) + need(len({j for j, _ in result}) == 216, "signed permutation on E") + return result + + +def add(left, right, scale=1): + need(len(left) <= 216 and len(right) <= 216, "sparse vector capacity") + out = dict(left) + for i, c in right.items(): + out[i] = out.get(i, 0) + scale * c + return {i: c for i, c in out.items() if c} + + +def act(actor, vector): + out = {} + for j, c in vector.items(): + i, sign = actor[j] + out[i] = out.get(i, 0) + sign * c + return {i: c for i, c in out.items() if c} + + +def image(matrix, vector): + out = {} + for i, row in enumerate(matrix): + c = sum(row[j] * value for j, value in vector.items()) + if c: + out[i] = c + return out + + +def projector(rotation): + cols = [] + for j in range(216): + v, total = {j: 1}, {} + for c in CHARACTER: + total = add(total, v, c) + v = act(rotation, v) + need(v == {j: 1}, "rotation order divides six") + cols.append(total) + return cols + + +def apply_columns(columns, vector): + result = {} + for j, c in vector.items(): + result = add(result, columns[j], c) + return result + + +def elimination(columns): + """Keep original columns and coordinate expressions for normalized pivots.""" + need(len(columns) <= 216, "column bound") + rows, selected, indices = {}, [], [] + for index, column in enumerate(columns): + v = {i: Fraction(c) for i, c in column.items()} + coeff = {len(selected): Fraction(1)} + for pivot, (row, coordinates) in rows.items(): + if pivot in v: + scalar = -v[pivot] + v = add(v, row, scalar) + coeff = add(coeff, coordinates, scalar) + if not v: + continue + pivot = min(v) + scale = v[pivot] + rows[pivot] = ({i: c / scale for i, c in v.items()}, + {i: c / scale for i, c in coeff.items()}) + selected.append(column) + indices.append(index) + return selected, indices, rows + + +def coordinates(vector, rows): + v = {i: Fraction(c) for i, c in vector.items()} + result = {} + for pivot, (row, coeff) in rows.items(): + if pivot in v: + scalar = v[pivot] + v = add(v, row, -scalar) + result = add(result, coeff, scalar) + need(not v, "image outside multiplicity space") + return result + + +def modular_rank(columns, prime=1_000_003): + """Independent dense row elimination; no rational construction is used.""" + need(len(columns) <= 216, "rank input capacity") + rows = [[int(v.get(i, 0)) % prime for v in columns] for i in range(216)] + rank = 0 + for col in range(len(columns)): + pivot = next((i for i in range(rank, 216) if rows[i][col]), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + inv = pow(rows[rank][col], -1, prime) + rows[rank] = [(x * inv) % prime for x in rows[rank]] + for i in range(rank + 1, 216): + scalar = rows[i][col] + if scalar: + rows[i] = [(a - scalar * b) % prime + for a, b in zip(rows[i], rows[rank], strict=True)] + rank += 1 + return rank + + +def intertwines(matrix, basis, k): + if len(basis) != 64 or len(k) != 64 or any(len(row) != 64 for row in k): + return False + for j, vector in enumerate(basis): + target = {i: k[i][j] for i in range(64) if k[i][j]} + if image(matrix, vector) != apply_columns(basis, target): + return False + return True + + +def dense_certificate(matrix, basis, partners, k): + """Check the rectangular integer identity using dense dot products.""" + ccols = [[v.get(i, 0) for i in range(216)] for v in basis + partners] + crows = [list(row) for row in zip(*ccols, strict=True)] + for j in range(128): + block = j // 64 + column = j % 64 + for i in range(216): + left = 2 * sum(a * b for a, b in zip(matrix[i], ccols[j], strict=True)) + right = sum(crows[i][block * 64 + t] * k[t][column] for t in range(64)) + need(left == right, "dense integer intertwiner") + return 216 * 128 + + +def construct(vectors, matrix, ports, columns): + rotation = orbit_action(R_INV, R_EPS, ports, columns, vectors) + reflection = orbit_action(U_INV, (1,) * 8, ports, columns, vectors) + p = projector(rotation) + need(sum(p[i].get(i, 0) for i in range(216)) == 768, "projector trace") + for j, column in enumerate(p): + need(apply_columns(p, column) == {i: 6 * c for i, c in column.items()}, + "scaled idempotent") + need(act(reflection, act(reflection, {j: 1})) == {j: 1}, "reflection square") + candidates = [add(v, act(reflection, v)) for v in p] + basis, selected, rows = elimination(candidates) + need(len(basis) == 64, "multiplicity dimension") + tcols = [coordinates(image(matrix, v), rows) for v in basis] + k = [[2 * tcols[j].get(i, 0) for j in range(64)] for i in range(64)] + need(all(c.denominator == 1 for row in k for c in row), "8T integral") + k = [[int(c) for c in row] for row in k] + partners = [act(rotation, v) for v in basis] + for v, rv in zip(basis, partners, strict=True): + need(act(reflection, v) == v, "reflection-positive basis") + need(act(rotation, rv) == add(rv, v, -1), "standard rotation block") + need(act(reflection, rv) == add(v, rv, -1), "standard reflection block") + need(apply_columns(p, v) == {i: 6 * c for i, c in v.items()}, "inside W") + twice_b = [[2 * c for c in row] for row in matrix] + need(intertwines(twice_b, basis, k), "first operator block") + need(intertwines(twice_b, partners, k), "second operator block") + need(modular_rank(basis + partners) == 128, "independent doubled basis") + return basis, partners, selected, k, p, twice_b + + +def controls(basis, partners, k, p, twice_b): + outcomes = [] + bad = [list(row) for row in k] + bad[0][0] += 1 + outcomes.append(not intertwines(twice_b, basis, bad)) + outcomes.append(not intertwines(twice_b, partners, bad)) + outcomes.append(not intertwines(twice_b, basis, [[2 * c for c in row] for row in k])) + outcomes.append(not intertwines(twice_b, basis[:-1], k)) + doubled = basis + partners + outcomes.append(modular_rank(doubled[:-1]) == 127) + outcomes.append(modular_rank(doubled[:-1] + [doubled[0]]) == 127) + outcomes.append(modular_rank(basis) == 64) + outcomes.append(any(apply_columns(p, {i: 1}) != {i: 6} for i in range(216))) + # A nonidentity relabeling of the domain changes the represented operator. + swapped = [dict(v) for v in basis] + pair = next((j for j in range(1, 64) if k[j] != k[0]), None) + need(pair is not None, "nonconstant matrix control") + swapped[0], swapped[pair] = swapped[pair], swapped[0] + outcomes.append(not intertwines(twice_b, swapped, k)) + need(all(outcomes), "semantic control failed") + return len(outcomes) + + +def certificate(basis, selected, k): + return {"convention": "T=K/8; C=[V,RV]; 2 B C=C diag(K,K)", + "selected_projector_columns": selected, + "V_columns": [sorted(v.items()) for v in basis], "K_rows": k} + + +def run(): + vectors, matrix, ports, columns, hashes = inputs() + basis, partners, selected, k, p, twice_b = construct(vectors, matrix, ports, columns) + count = controls(basis, partners, k, p, twice_b) + dense_entries = dense_certificate(matrix, basis, partners, k) + cert = certificate(basis, selected, k) + supports = sorted({len(v) for v in basis}) + return cert, {"marker": "PASS_A1_DIHEDRAL_MULTIPLICITY_MATRIX", + "multiplicity_dimension": 64, "doubled_rank": 128, + "K_nonzero_entries": sum(c != 0 for row in k for c in row), + "K_min": min(map(min, k)), "K_max": max(map(max, k)), + "V_support_sizes": supports, + "T_common_denominator": math.lcm(*(Fraction(c, 8).denominator + for row in k for c in row)), + "dense_integer_equalities": dense_entries, + "controls": count, "input_sha256": hashes} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", type=Path, help="create a new receipt outside the checkout") + parser.add_argument("--matrix", action="store_true", help="include the complete new matrix and basis") + args = parser.parse_args() + if args.emit is not None: + dest = args.emit.expanduser().resolve() + need(not dest.is_relative_to(ROOT), "receipt must be outside checkout") + need(not dest.exists(), "receipt already exists") + cert, result = run() + result["certificate_sha256"] = hashlib.sha256( + json.dumps(cert, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + result["package_sha256"] = {name: hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest() + for name in FILES} + result["python"] = sys.version + if args.matrix: + result["certificate"] = cert + output = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.emit is not None: + with dest.open("x", encoding="utf-8") as stream: + need(stream.write(output) == len(output), "complete receipt write") + print(output, end="") + + +if __name__ == "__main__": + main()