reggeActionFirstVariationInput_of_directional
plain-language theorem explainer
Packages directional criticality of the nonlinear Regge action at the flat zero potential into the named first-variation input structure. Anyone assembling the analytic first-variation package for a consistent 3D triangulation cites this. The body is a one-field structure constructor that applies the directional-to-full criticality conversion.
Claim. Given a 3D triangulation $K$ with consistent incidence, a flat analytic configuration at the base point, and the hypothesis that every directional derivative of the Regge action at the zero vertex potential vanishes, one obtains a first-variation input record whose sole field asserts that the Fréchet derivative of the Regge action at zero is the zero map.
background
This module targets 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; until the closed-form local identities are fully expanded, the module records the exact analytic statement and a named input bundle.
Directional criticality means: for every vertex potential $\eta$, the Fréchet derivative of the Regge action at the zero potential, applied to $\eta$, is zero. Full criticality is the same statement packaged as the derivative map being identically zero. A flat configuration supplies the arccos endpoint condition, zero-deficit flatness, and the smoothness needed for Taylor theory.
The structure ReggeActionFirstVariationInput is the named bundle whose single field is full criticality at zero. Its doc-comment sketches the intended lower-level proof: differentiate hinge-length and local dihedral factors, use zero deficit on the hinge term, then global Schläfli on the dihedral term.
proof idea
One-field structure constructor. The sole field firstVariation_zero is filled by applying reggeActionCriticalAtZero_of_directional, which converts the directional criticality hypothesis into full criticality by unfolding the full-criticality predicate and extensionality on the direction $\eta$. No further analytic work occurs here.
why it matters
Sits in the Geometry layer that prepares the first variation of the nonlinear Regge action. The module goal is vanishing of that variation at the flat conformal potential via Schläfli cancellation and zero deficit. This definition is the bridge from the directional form (natural when differentiating along lines) to the named input structure that downstream first-variation arguments are expected to consume.
No used_by edges are recorded yet, so it is presently a packaging step rather than a cited lemma. It does not itself invoke the forcing chain (T0–T8), RCL, or the phi-ladder mass formula; those enter only if the Regge criticality package is later tied to continuum limits or curvature matching in the broader Recognition framework. It closes no scaffold; it merely re-packages an already-proved conversion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.