edgeArea
plain-language theorem explainer
edgeArea supplies the signed weights A_ij for the second-order Regge action in the conformal weak-field limit. Researchers reducing Regge calculus to graph Laplacians cite it to assemble the Dirichlet form from linearization data. The definition is a direct negation of the bilinear coefficient matrix, enforcing the sign convention Q = -D from the quadratic form.
Claim. For linearization data $W$ on $n$ vertices, the edge-area weights are defined by $A_{ij} := -(dA_{ij} · dδ_{ij})$, where $dA_{ij}$ and $dδ_{ij}$ are the first-order responses of hinge area and deficit angle to conformal vertex perturbations.
background
The module develops the algebraic reduction of the Regge action under conformal edge-length perturbations. The structure packages the first-order coefficients dArea and dDeficit for each edge. bilinearCoefficient computes their entrywise product M_ij, which enters the second variation after the conformal expansion. The module documentation states that the reduction shows S^(2) equals (1/κ) times the sum over edges of (1/2)(ξ_i − ξ_j)^2 A_ij.
proof idea
One-line definition that negates the output of bilinearCoefficient W i j. This directly implements the relation edgeArea = − bilinearCoefficient stated in the doc-comment.
why it matters
This definition supplies the weights for the Dirichlet form in dirichletForm_edgeArea and the graph construction in edgeAreaGraph. It completes the algebraic step that converts the bilinear Regge form into the Laplacian action used in secondOrder_eq_half_laplacian_action. The construction realizes the graph-Laplacian decomposition for the conformal sector, linking to the Dirichlet form identity and the reduction of the Regge action to a quadratic form on differences.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.