weak_field_conformal_reduction_laplacianData_kappa
plain-language theorem explainer
The theorem shows that for symmetric edge weights A on n vertices, nonzero scalar κ, and log-potential ε, the second-order Regge action built from Laplacian data, when divided by κ, equals exactly (1/κ) times half the Dirichlet form of A on ε. Workers deriving the weak-field conformal limit of Regge gravity cite this identity to obtain the quadratic action on vertex potentials directly from the graph Laplacian. The proof is a one-line wrapper that invokes the prior unconditional reduction and applies field simplification to match the prefactors
Claim. For any natural number $n$, symmetric real matrix $A : Fin n → Fin n → ℝ$, nonzero real number κ, and log-potential ε : Fin n → ℝ, the second-order Regge action on the Laplacian Regge data of A, divided by κ, equals (1/κ) ⋅ (1/2) ⋅ the Dirichlet form of A on ε.
background
LogPotential n is the type Fin n → ℝ of vertex log-potentials ε with ε i = ln ψ(σ_i); the canonical conformal ansatz sets edge lengths proportional to exp((ε i + ε j)/2). dirichletForm M ε is defined as (1/2) Σ_{i,j} M_{ij} (ε i − ε j)^2, the quadratic form that appears after the graph-Laplacian decomposition. laplacianReggeData A hA packages WeakFieldReggeData with dArea = 1 and dDeficit equal to the Laplacian coefficient of A, enforcing the row-sum condition by construction. secondOrderReggeAction W ε expands to (1/4) Σ bilinearCoefficient W_{ij} (ε i + ε j)^2, the order-ξ² term obtained from the conformal expansion of ℓ_{ij}². The module establishes the algebraic core of the weak-field conformal reduction of the Regge action, turning the bilinear form into the Dirichlet form on differences.
proof idea
One-line wrapper that rewrites the left-hand side by the unconditional flat-sector reduction theorem weak_field_conformal_reduction_laplacianData A hA ε, then applies field_simp to cancel the common 1/κ factor and align the remaining 1/2 coefficient with the Dirichlet form definition.
why it matters
This supplies the κ-prefactor version of the reduction that feeds the certificate weakFieldConformalReggeCert. It completes the algebraic step that converts the second-order Regge action into the Dirichlet form, which is the structural link between the discretized Regge action and the quadratic form on conformal modes. The module documentation identifies this reduction as the core algebraic identity needed to move Regge’s notation into the gravity paper; the result is independent of the geometric computation of the area and deficit coefficients.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.