firstVariationFormula_of_directionalFormula
plain-language theorem explainer
Given a flat, incidence-consistent 3D triangulation, the directional first-variation formula for the nonlinear Regge action along every line through the zero potential upgrades to the Fréchet first-variation formula at that base point. Anyone assembling analytic input for vanishing first variation of the Regge action cites this bridge. The proof is uniqueness of one-variable derivatives: the line restriction's derivative equals both the Fréchet pairing and the hinge-deficit sum.
Claim. Let $K$ be an incidence-consistent 3-dimensional triangulation that is flat at the zero conformal potential. If for every vertex potential $\eta$ the map $t \mapsto S_{\mathrm{Regge}}(v_0 + t\eta)$ has derivative at $t=0$ equal to $\sum_e \ell'_e(\eta)\,\delta_e(v_0)$, then the Fréchet derivative of the Regge action at the zero potential satisfies $DS_{\mathrm{Regge}}(v_0)[\eta] = \sum_e \ell'_e(\eta)\,\delta_e(v_0)$ for every $\eta$.
background
The module targets vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential, via Schläfli cancellation plus zero deficit. Configurations live on a 3D triangulation $K$ with incidence consistency. The zero potential is the flat base point; a flat configuration packages arccos endpoint freeness, zero deficit, and the smoothness needed for Taylor theory on the nonlinear action.
Two named formula packages appear. The directional package asserts that along every affine line $t\mapsto v_0+t\eta$ through the zero potential, the ordinary derivative of the Regge action equals the sum over edges of hinge-measure directional derivatives times deficit angles at $v_0$. The Fréchet package asserts the same identity for $DS_{\mathrm{Regge}}(v_0)[\eta]$. An upstream lemma records that the line restriction is differentiable at $0$ with derivative equal to that Fréchet pairing.
proof idea
Term-mode construction of the Fréchet formula structure. For arbitrary direction $\eta$, obtain two HasDerivAt witnesses at $t=0$ for the same line map $t\mapsto S(v_0+t\eta)$: one from the upstream line-to-Fréchet lemma (value $DS(v_0)[\eta]$), and one from the directional-formula hypothesis (value equal to the hinge-deficit sum). Uniqueness of derivatives equates the two values, which is exactly the required Fréchet identity.
why it matters
This is the analytic bridge from one-variable product-rule calculations (the form natural after differentiating hinge and dihedral terms) to the Fréchet statement needed for the first-variation input package. Downstream, the local-angles constructor builds that input from the Fréchet formula together with a local dihedral directional-derivative package and conformal Schläfli cancellation.
In the Recognition geometry stack this feeds vanishing of the first variation at flat space, the discrete precursor to Einstein equations from the Regge action. The module frames the geometric content as Schläfli cancellation plus zero deficit; this lemma isolates the derivative-uniqueness step so the hard work stays in establishing the directional formula from closed-form local Schläfli identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.