cm3_continuous
plain-language theorem explainer
The Cayley-Menger polynomial in six squared edge lengths is continuous as a real map on edge-length space. Anyone building Regge second-variation or volume-from-edges arguments from the explicit tetrahedron polynomial would cite it. The proof is a one-line extraction of continuity from the already-proved fact that the same polynomial is C^n for every n.
Claim. The map $\mathrm{CM}_3:\mathbb{R}^6\to\mathbb{R}$ sending six squared edge lengths of a tetrahedron to the classical Cayley-Menger value is continuous.
background
This module fixes an explicit degree-3 polynomial $\mathrm{CM}_3$ in the six squared edge lengths of a tetrahedron (vertices $0,1,2,3$), with edges indexed by $\mathrm{Fin},6$ as opposite pairs $(0,5)$, $(1,4)$, $(2,3)$. Classically $288,V^2=\mathrm{CM}_3(a)$ for a genuine tetrahedron of volume $V$. The polynomial is written out by hand and checked on the regular and right-angle unit test points.
The local goal is Philip's Regge concern: the genuine second-variation coefficient matrix from Cayley-Menger / dihedral derivatives must eventually match face areas componentwise. Smoothness of $\mathrm{CM}_3$ in the squared lengths is the analytic prerequisite for those derivatives.
Upstream, $\mathrm{CM}_3$ is defined as that fixed multilinear combination of products of edge coordinates, and a companion theorem builds $\mathrm{ContDiff},\mathbb{R},n,\mathrm{CM}_3$ for every extended natural $n$ from evaluation maps and the standard $\mathrm{ContDiff}$ add/sub/mul combinators.
proof idea
One-line term proof. Instantiate the upstream smoothness theorem at order $n=0$ to obtain $\mathrm{ContDiff},\mathbb{R},0,\mathrm{CM}_3$, then apply the Mathlib fact that every $C^0$ map is continuous. No separate continuity argument is written; continuity is inherited from the ContDiff construction.
why it matters
Continuity of the explicit tetrahedron Cayley-Menger polynomial is the first analytic corollary after full $C^n$ smoothness. It sits in the Geometry layer that prepares genuine Regge second-variation data: once $\mathrm{CM}3$ is continuous (and smooth), volume-squared and its edge derivatives are legitimate real-analytic objects on squared-length space, so the planned componentwise comparison of the Hessian block $M{ij}$ to face areas can proceed without topology gaps.
No downstream consumers are wired yet in the graph; the declaration is infrastructure for the module's scaling and constancy lemmas and for later hinge-aware Regge analysis. Within Recognition Science it supports the geometric side of the forcing program (spatial $D=3$, discrete edge data) rather than a named T0-T8 step. It closes no open sorry; it simply makes the polynomial usable as a continuous observable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.