concreteM
plain-language theorem explainer
Defines the concrete second-variation coefficient matrix for a finite eight-vertex Freudenthal Regge star: each entry is the bilinear coefficient of the weak-field Laplacian data built from geometric area weights. Anyone comparing the discrete Regge Hessian to the Dirichlet form on this model cites it. The body is a one-line alias of that bilinear form.
Claim. For a concrete local Regge star $S$ (background edge length and hinge area) and vertices $i,j$ in the eight-vertex Freudenthal chart, $M_{ij}(S)$ is the bilinear second-variation coefficient of the weak-field Regge data induced by the geometric area weights of $S$.
background
The module supplies a fully concrete finite flat-sector model that the weak-field bridge can consume without new geometric axioms. The local chart has eight vertices (Fin 8), matching a cubic cell / Freudenthal neighborhood. A concrete Regge star packages positive background edge length and nonnegative hinge area; area weights on pairs of vertices come from the regular triangular hinge formula, and the weak-field data is the graph-Laplacian Regge package built from those symmetric weights.
The Cayley–Menger stack already gives regular tetrahedron values and dihedral data, but not yet full differentiable CM determinants or arbitrary-triangulation dihedral derivatives. So the comparison is proved only for this regular flat-sector model: off-diagonal coefficients equal minus area weights, rows sum to zero, and the second-order action is the geometric Dirichlet form.
Upstream, concreteWeakFieldReggeData is exactly laplacianReggeData of the area-weight matrix; the coefficient matrix is the bilinear form of that data.
proof idea
One-line definitional wrapper: unfold to the bilinear coefficient of concreteWeakFieldReggeData S at vertices $i,j$. No tactics or lemmas; the mathematical content lives in the Laplacian Regge data and the area-weight construction.
why it matters
This matrix is the named object on which the module’s component comparison is stated. Downstream theorems prove off-diagonal entries equal the negative area/face weights, every row sums to zero, and the certificate structure records that the second-order Regge action equals half the Dirichlet form for those weights. That closes the concrete finite model the weak-field bridge needs, and is the exact interface a future full Cayley–Menger / dihedral-derivative computation must match. It sits in the geometry layer feeding discrete gravity / Regge comparisons, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.