LocalEdgeVariation
plain-language theorem explainer
For a finite 3D Regge triangulation, a local edge variation is a real assignment of a derivative to each of the six edges on every tetrahedron. Discrete-geometry and Regge-calculus work cites this type when differentiating edge-length data without fixing a global length chart. It is a pure type abbreviation: the name expands to a function type and carries no proof content.
Claim. Given a finite 3D Regge triangulation $K$ with $n_T$ tetrahedra, a local edge variation is a map $\mathrm{Fin}(n_T)\to\mathrm{Fin}(6)\to\mathbb{R}$ that assigns a real derivative to each of the six edges of each tetrahedron.
background
The module supplies the finite incidence scaffold that lifts local tetrahedral identities to arbitrary 3D Regge triangulations. A triangulation records vertex, edge, and tetrahedron counts, incidence maps (edge endpoints, tetrahedron vertices, optional local edge index of a global edge inside a tetrahedron), and a nondegenerate squared-edge 6-tuple on every tetrahedron.
Each tetrahedron has six edges, indexed by $\mathrm{Fin},6$. The present abbreviation packages, for a fixed triangulation, one real number per tetrahedron per local edge. The doc-comment stresses the design choice: a global assignment of local derivatives, without committing to a single global length-coordinate chart.
The parameter name $K$ is the triangulation structure, not the dimensionless bridge ratio $\varphi^{1/2}$ nor the curvature functional from the constants modules; those appear only as name collisions in the dependency graph.
proof idea
Pure definitional abbreviation. The body is the function type $\mathrm{Fin},K.n_T\to\mathrm{Fin},6\to\mathbb{R}$. No lemmas, tactics, or algebraic reduction.
why it matters
This type is part of the finite 3D Regge incidence layer that lets local tetrahedral calculus (edge variations, deficit angles, discrete curvature) be stated uniformly on an arbitrary triangulation. The separated local representation deliberately postpones choosing a global edge-length chart, which keeps later variational identities chart-independent.
No downstream theorems currently depend on it in the graph, so it is scaffolding infrastructure rather than a proved forcing-chain step. It sits in the geometry domain that supports discrete realizations of spatial structure (cf. the $D=3$ landmark), not in the T0–T8 uniqueness chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.