canonicalJQuadraticTerm
plain-language theorem explainer
Defines the canonical quadratic J/Dirichlet term on a finite 3D Regge triangulation: half the quadratic form of the incidence dual-weight Hessian on a vertex conformal potential. Anyone citing the local nonlinear Regge/J-cost bridge or the exact flat-plus-quadratic-plus-remainder split uses this term. The body is a one-line scaling of the Hessian quadratic form.
Claim. For a finite 3D Regge triangulation $K$ with consistent incidence data and a vertex conformal potential $\xi$, the canonical quadratic J/Dirichlet term is $\tfrac12$ times the quadratic form of the canonical Regge incidence Hessian evaluated on $\xi$.
background
This module targets the nonlinear follow-on to the weak-field quadratic bridge in Recognition Gravity. It does not claim global equality of the full Regge action with a summed J-cost; the surface is local near a flat background: full nonlinear Regge equals its flat value plus a canonical J/Dirichlet quadratic jet, with an explicitly bounded cubic Taylor remainder.
A Triangulation3D carries finite vertex/edge/tet counts, incidence maps, and nondegenerate squared-edge data per tetrahedron. Vertex conformal potentials are real assignments on vertices. The canonical Regge Hessian is the graph-Laplacian matrix induced by incidence dual weights: diagonal equals the row sum of dual weights, off-diagonal equals minus the dual weight. The associated quadratic form is $\sum_{i,j} H_{ij}\xi_i\xi_j$.
In the broader framework the J-cost is the unique reciprocal cost $J(x)=(x+x^{-1})/2-1$ (T5), and the Dirichlet energy of the incidence Hessian is the geometric avatar of that quadratic jet on the triangulation.
proof idea
Pure definition: scale the Hessian quadratic form by one half. No tactics. The matrix is canonicalReggeHessian (incidence dual-weight Laplacian); the form is the double sum $\sum_i\sum_j H_{ij}\xi_i\xi_j$ from hessianQuadratic.
why it matters
This is the second-order jet that the full nonlinear Regge action sees at a flat background, so it is the geometric half of the local Regge/J-cost correspondence. Downstream, it is identified with half the canonical Dirichlet energy, proved nonnegative, and inserted into the exact algebraic split of the nonlinear Regge action into flat value + this quadratic term + remainder. That split feeds the local correspondence proposition (cubic remainder bound) and the certificate structure linking T5 J-uniqueness to the nonlinear Regge curvature-action bridge in the unified forcing chain. A physical six-tetrahedron instance also equates a periodic form of this term to an edge stencil. It sits on the geometry side of the T5 landmark without claiming the global nonlinear identification the module explicitly withholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.