Attack log — five-dimensional kissing number
2026-08-17 — start
- Folder empty except
PROBLEM.md. House rules: write only here; no git; do not invent a dent; a restricted numerical SDP without an exact positivity certificate is residue. - Tonight's target (house / PROBLEM.md): an exact dual certificate excluding some , or a new exact spherical code of size on .
Published record (fetched tonight)
Sources, all still stating :
- Tao constants page
C_{29}https://teorth.github.io/optimizationproblems/constants/29a.html (accessed 2026-08-17): range , conjectural value 40. - Cohn's living table https://cohn.mit.edu/kissing-numbers/ (crawled 2026-08-17): dim 5 is 40 / 44, ratio 1.100, citations [9] Korkine–Zolotareff and [17] Mittelmann–Vallentin.
- Boyvalenkov–Dodunekov–Musin survey, arXiv:1507.03631: “the first open case is in dimension five, where it is known that ” (story: Levenshtein , Odlyzko–Sloane 46.345, Bachoc– Vallentin 45, Mittelmann–Vallentin 44.998).
- Mittelmann–Vallentin, arXiv:0902.1105v3 / Exp. Math. 19 (2010): , hence . This is the published upper bound. High-accuracy SDP, not an exact SOS certificate in the paper.
- Cohn–Rajagopal, arXiv:2412.00937v3 (4 Mar 2026), published Discrete Comput. Geom. (doi 10.1007/s00454-026-00841-x): “the kissing number in five dimensions appears to be 40, although the best upper bound that has been proved is 44”. Four non-isometric 40-point codes: , (Leech 1967), (Szöllősi 2023 / Andreanov–Kallus), (Cohn–Rajagopal). None larger than 40.
- Wikipedia / MathWorld tables (MathWorld “as of August 2026”) still 40/44.
- No later accepted improvement of either endpoint found in arXiv search tonight (new work is lower bounds in high dimensions, or new 40-point geometries).
Independently I will re-verify the four 40-point Gram bounds and the classical Levenshtein number 48 before claiming any comparison.
Plan
- Exact coordinates and Gram checks for .
- Exact Delsarte / restricted-distance LPs (rational Gegenbauer).
- Structural restrictions that can be certified exactly: codes containing a 24-cell, codes with only inner products, Q5-equator extensions.
- Search for an exact 41-point spherical code (algebraic ansätze, layer replacement). Numerical SDP without a positivity certificate is residue.
2026-08-17 — replay of the four 40-point codes
- Implemented from the geometric descriptions in Cohn–Rajagopal §2, not by typing Table 2.2.
compute/verify_configs.py: all four have 40 points of squared norm 2, max normalised inner product exactly , and the unordered-pair histograms match Cohn–Rajagopal Table 2.1 exactly (including the exotic angles ).- Independently recomputed Levenshtein from the BDM
odd-bound formula (
compute/levenshtein.py). Matches the survey.
2026-08-17 — false start: add a 41st point to
- For unit , the inequalities are for all .
- On the unit sphere the min of the largest pair-sum is , with equality at the equal-coordinate points. Squares: .
- So is maximal as a spherical code. Exact, not a 41-point lead.
Script:
compute/extend_d5.py.
2026-08-17 — false start: complete the equator to a 24-cell
- slices as along the all-ones direction, equator (20 roots). The 4D kissing number is 24, so adding four equatorial points would give a 44-point candidate.
- Histogram check: is not isometric to any 24-cell minus two antipodal pairs (66 subsets, zero histogram matches).
- Stronger: on the equatorial 4-space , the
inequalities cut a polytope whose vertices are
two-level and satisfy . No new equatorial vector of
squared norm 2 exists at all. Script:
compute/q5_extend.py.
2026-08-17 — the D4-containing bound
- Any isometric 24-cell in spans a 4-space, so after rotation it is the equator . Extra points must have .
- Since on , one needs (or a pole).
- Two extra points in the same open hemisphere then have 4D blocks with , so their directions form a code in of max inner product .
- Rankin's is the exact Delsarte polynomial , on , .
- Poles conflict with every non-polar extra point in the same hemisphere ().
- Therefore a -containing 5D kissing code has size at most . This excludes in that class.
- Discrete check (
compute/d4_equator.py): the 24 holes of the 24-cell realise , their -graph has independence number 8, and there are exactly three maximum independent sets — Cohn's three inscribed cross-polytopes (one axis, two tesseract). - and contain a 24-cell, so they are covered. and do not.
2026-08-17 — restricted Delsarte, then exact duals
- Unrestricted Delsarte cannot beat (Odlyzko–Sloane) and the 3-point SDP of Mittelmann–Vallentin is . A floating SDP without a positivity certificate is residue; we did not rerun SDPA-GMP.
- For a finite inner-product set the dual only needs on , not on the whole interval . That can go below 44.
- Numerical LP (
compute/restricted_lp.py):- : bound
- : bound
- : bound (does not exclude 44)
- union of all known 40-point angles: bound
- The dual uses only and vanishes on
. Solving that interpolation over
(
compute/exact_duals.py) gives the exact polynomial incompute/certs/restricted_delsarte.json: . All , on . Replay:compute/verify_certificates.py. - Same method for : , , excludes 43 and 44 in that class.
2026-08-17 — integer distance distributions for
- Real Delsarte allows with fractional .
- Unordered pair counts must be integers.
- Exhaustive search at Gegenbauer degree 8 (
compute/integer_d5.py):- : feasible (including and nearby)
- : feasible, but every hit has (the slice is empty)
- : empty
- The witness survives degree 20 (
compute/check_integer_hits.py), so Delsarte+integrality alone does not kill 41. Combined with the root system of 20 antipodal pairs (a 40-point code, necessarily ) and the -obstruction, 41 dies too.
2026-08-17 — construction residue
- Cube vertices axes: 16+10=26.
- minus neighbourhoods plus even-sign holes: best size 40
(
compute/construct_search.py). - Numerical 41st-point slack against : all , the optimiser sitting on a deep hole (inner product ). Residue, not a certificate of maximality for .
- Enlarging by 's extra angles lifts the exact dual back
above 44 (
compute/more_duals.py). No unrestricted dual below 44.
Published record we compare against
- Lower bound 40 (Korkine–Zolotareff ; also ). We did not produce a spherical code of size .
- Upper bound 44 (Mittelmann–Vallentin ). We did not produce an unrestricted dual below 44.
- What we did certify is restricted: see RESEARCH.md.
2026-08-27 — continue (q1)
- Start from main. Folder
compute/q1/. House rules unchanged: do not claim ; a numerical SDP without an exact positivity certificate is residue; the published record is still . - Re-fetched tonight, all still : Tao https://teorth.github.io/optimizationproblems/constants/29a.html, Cohn table https://cohn.mit.edu/kissing-numbers/ (dim 5: 40 / 44, refs [9] Korkine–Zolotareff and [17] Mittelmann–Vallentin), Cohn–Rajagopal arXiv:2412.00937v3, Mittelmann–Vallentin arXiv:0902.1105v3. A Zenodo note claiming a Cohn–Kumar LP number is a lead, not a citation: unrestricted Delsarte is already , and there is no exact dual.
- Plan: (1) exact polar vertices of (maximality of was only numerical on 17 August); (2) integer Delsarte boxes for and ; (3) -containing height and the discrete vertex-extra graph; (4) more interpolating duals; (5) Szöllősi candidate graph on the known angles.
2026-08-27 — polar vertices: all four codes are maximal
- is a bounded rational polytope for each of (no recession ray).
- Exhaustive 5-subset vertex enumeration, twice:
compute/q1/polar.candpolar_vertices.py --python. Counts agree: 5504 vertices, 5440, 4024, 3960. - on every polar. Independent Fraction GE
(
replay_max_vertex.py) rebuilds the recorded vertex over : and attain at ; and at a coordinate half-axis. All inequalities hold. - So and are maximal as spherical codes. That was numerical slack on 17 August. and were already maximal by other exact arguments; the polar is a uniform proof.
- This excludes a 41st point on these four codes. It does not exclude an unrelated 41-point code. Unrestricted is unchanged.
2026-08-27 — integer slice empty at
- Real Delsarte on is still (no interpolating dual below 44; several supports certified only in the 45–60 range).
- Integer pair-counts: , .
integer_q5_44.cscans a box containing the HiGHS axis-aligned range by 15 in each coordinate ( in the full ). points, 0 hits. Tables matchdelsarte.py; the published histogram at passes every row.- Dent in this class: no spherical code in with distinct inner products in has 44 points. Does not exclude 41, 42 or 43, and is not an unrestricted dual.
2026-08-27 — integer does not kill 41–43
- is already empty by the 17 August dual .
- each have integer Delsarte-feasible distributions
(first hits in
integer_restricted.json), all with . Residue: integrality does not improve the dual.
2026-08-27 — extras and Szöllősi graph
- Height over a fixed equator: . Poles conflict with every other extra in the same hemisphere (). Discrete two-level vertex extras: independence 10 per hemisphere, 20 total, so plus vertex extras is at most 40. Continuous extras with are not in that graph.
- Szöllősi pool: 355 equal-norm vectors. Exact clique on 355 vertices was not run. Residue, not a 41-point code.
2026-08-27 — continue (q2)
- Start from current main (after q1). Folder
compute/q2/. House rules unchanged: do not claim ; a numerical SDP without an exact positivity certificate is residue; do not regress the restricted certificates already incompute/certs/andcompute/q1/certs/. - Replayed first, all still pass:
compute/verify_certificates.py(T_{D_5} bound 42; T_{L_5} bound );compute/q1/verify.py/replay_max_vertex.py(polar );compute/q1/check_q5_44_empty.py( integer slice empty at 44). - Re-fetched tonight, all still : Tao https://teorth.github.io/optimizationproblems/constants/29a.html, Cohn table https://cohn.mit.edu/kissing-numbers/ (dim 5: 40 / 44, refs [9] and [17]), Mittelmann–Vallentin arXiv:0902.1105v3 (), Cohn–Rajagopal arXiv:2412.00937v3 (4 Mar 2026). The unaffiliated Zenodo note that claimed a Cohn–Kumar number is now retracted (doi:10.5281/zenodo.18449600, removed 5 Feb 2026). Lead only; not a citation.
- Hunt: an exact dual that is nonpositive on the whole interval and excludes some , or a new exact 41-point code in . Plan: (1) exact clique on the leftover pool of 355; (2) exact kissing graph on (200 points; contains and ); (3) other hyperplane layer-swaps; (4) low-degree unrestricted Delsarte with Sturm / real-root certification.
2026-08-27 — q2 results (no unrestricted move)
- Unrestricted numerical Delsarte at degree is , matching Odlyzko–Sloane. Grid-rationalised polynomials fail the exact Sturm test (they change sign on ). An exact ansatz with gives bound , just above Levenshtein 48. No certified unrestricted dual has bound . No is excluded without a restricted angle set.
- pool, after including the basis: 360 rational vectors, all four
published 40-point codes are cliques. Five basis vectors are adjacent
to every other pool point, so a 41-clique exists iff the remaining
355-point graph has a 36-clique. The 41-search on those 355 vertices
is empty (
t5_clique.json, 607171 nodes). The 36-search was started and stopped without a hit or an emptiness proof (t5_36_residue.json). - Half-integer sphere : 200
points, no 41-clique (
sphere_d2.json). This class contains and . - sphere: 1480 points. 41-search incomplete
(
sphere_d4.json). Residue. - Layer-swaps of and across 546 short integer normals: 3148 swaps, kissing sizes , none 41.
- Signed-permutation orbit of a cap vector: 320 points, no
41-clique (
q5cap_clique.json, 7 nodes). - Unrestricted interval unchanged: . Did not beat Mittelmann–Vallentin. Did not produce a 41-point code.
2026-08-27 — continue (q3)
- Start from current main (after q2). Folder
compute/q3/. House rules unchanged: do not claim ; a numerical SDP without an exact positivity certificate is residue; do not regress the restricted certificates already incompute/certs/,compute/q1/,compute/q2/. - Re-fetched tonight, all still : Tao https://teorth.github.io/optimizationproblems/constants/29a.html (range , conjectural value 40; upper bound Mittelmann–Vallentin), Cohn table https://cohn.mit.edu/kissing-numbers/ (dim 5: 40 / 44, ratio 1.100, citations [9] Korkine–Zolotareff and [17] Mittelmann–Vallentin), Mittelmann–Vallentin arXiv:0902.1105v3 (), Cohn–Rajagopal arXiv:2412.00937v3 (4 Mar 2026; title “Variations on five-dimensional sphere packings”: “appears to be 40… best upper bound that has been proved is 44”). The unaffiliated Zenodo note remains retracted. Later-dimension news on Cohn’s table (Cohn–Li, Ho 2603.10425, Ma et al. 2511.13391, Takhanov et al. 2606.18984, Sun–Wang 2607.20359) does not touch dim 5.
- Hunt: an exact dual that is nonpositive on the whole interval and excludes some , or a new exact 41-point code. Leftover handles from q2, to verify independently: the 36-clique in the 355-point remainder, and the 1480-point graph. Own route if better: type analysis of , a pool on a larger exact angle set, a orbit, continuous extras at , and gapped duals that would need a geometric lemma to become unrestricted.
2026-08-27 — q3 results (no unrestricted move)
- Re-fetched Tao , Cohn, Mittelmann–Vallentin, Cohn–Rajagopal: still . Pfender's kernel (arXiv:math/0501493) does not give an exact dual below 44 in dim 5. The Zenodo note remains retracted.
- Unrestricted numerical Delsarte is still . Exact rationalizations fail the Sturm test. Gapped duals with only on have a numerical value , but there is no geometric lemma forbidding (every published 40-point code has such an angle) and the rational polynomials did not certify. Not an unrestricted dual. No is excluded on the whole interval .
- type analysis (
sphere_types.py,complete_slices.py): every extra vector kisses at most 36 of the 40 roots, so a 41-set has and at least 5 extras. Complete enumeration of every -superset of an actual missed-root set, , finds no extras-clique of size . Therefore the 1480-point graph has no 41-clique that uses 33 or more -type points. Replay:complete_slices.json,n1_ge_33_empty=true. The slice (at least 9 extras) was not emptied. Residue for the whole 1480-graph, not a 41-code. - remainder: exact repairs of the four published 35-cliques
(remove 1 add 2; remove 2 add 3, candidate cap 28) are empty
(
t5_repair.json). Coloured B&B to 40 million nodes found no 36-clique (t5_36_c.json). Incomplete, not an exclusion. - Larger (published angles plus ): 552-point pool, no 41-clique in 5 million nodes. Residue.
- plus the signed-permutation orbit of and the half-spinor layers (552 points over ): no 41-clique in 3 million nodes. Residue.
- Continuous extras at exact rational heights, mesh denominators 2, 3, 4: 40 northern extras at den 4, independence 4, not 11. No 41-code.
- Unrestricted interval unchanged: . Did not beat Mittelmann–Vallentin. Did not produce a 41-point code.
2026-08-27 — q4 unrestricted dual hunt
- Folder
compute/q4/. House rules unchanged: do not claim ; a numerical SDP without an exact positivity certificate is residue. - Re-fetched tonight, all still : Tao https://teorth.github.io/optimizationproblems/constants/29a.html, Cohn table https://cohn.mit.edu/kissing-numbers/ (dim 5: 40 / 44, refs [9] and [17]), Mittelmann–Vallentin arXiv:0902.1105v3 (), Bachoc–Vallentin arXiv:math/0608426v4 (3-point SDP, before MV; exact / formulas, Remark 3.4 monomial form), Cohn–Rajagopal arXiv:2412.00937v3. The unaffiliated Zenodo note remains retracted.
- Implemented exact over (
bv.py). Self-tests: , , , , for , matchesdelsarte.py. - 1-point continuum Delsarte at degree 12 is . One
rationalization (
den=1000) gives and fails Sturm. Did not spend the session re-rationalizing Gegenbauer polynomials. - Exact 3-point search, all residue or :
- constant-multiplier Putinar : HiGHS infeasible;
- diagonal grid LP: infeasible at , grid value at (matches 1-point Delsarte at degree 4);
- exact -span kernel at : 34 / 81 / 148 nonnegative kernel vectors, none make on ;
- square-dictionary LP: infeasible at ; numerical at does not snap to an identity over ;
- floating Putinar SDP at (Clarabel / SCS): solver values
below 40 or on the dummy cut ,
grid_ok=false. Discarded.
- Best certified unrestricted dual remains Levenshtein (the case of BV). No is excluded on the whole interval. Mittelmann–Vallentin is still the published upper bound; that hierarchy cannot go below its own optimum at , so a dual would need or a different hierarchy and an exact SOS certificate.
- Wrote
compute/q4/dual_exact.json. Nocerts/unrestricted_delsarte.jsonorcerts/bv_dual.json.
2026-08-27 — q4 leftover graphs (no unrestricted move)
- Same house rules. Re-fetched Tao , Cohn, Mittelmann–Vallentin , Cohn–Rajagopal arXiv:2412.00937v3: still . Did not claim .
- The 240 missed-set seeds on the 40 roots split as 160
four-seeds and 80 six-seeds. The ten special octads are the
coordinate-stars . Every four-seed lives in
exactly one star, as the sign choices on the other four axes
(
analyze_stars.py). Independent Rust rebuild (verify_n1.rs): each star has 16 four-seeds, extras pool 80, . - Same-missed extras are edgeless, so a clique takes at most one extra per seed. A 41-set with needs an extras-clique of size whose missed sets sit in some -set .
- (): complete -superset scan, C and Python agree
(, 10 promising octads, best extras 8, total 40).
(): C empty (
n1_le32_k9.json). - Seed-union BFS through is complete and empty of a 41-set
(
n1_complete_k12.json, Pythonreplay_unions.py). Promising unions only at (80 heptads), (10 stars), (960), (4640); each has , total 40. - Hash-free canonical DFS (
n1_dfs.c) continues the same family without a table: each union has a unique parent (all but the last irredundant seed). Through the counts match the BFS. Through the scan is complete and empty of a 41-set (n1_dfs_k18.json): unions. Promising pools at through have extras , total 40. Independent Python BFS matches the union census through (replay_unions_k13.json). Therefore there is no 41-set that uses 22 or more -type points. The slice remains residue for the whole 1480-graph, not a 41-code. - 40-colouring of the 1480-graph is UNSAT (Cadical and Glucose). That does not produce a 41-clique.
- remainder: no 35-colouring. Cadical and Glucose return no
36-clique (
t5_omega.json). UNSAT without a stored DRAT is not an emptiness proof. Share with each published 35 is empty (Python). Share 30 down to 24 are empty in C (t5_share30_c.jsonthrought5_share24_c.json). Any remaining 36-clique shares at most 23 with every published 35. - Construction hunts outside these two graphs (other , hyperplane, projections, QR reflections) produced no 41-code.
- Unrestricted interval unchanged: . Did not beat Mittelmann–Vallentin. Did not produce a 41-point code.
2026-08-27 — continue (q5)
- Start from the q4 branch (
cursor/kissing-5d-q4-cd01, PR #91 not on main). Foldercompute/q5/. House rules unchanged: do not claim ; a numerical SDP without an exact positivity certificate is residue; do not regress the restricted certificates already incompute/certs/,compute/q1/–q4/. Covering stays frozen. - Hunt: finish the two leftovers (a 41-set in the 1480-graph with , or a 36-clique sharing with every published 35), or produce an exact 41-point code, or an exact unrestricted dual below 44. Residue if the interval does not move.
2026-08-27 — q5 leftovers (interval unchanged so far)
- Re-fetched Tao , Cohn, Mittelmann–Vallentin , Cohn–Rajagopal arXiv:2412.00937v3: still . Did not claim .
- Extra types on the 1480-graph: 160 four-seeds (1 type A
+ 4 type B ) and 80 six-seeds (8 type C
). A type-A 20-clique exists with , total 26,
not a 41-set (
type_a_clique.json). Type-A leftover hunt (type_a_small_U.json) is complete: no type-A clique with and (196{,}750 nodes). - Seed compatibility graph is 240-vertex 231-regular
(
seed_graph.json). The 80 six-seeds form an 80-clique of union 40. Every 3-star union is leftover-tight: 80 pools and 40 pools . A seed-clique is a pool, not a 41-code. - Extras B&B on all 120 three-star pools is complete and empty of a
leftover 41-set (
triple_star_extras.json): extras on the 80 unions of size 21, on the 40 unions of size 22. With q4's empty, no 41-set has contained in three coordinate-stars. The leftover slice, if nonempty, has star-cover at least 4. - Part-count MILP on hits cutoff with verified
incumbents contained seeds (
n1_partcount.json). The leftover is not empty by part-count. Cutoff is not a proof of the maximum. - leftover SAT (30{,}678 vars) is running; no model yet.
Extras B&B 200M nodes: no 41-set, incomplete (
extras_clique.json). - remainder: PySAT Cadical195 returns UNSAT for a 36-clique
(
t5_36_proof.json, 16{,}548{,}926 proof lines). Heuledrat-trimon that ASCII file endeds NOT VERIFIED(no conflict). Native CaDiCaL 3.0.1 on the same CNF is UNSAT in 573s (9{,}921{,}324 conflicts) and writes a 671{,}198{,}215-byte binary DRAT.drat-trimon that file:s VERIFIED(756s; 4{,}787{,}602 of 10{,}804{,}713 lemmas in core; 0 RAT). There is no 36-clique in the 355-point remainder, so the Szöllősi pool has no 41-point kissing code. Share 23 is empty as well (t5_share23.json): neighbourhoods of each published remainder 35 have extras (need 13). Restricted finite-graph facts. Not an unrestricted bound. - No unrestricted dual below 44 (
dual_more.json: 1-point Delsarte still ; best certified ansatz ). No 41-code in the finished construction pools (construct_more.json). - Unrestricted interval unchanged: . Did not beat Mittelmann–Vallentin. Did not produce a 41-point code.
2026-08-27 — continue (q6)
- Start from the leftover branch after q5 (
cursor/kissing-5d-q4-cd01, PR #97 merged there). Foldercompute/q6/. House rules unchanged: do not claim ; a numerical SDP without an exact positivity certificate is residue; covering stays frozen. - Re-fetched tonight, all still : Tao https://teorth.github.io/optimizationproblems/constants/29a.html, Cohn table https://cohn.mit.edu/kissing-numbers/ (dim 5: 40 / 44, ratio 1.100, refs [9] and [17]; later-dimension news does not touch dim 5), Mittelmann–Vallentin arXiv:0902.1105v3 (), HTML https://ar5iv.labs.arxiv.org/html/0902.1105v3 Table 1, Bachoc–Vallentin arXiv:math/0608426v4, Cohn–Rajagopal arXiv:2412.00937v3 (“appears to be 40… best upper bound that has been proved is 44”).
- Hunt: empty the leftover slice of the 1480-point graph (star-cover ), or produce an explicit 41-set; in parallel an exact unrestricted dual below 44. Residue if the interval does not move.
- First measurement: greedy colouring of extras in every 4-star pool
(
four_star_color.json) uses 20 to 32 colours. So the 3-star colouring bound does not lift. Pools are 320 extras (, two full axes), 384 (), or 434 (). - C leftover-tight B&B on all 210 four-star pools is complete and
empty (
four_star_extras.json, 26{,}857{,}470 nodes,best=19is the start value). Independent Python leftover-tight replay of 38 pools (every two-axis pool and a stride of the rest) matches: 38/38 complete empty, no 41-set (replay_four_star.json). Restricted: no leftover 41-set has contained in four coordinate-stars. Not extras , not an unrestricted bound. The leftover slice, if nonempty, has star-cover at least 5. - Minimum with star-cover is 5 (
star_cover_min.json, Cadical hitting-set of the 210 four-star complements; witness independently checked). So is not empty by combinatorics. - Five-star colouring uses 28 to 39 colours; none
(
five_star_color.json). Four five-star C pools hit a 20M node cutoff incomplete (five_star_sample.json). - No unrestricted dual below 44 (
dual_more.json): 1-point Delsarte still ; rationalizations fail Sturm; 51 certified ansätze, best . Did not beat Mittelmann–Vallentin. Did not claim . - Two-axis leftover SAT: all ten pools are SAT-unsat
(
two_axis_extras.json). Nine of ten Python B&Bs were already complete empty. SAT-unsat without a stored DRAT is residue for those CNFs; the C / leftover-tight Python emptiness is the certificate. - Global leftover-tight extras B&B with the 4-star grow-prune
(
leftover_global.json,n_four_star=210) ran 200M nodes, no 41-set, incomplete. Same leftover as q5 extras B&B, plus the prune. - Leftover-tight SAT on the four five-star pools that hit the
C 20M cutoff is SAT-unsat (
five_star_sat.jsonsnapshot). Two more pools in that sample were still running. SAT-unsat without DRAT is residue. - Global leftover SAT with star-cover (30{,}678 vars,
Cadical195 and Kissat404 in parallel) had no model after half an
hour (
leftover_sat_status.json). Incomplete. Residue, not a lower bound. - Unrestricted interval unchanged: . Did not beat Mittelmann–Vallentin. Did not produce a 41-point code. Did not claim . Residue.
2026-08-27 — continue (q7)
- Start from main after PR #101 (
809cdad). Foldercompute/q7/. House rules unchanged: do not claim ; a numerical SDP without an exact positivity certificate is residue; covering andshare/2026-08-16stay frozen. - Re-fetched tonight, all still : Tao https://teorth.github.io/optimizationproblems/constants/29a.html (range , conjectural value 40; upper bound Mittelmann–Vallentin), Cohn table https://cohn.mit.edu/kissing-numbers/ (dim 5: 40 / 44, ratio 1.100, citations [9] Korkine–Zolotareff and [17] Mittelmann–Vallentin; dim 6 is 72 / 77; later-dimension news does not touch dim 5), Mittelmann–Vallentin arXiv:0902.1105v3 (), HTML https://ar5iv.labs.arxiv.org/html/0902.1105v3 Table 1, Bachoc–Vallentin arXiv:math/0608426v4, Cohn–Rajagopal arXiv:2412.00937v3 (“the kissing number in five dimensions appears to be 40, although the best upper bound that has been proved is 44”). Survey arXiv:1507.03631.
- Hunt: empty leftover with star-cover at least 5, or empty the 5-star leftover hosts (252 pools, three Aut() orbits), with stored native CaDiCaL DRAT; leftover-tight extras B&B past the q6 200M-node cutoff by dropping the grow cap; exact unrestricted dual below 44. Residue if the interval does not move.
- Plan: (1) classify 5-star hosts by signed-permutation orbits and
SAT leftover-tight CNFs on one representative of each type plus
the four q6 cutoff pools; (2) global leftover SAT
star-cover with native CaDiCaL / Kissat; (3) always-on
grow prune in
leftover_global.c; (4) one more dual grid, then drop that line if it stays above 44. - Signed permutations act transitively on each 5-star type
(
orbits.json: 60 of type , 160 of type , 32 of type ; Aut order ). - Minimum with star-cover is 5; with star-cover
is 8 (
star_cover_min.json). Neither empties . - Dual line dropped (
dual_more.json): 1-point Delsarte still ; exact duals that certify sit at best . Did not beat Mittelmann–Vallentin. - Native leftover-tight SAT on the orbit representative
(stars ) is UNSAT: CaDiCaL 3.0.1,
conflicts, binary DRAT bytes, Heule
drat-trims VERIFIED(five_star_sat.json). Combined with Aut transitivity this empties all 60 type- five-star leftover hosts. The q6 cutoff pool is likewise UNSAT with a verified DRAT ( conflicts). - All four q6 cutoff pools are UNSAT with verified native
DRATs (
five_q6_01235,five_q6_01236,five_q6_01237, and the orbit representative). Combined with Aut transitivity the type- leftover hosts are empty. - Leftover-tight extras B&B with always-on grow prune ran 400M
nodes in about 90 seconds, no 41-set, incomplete
(
leftover_global_400m.json). The cap was the cost; remaining missed-union is cheap. With the type- 5-star prune (five_mode=2) the same search ran nodes in seconds, no 41-set, incomplete (leftover_global.json). five_mode (types and , unions) ran another G nodes in seconds, no 41-set, incomplete (leftover_global_mode3.json). Past the q6 200M cutoff; still residue. - leftover-tight SAT is UNSAT with a verified native DRAT
(
five_k31_n1_3: conflicts, DRAT bytes,drat-trimof lemmas, resolution steps). Combined with Aut transitivity this empties all 160 type- five-star leftover hosts. Remaining 5-star leftover hosts are the 32 type- pools. - leftover-tight SAT and global leftover SAT were still writing native DRATs when this pass wrapped (past GB and GB). Incomplete. Residue, not a lower bound.
- Unrestricted interval unchanged: . Did not beat Mittelmann–Vallentin. Did not produce a 41-point code. Did not claim . Residue.
2026-08-27 — continue (q8)
- Start from main after PR #102 (
87674a7). Foldercompute/q8/. Covering frozen. Do not claim . - Re-opened tonight, still : Tao https://teorth.github.io/optimizationproblems/constants/29a.html, Cohn table https://cohn.mit.edu/kissing-numbers/ (dim 5: 40 / 44, ratio 1.100), Mittelmann–Vallentin arXiv:0902.1105v3, Cohn–Rajagopal arXiv:2412.00937v3.
- Leftover after q7: type- five-star hosts (32 pools, , 625 extras) and global leftover SAT with star-cover at least 5. The global CNF here also forbids the type- and type- five-star unions q7 emptied.
- Hunt: leftover-tight SAT / B&B on the type- orbit representative with a stored native DRAT, or a 41-set; stronger global leftover SAT. Residue if the interval does not move.
2026-08-29 — wrap (q8)
- Rebased onto
origin/main(b5a2b71). Covering andshare/2026-08-16untouched. Later README claims left as they stand (Caccetta leftover through , hole , ; ionization ; and the rest). - Re-opened the record: still (Tao , Cohn table dim 5: 40 / 44, Mittelmann–Vallentin , Cohn–Rajagopal arXiv:2412.00937v3).
- Type- leftover-tight CNF
(
certs/five_k30_n0_5.cnf.json, sha256cdec5e76…, same encoding as the unfinished q7 instance) and the stronger global leftover CNF (n1_k19_star5_no21_no13.cnf.json, 220 five-star forbids) were written and independently rebuilt. Cubes pin for (certs/k30_cubes.json). - Native CaDiCaL on the leftover-tight instance wrote a
binary DRAT past GB (about four hours of solver time) and
did not exit. The weaker q7 global leftover DRAT passed GB
and did not exit. Kissat probes on both q8 CNFs were unfinished.
No
drat-trims VERIFIED. Nocerts/code41.json. - leftover_k30 smoke (2000 nodes,
five_mode3) is not a certificate. q7 leftover extras B&B at G nodes with the type-/ prune was already incomplete. - Unrestricted interval unchanged: . Did not beat Mittelmann–Vallentin. Did not produce a 41-point code. Did not claim . Residue.