bilinearCoefficient_laplacianReggeData
plain-language theorem explainer
The theorem shows that the bilinear coefficient extracted from Laplacian Regge data built on any symmetric matrix A equals the Laplacian coefficient matrix of A. Workers on the weak-field conformal reduction of the Regge action cite this identity when confirming that the second-variation form reduces exactly to a Dirichlet form on edge differences. The proof is a direct unfolding of the two definitions followed by ring normalization.
Claim. Let $A$ be a symmetric real $n$ by $n$ matrix. Let $W$ be the weak-field Regge data with constant area response 1 and deficit response equal to the Laplacian coefficient matrix of $A$. Then the bilinear coefficient of $W$ at indices $i,j$ equals the Laplacian coefficient of $A$ at $i,j$, i.e., $W.dArea_{ij} · W.dDeficit_{ij} = L(A)_{ij}$ where $L(A)_{ij} = (δ_{ij} ∑_k A_{ik}) - A_{ij}$.
background
The module develops the algebraic core of the weak-field conformal reduction of the Regge action. It introduces the bilinear coefficient as the entrywise product of first-order area and deficit responses that appears in the second variation, and the Laplacian coefficient that builds a zero-row-sum matrix from symmetric edge weights $A$ by placing row sums on the diagonal and negatives off-diagonal. The laplacianReggeData packages the specific instance in which dArea is constantly 1 and dDeficit is exactly the Laplacian coefficient, so that their product recovers the Laplacian matrix itself. This construction sits inside the graph-Laplacian decomposition that converts the Regge bilinear form into the Dirichlet form on differences $(ξ_i - ξ_j)^2$.
proof idea
The proof is a one-line wrapper that unfolds bilinearCoefficient and laplacianReggeData, then applies the ring tactic to obtain the equality by direct algebraic cancellation.
why it matters
This identity supplies the concrete identification required by the downstream theorems dirichletForm_edgeArea_laplacianReggeData and schlaefliRowSum_laplacianReggeData. It closes the algebraic step that lets the second-variation Regge form reduce to the Dirichlet form on edge differences, which is the central structural lemma of the weak-field conformal reduction. The result aligns with the graph-Laplacian decomposition described in the module documentation and supports the row-sum discharge for the Laplacian choice of data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.