hessianQuadratic_linePotential
plain-language theorem explainer
The Hessian quadratic form on vertex potentials of a 3D triangulation is homogeneous of degree two: evaluating it on the ray t·ξ multiplies the value by t². Second-variation and spacing-normalization proofs for the nonlinear Regge action cite this identity. The argument unfolds the double-sum definition, factors t out of each index twice, and closes by ring.
Claim. Let $K$ be a 3D triangulation, $H$ a real matrix indexed by pairs of vertices, $\xi$ a vertex potential on $K$, and $t\in\mathbb{R}$. Write $(t\cdot\xi)_i:=t\,\xi_i$. Then the Hessian quadratic form satisfies $Q_H(t\cdot\xi)=t^2\,Q_H(\xi)$.
background
The module packages second-variation and cubic-remainder targets for the nonlinear Regge action on a 3D triangulation, keeping the heavy Cayley–Menger/arccos expansion behind named input structures until it is fully formalized.
A vertex potential assigns a real number to each vertex of $K$. The line through the flat (zero) potential in direction $\xi$ is the ray $t\mapsto t\cdot\xi$, defined componentwise by $(t\cdot\xi)i=t,\xi_i$. The Hessian quadratic form $Q_H$ is the standard double sum $\sum{i,j}H_{ij}\phi_i\phi_j$ associated to a bilinear matrix $H$ on vertex potentials (imported from the 3D Regge Hessian layer).
The identity is pure bilinearity: no incidence consistency, curvature, or Regge edge-length map is required.
proof idea
Term-mode proof by unfolding. Expand $Q_H$ and the line potential into the double Finset sum $\sum_i\sum_j H_{ij}(t\xi_i)(t\xi_j)$. Apply Finset.mul_sum on the outer index to extract one factor of $t$, then again on the inner index to extract the second factor, obtaining $t^2$ times the original double sum. The remaining pointwise identity $H_{ij}(t\xi_i)(t\xi_j)=t^2 H_{ij}\xi_i\xi_j$ is discharged by ring under Finset.sum_congr.
why it matters
Homogeneity is the algebraic step that turns the abstract quadratic form into a genuine second derivative along rays. It is used immediately to prove that $t\mapsto\tfrac12 Q_H(t\cdot\xi)$ has second derivative $Q_H(\xi)$ at $t=0$, and to obtain differentiability and first-derivative formulas for the canonical quadratic along a line in the nonlinear Hessian proof layer.
Downstream, the gravity instance for the physical six-tetrahedron cubic Dirichlet problem invokes it to normalize the spacing-scaled second-order Regge action: when the flat action vanishes, the second-order piece on $a\cdot\xi$, divided by $|a|^2$, equals exactly $\tfrac12 Q_H(\xi)$ for every nonzero spacing $a$. That normalization sits inside the discrete-gravity side of the Recognition geometry stack (Regge calculus in $D=3$, forced by the T8 landmark).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.