bilinearCoefficient
plain-language theorem explainer
The bilinear coefficient is the entrywise product of the first-order area and deficit responses extracted from the weak-field linearization data for a Regge configuration. Workers on discrete gravity reductions cite this definition when assembling the quadratic form that converts the second-order action into a Dirichlet energy on vertex potentials. It is realized by the direct product of the two response fields inside the WeakFieldReggeData record.
Claim. Let $M_{ij} = dA_{ij} · dδ_{ij}$, where $dA_{ij}$ is the coefficient of the linear area response to the conformal perturbation on edge $⟨i,j⟩$ and $dδ_{ij}$ is the corresponding linear response of the deficit angle.
background
In the weak-field conformal reduction of the Regge action the second-order term is assembled from the product of first-order variations. The WeakFieldReggeData structure packages these responses: dArea supplies the coefficient of $(ξ_i + ξ_j)/2$ in the area expansion while dDeficit does the same for the deficit angle. The module proves the algebraic identity that converts the resulting bilinear form into the Dirichlet form on differences $(ξ_i − ξ_j)^2$, once the Schläfli row-sum condition holds.
proof idea
One-line definition that multiplies the dArea and dDeficit fields of the supplied WeakFieldReggeData record at the given indices.
why it matters
This definition supplies the coefficient matrix for the second-order Regge action in the conformal sector. It is used by bilinearCoefficient_laplacianReggeData, dirichletForm_edgeArea, edgeArea, and secondOrderReggeAction to reach the Dirichlet form. In the Recognition framework it completes the algebraic step that reduces the linearized Regge action to a quadratic form on differences, consistent with the conformal expansion and graph-Laplacian decomposition laid out in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.