secondOrder_eq_half_laplacian_action

formal source

 539    Combined with `EdgeLengthFromPsi.field_curvature_identity_under_linearization`,
 540    this is the explicit second-order content of the bridge identity:
 541    "J-cost Dirichlet energy = (1/κ) · Regge sum, at second order in ξ". -/
 542theorem secondOrder_eq_half_laplacian_action
 543    {n : ℕ} (W : WeakFieldReggeData n)
 544    (hSchl : SchlaefliRowSum W)
 545    (hpos : ∀ i j, 0 ≤ edgeArea W i j)
 546    (ε : LogPotential n) :
 547    secondOrderReggeAction W ε
 548      = (1 / 2) * laplacian_action (edgeAreaGraph W hpos) ε := by
 549  rw [weak_field_conformal_reduction W hSchl ε]
 550  unfold dirichletForm laplacian_action edgeAreaGraph
 551  rfl
 552
 553/-! ## §5b. Discharging the row-sum condition by a graph Laplacian
 554
 555The row-sum condition is not a new physical assumption once the
 556second-variation bilinear is written in Laplacian form. Given symmetric
 557edge-area weights `A_{ij}`, define the bilinear coefficient matrix
 558
 559  `M_{ij} = δ_{ij} · Σ_k A_{ik} - A_{ij}`.
 560
 561Then `Σ_j M_{ij} = 0` exactly. This is the finite-dimensional version of
 562the flat-background Schläfli statement: a constant conformal rescaling is
 563a pure scale mode and cannot create curvature.
 564
 565The diagonal entries of `M` do not contribute to the Dirichlet energy
 566because `(ξ_i - ξ_i)^2 = 0`; the off-diagonal entries recover the edge
 567weights `A_{ij}`.
 568-/
 569
 570/-- The Laplacian bilinear coefficient matrix associated with symmetric
 571    edge-area weights `A`. The diagonal is chosen so every row sums to
 572    zero. -/