{"id":"palomar/PALOMAR-2026-10-16-000020","url":"https://github.com/JD-Jones-ASES/augmented-descartes-lean/tree/44bdbf1dec3ffab07c97da8544aca6255826ded2","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-16-000020-v1.json","repo":"https://github.com/JD-Jones-ASES/augmented-descartes-lean","tags":["math.MG","msc:52C26","msc:51M04","msc:51B10","discrete-geometry","descartes-theorem","lean-formalization","sphere-packing"],"score":0,"title":"The augmented Descartes theorem in every dimension, its converses, and Soddy's two spheres","trust":"high","domain":"math.MG","source":"palomar","authors":["JD Jones"],"reviews":0,"subject":"math.MG","summary":"A Lean 4 development of Section 3 of Lagarias, Mallows and Wilks, Beyond the Descartes circle theorem (Amer. Math. Monthly 109 (2002) 338-361), in the Lorentz form. An oriented sphere in R^n with centre x and signed radius r has the augmented curvature-centre row (|x|^2/r - r, 1/r, x/r); an oriented hyperplane = delta with unit normal h has the row (2 delta, 0, h) (LMW Definition 3.2, (3.7)-(3.9)). Tangency is distance-encoded in LMW's oriented sense: two spheres dist^2 = (r + s)^2 (external tangency for two positive radii, internal when one radius is negative), a sphere and a hyperplane -…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-16","reactions":{},"formalized":true,"formalizes":[{"title":"Beyond the Descartes circle theorem","identifier":"doi:10.1080/00029890.2002.11920896","relationship":"formalizes"},{"title":"Apollonian circle packings: geometry and group theory III. Higher dimensions (arXiv versions 1 and 2)","identifier":"arXiv:math/0010324v2","relationship":"formalizes"},{"title":"Apollonian circle packings: geometry and group theory I. The Apollonian group","identifier":"doi:10.1007/s00454-005-1196-9","relationship":"formalizes"}]}