reggeActionCriticalAtZero_of_directional
plain-language theorem explainer
Directional vanishing of the Fréchet derivative of the nonlinear Regge action at the flat vertex potential upgrades to full criticality (the derivative map is identically zero). Anyone who has established the first variation along lines can cite this to obtain the operator-level statement. The argument is pure extensionality after unfolding the two criticality predicates.
Claim. Let $K$ be an incidence-consistent 3-dimensional triangulation. If for every vertex potential $\eta$ one has $D(\mathrm{Regge\,action})_0(\eta)=0$ at the flat (zero) potential, then the Fréchet derivative of the nonlinear Regge action at the flat potential is the zero continuous linear map.
background
This module targets the vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential. The geometric engine is Schläfli cancellation plus zero deficit; the analytic work is to differentiate hinge and dihedral terms and apply global Schläfli to the angle contribution.
Two criticality predicates sit side by side. Full criticality asserts that the Fréchet derivative of the Regge action at the zero potential is the zero map. Directional criticality asserts the same fact pointwise: the derivative applied to every vertex potential $\eta$ is zero. The directional form is the natural output of differentiating along affine lines through the flat configuration.
The ambient objects are a 3D triangulation $K$ and an incidence-consistency hypothesis ensuring the combinatorial skeleton supports well-defined hinge measures and dihedral angles.
proof idea
One-line bridge between the two Prop wrappers. Unfold full criticality to the equality of continuous linear maps, then apply function extensionality on the domain of vertex potentials; each pointwise evaluation is exactly the directional hypothesis. No geometric or analytic lemma is invoked.
why it matters
This is the glue that lets line-wise first-variation calculations discharge the operator-level criticality goal used downstream. The parent theorem reggeActionCriticalAtZero_of_firstVariationFormula_of_zeroDeficit reduces criticality under a global zero-deficit hypothesis and an explicit first-variation formula to a directional check, then applies this lemma. The companion constructor reggeActionFirstVariationInput_of_directional packages the same upgrade into the named input bundle for the first-variation pipeline.
In the Recognition geometry stack this sits under the Regge-action analysis that supports discrete curvature and flat-background stability. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure functional-analysis bookkeeping inside the Regge module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.