diff --git a/research/cyclic-42-design/PROOF.md b/research/cyclic-42-design/PROOF.md new file mode 100644 index 0000000000..1006662157 --- /dev/null +++ b/research/cyclic-42-design/PROOF.md @@ -0,0 +1,135 @@ +# A uniform design with exactly one orthonormal basis + +Put S=(0,1,4,10,12,17), zeta=exp(2 pi i/36), and + + v_k = (zeta^(k s))_(s in S) / sqrt(6), 0 <= k < 36. + +Let X consist of these 36 rays and the six coordinate rays in C^6. Then X +has 42 distinct rays, its uniform measure is a projective 2-design, and +its orthogonality graph is K6 together with 36 isolated vertices. Consequently +the coordinate rays are its only orthonormal basis, counted as an unordered +set of rays. In particular X cannot be partitioned into seven bases. + +This is a finite explicit construction and a scoped algebraic proof. The +harmonic construction is Bodmann and Haas's; the Sidon-set design theorem +is Jasper and Mixon's. The new claim here concerns this literal uniform +instance and its complete orthogonality structure. Neither the general +construction nor existence of designs in dimension six is claimed as new. + +## Distinct rays + +Each v_k is unit length. Its first coordinate is 1/sqrt(6), and its second +is zeta^k/sqrt(6). Therefore equality of two rays forces the proportionality +scalar to be one and then forces k=l modulo 36. Every coordinate of a flat +vector is nonzero, so no such ray equals a coordinate ray. The coordinate +rays themselves are distinct. + +## The second moment + +The positive pairwise differences of S are + + 1,2,3,4,5,6,7,8,9,10,11,12,13,16,17. + +They are distinct and smaller than 18. Thus all 30 ordered differences +between distinct marks are distinct modulo 36. Equivalently, S is Sidon +modulo 36: s_a+s_c=s_b+s_d holds modulo 36 exactly when the two unordered +pairs of marks, including repetitions, agree. For completeness, a +nontrivial equality of sums can be rearranged into an equality of ordered +nonzero differences. Distinctness of those differences forces the trivial +matching. This argument also excludes a collision involving a doubled mark. + +Write P_x=xx* for a unit vector. The ((a,c),(b,d)) entry of the sum over +the flat vectors is + + (1/36) sum_(k=0)^35 zeta^[k(s_a+s_c-s_b-s_d)]. + +The geometric series equals one if the frequency is zero modulo 36 and +zero otherwise. By the Sidon property this gives one for each of the +two matching patterns a=b,c=d and a=d,c=b, except that the all-equal case +is counted just once. The coordinate-ray contribution is one exactly +in that all-equal case. Hence, on C^6 tensor C^6, + + sum_(x in X) P_x tensor P_x = I + Swap. + +Dividing by 42=6(6+1) proves the projective 2-design identity, with weight +1/42 on every distinct ray. This is the operational definition in atlas +B042. It is stronger than a numerical fourth-potential test. + +## All orthogonality relations + +A coordinate vector has nonzero overlap with every v_k. Distinct coordinate +vectors are orthogonal. It remains to exclude flat-flat orthogonality. +Set + + P(t)=1+t+t^4+t^10+t^12+t^17. + +Then =P(zeta^(l-k))/6. For k different from l the order n of +zeta^(l-k) is one of 2,3,4,6,9,12,18,36. The remainders of P modulo +the corresponding cyclotomic polynomials are as follows. Coefficients +are in ascending powers in the verifier; this table uses ordinary notation. + +| Root order n | Remainder of P modulo Phi_n | +| --- | --- | +| 2 | 2 | +| 3 | 1 + 2 t | +| 4 | 2 + 2 t | +| 6 | 3 - 2 t | +| 9 | 1 + 2 t - t^2 + t^3 + t^4 - t^5 | +| 12 | 2 + t^3 | +| 18 | 1 + t^2 - t^3 + t^4 - t^5 | +| 36 | t + t^4 - t^5 + t^6 + t^10 + t^11 | + +Every listed polynomial is nonzero and has degree below phi(n). The +standard irreducibility theorem for cyclotomic polynomials therefore +implies P(w) is nonzero for every primitive nth root w. This excludes +every possible difference l-k. The verifier independently evaluates all +35 differences in Q[t]/(t^12-t^6+1), as well as every unordered ray pair. + +Thus all orthogonality edges lie among the coordinate rays and all 15 +such edges occur. Every orthonormal basis among X must be a six-clique +in this graph, so it is precisely the coordinate basis. The checker also +enumerates these cliques from each vertex's neighbor set. + +## A restriction on this construction, not on all designs + +The uniform-weight condition is forced in the coordinate-plus-flat model. +Suppose d>=2, there are M flat unit vectors and all d coordinate rays, +and the M+d indexed vectors carry uniform weight. A diagonal fourth +moment is (1+M/d^2)/(M+d). Equating it to 2/[d(d+1)] forces M=d^2. +For a complete cyclic character orbit with d distinct exponents, the +off-diagonal tensor equations then hold exactly when the exponents are +Sidon modulo d^2, by the same character sum above. This explains the +choice 36 and the exact 42-ray budget. It is a specialization of the +credited harmonic method, not an existence theorem in arbitrary d. + +## Proof and implementation boundary + +The universal complex-field implications are the geometric-series and +cyclotomic arguments above. The checker uses integer polynomial division, +without floating-point tolerances. It checks all 1,296 tensor entries, +all 861 unordered ray pairs and all 630 flat-ray distinctness pairs. +The printed receipt is computed from these checks and binds all six package +source files by SHA256. It is generated on stdout and never committed. + +All loops have fixed finite domains. The largest mathematical Cartesian +domain has 6^4 entries, each with 36 character terms and 12 coefficients. +Functions are below 60 physical lines. Checks use explicit exceptions and +remain active under optimized Python. Managed Python allocation is an +explicit Power of Ten deviation: arrays have at most 72 polynomial +coefficients, the graph has 42 vertices, and source hashing reads six +bounded package files. No global diagnostics or predecessor code is changed. + +This is not a native circuit, physical supplier, multiplication theorem, +SIC, MUB construction or selected-frontier update. Independent human and +formal proof-kernel review and global literature priority are unclaimed. +No predecessor verifier is replayed as the scientific deliverable. + +## Credit + +This contribution was produced by Nick Petalas. David Ganz's atlas PR2849, +B100 supplies the finite construction question, and B042 supplies the +moment convention. Gary S. Bloom's classical six-mark ruler supplies S; +the ruler is not a new discovery. Credit Bernhard G. Bodmann and John Haas +for the harmonic design construction and John Jasper and Dustin G. Mixon +for its Sidon-set formulation. Their results are cited methods, not audited +claims or original results of this package. See the README for references. diff --git a/research/cyclic-42-design/README.md b/research/cyclic-42-design/README.md new file mode 100644 index 0000000000..d81d9a9669 --- /dev/null +++ b/research/cyclic-42-design/README.md @@ -0,0 +1,111 @@ +# A cyclic 42-ray uniform design with exactly one basis + +In C^6, take the six coordinate rays and + + v_k = (1, zeta^k, zeta^(4k), zeta^(10k), zeta^(12k), zeta^(17k)) / sqrt(6), + zeta = exp(2 pi i / 36), 0 <= k < 36. + +These are 42 distinct rays. With uniform weight 1/42 they form a complex +projective 2-design. Their orthogonality graph is K6 plus 36 isolated vertices, +so they contain exactly one orthonormal basis, the six coordinate rays. +This gives the finite dimension-six example requested in David Ganz's atlas +[B100](../pure-math-atlas-400/volumes/02-geometry.md#b100), and shows directly +why a uniform design at cardinality d(d+1) need not be a union of bases. + +Claim type: scoped written algebraic proof with a finite exact certificate. +The new result is this explicit cyclic instance with its complete +orthogonality structure. The harmonic construction, its Sidon-set criterion, +the six-mark ruler and existence of designs in dimension six retain their +predecessors' credit. Global literature priority is unclaimed. + +## Proof and evidence + +[PROOF.md](PROOF.md) proves the literal tensor identity + + sum_(x in X) P_x tensor P_x = I + Swap, + P_x = x x*. + +It then excludes all flat-flat orthogonality using eight nonzero cyclotomic +remainders, one for each possible order of a nontrivial 36th root. The proof +also explains why uniform weights in the coordinate-plus-flat character-orbit +model force exactly d^2 flat vectors. That restriction concerns this model. + +The standard-library verifier reconstructs all 1,296 tensor matrix entries +in Q[zeta], every one of the 861 unordered ray pairs, 630 flat-ray +distinctness pairs, and all six-cliques in the resulting graph. It checks +the 21 unordered pair sums and all 35 nontrivial character differences. +Its six rejecting controls cover sum collisions, a false second moment, +a missing coordinate ray, extra orthogonality, repeated rays and an +incorrect uniform weight. The output is a generated hash-bound receipt; +no receipt is written by hand or committed. + +## Reproduction + +From the repository root, using CPython 3.12 and no additional dependencies: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/cyclic-42-design/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/cyclic-42-design/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/cyclic-42-design +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/cyclic-42-design --check-source-history +``` + +The direct commands also run from an exported package without Git or the +predecessor files. Both registered checks have 60-second limits. Exact local +timings and hosted CI status belong in the PR body. All generated output +belongs outside the checkout. + +## Scope and overlap + +The scientific base is ff3cc58e370d0f678e529246f8c73e8094e18fcf, priority +revision 7. The formal-interface-lemma card is changed to B100's algebraic +side question, rather than a formal proof or selected supplier audit. +The selected source-binding orientation passed; it is not scientific +verification of this construction. See TASK.json for the original card, +scope change and structured next questions. SOURCES.json pins the atlas, +catalogue and selected record as historical provenance. The verifier has +no runtime dependency on them. + +The live open/account PR lists, active Discussions, recent claims, targeted +main-tree and merged-PR searches and cached overlap were checked. The cached +scan covered 311 open PRs and 4,493 Discussion records, with complete remote +pagination, but only 160 of 7,091 local HEAD notes were materialized before +the atlas was added. Targeted all-main searches supplement that sparse scan. +Arbitrary historical diffs and unpublished work remain outside coverage. +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19147110). + +This does not construct seven MUBs, improve a multiplication exponent, +change the selected frontier or certify a native supplier. Acquisition, +frames, ownership, restoration, routing, stock, precision/tape, compiler +and the complete consumer bill are unpriced. Lean, Docker and the selected +supplier's cold replay are unrun. Independent human and formal proof-kernel +review are unclaimed. + +## Open next questions + +- Which further dimensions admit a cyclic uniform design with only its + coordinate basis? Begin with one specified classical ruler modulo d^2 + and its cyclotomic zero test. A general existence theorem is absent. +- Can this instance serve an actual native decoder or measurement caller? + Begin with one explicit contract and the complete acquisition, delivery, + restoration and consumer invoice. No such cost model is supplied here. + +These questions are unreserved. The investigation stops at the first +construction above; no dimension scan or ruler census was performed. + +## Credit and references + +produced by Nick Petalas. Apache-2.0. + +David Ganz's [PR2849](https://github.com/CrocSwap/integer-mult-bounds/pull/2849) +supplies atlas B100's finite example request and B042's moment convention. +Gary S. Bloom's classical ruler is used without a novelty claim for its marks; +see [A counterexample to a theorem of S. Piccard](https://doi.org/10.1016/0097-3165(77)90013-9). +Bernhard G. Bodmann and John Haas supply the +[harmonic construction](https://arxiv.org/abs/1509.05333). +John Jasper and Dustin G. Mixon's +[Theorem 7](https://arxiv.org/html/2501.14938v1#S2) +gives its Sidon-set formulation and cites Bodmann and Haas's construction. +Their methods are cited premises, not audited deliverables or original results +claimed here. The literal moment calculation and full orthogonality proof +above are self-contained. diff --git a/research/cyclic-42-design/SOURCES.json b/research/cyclic-42-design/SOURCES.json new file mode 100644 index 0000000000..8e4302e892 --- /dev/null +++ b/research/cyclic-42-design/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/pure-math-atlas-400/volumes/02-geometry.md", + "usage": "provenance", + "git_blob": "baef1e69c08c7cbd4dfd020862870fa5161afc86", + "sha256": "39fc97bdfa29337b79d1308e35df41e867ce2102d44755fd407aa09ff8352b39" + } + ] +} diff --git a/research/cyclic-42-design/TASK.json b/research/cyclic-42-design/TASK.json new file mode 100644 index 0000000000..33633bea87 --- /dev/null +++ b/research/cyclic-42-design/TASK.json @@ -0,0 +1,106 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "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 a uniform 42-ray projective 2-design in C^6 and prove that its only orthonormal basis is the coordinate basis.", + "scope_change_reason": "The explicit dimension-six construction requested by David Ganz in atlas B100 is an algebraic side question. This is a written proof with an exact certificate, rather than a selected-interface formalization or predecessor audit.", + "bottleneck_link": "Scoped design geometry: supplies exact moment data at the MUB cardinality scale while proving that this instance has only one basis. Physical supplier costs and multiplication savings are unclaimed.", + "budget_minutes": 60, + "stop_rule": "Stop after the first verified explicit construction and orthogonality proof. Do not extend to other dimensions, classify rulers or optimize cardinality.", + "outcome": "completed", + "evidence": "PROOF.md and the generated PASS_CYCLIC_42_DESIGN receipt from verify.py; full moment entries, pair relations and rejecting controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which dimensions d admit a d-element Sidon subset of Z/(d^2) whose harmonic orbit has no orthogonal pair?", + "why_it_matters": "Such instances would distinguish uniform MUB-scale designs from basis collections in further dimensions.", + "first_step": "Check a specified classical ruler modulo d^2 and the finite cyclotomic divisibility conditions.", + "blocked_by": "No general existence or classification is supplied; check live overlap before selecting a dimension." + }, + { + "question": "Can this exact 42-ray design support a fully priced native decoder or measurement interface?", + "why_it_matters": "The moment identity alone gives no physical multiplication saving.", + "first_step": "Specify one actual caller, its support tariff, acquisition, restoration and complete consumer bill.", + "blocked_by": "No native contract or physical cost model has been established for this instance." + } + ], + "environment": { + "python": "3.12.15", + "platform": "Darwin arm64", + "dependencies": "Python standard library only" + } +} diff --git a/research/cyclic-42-design/VERIFY.json b/research/cyclic-42-design/VERIFY.json new file mode 100644 index 0000000000..164bc6d517 --- /dev/null +++ b/research/cyclic-42-design/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "All literal second-moment entries, distinct rays, full orthogonality graph, basis enumeration, cyclotomic order table and semantic rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Repeat the full certificate with Python assertions disabled; checks must still reject the controls." + } + ] +} diff --git a/research/cyclic-42-design/verify.py b/research/cyclic-42-design/verify.py new file mode 100644 index 0000000000..19f8eb4fd3 --- /dev/null +++ b/research/cyclic-42-design/verify.py @@ -0,0 +1,215 @@ +#!/usr/bin/env python3 +"""Exact second moments and orthogonality for the fixed cyclic 42-ray design.""" + +from hashlib import sha256 +from itertools import combinations, product +import json +from pathlib import Path + + +EXPONENTS = (0, 1, 4, 10, 12, 17) +ORDER = 36 +DIMENSION = 6 +PHI36 = (1, 0, 0, 0, 0, 0, -1, 0, 0, 0, 0, 0, 1) +CYCLOTOMICS = { + 2: (1, 1), + 3: (1, 1, 1), + 4: (1, 0, 1), + 6: (1, -1, 1), + 9: (1, 0, 0, 1, 0, 0, 1), + 12: (1, 0, -1, 0, 1), + 18: (1, 0, 0, -1, 0, 0, 1), + 36: PHI36, +} + + +def require(condition: bool, message: str) -> None: + """Keep mathematical checks active under optimized Python.""" + if not condition: + raise ValueError(message) + + +def remainder(coefficients: tuple[int, ...], modulus: tuple[int, ...]) -> tuple[int, ...]: + require(1 < len(modulus) <= 37 and modulus[-1] == 1, "monic modulus bound") + require(len(coefficients) <= 72, "polynomial degree bound") + degree = len(modulus) - 1 + values = list(coefficients) + [0] * max(0, degree - len(coefficients)) + for index in range(len(values) - 1, degree - 1, -1): + leading = values[index] + for offset in range(degree + 1): + values[index - degree + offset] -= leading * modulus[offset] + require(not any(values[degree:]), "division did not clear high coefficients") + return tuple(values[:degree]) + + +def polynomial(exponents: tuple[int, ...]) -> tuple[int, ...]: + require(len(exponents) <= 36, "term bound") + values = [0] * ORDER + for exponent in exponents: + values[exponent % ORDER] += 1 + return tuple(values) + + +def add(left: tuple[int, ...], right: tuple[int, ...]) -> tuple[int, ...]: + require(len(left) == len(right) == 12, "field element shape") + return tuple(a + b for a, b in zip(left, right, strict=True)) + + +def sidon(exponents: tuple[int, ...]) -> bool: + require(len(exponents) == DIMENSION, "six exponents required") + sums = [(a + b) % ORDER for i, a in enumerate(exponents) for b in exponents[i:]] + return len(set(sums)) == len(sums) + + +def check_moment(exponents: tuple[int, ...], coordinate_count: int = 6, + denominator: int = 42) -> int: + """Sum all 36 literal characters for every tensor matrix entry.""" + require(len(exponents) == DIMENSION, "moment dimension") + require(0 <= coordinate_count <= DIMENSION, "coordinate-ray bound") + require(1 <= denominator <= 84, "weight denominator bound") + powers = tuple(remainder(polynomial((n,)), PHI36) for n in range(ORDER)) + checked = 0 + for a, c, b, d in product(range(DIMENSION), repeat=4): + frequency = exponents[a] + exponents[c] - exponents[b] - exponents[d] + actual = (0,) * 12 + for k in range(ORDER): + actual = add(actual, powers[(k * frequency) % ORDER]) + # Multiply the unnormalized moment by 36 to keep every entry integral. + coordinate = int(a == b == c == d and a < coordinate_count) + actual = add(actual, (36 * coordinate,) + (0,) * 11) + target = 36 * denominator * (int(a == b and c == d) + int(a == d and c == b)) + scaled = tuple(42 * entry for entry in actual) + require(scaled == (target,) + (0,) * 11, f"second moment failed at {(a,c,b,d)}") + checked += 1 + return checked + + +def flat_inner_numerator(exponents: tuple[int, ...], difference: int) -> tuple[int, ...]: + require(len(exponents) == DIMENSION and 0 <= difference < ORDER, "inner-product domain") + return remainder(polynomial(tuple(difference * s for s in exponents)), PHI36) + + +def check_orthogonality(exponents: tuple[int, ...]) -> tuple[int, list[list[int]]]: + require(len(exponents) == DIMENSION, "orthogonality dimension") + neighbors = [[] for _ in range(42)] + checked = 0 + for left, right in combinations(range(42), 2): + if right < 6: + zero = True + elif left < 6: + zero = False # Every flat coordinate has squared modulus 1/6. + else: + zero = not any(flat_inner_numerator(exponents, right - left)) + if zero: + neighbors[left].append(right) + neighbors[right].append(left) + checked += 1 + expected = [[j for j in range(6) if j != i] if i < 6 else [] for i in range(42)] + require(neighbors == expected, "orthogonality graph is not K6 plus 36 isolated vertices") + return checked, neighbors + + +def check_distinctness(exponents: tuple[int, ...]) -> int: + require(len(exponents) == DIMENSION, "distinctness dimension") + checked = 0 + for left, right in combinations(range(ORDER), 2): + phases = {((right - left) * (s - exponents[0])) % ORDER for s in exponents} + require(phases != {0}, "two flat rays coincide") + checked += 1 + # Flat rays have six nonzero coordinates, so none equals a coordinate ray. + return checked + + +def count_bases(neighbors: list[list[int]]) -> int: + require(len(neighbors) == 42 and max(map(len, neighbors)) <= 5, "clique search bound") + bases = set() + for vertex in range(42): + for others in combinations(neighbors[vertex], 5): + candidate = tuple(sorted((vertex,) + others)) + if all(b in neighbors[a] for a, b in combinations(candidate, 2)): + bases.add(candidate) + require(bases == {tuple(range(6))}, "unexpected orthonormal bases") + return len(bases) + + +def check_order_table() -> dict[str, list[int]]: + table = {} + for order, modulus in CYCLOTOMICS.items(): + value = remainder(polynomial(EXPONENTS), modulus) + require(any(value), f"orthogonal flat difference of order {order}") + table[str(order)] = list(value) + # Independently connect every actual difference to its Galois-order class. + for difference in range(1, ORDER): + require(any(flat_inner_numerator(EXPONENTS, difference)), "zero actual inner product") + return table + + +def expect_rejection(action: str) -> None: + try: + if action == "collision": + require(sidon((0, 1, 2, 3, 4, 5)), "colliding pair sums") + elif action == "bad-moment": + check_moment((0, 1, 2, 3, 4, 5)) + elif action == "missing-axis": + check_moment(EXPONENTS, coordinate_count=5) + elif action == "extra-orthogonality": + check_orthogonality((0, 1, 2, 3, 4, 5)) + elif action == "repeated-rays": + check_distinctness(tuple(2 * s for s in EXPONENTS)) + elif action == "wrong-normalization": + check_moment(EXPONENTS, denominator=84) + else: + raise RuntimeError("unknown control") + except ValueError: + return + raise RuntimeError(f"control did not reject: {action}") + + +def source_hashes() -> dict[str, str]: + root = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {} + for name in names: + with (root / name).open("rb") as source: + data = source.read(2 * 1024 * 1024 + 1) + require(len(data) <= 2 * 1024 * 1024, "package source size bound") + hashes[name] = sha256(data).hexdigest() + return hashes + + +def main() -> None: + require(len(set(EXPONENTS)) == DIMENSION and EXPONENTS[:2] == (0, 1), "fixed fixture") + require(sidon(EXPONENTS), "candidate is not Sidon") + require(remainder(polynomial((0, 18)), PHI36) == (0,) * 12, "zeta^18 = -1 control") + table = check_order_table() + moments = check_moment(EXPONENTS) + pairs, neighbors = check_orthogonality(EXPONENTS) + bases = count_bases(neighbors) + distinct = check_distinctness(EXPONENTS) + controls = ("collision", "bad-moment", "missing-axis", "extra-orthogonality", + "repeated-rays", "wrong-normalization") + for control in controls: + expect_rejection(control) + result = { + "status": "PASS_CYCLIC_42_DESIGN", + "claim_type": "scoped proof with finite exact certificate", + "dimension": DIMENSION, + "rays": 42, + "uniform_weight": "1/42", + "exponents": EXPONENTS, + "pair_sums": len({(a + b) % ORDER for i, a in enumerate(EXPONENTS) for b in EXPONENTS[i:]}), + "second_moment_entries": moments, + "unordered_ray_pairs": pairs, + "flat_distinctness_pairs": distinct, + "orthogonal_pairs": sum(map(len, neighbors)) // 2, + "orthogonality_degrees": list(map(len, neighbors)), + "orthonormal_bases": bases, + "cyclotomic_remainders": table, + "rejection_controls": list(controls), + "source_sha256": source_hashes(), + } + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()