secondOrder_eq_half_laplacian_action
plain-language theorem explainer
The second-order Regge action for a conformal weak-field perturbation on a flat background equals half the graph Laplacian action with edge-area weights. Researchers in discrete gravity and Regge calculus cite this to recast the quadratic action as a Dirichlet energy on vertex potentials. The proof is a one-line rewrite using the conformal reduction lemma followed by unfolding the Dirichlet form and Laplacian definitions to reflexivity.
Claim. Let $n$ be a natural number, $W$ a weak-field Regge data structure satisfying the Schläfli row-sum condition with nonnegative edge areas, and $ε$ a logarithmic potential. Then the second-order term in the Regge action equals half the action of the graph Laplacian on the edge-area weighted graph applied to $ε$.
background
WeakFieldReggeData packages the first-order linear responses of hinge areas and deficit angles to conformal vertex shifts. SchlaefliRowSum requires the induced bilinear coefficient matrix to have zero row sums, which follows from Schläfli's identity on a flat background. This forces the quadratic form to contain no linear term under constant rescaling.
proof idea
This is a one-line wrapper that applies the weak_field_conformal_reduction lemma to equate the second-order action to the Dirichlet form, then unfolds the definitions of dirichletForm, laplacian_action, and edgeAreaGraph to obtain the Laplacian expression by reflexivity.
why it matters
This supplies the explicit identification of the second-order Regge action with half the Laplacian action, completing the algebraic bridge in the weak-field conformal sector. It directly supports the bridge identity linking J-cost Dirichlet energy to the Regge sum at second order. In the Recognition Science framework the reduction shows how the discrete gravity action collapses to a quadratic form on phi-ladder perturbations, consistent with the eight-tick octave and D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.