laplacianReggeData
plain-language theorem explainer
The definition constructs WeakFieldReggeData for any symmetric real matrix A on Fin n by setting the area response to the constant function 1 and the deficit response to the graph Laplacian of A. Researchers reducing the second-order Regge action under conformal perturbations cite it to obtain an explicit Laplacian bilinear form. The body is a direct record literal that delegates deficit symmetry to the companion lemma laplacianCoefficient_symm.
Claim. Let $A$ be a symmetric real matrix indexed by $Fin n$. The associated weak-field Regge data is the structure with $dArea_{ij}=1$ for all $i,j$, $dDeficit_{ij}=L_{ij}(A)$ where $L_{ij}(A)=[i=j]·∑_k A_{ik}-A_{ij}$, and both fields symmetric.
background
WeakFieldReggeData is the structure whose fields dArea and dDeficit record the first-order linear responses of hinge area and deficit angle to conformal vertex shifts; the induced bilinear coefficient is their pointwise product. The module develops the algebraic core of the weak-field conformal reduction of the Regge action: under the ansatz ℓ_{ij}=ℓ_0 exp((ξ_i+ξ_j)/2) the second variation reduces to a Dirichlet form on differences (ξ_i−ξ_j)^2. Upstream, laplacianCoefficient defines the zero-row-sum matrix L_{ij}=(i=j?∑k A{ik}:0)−A_{ij} and laplacianCoefficient_symm proves its symmetry when A is symmetric.
proof idea
The definition is a record literal. It sets dArea to the constant-1 function and dDeficit to laplacianCoefficient A. Symmetry of dArea is discharged by reflexivity. Symmetry of dDeficit is discharged by direct application of the theorem laplacianCoefficient_symm A hA.
why it matters
This supplies the canonical WeakFieldReggeData whose bilinear coefficient is exactly the graph Laplacian, so that the downstream theorems weak_field_conformal_reduction_laplacianData and weak_field_conformal_reduction_laplacianData_kappa conclude unconditionally that the second-order Regge action equals (1/2) times the Dirichlet form with weights A. It realizes the graph-Laplacian decomposition step of the module, converting any symmetric zero-row-sum matrix into admissible Regge second-variation data and thereby closing the algebraic reduction in the gravity paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.