Open Research Index

JD-Jones-ASES/Hadamard-formal

JD Jones

Palomar Registrypalomar/PALOMAR-2026-08-31-000001Aug 31, 2026math.COscore 0

A Lean 4 formalization of the periodic Cooper-Wallis construction and of Hadamard existence at eight orders: from kernel-checked periodic T-matrix quadruples of orders 103 and 163 and seven symmetric-circulant Williamson quadruples, the development proves that Hadamard matrices of orders 2884, 4532, 7004, 7172, 7828, 8476, 9476, and 11948 exist. Each of the eight orders lands on an entry of Table 4 of Cati and Pasechnik's maintained construction database (arXiv:2411.18897v2, 2025-08-30) recording no Hadamard matrix of that order as known, and the source repositories' firsthand audit of the…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-08-31-000001
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-31-000001/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-31-000001/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'