secondOrderReggeAction
plain-language theorem explainer
The second-order Regge action in the conformal sector is defined as one-fourth the double sum over vertex pairs of the bilinear coefficient matrix times the square of the summed log-potential perturbations at each endpoint. Discrete gravity researchers reducing Regge calculus to a graph Dirichlet form would cite this expression when isolating quadratic fluctuations around a flat background. The definition assembles the surviving quadratic terms after conformal edge-length expansion and Schläfli cancellation of the diagonal contributions.
Claim. Let $W$ be the weak-field linearization data consisting of first-order hinge-area responses $dA_{ij}$ and deficit responses $dδ_{ij}$. Let $ε$ be a real-valued log-potential on the $n$ vertices. The second-order Regge action is $S^{(2)}[ε] = (1/4) ∑_{i,j} M_{ij} (ε_i + ε_j)^2$, where the bilinear coefficient matrix is the entrywise product $M_{ij} = dA_{ij} · dδ_{ij}$.
background
The module isolates the algebraic core of the weak-field conformal reduction of the Regge action. The starting point is the classical expression $S = (1/κ) ∑h A_h δ_h$. Under the conformal ansatz $ℓ{ij} = ℓ_0 exp((ξ_i + ξ_j)/2)$, the edge lengths are expanded to second order in the conformal factor ξ, which is identified with the log-potential ε. The structure WeakFieldReggeData packages the linear responses: dArea records the coefficient of (ξ_i + ξ_j)/2 in the first-order area change for each hinge, while dDeficit records the corresponding linear response of the deficit angle.
proof idea
This is a direct definition that assembles the quadratic form by summing the bilinear coefficients (the entrywise product of dArea and dDeficit) against the squared sum of perturbations at each pair of vertices. The factor 1/4 originates from the two appearances of the averaged conformal shift, once in the area linearization and once in the deficit linearization, as stated in the module doc-comment.
why it matters
This definition supplies the explicit quadratic functional that the reduction theorems convert into the Dirichlet form on edge areas. It is invoked by weak_field_conformal_reduction to obtain equality with (1/2) dirichletForm (edgeArea W) under the Schläfli row-sum hypothesis, and by secondOrder_eq_half_laplacian_action to identify it with half the Laplacian action on the edge-area graph. In the Recognition framework it realizes the discrete bridge from Regge calculus to the Laplacian action on the simplicial ledger, consistent with the identification (1/2) Σ w_ij (ε_i − ε_j)^2 = (1/κ) Σ δ_h A_h from the ContinuumBridge structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.