reggeActionSecondVariationInput_of_directionalSecondVariation
plain-language theorem explainer
Packages a directional second-variation hypothesis into the named second-variation input for the nonlinear Regge action. Given that the action along every conformal line has second derivative equal to the canonical incidence Hessian quadratic form at the flat potential, this builds the structure that Phase-D theorems consume. Downstream nonlinear Hessian proofs cite it as the packaging step. Pure structure constructor: one field assignment.
Claim. Let $K$ be an incidence-consistent 3D triangulation with a flat configuration. Suppose that for every vertex potential $\xi$, the nonlinear Regge action along the conformal line through $\xi$ has second derivative at zero equal to the quadratic form of the canonical incidence Hessian on $\xi$. Then these data assemble into a valid second-variation input package for the full nonlinear action.
background
The module fixes the 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 that the expansion will eventually supply live in named input structures.
CanonicalHessianSecondVariationAtZero asserts that for every vertex potential $\xi$, the map $t \mapsto$ action along the conformal line through $\xi$ has second derivative at $t=0$ equal to the quadratic form of the canonical incidence Hessian on $\xi$. ReggeActionSecondVariationInput is the structure that packages exactly that assertion (under a flat configuration) as the field canonical_secondVariation.
Flat configuration means the discrete geometry sits at the zero-curvature background where the first variation vanishes and the Hessian is the leading nontrivial term. The ambient setting is 3D triangulations, matching the forced spatial dimension $D=3$.
proof idea
One-line structure constructor. The sole field of ReggeActionSecondVariationInput is canonical_secondVariation; the proof assigns the incoming hypothesis hSecond : CanonicalHessianSecondVariationAtZero K hK to that field. No lemmas are applied.
why it matters
This is the packaging bridge between a raw directional second-variation hypothesis and the named input that Phase-D second-variation theorems require. Two constructors in ReggeActionNonlinearHessianProof call it: one from a flat nonlinear Hessian theorem, one from a nonlinear directional Hessian theorem; both reduce to this packaging step.
In the Recognition geometry stack, the second variation of the Regge action at the flat background is the discrete analogue of the Einstein-Hilbert Hessian. Packaging it as a named input lets the nonlinear Hessian program proceed while the full Cayley-Menger expansion remains incomplete. It does not itself touch T0-T8 or the RCL; it is infrastructure for the discrete gravity side of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.