reggeAction_secondVariation_eq_canonicalHessian
plain-language theorem explainer
At a flat configuration of an incidence-consistent 3D triangulation, the second variation of the nonlinear Regge action equals the canonical incidence Hessian quadratic form, conditional on a named analytic input. Discrete-gravity and Regge-calculus workers in Recognition Science cite this as the Phase-D second-variation statement. The proof is a one-line field projection from that input structure.
Claim. Let $K$ be an incidence-consistent 3-dimensional triangulation in a flat edge-length configuration. If the nonlinear Regge action satisfies the named second-variation input (second derivative along every conformal line of vertex potentials equals the canonical Hessian quadratic), then for every vertex potential $\xi$ the map $t \mapsto S_K(t\xi)$ has second derivative at $t=0$ equal to the quadratic form of the canonical Regge Hessian on $\xi$.
background
The module packages nonlinear second-variation and cubic-remainder targets for the Regge action on a 3D triangulation before the full Cayley-Menger/arccos chain-rule expansion is finished. Analytic content that is not yet expanded lives in named input structures rather than as free-standing lemmas.
A flat configuration means edge lengths realize zero deficit (locally Euclidean). Vertex potentials $\xi$ parameterize conformal line deformations of those lengths. The action along a line is $t \mapsto S_K(t\xi)$; the target property asserts that this real function has second derivative at $t=0$ equal to the quadratic form of the canonical incidence Hessian of $K$.
The named input structure simply records that second-variation fact as a hypothesis bundle. The conclusion proposition is the same statement quantified over all vertex potentials: every conformal line has the canonical Hessian as its second derivative at the flat point.
proof idea
One-line term proof: project the field canonical_secondVariation out of the input structure ReggeActionSecondVariationInput. No algebraic rewriting, no tactic steps, and no appeal to external lemmas beyond that field access. The theorem is the packaging interface that turns the named hypothesis into the stand-alone second-variation proposition used elsewhere in the geometry stack.
why it matters
This is the Phase-D second-variation theorem for the nonlinear Regge action, stated so it can be cited while the lower-level Cayley-Menger expansion remains incomplete. It pins the discrete Einstein-Hilbert second variation at flat space to the canonical incidence Hessian, the natural quadratic form built from the triangulation's incidence data.
No downstream consumers are wired yet (used_by is empty); the sibling remainder targets in the same module (zero second variation of the canonical nonlinear remainder at the flat potential) are the natural next layer. In the broader Recognition geometry program this is the discrete-curvature stability statement at the flat background, complementary to the first-variation module imported here. Closing the scaffold means discharging the named input by an explicit second-derivative computation rather than by hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.