ReggeActionDirectionalCriticalAtZero
plain-language theorem explainer
Directional criticality of the concrete 3D Regge action at the zero conformal potential: the Fréchet derivative in every vertex-potential direction vanishes. Cited by anyone discharging first-variation vanishing via line derivatives or Schläfli-plus-zero-deficit. Pure Prop definition quantifying over directions; no proof body.
Claim. For an incidence-consistent finite 3D triangulation $K$, the Regge action is directionally critical at the zero conformal potential when, for every vertex potential $\eta$, the Fréchet derivative of the Regge action at zero applied to $\eta$ is zero: $(D\,S_{\mathrm{Regge}})(0)\cdot\eta=0$.
background
The module records the analytic first-variation statement for the nonlinear Regge action under the vertex-conformal ansatz. The geometric target is vanishing of that variation at the flat (zero) conformal potential, via Schläfli cancellation plus zero deficit.
A finite 3D triangulation carries abstract incidence data and a nondegenerate squared-edge tuple on every tetrahedron. Vertex conformal potentials are real assignments to vertices; the zero potential is the constant-zero map. The concrete Regge action sums, over edges, hinge measure times deficit angle evaluated under the conformal deformation of edge lengths.
Directional criticality is the form convenient while differentiating the action along affine lines through zero, before packaging the result as a full Fréchet-criticality statement.
proof idea
Definition only: the body is the universal quantification that the Fréchet derivative of the concrete Regge action at the zero potential annihilates every vertex-potential direction. No tactics, no lemmas applied, no obligations discharged.
why it matters
Working form of criticality while the first variation is derived by line differentiation. Downstream, directionalCritical_of_firstVariationFormula_of_zeroDeficit proves this Prop from a named first-variation formula plus global zero deficit at flat; reggeActionCriticalAtZero_of_directional converts it to full criticality (extensional equality of the derivative map with zero); and reggeActionFirstVariationInput_of_directional packages the directional fact into the structured input expected by the module's target theorem.
In the broader Recognition geometry chain this is the analytic hinge between discrete Schläfli identities on tetrahedra and the claim that the flat conformal configuration is a critical point of the Regge action, the discrete precursor to vacuum Einstein equations in three spatial dimensions (forcing landmark T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.