The augmented Descartes theorem in every dimension, its converses, and Soddy's two spheres
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 -…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-16-000020
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-16-000020/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-10-16-000020/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'