Construct a uniform 42-ray design with exactly one basis (no new κ)

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 <v_k,v_l>=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.

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.

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"
+    }
+  ]
+}

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"
+  }
+}