conformalSqEdge
plain-language theorem explainer
Defines the conformal squared-edge map on a tetrahedron: given background length ℓ₀ and vertex conformal factors ξ, each of the six edges receives squared length ℓ₀² exp(ξ_i + ξ_j). Geometers working the Regge Hessian under a conformal ansatz cite it as the edge-length input. The body is a direct pointwise formula via the edge-to-vertex pairing.
Claim. For a background length $\ell_0 \in \mathbb{R}$ and vertex conformal factors $\xi : \{0,1,2,3\} \to \mathbb{R}$, the conformal squared-edge assignment is the map $e \mapsto \ell_0^2 \exp(\xi_i + \xi_j)$ on the six edges of a tetrahedron, where $(i,j)$ are the endpoints of edge $e$.
background
This module builds the rigorous base for the 3D Regge component theorem $M_{ij} = -\mathrm{area}(f_{ij})$. It packages the Cayley-Menger polynomial $\mathrm{CM}_3$ in six squared edge lengths, its gradient and Taylor identity, and named classical hypotheses (Schläfli, dihedral cosines, smoothness on the realisability cone) needed to lift those into a conditional Hessian statement under a conformal edge ansatz.
Squared edge lengths live in $\mathrm{SqEdges} := \mathrm{Fin},6 \to \mathbb{R}$. The helper edgeVertices pairs each edge index with its two endpoints among the four tetrahedron vertices: edge 0 is $(0,1)$, edge 1 is $(0,2)$, and so on through edge 5 = $(2,3)$. The conformal ansatz multiplies a flat background $\ell_0^2$ by an exponential of the sum of the conformal factors at those two vertices, so edge lengths stay positive whenever $\ell_0 \neq 0$.
proof idea
Pure definition, not a proof. For each edge index $e$, look up the endpoint pair $(v_1,v_2)$ via the fixed edge-to-vertex table, then return $\ell_0^2 \cdot \exp(\xi_{v_1}+\xi_{v_2})$. No lemmas are applied; the expression is the entire content.
why it matters
The conformal edge ansatz is the geometric input to the conditional Regge component theorem in this module: under named classical hypotheses, the Regge Hessian off-diagonals become $M_{ij}=-\mathrm{area}(f_{ij})$. Downstream, the zero-section identity shows that $\xi\equiv 0$ recovers the constant regular assignment $\ell_0^2$; smoothness of the map in $\xi$ (each component is a constant times $\exp$ of a linear form) and smoothness of $\mathrm{CM}_3$ composed with it feed the certificate structure that packages the foundation. Without this map there is no conformal family on which to differentiate volumes and dihedral angles toward the component formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.