A computer-assisted upper bound m_1(R^3) ≤ 0.149564 for measurable sets avoiding unit distance (certificate and short note)

Let m1(R3) be the largest upper density of a Lebesgue measurable set in R3 with no two points at distance 1. DeCorte, de Oliveira Filho and Vallentin (Math. Program. 191 (2022); arXiv:1804.09099) proved m1(R3) ≤ 0.1532996 using Boolean-quadric constraints on point sets without unit distances. We add constraints on small configurations that contain exact unit distances; on such a configuration a constraint only has to hold on the independent sets of its unit-distance graph. With 15 constraints we obtain m1(R3) ≤ 0.149564. On their supports, 10 are three-point collinear triangle inequalities and 5 contain exact unit pairs; controls in the note show that the triangle inequalities alone give only 0.15292 and that almost all of the improvement comes from the constraints with unit pairs. Verification: (1) every constraint is checked exactly to be valid on all independent sets (check_validity.py, standard library only); (2) the configurations are exactified in 60-digit arithmetic, changing every used distance by at most 1.8e-16 (d3_exact.py); (3) the dual solution is checked by the unchanged verification program rn_verify of DeCorte, de Oliveira Filho and Vallentin (128-bit MPFR), output: minimum = -0.000100941112431; bound = 0.149563797200544. rn_verify itself is not redistributed; see README.md for the sha256 of the version used. The bound is above 1/7, so it does not improve the lower bound 7 for the measurable chromatic number of R3. This record has not been refereed; corrections are welcome.