 524    Non-negativity is a property of the lattice (e.g., automatic for
 525    regular cubic lattices where `A_{ij}` is a true area), so we
 526    package it as an explicit hypothesis. -/
 527def edgeAreaGraph {n : ℕ} (W : WeakFieldReggeData n)
 528    (hpos : ∀ i j, 0 ≤ edgeArea W i j) : WeightedLedgerGraph n :=
 529  { weight := edgeArea W
 530  , weight_nonneg := hpos
 531  , weight_symm := edgeArea_symm W }
 532
 533/-- **BRIDGE TO `laplacian_action`.**
 534    The second-order Regge action equals `(1/2) · laplacian_action`
 535    on the `edgeAreaGraph`. Concretely:
 536
 537        S^(2)[ξ] = (1/2) · laplacian_action (edgeAreaGraph W) ε.
 538
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.