weak_field_conformal_reduction_kappa
plain-language theorem explainer
The theorem equates the κ-normalized second-order Regge action on conformal vertex perturbations to (1/κ) times half the Dirichlet form generated by the edge-area matrix. Physicists linearizing Regge calculus for weak-field gravity would cite this identity to obtain the quadratic graph-Laplacian form. The proof is a one-line wrapper that substitutes the un-normalized reduction and clears denominators via field simplification.
Claim. For weak-field Regge data $W$ on $n$ vertices obeying the Schläfli row-sum condition, nonzero coupling constant $κ$, and log-potential $ε$, the normalized second-order Regge action satisfies $S^{(2)}(W,ε)/κ = (1/κ)·(1/2)·D(ε;A_W)$, where $D$ denotes the Dirichlet form on the edge-area matrix $A_W$ induced by $W$.
background
The module isolates the algebraic core of the conformal weak-field reduction of the Regge action. WeakFieldReggeData packages the first-order linear responses dArea and dDeficit of hinge areas and deficits under conformal edge-length perturbations ℓ_ij = ℓ_0 exp((ξ_i + ξ_j)/2). SchlaefliRowSum encodes the flat-background identity that the induced bilinear matrix M_ij = dArea_ij · dDeficit_ij has vanishing row sums, ∑j M_ij = 0 for each vertex i. The Dirichlet form is the quadratic functional (1/2) ∑{i,j} M_ij (ε_i − ε_j)^2, which is algebraically equivalent to the graph Laplacian precisely when the row-sum condition holds.
proof idea
The proof is a one-line wrapper that applies the un-normalized reduction theorem weak_field_conformal_reduction and then invokes field_simp to absorb the common factor 1/κ.
why it matters
This identity supplies Jon's equation (d) and feeds directly into the certification theorem weakFieldConformalReggeCert that assembles the exact conformal expansion, Taylor remainder, and Laplacian decomposition. It realizes the algebraic step that converts the linearized Regge action into the Dirichlet form on log-potentials, bridging the discrete Regge calculus to the continuum quadratic action in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.