dihedralCos3Sq_conformal_continuousAt_zero
plain-language theorem explainer
At the flat (zero) vertex potential, the squared dihedral cosine of any face pair on a tetrahedron remains continuous when edges are read from the conformal squared-edge chart. Nonlinear Regge and Hessian arguments cite this to justify differentiating the action through the arccos of that cosine. The proof is ContinuousAt.comp of local dihedral continuity with C^infty continuity of the conformal edge map at zero.
Claim. Let $K$ be a 3D triangulation, $\tau$ a tetrahedron of $K$, and $f\in\{0,\ldots,5\}$ an edge index. The map sending a vertex potential $\xi$ to the squared cosine of the dihedral angle associated with $f$, computed from the six squared edge lengths of the conformally deformed tetrahedron at $\xi$, is continuous at the zero potential.
background
This module supplies analytic inputs for the full nonlinear Regge action on a 3D triangulation: the conformal edge chart must stay in the nondegenerate tetrahedral cone, arccos arguments must avoid $\pm 1$, and the finite action must be smooth at the flat potential. Those requirements are packaged as named configuration facts rather than axioms.
Squared edge lengths of a tetrahedron are the type SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The Cayley–Menger polynomial in those six lengths yields volumes and, via cofactors, the squared cosine of a dihedral angle (dihedralCos3Sq). The conformal chart conformalTetSqEdges deforms the six edges of tetrahedron $\tau$ by a vertex potential $\xi$; at the zero potential the chart recovers the background edges.
A sibling lemma already gives continuity of dihedralCos3Sq at the image of the zero potential whenever the local denominator polynomial is nonzero (interior nondegeneracy). Continuity of the conformal chart itself follows from its $C^\infty$ regularity on the potential space.
proof idea
Three steps, then composition.
- Invoke the sibling
local_dihedralCos3Sq_continuousAtfor $(K,\tau,f)$: dihedral cosine-squared is continuous at the squared-edge tuple of the zero potential. - Continuity of the conformal chart $\xi\mapsto\mathrm{conformalTetSqEdges}(K,\xi,\tau)$ at zero comes from
conformalTetSqEdges_contDiffat order $0$, then.continuous.continuousAt. - Rewrite the base continuity point via
conformalTetSqEdges_zeroso the dihedral map is continuous exactly at the chart image of zero.
Finish with ContinuousAt.comp: outer map is dihedral cosine-squared on SqEdges, inner map is the conformal chart, evaluation point is the zero potential.
why it matters
The closed second-order Regge component uses an exact quadratic truncation; the full nonlinear action needs this continuity so arccos of the dihedral cosine stays well-defined and differentiable through the conformal chart at flat space.
The sole recorded consumer is dihedralCos3Sq_conformalTetSqEdges_line_endpoint_free_eventually in ReggeActionNonlinearHessianProof, which upgrades pointwise continuity at zero to an eventually-free statement along real lines through the flat configuration (needed for Hessian and higher jet control).
In the broader Recognition geometry stack this is scaffolding for smoothness of the discrete gravitational action at the flat potential, not a forcing-chain (T0–T8) step. It closes an analytic gap between polynomial Cayley–Menger identities and the nonlinear action’s local chart.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.