canonicalWeakFieldData_bilinearCoefficient
plain-language theorem explainer
For any incidence-consistent 3D Regge triangulation, the bilinear coefficient matrix of the canonical weak-field data equals the canonical Regge Hessian from dual weights. Discrete-gravity workers matching weak-field expansions to graph Laplacians cite this bridge. The proof unfolds the data constructor and rewrites by the Laplacian-Regge coefficient identity, then closes by definitional equality.
Claim. Let $K$ be a finite 3D Regge triangulation that is incidence-consistent, and let $i,j$ be vertices of $K$. Then the bilinear coefficient of the canonical weak-field Regge data induced by the incidence dual weights equals the canonical graph-Laplacian Hessian of $K$ at the pair $(i,j)$.
background
A Triangulation3D is a finite 3D Regge complex: vertex/edge/tet counts, edge endpoints, and tetrahedron vertex maps, together with nondegenerate squared-edge data on each tet. IncidenceConsistent strengthens this with a global squared-edge assignment, agreement of local tet edge slots with global endpoints (up to orientation), and the local closed-form Schläfli data needed for a global Schläfli identity without caller-supplied packages.
From those dual weights one builds two parallel objects: the canonical graph-Laplacian Hessian $(i,j)\mapsto (\delta_{ij}\sum_k w_{ik})-w_{ij}$, and the canonical weak-field Regge dataset obtained by feeding the same symmetric dual-weight matrix into the Laplacian-style weak-field constructor. The bilinear coefficient is the quadratic-form matrix extracted from any such weak-field dataset.
This module isolates the independent dual-weight construction from that coefficient matrix and records the comparison lemmas that turn the geometric computation into a ReggeComponentComparison statement.
proof idea
Short definitional bridge. Unfold the canonical weak-field data: it is exactly the Laplacian-Regge dataset built from the incidence dual weights (and their symmetry). Rewrite the left-hand side by the general identity that the bilinear coefficient of any Laplacian-Regge dataset is the corresponding graph Laplacian. The resulting expression matches the definition of the canonical Regge Hessian, so rfl finishes.
why it matters
Immediate parent is the off-diagonal component match: once bilinear coefficients equal the Hessian, off-diagonal entries reduce to minus the independent dual weights, which is the concrete component comparison the module is aiming at. That comparison is the final step that turns the geometric dual-weight computation into a ReggeComponentComparison in 3D.
In the broader Recognition framework this sits in the gravity sector after the forcing chain has already fixed $D=3$ (T8) and the eight-tick discrete structure (T7). It does not itself invoke $J$-cost or the RCL; it supplies the discrete weak-field quadratic form that later continuum or phenomenological gravity arguments can quote when they need a proved Laplacian match on an incidence-consistent triangulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.