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
proof body
Term-mode proof.
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. -/
depends on (30)
Lean names referenced from this declaration's body.