ReggeFirstVariationFormula
plain-language theorem explainer
Packages the first-variation identity for the conformal nonlinear Regge action on a 3D triangulation: at the zero vertex potential, the Fréchet derivative equals the pairing of hinge deficit angles with conformal edge-length directions. Gravity and discrete GR workers cite it as the named input that turns criticality into zero deficit once incidence rank is known. The structure is pure data; a unit-edge constructor reduces it from the geometry-layer first-variation formula by rescaling coefficients.
Claim. For an incidence-consistent 3D triangulation $K$, a first-variation formula is a certificate that for every vertex potential $\eta$, $$D(\text{Regge action})_0(\eta)=\sum_e \varepsilon_e(0)\,\ell'_e(\eta),$$ where $\varepsilon_e(0)$ is the deficit angle at hinge $e$ in the flat (zero-potential) background and $\ell'_e(\eta)$ is the directional conformal length coefficient of edge $e$ along $\eta$.
background
This module treats the discrete vacuum Einstein equation for the conformal nonlinear Regge action. The vacuum condition is zero deficit at every hinge. Forward implication (zero deficit $\Rightarrow$ criticality) uses global Schläfli cancellation; the reverse needs a nondegeneracy/rank hypothesis on the conformal edge-incidence derivative. The module records that equivalence as a named input rather than an axiom.
The structure lives before zero-deficit is imposed. The Regge action is differentiated at the zero vertex potential (the flat conformal background). Each hinge contributes its deficit angle times a directional length coefficient that records how conformal vertex potentials stretch that edge. Incidence consistency of $K$ supplies a well-defined global squared edge-length field used by the geometry layer.
Upstream, the geometry module supplies a first-variation formula whose hinge measure derivatives still carry explicit $\sqrt{\text{globalSqEdge}}$ factors. When those lengths are normalized to one, the dimensionless vacuum pairing above is exactly the geometry formula.
proof idea
The declaration itself is a structure: one field, the $\forall\eta$ identity, with no proof obligation.
The companion constructor ofGeometryFormula_unitEdges is a short algebraic reduction. Fix $\eta$, rewrite by the geometry-layer first-variation identity, then compare summands edgewise: replace each hinge-measure directional derivative by $\sqrt{\text{globalSqEdge}(e)}\cdot\ell'_e(\eta)$, cancel the unit-edge hypothesis $\sqrt{\text{globalSqEdge}(e)}=1$, and finish with ring. No analytic estimates enter.
why it matters
This is the hinge between geometry-layer Regge calculus and the discrete vacuum Einstein package. Downstream, zero_deficit_of_critical_of_variationFormula_of_separating uses the formula plus incidence-deficit separation to conclude zero deficit from criticality at flat backgrounds. The constructors discreteVacuumEinsteinInput_of_variationFormula_of_separating and discreteVacuumEinsteinInput_of_recoveringIncidence bundle it into the full vacuum-Einstein input; the restricted-incidence module reuses the same pairing on a declared deficit subspace.
In Recognition Science gravity, the continuum Einstein vacuum equation is recovered from a discrete ledger via Regge action. The first-variation pairing is the exact discrete analogue of $\delta S=\int G_{\mu\nu}\delta g^{\mu\nu}$: deficits play the role of Einstein curvature, conformal length directions the role of metric variations. It does not itself force $D=3$ or the eight-tick structure (those sit in the T0–T8 chain); it is the local variational step once a 3D triangulation is given.
Open work is discharging the structure on concrete triangulations (recovering or separating incidence) rather than leaving it as an input hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.