dirichletForm_edgeArea

formal source

 375/-- The Dirichlet form on `edgeArea W` is the negation of the Dirichlet
 376    form on `bilinearCoefficient W`. Direct from `dirichletForm_neg`
 377    plus the definition `edgeArea = − bilinearCoefficient`. -/
 378theorem dirichletForm_edgeArea
 379    {n : ℕ} (W : WeakFieldReggeData n) (ε : LogPotential n) :
 380    dirichletForm (edgeArea W) ε
 381      = - dirichletForm (bilinearCoefficient W) ε := by
 382  have h := dirichletForm_neg (bilinearCoefficient W) ε
 383  -- `(fun i j => - bilinearCoefficient W i j)` is definitionally `edgeArea W`.
 384  exact h
 385
 386/-- **WEAK-FIELD CONFORMAL REDUCTION (the main theorem).**
 387
 388    Under the Schläfli row-sum hypothesis (§3) on the linearization
 389    data `W`, the second-order Regge action equals the discrete
 390    Dirichlet energy on the conformal mode `ε`, with edge weights
 391    `A_{ij} = − dArea_{ij} · dDeficit_{ij}`:
 392
 393        secondOrderReggeAction W ε
 394            = (1/2) · Σ_{i,j} ½ · (ε i − ε j)² · A_{ij}
 395            = ½ · dirichletForm A ε.
 396
 397    Multiplying through by `1/κ` recovers Jon's equation (d):
 398
 399        S^(2)/κ = (1/κ) · Σ_⟨i,j⟩ ½ · (ξ_i − ξ_j)² · A_{ij}.
 400
 401    Proof:
 402    1. Expand `(ξ_i + ξ_j)² = ξ_i² + 2 ξ_i ξ_j + ξ_j²`.
 403    2. The `ξ_i²` and `ξ_j²` pieces collapse via Schläfli row-sum.
 404    3. The `2 ξ_i ξ_j` piece is `quadraticForm M ε = − dirichletForm M ε`
 405       by `dirichlet_eq_neg_quadratic` (§2).
 406    4. `dirichletForm (edgeArea W) ε = − dirichletForm M ε`
 407       by `dirichletForm_edgeArea`.
 408    Combining: LHS = `(1/4)·(0 + 2·(−D) + 0) = −D/2 = (1/2)·(−D)