The problem, in plain language
The kissing number \(\tau(5)\) is the largest number of unit spheres that can all touch one fixed unit sphere in five dimensions without overlapping each other.
On the unit four-sphere this becomes a point-packing question: find as many unit vectors as possible while keeping every pairwise inner product at most \(1/2\). Forty points come from the \(D_5\) root system. The challenge is to decide whether 41, 42, 43, or 44 points can exist.
Recent published work also emphasizes how little symmetry can be assumed: at least four non-isometric 40-point configurations are known. So a proof cannot safely insist that an optimum looks like \(D_5\), is antipodal, or has a prescribed contact graph.
What the run actually accomplished
We tried both directions at once: build 41–44 points, and prove that 41 points cannot exist. The project produced exact necessary conditions, reproducible near misses, and several useful counterexamples to attractive proof ideas. It did not find the missing global argument.
The lower bound is completely explicit. An independent checker reconstructs all 40 normalized \(D_5\) roots, verifies every norm, and checks all 780 unordered pairs with exact integer arithmetic.
The recurring difficulty was not finding another local restriction. It was proving that all local views must come from one common rank-five Gram matrix. Many pair, triple, cap, and finite local models can look perfectly feasible while failing that global compatibility test.
Exact findings that survived audit
Local geometry
Exact cap projections bound how many other code points can sit high above any anchor. At heights \(1/4,3/10,1/3,3/8,\) and \(2/5\), the respective occupancy bounds are 23, 22, 21, 20, and 19. These are universal necessary conditions, but averaging them does not yet give a 40-point upper bound.
Many antipodal pairs
If a hypothetical 41-point code contains \(r\) antipodal pairs, those pairs become isolated components in its graph of very negative inner products. At \(r=18\), exact graph bookkeeping forces the remaining five points into a five-cycle. A projective-harmonic inequality then forces one residual cycle pair to be especially negative. This sharply narrows the branch, but it does not rule it out.
A finite quarter-grid model
When every inner product is artificially restricted to a multiple of \(1/4\), exact certificates eliminate the cases with 14, 15, or 16 antipodal pairs. Separate ADE calculations eliminate one named 12-pair endpoint and all 38 profiles in a stored 11-pair export.
Important limitation: the independent generators proving those 11- and 12-pair lists exhaustive were temporary and did not survive. We therefore do not claim complete 11- or 12-pair exclusions, and none of this is a discretization theorem for arbitrary spherical codes.
The five-cycle subproblem
On the closed five-cycle sign cell, an exact analytic argument gives a largest Gram eigenvalue at most 3. A separate exact Bernstein certificate proves the desired quartic-energy bound on one minimal metric face. The rest of the metric polytope remains open, so this partial result cannot close the 18-antipode branch.
Counterexamples that saved us from false proofs
Several plausible shortcuts failed exactly. Local rank-five mixtures need not glue globally. A degree-three rooted-triangle dual that works on a finite 1,782-atom catalog is violated by an exact rank-five atom outside the catalog. Two natural Hall-style charging principles fail on a fixed \(D_5\) extension problem. These failures are part of the useful output: they mark where local or finite information stops being universal.
What the construction searches said
Unrestricted and structured searches did not find a code of size 41–44. The best repeatedly reproduced 41-point basin has maximum inner product about \(0.51499465\), above the required \(0.5\).
| Points | Best stored maximum inner product | Needed |
|---|---|---|
| 41 | 0.5149946525 | \(\le0.5\) |
| 42 | 0.51824116 | \(\le0.5\) |
| 43 | 0.52470960 | \(\le0.5\) |
| 44 | 0.52745771 | \(\le0.5\) |
That persistent gap is suggestive, but it proves nothing about a configuration the searches did not find. Numerical failure is not a lower bound on the best possible maximum inner product.
Why we paused
The same bottleneck kept reappearing: global compatibility in five dimensions. We can control many local views, finite-support shadows, and moment tables, but we do not have a rigorous bridge that covers continuously varying inner products while preserving rank at most five.
Returns had narrowed to more elaborate versions of the same restricted models, while the global bounds stayed fixed. We paused rather than let a finite-grid exclusion, a solver status, or a missing enumeration package drift into a claimed solution.
If this program resumes, the strongest target is a new common-source inequality coupling overlapping local views, a genuine continuous-to-finite theorem, or an exact higher-order SDP/SOS dual below 41—not merely a finer grid or more random seeds.
Reproduce and inspect
The repository separates search code, exact certificates, tests, and smaller independent verifiers. Start with these files:
STATUS.md— concise paused-state report, exact bounds, surviving claims, and unresolved gaps.RESUME.md— clean setup, five-minute smoke tests, missing artifacts, and restart priorities.CLAIMS_LEDGER.md— every important statement labeled proved, computationally certified, numerical only, conjectural, or refuted.APPROACH_REGISTRY.md— mechanisms, artifacts, counterexamples, restrictions, and exact bottlenecks.proofs/lower_bound_d5.mdandverifiers/verify_d5.py— the exact 40-point construction and small checker.kissing_number_5/— complete source, experiments, certificates, tests, logs, and checksum manifest.
Published context
- Henry Cohn and Isaac Rajagopal, “Variations on Five-Dimensional Sphere Packings” (2026): four non-isometric 40-point configurations and the still-best upper bound 44.
- Hans D. Mittelmann and Frank Vallentin, “High accuracy semidefinite programming bounds for kissing numbers” (2010): the high-precision SDP computation behind the published five-dimensional upper bound.
- Christine Bachoc and Frank Vallentin, “New upper bounds for kissing numbers from semidefinite programming”: the three-point SDP framework used as a baseline throughout the project.
Scope and AI-assistance disclosure
This page is a checkpoint, not a paper or a claim of priority. The exploratory mathematics, proof drafting, programs, audits, and website were developed with heavy assistance from ChatGPT 5.6 Sol under Alec Kriebel's direction. Alec Kriebel is a complete amateur and cannot independently validate the mathematics. The work has not been peer reviewed.