Pith. sign in
theorem

hessianQuadratic_zeroPotential

proved
show as:
module
IndisputableMonolith.Geometry.ReggeActionConcrete
domain
Geometry
line
98 · github
papers citing
none yet

plain-language theorem explainer

On any finite 3D triangulation, the candidate Hessian quadratic form vanishes when evaluated at the flat (identically zero) vertex potential. Anyone assembling the Taylor split of the conformal Regge action cites this to clear the constant and linear layers at the flat background. The proof is a two-step unfold-and-simp: both sides reduce to the empty sum over vertices.

Claim. Let $K$ be a finite 3D triangulation and let $H$ be any real bilinear form on pairs of vertices. If $\phi_0$ denotes the identically zero vertex potential on $K$, then the associated Hessian quadratic form satisfies $Q_H(\phi_0)=0$.

background

The module isolates the final analytic Hessian step for a finite 3D Regge triangulation under the conformal ansatz. A concrete action package supplies the Regge action and its second variation; this file packages that data into the existing Regge-Hessian interface.

Vertex potentials are real assignments to the vertices of $K$. The zero potential is the flat background (every vertex value zero). The Hessian quadratic form $Q_H$ is the candidate second-order piece built from a bilinear kernel $H$ on vertex pairs; it is the quadratic term that should match the second variation of the Regge action at flat space.

Nearby siblings define the conformal edge lengths, dihedral angles under the conformal ansatz, deficit angles, hinge measures, the full nonlinear Regge action, its quadratic truncation, and the nonlinear remainder. The present identity is the base case that makes the Taylor decomposition clean at the origin of potential space.

proof idea

Pure definitional reduction. Unfold the Hessian quadratic form and the zero potential; both become explicit sums (or products) whose every summand contains a factor of the potential. With the potential identically zero, simp collapses the expression to $0$. No geometric lemmas, incidence hypotheses, or analytic estimates are required.

why it matters

Feeds two immediate parents in the same module. First, reggeActionRemainder_zero: the nonlinear remainder vanishes at the flat potential for every candidate Hessian, proved by rewriting with this identity. Second, reggeActionSecondOrder_secondVariation: the exact second variation of the quadratic truncation equals half the Hessian quadratic form, again using vanishing at zero as the base point.

Together these close the concrete Taylor package that turns the conformal Regge action into ReggeHessianData. In the broader Recognition geometry chain this is the local flat-space check that the second-order piece is truly quadratic and has no constant offset, so the continuum Hessian target is well-posed before any continuum or curvature identification is attempted. It does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law; it is pure discrete-geometry bookkeeping inside the Regge layer.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.