weak_field_conformal_reduction
plain-language theorem explainer
Gravitational physicists working on discrete Regge calculus cite this identity when reducing the second-order action on conformal vertex perturbations to a discrete Dirichlet energy. For weak-field Regge data W satisfying the Schläfli row-sum condition, the second-order Regge action on a log-potential ε equals half the Dirichlet form weighted by the induced edge areas. The proof expands the squared bilinear terms, cancels the diagonal contributions via zero row sums, invokes the graph-Laplacian decomposition, and finishes with algebraic ring.
Claim. Let $W$ be weak-field Regge data on $n$ vertices whose bilinear coefficients satisfy the Schläfli row-sum condition, and let $ε$ be a conformal log-potential. Then the second-order Regge action equals half the Dirichlet form on the edge-area weights: $S^{(2)}(W,ε)=(1/2)·dirichletForm(edgeArea(W),ε)$.
background
The module develops the algebraic core of the weak-field conformal reduction of the Regge action. WeakFieldReggeData packages the first-order linear responses dArea and dDeficit of hinge areas and deficits under conformal edge-length changes ℓ_ij=ℓ_0 exp((ξ_i+ξ_j)/2). The bilinear coefficient matrix is their entrywise product M_ij=dArea_ij·dDeficit_ij, so that the second-order action is (1/4)Σ M_ij(ξ_i+ξ_j)^2. SchlaefliRowSum asserts that this matrix has zero row sums, which follows from Schläfli's identity on a flat background.
proof idea
Set M to bilinearCoefficient W. Expand Σ M_ij(ε_i+ε_j)^2 into three sums via ring. Apply sum_const_mul_right and zero_mul to show the two diagonal sums vanish once the row sums are zero. Use dirichlet_eq_neg_quadratic (with the symmetry and row-sum hypotheses) to replace the cross term quadraticForm by -dirichletForm. Rewrite the target Dirichlet form via dirichletForm_edgeArea, unfold the action, and close with ring.
why it matters
This supplies the finite-dimensional algebra that converts the linearized Regge bilinear form into the Dirichlet energy on differences, realizing Jon's equation (d) in the gravity paper. It is invoked directly by weak_field_conformal_reduction_kappa (the κ-normalized version) and by secondOrder_eq_half_laplacian_action (the bridge to laplacian_action). The result closes the conformal-sector reduction step, leaving only the geometric task of verifying the row-sum condition on concrete lattices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.