ReggeActionSecondVariationInput
plain-language theorem explainer
Named input package asserting that the full nonlinear Regge action has second variation equal to the canonical incidence Hessian at a flat configuration, tested along every conformal line of vertex potentials. Downstream Hessian proofs and the combined local Taylor inputs cite this structure as the second-variation hypothesis. It is a pure data structure with one Prop field, not a proved identity.
Claim. For a finite 3D Regge triangulation $K$ with incidence consistency and a flat analytic configuration, a second-variation input is the assertion that for every vertex potential $\xi$, the scalar map $t \mapsto S(t\xi)$ (nonlinear action along the conformal line) has second derivative at $t=0$ equal to the quadratic form of the canonical Regge Hessian evaluated on $\xi$.
background
The module packages nonlinear second-variation and cubic-remainder targets for the Regge action in a form usable before the full Cayley-Menger/arccos chain-rule expansion is complete. Analytic facts therefore live in named input structures rather than as unconditional theorems.
A Triangulation3D is a finite abstract 3D Regge complex (vertices, edges, tets) with nondegenerate squared-edge data. Incidence consistency supplies global squared edges, local-to-global edge agreement, and the closed-form Schläfli data needed for global identities. A flat configuration adds the arccos endpoint condition, zero deficit at the base point, and the smoothness fact required for Taylor theory.
The single field of this structure is the proposition that, for every vertex potential $\xi$, the action restricted to the line $t\mapsto t\xi$ has second derivative at zero equal to the quadratic form of the canonical incidence Hessian on $\xi$.
proof idea
No proof: this is a structure definition. It binds one field, the proposition that the nonlinear action has the canonical incidence Hessian as second variation at the flat potential on every conformal line. Constructors in the nonlinear Hessian proof module later inhabit the structure from directional-Hessian or linearization packages; the structure itself only names the interface.
why it matters
This is the second-variation half of the local nonlinear input bundle. The combined structure NonlinearReggeLocalHessianTaylorInputs takes it as the field action_secondVariation, together with remainder and cubic-remainder inputs, so that Hessian-branch and cubic-Taylor-branch results can be assembled without re-stating analytic hypotheses.
Several constructors in the nonlinear Hessian proof module produce inhabitants from eventually-zero weighted deficits, edge stencils, action-derivative linearization, first-order tangency, tangency-to-quadratic, or a full directional Hessian theorem. The in-module theorem equating second variation to the canonical Hessian consumes the same package. Until the large Cayley-Menger expansion is fully materialized, this named input is how second-variation facts enter the Regge geometry scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.